[STATEMENT]
lemma run_upd[run_elims]:
  assumes "run (Array.upd i x a) \<sigma> \<sigma>' res"
          "\<not>is_exn \<sigma>"
  obtains "\<not> i < Array.length (the_state \<sigma>) a"
          "\<sigma>' = None"
  |
          "i < Array.length (the_state \<sigma>) a"
          "\<sigma>' = Some (Array.update a i x (the_state \<sigma>))"
          "res = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.upd i x a) \<sigma> \<sigma>' res
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis; run (Array.upd i x a) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis; run (Array.upd i x a) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = Some aa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis; run (Array.upd i x a) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = Some aa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "i < Array.length (the_state \<sigma>) a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis; run (Array.upd i x a) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = Some aa; i < Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>i < Array.length (the_state \<sigma>) a; \<sigma>' = Some (Array.update a i x (the_state \<sigma>)); res = a\<rbrakk> \<Longrightarrow> thesis; run (Array.upd i x a) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = Some aa; \<not> i < Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa. \<lbrakk>\<sigma> = Some aa; i < Array.length aa a; execute (Array.upd i x a) aa = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa h'. \<lbrakk>\<lbrakk>h' = Array.update a i x aa; res = a\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; execute (Array.upd i x a) aa = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
 3. \<And>aa h'. \<lbrakk>\<sigma> = Some aa; \<not> i < Array.length aa a; execute (Array.upd i x a) aa = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp_all only: execute_simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa. \<lbrakk>\<sigma> = Some aa; i < Array.length aa a; Some (a, Array.update a i x aa) = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa h'. \<lbrakk>\<lbrakk>h' = Array.update a i x aa; res = a\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; Some (a, Array.update a i x aa) = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
 3. \<And>aa h'. \<lbrakk>\<sigma> = Some aa; \<not> i < Array.length aa a; None = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa h'. \<lbrakk>\<sigma> = Some aa; \<not> i < Array.length aa a; None = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<sigma> = Some aa; i < Array.length aa a; Some (a, Array.update a i x aa) = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 3. \<And>aa h'. \<lbrakk>\<lbrakk>h' = Array.update a i x aa; res = a\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; Some (a, Array.update a i x aa) = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa h'. \<lbrakk>\<lbrakk>h' = Array.update a i x aa; res = a\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; Some (a, Array.update a i x aa) = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa h'. \<lbrakk>\<lbrakk>h' = Array.update a i x aa; res = a\<rbrakk> \<Longrightarrow> thesis; i < Array.length aa a; Some (a, Array.update a i x aa) = Some (res, h')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal premises prems for aa h'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(3)
[PROOF STATE]
proof (chain)
picking this:
Some (a, Array.update a i x aa) = Some (res, h')
[PROOF STEP]
have "h' = Array.update a i x aa" "res = a"
[PROOF STATE]
proof (prove)
using this:
Some (a, Array.update a i x aa) = Some (res, h')

goal (1 subgoal):
 1. h' = Array.update a i x aa &&& res = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h' = Array.update a i x aa
res = a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h' = Array.update a i x aa
res = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h' = Array.update a i x aa
res = a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma run_nth[run_elims]:
  assumes "run (Array.nth a i) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<not>is_exn \<sigma>"
    "i < Array.length (the_state \<sigma>) a"
    "r = (Array.get (the_state \<sigma>) a) ! i"
    "\<sigma>' = \<sigma>"
  |
    "\<not> i < Array.length (the_state \<sigma>) a"
    "\<sigma>' = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.nth a i) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; run (Array.nth a i) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; run (Array.nth a i) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some aa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; run (Array.nth a i) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some aa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "i < Array.length (the_state \<sigma>) a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; run (Array.nth a i) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some aa; i < Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; i < Array.length (the_state \<sigma>) a; r = Array.get (the_state \<sigma>) a ! i; \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> i < Array.length (the_state \<sigma>) a; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis; run (Array.nth a i) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some aa; \<not> i < Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa. \<lbrakk>\<sigma> = Some aa; i < Array.length aa a; execute (Array.nth a i) aa = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa h'. \<lbrakk>\<lbrakk>r = Array.get aa a ! i; h' = aa\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; execute (Array.nth a i) aa = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
 3. \<And>aa h'. \<lbrakk>\<sigma> = Some aa; \<not> i < Array.length aa a; execute (Array.nth a i) aa = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp_all only: execute_simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa. \<lbrakk>\<sigma> = Some aa; i < Array.length aa a; Some (Array.get aa a ! i, aa) = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa h'. \<lbrakk>\<lbrakk>r = Array.get aa a ! i; h' = aa\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; Some (Array.get aa a ! i, aa) = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
 3. \<And>aa h'. \<lbrakk>\<sigma> = Some aa; \<not> i < Array.length aa a; None = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa h'. \<lbrakk>\<sigma> = Some aa; \<not> i < Array.length aa a; None = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<sigma> = Some aa; i < Array.length aa a; Some (Array.get aa a ! i, aa) = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 3. \<And>aa h'. \<lbrakk>\<lbrakk>r = Array.get aa a ! i; h' = aa\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; Some (Array.get aa a ! i, aa) = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa h'. \<lbrakk>\<lbrakk>r = Array.get aa a ! i; h' = aa\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some aa; i < Array.length aa a; Some (Array.get aa a ! i, aa) = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa h'. \<lbrakk>\<lbrakk>r = Array.get aa a ! i; h' = aa\<rbrakk> \<Longrightarrow> thesis; i < Array.length aa a; Some (Array.get aa a ! i, aa) = Some (r, h')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal premises prems for aa h'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(3)
[PROOF STATE]
proof (chain)
picking this:
Some (Array.get aa a ! i, aa) = Some (r, h')
[PROOF STEP]
have "r = Array.get aa a ! i" "h' = aa"
[PROOF STATE]
proof (prove)
using this:
Some (Array.get aa a ! i, aa) = Some (r, h')

goal (1 subgoal):
 1. r = Array.get aa a ! i &&& h' = aa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = Array.get aa a ! i
h' = aa

goal (1 subgoal):
 1. thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = Array.get aa a ! i
h' = aa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = Array.get aa a ! i
h' = aa

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma run_of_list[run_elims]:
  assumes "run (Array.of_list xs) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>)))"
          "r = fst (Array.alloc xs (the_state \<sigma>))"
          "Array.get (the_state \<sigma>') r = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>))); r = fst (Array.alloc xs (the_state \<sigma>)); Array.get (the_state \<sigma>') r = xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.of_list xs) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>))); r = fst (Array.alloc xs (the_state \<sigma>)); Array.get (the_state \<sigma>') r = xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>))); r = fst (Array.alloc xs (the_state \<sigma>)); Array.get (the_state \<sigma>') r = xs\<rbrakk> \<Longrightarrow> thesis; run (Array.of_list xs) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>))); r = fst (Array.alloc xs (the_state \<sigma>)); Array.get (the_state \<sigma>') r = xs\<rbrakk> \<Longrightarrow> thesis; run (Array.of_list xs) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc xs (the_state \<sigma>))); r = fst (Array.alloc xs (the_state \<sigma>)); Array.get (the_state \<sigma>') r = xs\<rbrakk> \<Longrightarrow> thesis; run (Array.of_list xs) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<sigma> = Some a; execute (Array.of_list xs) a = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc xs a); r = fst (Array.alloc xs a); Array.get (snd (Array.alloc xs a)) (fst (Array.alloc xs a)) = xs\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Array.of_list xs) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: execute_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc xs a); r = fst (Array.alloc xs a); Array.get (snd (Array.alloc xs a)) (fst (Array.alloc xs a)) = xs\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Array.of_list xs) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: Array.get_alloc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc xs a); r = fst (Array.alloc xs a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Array.of_list xs) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc xs a); r = fst (Array.alloc xs a)\<rbrakk> \<Longrightarrow> thesis; execute (Array.of_list xs) a = Some (r, h')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal premises prems for a h'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
execute (Array.of_list xs) a = Some (r, h')
[PROOF STEP]
have "h' = snd (Array.alloc xs a)"
      "r = fst (Array.alloc xs a)"
[PROOF STATE]
proof (prove)
using this:
execute (Array.of_list xs) a = Some (r, h')

goal (1 subgoal):
 1. h' = snd (Array.alloc xs a) &&& r = fst (Array.alloc xs a)
[PROOF STEP]
by (auto simp add: execute_simps)
[PROOF STATE]
proof (state)
this:
h' = snd (Array.alloc xs a)
r = fst (Array.alloc xs a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h' = snd (Array.alloc xs a)
r = fst (Array.alloc xs a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h' = snd (Array.alloc xs a)
r = fst (Array.alloc xs a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma run_freeze[run_elims]:
  assumes "run (Array.freeze a) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = \<sigma>"
          "r = Array.get (the_state \<sigma>) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = \<sigma>; r = Array.get (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.freeze a) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = \<sigma>; r = Array.get (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<sigma>' = \<sigma>; r = Array.get (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis; run (Array.freeze a) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<lbrakk>\<sigma>' = \<sigma>; r = Array.get (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis; run (Array.freeze a) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some aa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: run.simps execute_simps)


[STATEMENT]
lemma run_new_ref[run_elims]:
  assumes "run (ref x) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>)))"
          "r = fst (Ref.alloc x (the_state \<sigma>))"
          "Ref.get (the_state \<sigma>') r = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>))); r = fst (Ref.alloc x (the_state \<sigma>)); Ref.get (the_state \<sigma>') r = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (ref x) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>))); r = fst (Ref.alloc x (the_state \<sigma>)); Ref.get (the_state \<sigma>') r = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>))); r = fst (Ref.alloc x (the_state \<sigma>)); Ref.get (the_state \<sigma>') r = x\<rbrakk> \<Longrightarrow> thesis; run (ref x) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>))); r = fst (Ref.alloc x (the_state \<sigma>)); Ref.get (the_state \<sigma>') r = x\<rbrakk> \<Longrightarrow> thesis; run (ref x) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Ref.alloc x (the_state \<sigma>))); r = fst (Ref.alloc x (the_state \<sigma>)); Ref.get (the_state \<sigma>') r = x\<rbrakk> \<Longrightarrow> thesis; run (ref x) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<sigma> = Some a; execute (ref x) a = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Ref.alloc x a); r = fst (Ref.alloc x a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (ref x) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: execute_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Ref.alloc x a); r = fst (Ref.alloc x a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (ref x) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Ref.alloc x a); r = fst (Ref.alloc x a)\<rbrakk> \<Longrightarrow> thesis; execute (ref x) a = Some (r, h')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal premises prems for a h'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
execute (ref x) a = Some (r, h')
[PROOF STEP]
have
      "h' = snd (Ref.alloc x a)"
      "r = fst (Ref.alloc x a)"
[PROOF STATE]
proof (prove)
using this:
execute (ref x) a = Some (r, h')

goal (1 subgoal):
 1. h' = snd (Ref.alloc x a) &&& r = fst (Ref.alloc x a)
[PROOF STEP]
by (auto simp add: execute_simps)
[PROOF STATE]
proof (state)
this:
h' = snd (Ref.alloc x a)
r = fst (Ref.alloc x a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h' = snd (Ref.alloc x a)
r = fst (Ref.alloc x a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h' = snd (Ref.alloc x a)
r = fst (Ref.alloc x a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma run_update[run_elims]:
  assumes "run (p := x) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (Ref.set p x (the_state \<sigma>))" "r = ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (Ref.set p x (the_state \<sigma>)); r = ()\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (p := x) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (Ref.set p x (the_state \<sigma>)); r = ()\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Ref.update_def
[PROOF STATE]
proof (prove)
using this:
run (Heap_Monad.heap (\<lambda>h. ((), Ref.set p x h))) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (Ref.set p x (the_state \<sigma>)); r = ()\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: run_heap)


[STATEMENT]
lemma run_lookup[run_elims]:
  assumes "run (!p) \<sigma> \<sigma>' r"
          "\<not> is_exn \<sigma>"
  obtains "\<not>is_exn \<sigma>" "\<sigma>' = \<sigma>" "r = Ref.get (the_state \<sigma>) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Ref.get (the_state \<sigma>) p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (!p) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Ref.get (the_state \<sigma>) p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Ref.get (the_state \<sigma>) p\<rbrakk> \<Longrightarrow> thesis; run (!p) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Ref.get (the_state \<sigma>) p\<rbrakk> \<Longrightarrow> thesis; run (!p) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: run.simps execute_simps)


[STATEMENT]
lemma epath_shift:
  assumes "epath (srs @- steps)"
  shows "epath steps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. epath steps
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
epath (srs @- steps)

goal (1 subgoal):
 1. epath steps
[PROOF STEP]
by (induction srs arbitrary: steps) (auto elim: epath.cases)


[STATEMENT]
theorem soundness:
  assumes f: "tfinite t" and w: "wf t"
  shows "ssat (fst (root t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssat (fst (tree.root t))
[PROOF STEP]
using f w
[PROOF STATE]
proof (prove)
using this:
tfinite t
local.wf t

goal (1 subgoal):
 1. ssat (fst (tree.root t))
[PROOF STEP]
proof (induction t rule: tfinite.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<And>t'. t' |\<in>| cont t \<Longrightarrow> tfinite t'; \<And>t'. \<lbrakk>t' |\<in>| cont t; local.wf t'\<rbrakk> \<Longrightarrow> ssat (fst (tree.root t')); local.wf t\<rbrakk> \<Longrightarrow> ssat (fst (tree.root t))
[PROOF STEP]
case (tfinite t)
[PROOF STATE]
proof (state)
this:
?t'1 |\<in>| cont t \<Longrightarrow> tfinite ?t'1
\<lbrakk>?t'1 |\<in>| cont t; local.wf ?t'1\<rbrakk> \<Longrightarrow> ssat (fst (tree.root ?t'1))
local.wf t

goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<And>t'. t' |\<in>| cont t \<Longrightarrow> tfinite t'; \<And>t'. \<lbrakk>t' |\<in>| cont t; local.wf t'\<rbrakk> \<Longrightarrow> ssat (fst (tree.root t')); local.wf t\<rbrakk> \<Longrightarrow> ssat (fst (tree.root t))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssat (fst (tree.root t))
[PROOF STEP]
by (rule local_soundness[of "snd (root t)" _ "fimage (fst o root) (cont t)"], insert tfinite)
      (fastforce elim!: wf.cases)+
[PROOF STATE]
proof (state)
this:
ssat (fst (tree.root t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma admits_small_V_tupling:
    assumes "small (I :: V set)"
    shows "admits_tupling I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admits_tupling I
[PROOF STEP]
proof (unfold admits_tupling_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
let ?\<pi> = "\<lambda>f. UP (VLambda (ZFC_in_HOL.set I) (DN o f))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
have "?\<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ
[PROOF STEP]
using UP_mapsto
[PROOF STATE]
proof (prove)
using this:
arr_of \<in> UNIV \<rightarrow> Univ

goal (1 subgoal):
 1. (\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ

goal (1 subgoal):
 1. \<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ

goal (1 subgoal):
 1. \<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
have "inj_on ?\<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (I \<rightarrow> Univ) \<inter> extensional' I; y \<in> (I \<rightarrow> Univ) \<inter> extensional' I; arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> x)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> y))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix f g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (I \<rightarrow> Univ) \<inter> extensional' I; y \<in> (I \<rightarrow> Univ) \<inter> extensional' I; arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> x)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> y))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume f: "f \<in> (I \<rightarrow> Univ) \<inter> extensional' I"
[PROOF STATE]
proof (state)
this:
f \<in> (I \<rightarrow> Univ) \<inter> extensional' I

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (I \<rightarrow> Univ) \<inter> extensional' I; y \<in> (I \<rightarrow> Univ) \<inter> extensional' I; arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> x)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> y))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume g: "g \<in> (I \<rightarrow> Univ) \<inter> extensional' I"
[PROOF STATE]
proof (state)
this:
g \<in> (I \<rightarrow> Univ) \<inter> extensional' I

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (I \<rightarrow> Univ) \<inter> extensional' I; y \<in> (I \<rightarrow> Univ) \<inter> extensional' I; arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> x)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> y))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume eq: "UP (VLambda (ZFC_in_HOL.set I) (DN \<circ> f)) =
                    UP (VLambda (ZFC_in_HOL.set I) (DN \<circ> g))"
[PROOF STATE]
proof (state)
this:
arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> g))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (I \<rightarrow> Univ) \<inter> extensional' I; y \<in> (I \<rightarrow> Univ) \<inter> extensional' I; arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> x)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> y))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have 1: "VLambda (ZFC_in_HOL.set I) (DN \<circ> f) = VLambda (ZFC_in_HOL.set I) (DN \<circ> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set I) (DN \<circ> f) = VLambda (ZFC_in_HOL.set I) (DN \<circ> g)
[PROOF STEP]
using f g eq
[PROOF STATE]
proof (prove)
using this:
f \<in> (I \<rightarrow> Univ) \<inter> extensional' I
g \<in> (I \<rightarrow> Univ) \<inter> extensional' I
arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> g))

goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set I) (DN \<circ> f) = VLambda (ZFC_in_HOL.set I) (DN \<circ> g)
[PROOF STEP]
by (meson injD inj_UP)
[PROOF STATE]
proof (state)
this:
VLambda (ZFC_in_HOL.set I) (DN \<circ> f) = VLambda (ZFC_in_HOL.set I) (DN \<circ> g)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (I \<rightarrow> Univ) \<inter> extensional' I; y \<in> (I \<rightarrow> Univ) \<inter> extensional' I; arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> x)) = arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> y))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
have "x \<notin> I \<Longrightarrow> f x = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> I \<Longrightarrow> f x = g x
[PROOF STEP]
using f g extensional'_def [of I]
[PROOF STATE]
proof (prove)
using this:
f \<in> (I \<rightarrow> Univ) \<inter> extensional' I
g \<in> (I \<rightarrow> Univ) \<inter> extensional' I
extensional' I \<equiv> {f. \<forall>x. x \<notin> I \<longrightarrow> f x = unity}

goal (1 subgoal):
 1. x \<notin> I \<Longrightarrow> f x = g x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> I \<Longrightarrow> f x = g x

goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> I \<Longrightarrow> f x = g x

goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
have "x \<in> I \<Longrightarrow> f x = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> I \<Longrightarrow> f x = g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> I \<Longrightarrow> f x = g x
[PROOF STEP]
assume x: "x \<in> I"
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (1 subgoal):
 1. x \<in> I \<Longrightarrow> f x = g x
[PROOF STEP]
hence "(DN o f) x = (DN o g) x"
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. (DN \<circ> f) x = (DN \<circ> g) x
[PROOF STEP]
using assms 1 x elts_of_set VLambda_eq_D2
[PROOF STATE]
proof (prove)
using this:
x \<in> I
small I
VLambda (ZFC_in_HOL.set I) (DN \<circ> f) = VLambda (ZFC_in_HOL.set I) (DN \<circ> g)
x \<in> I
elts (ZFC_in_HOL.set ?X) = (if small ?X then ?X else {})
\<lbrakk>VLambda ?A ?f = VLambda ?A ?g; ?x \<in> elts ?A\<rbrakk> \<Longrightarrow> ?f ?x = ?g ?x

goal (1 subgoal):
 1. (DN \<circ> f) x = (DN \<circ> g) x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(DN \<circ> f) x = (DN \<circ> g) x

goal (1 subgoal):
 1. x \<in> I \<Longrightarrow> f x = g x
[PROOF STEP]
thus "f x = g x"
[PROOF STATE]
proof (prove)
using this:
(DN \<circ> f) x = (DN \<circ> g) x

goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
using f g x comp_apply UP_DN
[PROOF STATE]
proof (prove)
using this:
(DN \<circ> f) x = (DN \<circ> g) x
f \<in> (I \<rightarrow> Univ) \<inter> extensional' I
g \<in> (I \<rightarrow> Univ) \<inter> extensional' I
x \<in> I
(?f \<circ> ?g) ?x = ?f (?g ?x)
?t \<in> range arr_of \<Longrightarrow> arr_of (DN ?t) = ?t

goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
by (metis IntD1 PiE bij_arr_of bij_betw_imp_surj_on)
[PROOF STATE]
proof (state)
this:
f x = g x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> I \<Longrightarrow> f x = g x

goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> I \<Longrightarrow> f x = g x
x \<in> I \<Longrightarrow> f x = g x
[PROOF STEP]
show "f x = g x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> I \<Longrightarrow> f x = g x
x \<in> I \<Longrightarrow> f x = g x

goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f x = g x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f = g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) ((I \<rightarrow> Univ) \<inter> extensional' I)

goal (1 subgoal):
 1. \<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ
inj_on (\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
show "\<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and>
                           inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ
inj_on (\<lambda>f. arr_of (VLambda (ZFC_in_HOL.set I) (DN \<circ> f))) ((I \<rightarrow> Univ) \<inter> extensional' I)

goal (1 subgoal):
 1. \<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<pi>. \<pi> \<in> (I \<rightarrow> Univ) \<inter> extensional' I \<rightarrow> Univ \<and> inj_on \<pi> ((I \<rightarrow> Univ) \<inter> extensional' I)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_small_products:
    assumes "small (I :: 'i set)" and "I \<noteq> UNIV"
    shows "has_products I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_products I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. has_products I
[PROOF STEP]
have 1: "\<And>I :: V set. small I \<Longrightarrow> has_products I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I. small I \<Longrightarrow> has_products I
[PROOF STEP]
using big_UNIV
[PROOF STATE]
proof (prove)
using this:
\<not> small UNIV

goal (1 subgoal):
 1. \<And>I. small I \<Longrightarrow> has_products I
[PROOF STEP]
by (metis admits_small_tupling has_products_iff_admits_tupling)
[PROOF STATE]
proof (state)
this:
small ?I1 \<Longrightarrow> has_products ?I1

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
obtain V_of where V_of: "inj_on V_of I \<and> V_of ` I \<in> range elts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V_of. inj_on V_of I \<and> V_of ` I \<in> range elts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms small_def
[PROOF STATE]
proof (prove)
using this:
small I
I \<noteq> UNIV
small ?X \<equiv> \<exists>V_of. inj_on V_of ?X \<and> V_of ` ?X \<in> range elts

goal (1 subgoal):
 1. (\<And>V_of. inj_on V_of I \<and> V_of ` I \<in> range elts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inj_on V_of I \<and> V_of ` I \<in> range elts

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
have "bij_betw (inv_into I V_of) (V_of ` I) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (inv_into I V_of) (V_of ` I) I
[PROOF STEP]
using V_of bij_betw_inv_into bij_betw_imageI
[PROOF STATE]
proof (prove)
using this:
inj_on V_of I \<and> V_of ` I \<in> range elts
bij_betw ?f ?A ?B \<Longrightarrow> bij_betw (inv_into ?A ?f) ?B ?A
\<lbrakk>inj_on ?f ?A; ?f ` ?A = ?B\<rbrakk> \<Longrightarrow> bij_betw ?f ?A ?B

goal (1 subgoal):
 1. bij_betw (inv_into I V_of) (V_of ` I) I
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
bij_betw (inv_into I V_of) (V_of ` I) I

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw (inv_into I V_of) (V_of ` I) I

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
have "small (V_of ` I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (V_of ` I)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
small I
I \<noteq> UNIV

goal (1 subgoal):
 1. small (V_of ` I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
small (V_of ` I)

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw (inv_into I V_of) (V_of ` I) I
small (V_of ` I)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw (inv_into I V_of) (V_of ` I) I
small (V_of ` I)

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
using assms 1 has_products_preserved_by_bijection
[PROOF STATE]
proof (prove)
using this:
bij_betw (inv_into I V_of) (V_of ` I) I
small (V_of ` I)
small I
I \<noteq> UNIV
small ?I1 \<Longrightarrow> has_products ?I1
\<lbrakk>has_products ?I; bij_betw ?\<phi> ?I ?I'; ?I' \<noteq> UNIV\<rbrakk> \<Longrightarrow> has_products ?I'

goal (1 subgoal):
 1. has_products I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
has_products I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem has_small_limits:
    assumes "small (UNIV :: 'i set)"
    shows "has_limits (undefined :: 'i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_limits undefined
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. has_limits undefined
[PROOF STEP]
have "\<forall>I :: 'i set. I \<noteq> UNIV \<longrightarrow> admits_tupling I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>I. I \<noteq> UNIV \<longrightarrow> admits_tupling I
[PROOF STEP]
using assms smaller_than_small subset_UNIV admits_small_tupling
[PROOF STATE]
proof (prove)
using this:
small UNIV
\<lbrakk>small ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> small ?B
?A \<subseteq> UNIV
small ?I \<Longrightarrow> admits_tupling ?I

goal (1 subgoal):
 1. \<forall>I. I \<noteq> UNIV \<longrightarrow> admits_tupling I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>I. I \<noteq> UNIV \<longrightarrow> admits_tupling I

goal (1 subgoal):
 1. has_limits undefined
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>I. I \<noteq> UNIV \<longrightarrow> admits_tupling I

goal (1 subgoal):
 1. has_limits undefined
[PROOF STEP]
using assms has_limits_iff_admits_tupling
[PROOF STATE]
proof (prove)
using this:
\<forall>I. I \<noteq> UNIV \<longrightarrow> admits_tupling I
small UNIV
has_limits undefined = (\<forall>I. I \<noteq> UNIV \<longrightarrow> admits_tupling I)

goal (1 subgoal):
 1. has_limits undefined
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
has_limits undefined

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_sub_set_category:
    shows "sub_set_category Cls.comp (\<lambda>A. A \<subseteq> Cls.Univ) (\<lambda>A. A \<subseteq> Cls.Univ \<and> small A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_set_category Cls.comp (\<lambda>A. A \<subseteq> Cls.Univ) (\<lambda>A. A \<subseteq> Cls.Univ \<and> small A)
[PROOF STEP]
using sub_set_category_axioms
[PROOF STATE]
proof (prove)
using this:
sub_set_category Cls.comp (\<lambda>A. A \<subseteq> Cls.Univ) (\<lambda>A. A \<subseteq> Cls.Univ \<and> small A)

goal (1 subgoal):
 1. sub_set_category Cls.comp (\<lambda>A. A \<subseteq> Cls.Univ) (\<lambda>A. A \<subseteq> Cls.Univ \<and> small A)
[PROOF STEP]
by blast


[STATEMENT]
lemma bij_betw_ide_V:
    shows "V_of_ide \<in> Collect ide \<rightarrow> UNIV"
    and "ide_of_V \<in> UNIV \<rightarrow> Collect ide"
    and [simp]: "ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a"
    and [simp]: "V_of_ide (ide_of_V A) = A"
    and "bij_betw V_of_ide (Collect ide) UNIV"
    and "bij_betw ide_of_V UNIV (Collect ide)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V_of_ide \<in> Collect ide \<rightarrow> UNIV &&& ide_of_V \<in> UNIV \<rightarrow> Collect ide &&& (ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a)) &&& V_of_ide (ide_of_V A) = A &&& bij_betw V_of_ide (Collect ide) UNIV &&& bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. V_of_ide \<in> Collect ide \<rightarrow> UNIV
 2. ide_of_V \<in> UNIV \<rightarrow> Collect ide
 3. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
 4. V_of_ide (ide_of_V A) = A
 5. bij_betw V_of_ide (Collect ide) UNIV
 6. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
have "Univ = Cls.Univ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Univ = Cls.Univ
[PROOF STEP]
using terminal_char
[PROOF STATE]
proof (prove)
using this:
terminal ?t = Cls.terminal ?t

goal (1 subgoal):
 1. Univ = Cls.Univ
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
Univ = Cls.Univ

goal (6 subgoals):
 1. V_of_ide \<in> Collect ide \<rightarrow> UNIV
 2. ide_of_V \<in> UNIV \<rightarrow> Collect ide
 3. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
 4. V_of_ide (ide_of_V A) = A
 5. bij_betw V_of_ide (Collect ide) UNIV
 6. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
show 1: "V_of_ide \<in> Collect ide \<rightarrow> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V_of_ide \<in> Collect ide \<rightarrow> UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V_of_ide \<in> Collect ide \<rightarrow> UNIV

goal (5 subgoals):
 1. ide_of_V \<in> UNIV \<rightarrow> Collect ide
 2. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
 3. V_of_ide (ide_of_V A) = A
 4. bij_betw V_of_ide (Collect ide) UNIV
 5. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
show 2: "ide_of_V \<in> UNIV \<rightarrow> Collect ide"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide_of_V \<in> UNIV \<rightarrow> Collect ide
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ide_of_V x \<in> Collect ide
[PROOF STEP]
fix A :: V
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ide_of_V x \<in> Collect ide
[PROOF STEP]
have "small (elts A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (elts A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
small (elts A)

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ide_of_V x \<in> Collect ide
[PROOF STEP]
have "Cls.UP ` elts A \<subseteq> Univ \<and> small (Cls.UP ` elts A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.arr_of ` elts A \<subseteq> Univ \<and> small (Cls.arr_of ` elts A)
[PROOF STEP]
using Cls.UP_mapsto terminal_char
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of \<in> UNIV \<rightarrow> Cls.Univ
terminal ?t = Cls.terminal ?t

goal (1 subgoal):
 1. Cls.arr_of ` elts A \<subseteq> Univ \<and> small (Cls.arr_of ` elts A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.arr_of ` elts A \<subseteq> Univ \<and> small (Cls.arr_of ` elts A)

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ide_of_V x \<in> Collect ide
[PROOF STEP]
hence "ide (mkIde (Cls.UP ` elts A))"
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of ` elts A \<subseteq> Univ \<and> small (Cls.arr_of ` elts A)

goal (1 subgoal):
 1. ide (mkIde (Cls.arr_of ` elts A))
[PROOF STEP]
using ide_mkIde \<open>Univ = Cls.Univ\<close>
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of ` elts A \<subseteq> Univ \<and> small (Cls.arr_of ` elts A)
?A \<subseteq> Cls.Univ \<and> small ?A \<Longrightarrow> ide (mkIde ?A)
Univ = Cls.Univ

goal (1 subgoal):
 1. ide (mkIde (Cls.arr_of ` elts A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide (mkIde (Cls.arr_of ` elts A))

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ide_of_V x \<in> Collect ide
[PROOF STEP]
thus "ide_of_V A \<in> Collect ide"
[PROOF STATE]
proof (prove)
using this:
ide (mkIde (Cls.arr_of ` elts A))

goal (1 subgoal):
 1. ide_of_V A \<in> Collect ide
[PROOF STEP]
using ide_of_V_def ide_char\<^sub>S\<^sub>S\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide (mkIde (Cls.arr_of ` elts A))
ide_of_V ?A \<equiv> Cls.mkIde (Cls.arr_of ` elts ?A)
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))

goal (1 subgoal):
 1. ide_of_V A \<in> Collect ide
[PROOF STEP]
by (metis (no_types, lifting) Cls.ide_mkIde Cls.set_mkIde arr_mkIde ide_char'
              mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
ide_of_V A \<in> Collect ide

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ide_of_V \<in> UNIV \<rightarrow> Collect ide

goal (4 subgoals):
 1. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
 2. V_of_ide (ide_of_V A) = A
 3. bij_betw V_of_ide (Collect ide) UNIV
 4. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
show 3: "\<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
assume a: "ide a"
[PROOF STATE]
proof (state)
this:
ide a

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
have "ide_of_V (V_of_ide a) =
              Cls.mkIde (Cls.UP ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide_of_V (V_of_ide a) = Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)))
[PROOF STEP]
unfolding ide_of_V_def V_of_ide_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a))) = Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide_of_V (V_of_ide a) = Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)))

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ide_of_V (V_of_ide a) = Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a)))

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
have "... = Cls.mkIde (Cls.UP ` Cls.DN ` Cls.set a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a))) = Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a)
[PROOF STEP]
using setp_set_ide a ide_char\<^sub>S\<^sub>S\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide ?a \<Longrightarrow> local.set ?a \<subseteq> Cls.Univ \<and> small (local.set ?a)
ide a
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))

goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a))) = Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a))) = Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a)

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Cls.mkIde (Cls.arr_of ` elts (ZFC_in_HOL.set (Cls.DN ` Cls.set a))) = Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a)

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
have "... = Cls.mkIde (Cls.set a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)
[PROOF STEP]
have "Cls.set a \<subseteq> Cls.Univ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ
[PROOF STEP]
using a ide_char\<^sub>S\<^sub>S\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.set a \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)
[PROOF STEP]
hence "Cls.UP ` Cls.DN ` Cls.set a = Cls.set a"
[PROOF STATE]
proof (prove)
using this:
Cls.set a \<subseteq> Cls.Univ

goal (1 subgoal):
 1. Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<Longrightarrow> Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a
[PROOF STEP]
have "\<And>x. x \<in> Cls.set a \<Longrightarrow> x \<in> Cls.UP ` Cls.DN ` Cls.set a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> x \<in> Cls.arr_of ` Cls.DN ` Cls.set a
[PROOF STEP]
using Cls.UP_DN \<open>Cls.set a \<subseteq> Cls.Univ\<close>
[PROOF STATE]
proof (prove)
using this:
?t \<in> range Cls.arr_of \<Longrightarrow> Cls.arr_of (Cls.DN ?t) = ?t
Cls.set a \<subseteq> Cls.Univ

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.set a \<Longrightarrow> x \<in> Cls.arr_of ` Cls.DN ` Cls.set a
[PROOF STEP]
by (metis Cls.bij_arr_of bij_betw_def image_inv_into_cancel)
[PROOF STATE]
proof (state)
this:
?x1 \<in> Cls.set a \<Longrightarrow> ?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<Longrightarrow> Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x1 \<in> Cls.set a \<Longrightarrow> ?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<Longrightarrow> Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a
[PROOF STEP]
have "\<And>x. x \<in> Cls.UP ` Cls.DN ` Cls.set a \<Longrightarrow> x \<in> Cls.set a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.arr_of ` Cls.DN ` Cls.set a \<Longrightarrow> x \<in> Cls.set a
[PROOF STEP]
using \<open>Cls.set a \<subseteq> Cls.Univ\<close>
[PROOF STATE]
proof (prove)
using this:
Cls.set a \<subseteq> Cls.Univ

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.arr_of ` Cls.DN ` Cls.set a \<Longrightarrow> x \<in> Cls.set a
[PROOF STEP]
by (metis Cls.bij_arr_of bij_betw_def image_inv_into_cancel)
[PROOF STATE]
proof (state)
this:
?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a \<Longrightarrow> ?x1 \<in> Cls.set a

