theory LemmaBucket

lemma in_ran_map_app: "x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs" proof - assume a1: "x \<in> ran (xs ++ ys ++ zs)" obtain bb :: "'a \<Rightarrow> ('b \<Rightarrow> 'a option) \<Rightarrow> 'b" where
      "\<forall>x0 x1. (\<exists>v2. x1 v2 = Some x0) = (x1 (bb x0 x1) = Some x0)" by moura hence f2: "\<forall>f a. (\<not> (\<exists>b. f b = Some a) \<or> f (bb a f) = Some a) \<and> ((\<exists>b. f b = Some a) \<or> (\<forall>b. f b \<noteq> Some a))" by blast have "\<exists>b. (xs ++ ys ++ zs) b = Some x" using a1 by (simp add: ran_def) hence f3: "(xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x" using f2 by meson { assume "ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x" { assume "ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x)" hence "\<exists>b. zs b = Some x" using f3 by auto hence ?thesis by (simp add: ran_def) } hence ?thesis using ran_def by fastforce } thus ?thesis using ran_def by fastforce qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
x \<in> ran (xs ++ ys ++ zs)

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
goal (1 subgoal):
 1. (\<And>bb. \<forall>x0 x1. (\<exists>v2. x1 v2 = Some x0) = (x1 (bb x0 x1) = Some x0) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<forall>x0 x1. (\<exists>v2. x1 v2 = Some x0) = (x1 (bb x0 x1) = Some x0)

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
\<forall>x0 x1. (\<exists>v2. x1 v2 = Some x0) = (x1 (bb x0 x1) = Some x0)

goal (1 subgoal):
 1. \<forall>f a. ((\<nexists>b. f b = Some a) \<or> f (bb a f) = Some a) \<and> ((\<exists>b. f b = Some a) \<or> (\<forall>b. f b \<noteq> Some a)) proof (state)
this:
\<forall>f a. ((\<nexists>b. f b = Some a) \<or> f (bb a f) = Some a) \<and> ((\<exists>b. f b = Some a) \<or> (\<forall>b. f b \<noteq> Some a))

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
goal (1 subgoal):
 1. \<exists>b. (xs ++ ys ++ zs) b = Some x proof (prove)
using this:
x \<in> ran (xs ++ ys ++ zs)

goal (1 subgoal):
 1. \<exists>b. (xs ++ ys ++ zs) b = Some x proof (state)
this:
\<exists>b. (xs ++ ys ++ zs) b = Some x

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
\<exists>b. (xs ++ ys ++ zs) b = Some x

goal (1 subgoal):
 1. (xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x proof (prove)
using this:
\<exists>b. (xs ++ ys ++ zs) b = Some x
\<forall>f a. ((\<nexists>b. f b = Some a) \<or> f (bb a f) = Some a) \<and> ((\<exists>b. f b = Some a) \<or> (\<forall>b. f b \<noteq> Some a))

goal (1 subgoal):
 1. (xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x proof (state)
this:
(xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
(xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x)

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x)

goal (1 subgoal):
 1. \<exists>b. zs b = Some x proof (prove)
using this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x)
(xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x

goal (1 subgoal):
 1. \<exists>b. zs b = Some x proof (state)
this:
\<exists>b. zs b = Some x

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
\<exists>b. zs b = Some x

goal (1 subgoal):
 1. x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal (1 subgoal):
 1. x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs
ran ?m = {b. \<exists>a. ?m a = Some b}

goal (1 subgoal):
 1. x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal (1 subgoal):
 1. x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal (1 subgoal):
 1. x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (prove)
using this:
ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs
ran ?m = {b. \<exists>a. ?m a = Some b}

goal (1 subgoal):
 1. x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs proof (state)
this:
x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs

goal:
No subgoals!