goal (1 subgoal):
 1. Cls.set a \<subseteq> Cls.Univ \<Longrightarrow> Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x1 \<in> Cls.set a \<Longrightarrow> ?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a
?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a \<Longrightarrow> ?x1 \<in> Cls.set a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> Cls.set a \<Longrightarrow> ?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a
?x1 \<in> Cls.arr_of ` Cls.DN ` Cls.set a \<Longrightarrow> ?x1 \<in> Cls.set a

goal (1 subgoal):
 1. Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a

goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of ` Cls.DN ` Cls.set a = Cls.set a

goal (1 subgoal):
 1. Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Cls.mkIde (Cls.arr_of ` Cls.DN ` Cls.set a) = Cls.mkIde (Cls.set a)

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
have "... = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.mkIde (Cls.set a) = a
[PROOF STEP]
using a Cls.mkIde_set ide_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide a
Cls.ide ?a \<Longrightarrow> Cls.mkIde (Cls.set ?a) = ?a
ide ?a = (arr ?a \<and> Cls.ide ?a)

goal (1 subgoal):
 1. Cls.mkIde (Cls.set a) = a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.mkIde (Cls.set a) = a

goal (1 subgoal):
 1. \<And>a. ide a \<Longrightarrow> ide_of_V (V_of_ide a) = a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ide_of_V (V_of_ide a) = a
[PROOF STEP]
show "ide_of_V (V_of_ide a) = a"
[PROOF STATE]
proof (prove)
using this:
ide_of_V (V_of_ide a) = a

goal (1 subgoal):
 1. ide_of_V (V_of_ide a) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide_of_V (V_of_ide a) = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ide ?a1 \<Longrightarrow> ide_of_V (V_of_ide ?a1) = ?a1

goal (3 subgoals):
 1. V_of_ide (ide_of_V A) = A
 2. bij_betw V_of_ide (Collect ide) UNIV
 3. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
show 4: "\<And>A. V_of_ide (ide_of_V A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
have "V_of_ide (ide_of_V A) =
              ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.UP ` elts A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V_of_ide (ide_of_V A) = ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A)))
[PROOF STEP]
unfolding V_of_ide_def ide_of_V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A))) = ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_of_ide (ide_of_V A) = ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A)))

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
V_of_ide (ide_of_V A) = ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A)))

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
have "... = ZFC_in_HOL.set (Cls.DN ` Cls.UP ` elts A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A))) = ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A)
[PROOF STEP]
using Cls.set_mkIde [of "Cls.UP ` elts A"] Cls.UP_mapsto
[PROOF STATE]
proof (prove)
using this:
Cls.arr_of ` elts A \<subseteq> Cls.Univ \<Longrightarrow> Cls.set (Cls.mkIde (Cls.arr_of ` elts A)) = Cls.arr_of ` elts A
Cls.arr_of \<in> UNIV \<rightarrow> Cls.Univ

goal (1 subgoal):
 1. ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A))) = ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A))) = ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A)

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set (Cls.DN ` Cls.set (Cls.mkIde (Cls.arr_of ` elts A))) = ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A)

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
have "... = ZFC_in_HOL.set (elts A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A) = ZFC_in_HOL.set (elts A)
[PROOF STEP]
using Cls.DN_UP
[PROOF STATE]
proof (prove)
using this:
?x \<in> UNIV \<Longrightarrow> Cls.DN (Cls.arr_of ?x) = ?x

goal (1 subgoal):
 1. ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A) = ZFC_in_HOL.set (elts A)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A) = ZFC_in_HOL.set (elts A)

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set (Cls.DN ` Cls.arr_of ` elts A) = ZFC_in_HOL.set (elts A)

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
have "... = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set (elts A) = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set (elts A) = A

goal (1 subgoal):
 1. \<And>A. V_of_ide (ide_of_V A) = A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
V_of_ide (ide_of_V A) = A
[PROOF STEP]
show "V_of_ide (ide_of_V A) = A"
[PROOF STATE]
proof (prove)
using this:
V_of_ide (ide_of_V A) = A

goal (1 subgoal):
 1. V_of_ide (ide_of_V A) = A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V_of_ide (ide_of_V A) = A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
V_of_ide (ide_of_V ?A1) = ?A1

goal (2 subgoals):
 1. bij_betw V_of_ide (Collect ide) UNIV
 2. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
show "bij_betw V_of_ide (Collect ide) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw V_of_ide (Collect ide) UNIV
[PROOF STEP]
using 1 2 3 4
[PROOF STATE]
proof (prove)
using this:
V_of_ide \<in> Collect ide \<rightarrow> UNIV
ide_of_V \<in> UNIV \<rightarrow> Collect ide
ide ?a1 \<Longrightarrow> ide_of_V (V_of_ide ?a1) = ?a1
V_of_ide (ide_of_V ?A1) = ?A1

goal (1 subgoal):
 1. bij_betw V_of_ide (Collect ide) UNIV
[PROOF STEP]
by (intro bij_betwI) auto
[PROOF STATE]
proof (state)
this:
bij_betw V_of_ide (Collect ide) UNIV

goal (1 subgoal):
 1. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
show "bij_betw ide_of_V UNIV (Collect ide)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
using 1 2 3 4
[PROOF STATE]
proof (prove)
using this:
V_of_ide \<in> Collect ide \<rightarrow> UNIV
ide_of_V \<in> UNIV \<rightarrow> Collect ide
ide ?a1 \<Longrightarrow> ide_of_V (V_of_ide ?a1) = ?a1
V_of_ide (ide_of_V ?A1) = ?A1

goal (1 subgoal):
 1. bij_betw ide_of_V UNIV (Collect ide)
[PROOF STEP]
by (intro bij_betwI) blast+
[PROOF STATE]
proof (state)
this:
bij_betw ide_of_V UNIV (Collect ide)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_Collect_vfun:
    shows "small (Collect (vfun A B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (Collect (vfun A B))
[PROOF STEP]
unfolding vfun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {f \<in> elts (VPow (vtimes A B)). elts A = Domain (pairs f) \<and> single_valued (pairs f)}
[PROOF STEP]
by (metis (full_types) small_Collect small_elts)


[STATEMENT]
lemma vfunI:
    assumes "f \<in> elts A \<rightarrow> elts B"
    shows "vfun A B (VLambda A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfun A B (VLambda A f)
[PROOF STEP]
proof (unfold vfun_def, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. VLambda A f \<in> elts (VPow (vtimes A B))
 2. elts A = Domain (pairs (VLambda A f))
 3. single_valued (pairs (VLambda A f))
[PROOF STEP]
show "VLambda A f \<in> elts (VPow (vtimes A B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VLambda A f \<in> elts (VPow (vtimes A B))
[PROOF STEP]
using assms VLambda_def
[PROOF STATE]
proof (prove)
using this:
f \<in> elts A \<rightarrow> elts B
VLambda ?A ?b \<equiv> ZFC_in_HOL.set ((\<lambda>x. \<langle>x, ?b x\<rangle>) ` elts ?A)

goal (1 subgoal):
 1. VLambda A f \<in> elts (VPow (vtimes A B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
VLambda A f \<in> elts (VPow (vtimes A B))

goal (2 subgoals):
 1. elts A = Domain (pairs (VLambda A f))
 2. single_valued (pairs (VLambda A f))
[PROOF STEP]
show "elts A = Domain (pairs (VLambda A f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts A = Domain (pairs (VLambda A f))
[PROOF STEP]
using assms VLambda_def [of A f]
[PROOF STATE]
proof (prove)
using this:
f \<in> elts A \<rightarrow> elts B
VLambda A f \<equiv> ZFC_in_HOL.set ((\<lambda>x. \<langle>x, f x\<rangle>) ` elts A)

goal (1 subgoal):
 1. elts A = Domain (pairs (VLambda A f))
[PROOF STEP]
by (metis Domain_fst fst_pairs_VLambda)
[PROOF STATE]
proof (state)
this:
elts A = Domain (pairs (VLambda A f))

goal (1 subgoal):
 1. single_valued (pairs (VLambda A f))
[PROOF STEP]
show "single_valued (pairs (VLambda A f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (pairs (VLambda A f))
[PROOF STEP]
using assms VLambda_def single_valued_def pairs_iff_elts
[PROOF STATE]
proof (prove)
using this:
f \<in> elts A \<rightarrow> elts B
VLambda ?A ?b \<equiv> ZFC_in_HOL.set ((\<lambda>x. \<langle>x, ?b x\<rangle>) ` elts ?A)
single_valued ?r = (\<forall>x y. (x, y) \<in> ?r \<longrightarrow> (\<forall>z. (x, z) \<in> ?r \<longrightarrow> y = z))
((?x, ?y) \<in> pairs ?z) = (\<langle>?x, ?y\<rangle> \<in> elts ?z)

goal (1 subgoal):
 1. single_valued (pairs (VLambda A f))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
single_valued (pairs (VLambda A f))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma app_vfun_mapsto:
    assumes "vfun A B F"
    shows "app F \<in> elts A \<rightarrow> elts B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app F \<in> elts A \<rightarrow> elts B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app F x \<in> elts B
[PROOF STEP]
have "F \<in> elts (VPow (vtimes A B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> elts (VPow (vtimes A B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)
[PROOF STEP]
using assms vfun_def
[PROOF STATE]
proof (prove)
using this:
vfun A B F
vfun ?A ?B ?f \<equiv> ?f \<in> elts (VPow (vtimes ?A ?B)) \<and> elts ?A = Domain (pairs ?f) \<and> single_valued (pairs ?f)

goal (1 subgoal):
 1. F \<in> elts (VPow (vtimes A B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<in> elts (VPow (vtimes A B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app F x \<in> elts B
[PROOF STEP]
hence 1: "F \<in> elts (VPi A (\<lambda>_. B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)"
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPow (vtimes A B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. F \<in> elts (VPi A (\<lambda>_. B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)
[PROOF STEP]
unfolding VPi_def
[PROOF STATE]
proof (prove)
using this:
F \<in> elts (VPow (vtimes A B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. F \<in> elts (ZFC_in_HOL.set {f \<in> elts (VPow (vtimes A B)). elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)
[PROOF STEP]
by (metis (no_types, lifting) down elts_of_set mem_Collect_eq subsetI)
[PROOF STATE]
proof (state)
this:
F \<in> elts (VPi A (\<lambda>_. B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)

goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app F x \<in> elts B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app F x \<in> elts B
[PROOF STEP]
assume x: "x \<in> elts A"
[PROOF STATE]
proof (state)
this:
x \<in> elts A

goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app F x \<in> elts B
[PROOF STEP]
have "x \<in> Domain (pairs F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Domain (pairs F)
[PROOF STEP]
using assms x vfun_def
[PROOF STATE]
proof (prove)
using this:
vfun A B F
x \<in> elts A
vfun ?A ?B ?f \<equiv> ?f \<in> elts (VPow (vtimes ?A ?B)) \<and> elts ?A = Domain (pairs ?f) \<and> single_valued (pairs ?f)

goal (1 subgoal):
 1. x \<in> Domain (pairs F)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> Domain (pairs F)

goal (1 subgoal):
 1. \<And>x. x \<in> elts A \<Longrightarrow> app F x \<in> elts B
[PROOF STEP]
thus "app F x \<in> elts B"
[PROOF STATE]
proof (prove)
using this:
x \<in> Domain (pairs F)

goal (1 subgoal):
 1. app F x \<in> elts B
[PROOF STEP]
using x 1 VPi_D [of F A "\<lambda>_. B" x]
[PROOF STATE]
proof (prove)
using this:
x \<in> Domain (pairs F)
x \<in> elts A
F \<in> elts (VPi A (\<lambda>_. B)) \<and> elts A = Domain (pairs F) \<and> single_valued (pairs F)
\<lbrakk>F \<in> elts (VPi A (\<lambda>_. B)); x \<in> elts A\<rbrakk> \<Longrightarrow> app F x \<in> elts B

goal (1 subgoal):
 1. app F x \<in> elts B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
app F x \<in> elts B

goal:
No subgoals!
[PROOF STEP]
qed