[STATEMENT]
lemma circular_list_rev_II:
 "\<Gamma>\<turnstile>
 \<lbrace>\<acute>p = r \<and> distPath \<acute>p \<acute>next \<acute>p (r#Ps)\<rbrace>
\<acute>q:==Null;;
WHILE \<acute>p \<noteq> Null
INV
 \<lbrace> ((\<acute>q = Null) \<longrightarrow> (\<exists>ps. distPath \<acute>p \<acute>next r ps  \<and>  ps = r#Ps)) \<and>
  ((\<acute>q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath \<acute>q \<acute>next r qs  \<and> List \<acute>p \<acute>next ps  \<and>
                   set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
  \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null )
   \<rbrace>
DO
  \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q:==\<acute>tmp
OD
 \<lbrace>\<acute>q = r \<and> distPath \<acute>q \<acute>next \<acute>q (r # rev Ps)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>p = r \<and> distPath \<acute>p \<acute>next \<acute>p (r # Ps)\<rbrace> \<acute>q :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>(\<acute>q = Null \<longrightarrow> (\<exists>ps. distPath \<acute>p \<acute>next r ps \<and> ps = r # Ps)) \<and> (\<acute>q \<noteq> Null \<longrightarrow> (\<exists>ps qs. distPath \<acute>q \<acute>next r qs \<and> List \<acute>p \<acute>next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null)\<rbrace> DO \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>tmp OD \<lbrace>\<acute>q = r \<and> distPath \<acute>q \<acute>next \<acute>q (r # rev Ps)\<rbrace>
[PROOF STEP]
apply (simp only:distPath_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>p = r \<and> Path \<acute>p \<acute>next \<acute>p (r # Ps) \<and> distinct (r # Ps)\<rbrace> \<acute>q :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>(\<acute>q = Null \<longrightarrow> (\<exists>ps. (Path \<acute>p \<acute>next r ps \<and> distinct ps) \<and> ps = r # Ps)) \<and> (\<acute>q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (Path \<acute>q \<acute>next r qs \<and> distinct qs) \<and> List \<acute>p \<acute>next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null)\<rbrace> DO \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>tmp OD \<lbrace>\<acute>q = r \<and> Path \<acute>q \<acute>next \<acute>q (r # rev Ps) \<and> distinct (r # rev Ps)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next p. \<lbrakk>Path p next p (p # Ps); distinct (p # Ps)\<rbrakk> \<Longrightarrow> (Null = Null \<longrightarrow> (\<exists>ps. Path p next p ps \<and> distinct ps \<and> ps = p # Ps)) \<and> (Null \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path Null next p qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [p])) \<and> \<not> (p = Null \<and> Null = Null \<and> p = Null)
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); p \<noteq> Null\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> (\<exists>ps. Path (next p) (next(p := q)) r ps \<and> distinct ps \<and> ps = r # Ps)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path p (next(p := q)) r qs \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (next p = Null \<and> p = Null \<and> r = Null)
 3. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); p \<noteq> Null\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> (\<exists>ps. Path (next p) (next(p := q)) r ps \<and> distinct ps \<and> ps = r # Ps)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path p (next(p := q)) r qs \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (next p = Null \<and> p = Null \<and> r = Null)
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (case_tac "(q = Null)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q = Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 3. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   (fastforce intro: path_is_list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x="psa" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> \<exists>qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) psa \<and> set psa \<inter> set qs = {} \<and> rev qs @ psa = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x=" p # qs" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> (p # qs = [] \<and> r = p \<or> (\<exists>ps. p # qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct (p # qs) \<and> List (next p) (next(p := q)) psa \<and> set psa \<inter> set (p # qs) = {} \<and> rev (p # qs) @ psa = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unit_not_var:
  shows "Unit \<noteq> Var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Unit \<noteq> Var x
[PROOF STEP]
proof(transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<not> PUnit \<approx> PVar x
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<not> PUnit \<approx> PVar x
[PROOF STEP]
show "\<not> PUnit \<approx> PVar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> PUnit \<approx> PVar x
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> PUnit \<approx> PVar x \<Longrightarrow> \<not> PUnit \<approx> PVar x
[PROOF STEP]
assume "\<not>\<not> PUnit \<approx> PVar x"
[PROOF STATE]
proof (state)
this:
\<not> \<not> PUnit \<approx> PVar x

goal (1 subgoal):
 1. \<not> \<not> PUnit \<approx> PVar x \<Longrightarrow> \<not> PUnit \<approx> PVar x
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> PUnit \<approx> PVar x

goal (1 subgoal):
 1. False
[PROOF STEP]
using unitE
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> PUnit \<approx> PVar x
\<lbrakk>PUnit \<approx> ?Y; ?Y = PUnit \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> \<not> PUnit \<approx> PVar x \<Longrightarrow> \<not> PUnit \<approx> PVar x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<not> PUnit \<approx> PVar x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> PUnit \<approx> PVar x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> PUnit \<approx> PVar x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_Gromov_completion_continuous:
  "continuous_on UNIV to_Gromov_completion"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV to_Gromov_completion
[PROOF STEP]
by (rule homeomorphism_on_continuous[OF to_Gromov_completion_homeomorphism])


[STATEMENT]
lemma ord_of_nat_add: "ord_of_nat (m+n) = ord_of_nat m + ord_of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of_nat (m + n) = ord_of_nat m + ord_of_nat n
[PROOF STEP]
by (induction n) (auto simp: plus_V_succ_right)


[STATEMENT]
lemma mult_add_mem:
  assumes "a*x + r \<in> elts (a*y)" "r \<sqsubset> a"
  shows "x \<in> elts y" "r \<in> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> elts y &&& r \<in> elts a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> elts y
 2. r \<in> elts a
[PROOF STEP]
obtain v s where v: "a * x + r = a * v + s" "v \<in> elts y" "s \<in> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v s. \<lbrakk>a * x + r = a * v + s; v \<in> elts y; s \<in> elts a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a * x + r \<in> elts (a * y)
r \<sqsubset> a

goal (1 subgoal):
 1. (\<And>v s. \<lbrakk>a * x + r = a * v + s; v \<in> elts y; s \<in> elts a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mult [of a y] lift_def
[PROOF STATE]
proof (prove)
using this:
a * x + r \<in> elts (\<Squnion>u\<in>elts y. set ((+) (a * u) ` elts a))
r \<sqsubset> a

goal (1 subgoal):
 1. (\<And>v s. \<lbrakk>a * x + r = a * v + s; v \<in> elts y; s \<in> elts a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * x + r = a * v + s
v \<in> elts y
s \<in> elts a

goal (2 subgoals):
 1. x \<in> elts y
 2. r \<in> elts a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a * x + r = a * v + s
v \<in> elts y
s \<in> elts a
[PROOF STEP]
show "x \<in> elts y"
[PROOF STATE]
proof (prove)
using this:
a * x + r = a * v + s
v \<in> elts y
s \<in> elts a

goal (1 subgoal):
 1. x \<in> elts y
[PROOF STEP]
by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma vsubsetD)
[PROOF STATE]
proof (state)
this:
x \<in> elts y

goal (1 subgoal):
 1. r \<in> elts a
[PROOF STEP]
show "r \<in> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> elts a
[PROOF STEP]
by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma v(1) v(3) vsubsetD)
[PROOF STATE]
proof (state)
this:
r \<in> elts a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma semicategoryI':
  assumes "\<Z> \<alpha>"
    and "vfsequence \<CC>"
    and "vsv (\<CC>\<lparr>Comp\<rparr>)"
    and "vcard \<CC> = 5\<^sub>\<nat>"
    and "vsv (\<CC>\<lparr>Dom\<rparr>)"
    and "vsv (\<CC>\<lparr>Cod\<rparr>)"
    and "\<D>\<^sub>\<circ> (\<CC>\<lparr>Dom\<rparr>) = \<CC>\<lparr>Arr\<rparr>"
    and "\<R>\<^sub>\<circ> (\<CC>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
    and "\<D>\<^sub>\<circ> (\<CC>\<lparr>Cod\<rparr>) = \<CC>\<lparr>Arr\<rparr>"
    and "\<R>\<^sub>\<circ> (\<CC>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
    and "\<And>gf. gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<CC>\<lparr>Comp\<rparr>) \<longleftrightarrow>
      (\<exists>g f b c a. gf = [g, f]\<^sub>\<circ> \<and> g : b \<mapsto>\<^bsub>\<CC>\<^esub> c \<and> f : a \<mapsto>\<^bsub>\<CC>\<^esub> b)"
    and "\<And>b c g a f. \<lbrakk> g : b \<mapsto>\<^bsub>\<CC>\<^esub> c; f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f : a \<mapsto>\<^bsub>\<CC>\<^esub> c"
    and "\<And>c d h b g a f. \<lbrakk> h : c \<mapsto>\<^bsub>\<CC>\<^esub> d; g : b \<mapsto>\<^bsub>\<CC>\<^esub> c; f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<rbrakk> \<Longrightarrow>
        (h \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g) \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = h \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)"
    and "\<CC>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
    and "\<And>A B. \<lbrakk> A \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha> \<rbrakk> \<Longrightarrow>
      (\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. Hom \<CC> a b) \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "semicategory \<alpha> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> \<CC>
[PROOF STEP]
by (intro semicategoryI digraphI, unfold slicing_simps)
    (simp_all add: assms  nat_omega_simps smc_dg_def)


[STATEMENT]
lemma \<delta>_statesI:
  assumes A: "(q \<rightarrow> l qs)\<in>\<delta>"
  shows "q\<in>\<delta>_states \<delta>"
        "set qs \<subseteq> \<delta>_states \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> \<delta>_states \<delta> &&& set qs \<subseteq> \<delta>_states \<delta>
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
q \<rightarrow> l qs \<in> \<delta>

goal (1 subgoal):
 1. q \<in> \<delta>_states \<delta> &&& set qs \<subseteq> \<delta>_states \<delta>
[PROOF STEP]
apply (unfold \<delta>_states_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q \<rightarrow> l qs \<in> \<delta> \<Longrightarrow> q \<in> \<Union> (rule_states ` \<delta>)
 2. q \<rightarrow> l qs \<in> \<delta> \<Longrightarrow> set qs \<subseteq> \<Union> (rule_states ` \<delta>)
[PROOF STEP]
by (auto split: ta_rule.split simp add: rule_states_simp)


[STATEMENT]
lemma leaf_not_mem_awalk:
  "\<lbrakk> leaf x; awalk u p v; v \<noteq> x \<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p)
[PROOF STEP]
proof(induction p arbitrary: u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. \<lbrakk>leaf x; awalk u [] v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u [])
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
leaf x
awalk u [] v
v \<noteq> x

goal (2 subgoals):
 1. \<And>u. \<lbrakk>leaf x; awalk u [] v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u [])
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leaf x
awalk u [] v
v \<noteq> x
[PROOF STEP]
have "u = v"
[PROOF STATE]
proof (prove)
using this:
leaf x
awalk u [] v
v \<noteq> x

goal (1 subgoal):
 1. u = v
[PROOF STEP]
unfolding awalk_conv
[PROOF STATE]
proof (prove)
using this:
leaf x
set (awalk_verts u []) \<subseteq> verts T \<and> set [] \<subseteq> arcs T \<and> awhd u [] = u \<and> awlast u [] = v \<and> cas u [] v
v \<noteq> x

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. \<And>u. \<lbrakk>leaf x; awalk u [] v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u [])
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
with Nil
[PROOF STATE]
proof (chain)
picking this:
leaf x
awalk u [] v
v \<noteq> x
u = v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
leaf x
awalk u [] v
v \<noteq> x
u = v

goal (1 subgoal):
 1. x \<notin> set (awalk_verts u [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts u [])

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>leaf x; awalk ?u2 p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts ?u2 p)
leaf x
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>leaf x; awalk ?u2 p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts ?u2 p)
leaf x
awalk u (a # p) v
v \<noteq> x
[PROOF STEP]
have "x \<notin> set (awalk_verts (head T a) p)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>leaf x; awalk ?u2 p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts ?u2 p)
leaf x
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. x \<notin> set (awalk_verts (head T a) p)
[PROOF STEP]
by (simp add: awalk_Cons_iff)
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts (head T a) p)

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts (head T a) p)

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
leaf x
awalk u (a # p) v
v \<noteq> x
[PROOF STEP]
have "tail T a \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
leaf x
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. tail T a \<noteq> x
[PROOF STEP]
unfolding leaf_def out_arcs_def
[PROOF STATE]
proof (prove)
using this:
x \<in> verts T \<and> {e \<in> arcs T. tail T e = x} = {}
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. tail T a \<noteq> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tail T a \<noteq> x

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set (awalk_verts (head T a) p)
tail T a \<noteq> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (awalk_verts (head T a) p)
tail T a \<noteq> x

goal (1 subgoal):
 1. x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts u (a # p))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma depth_lowerB: "v \<in> verts T \<Longrightarrow> depth w \<ge> \<mu> w root v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
assume "v \<in> verts T"
[PROOF STATE]
proof (state)
this:
v \<in> verts T

goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> verts T
[PROOF STEP]
have "\<mu> w root v \<in> {\<mu> w root v|v. v \<in> verts T}"
[PROOF STATE]
proof (prove)
using this:
v \<in> verts T

goal (1 subgoal):
 1. \<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}

goal (1 subgoal):
 1. v \<in> verts T \<Longrightarrow> \<mu> w root v \<le> depth w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}
[PROOF STEP]
show "depth w \<ge> \<mu> w root v"
[PROOF STATE]
proof (prove)
using this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}

goal (1 subgoal):
 1. \<mu> w root v \<le> depth w
[PROOF STEP]
unfolding depth_def
[PROOF STATE]
proof (prove)
using this:
\<mu> w root v \<in> {\<mu> w root v |v. v \<in> verts T}

goal (1 subgoal):
 1. \<mu> w root v \<le> Sup {\<mu> w root v |v. v \<in> verts T}
[PROOF STEP]
by (simp add: Sup_upper)
[PROOF STATE]
proof (state)
this:
\<mu> w root v \<le> depth w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem app_eq: "app xs ys zs = (zs = xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app xs ys zs = (zs = xs @ ys)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. app xs ys zs \<Longrightarrow> zs = xs @ ys
 2. zs = xs @ ys \<Longrightarrow> app xs ys zs
[PROOF STEP]
apply (erule app_eq2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zs = xs @ ys \<Longrightarrow> app xs ys zs
[PROOF STEP]
apply (erule app_eq1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Var':
  "l V = Some v \<Longrightarrow>
  P,E \<turnstile> \<langle>Var V,(h,l)\<rangle> \<Rightarrow>' \<langle>Val v,(h,l)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l V = \<lfloor>v\<rfloor> \<Longrightarrow> P,E \<turnstile> \<langle>Var V,(h, l)\<rangle> \<Rightarrow>' \<langle>Val v,(h, l)\<rangle>
[PROOF STEP]
by transfer(rule Var)


[STATEMENT]
lemma (in lbv) merge_pres:
  assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
  shows "merge c pc ss x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
from s0
[PROOF STATE]
proof (chain)
picking this:
snd ` set ss \<subseteq> A
[PROOF STEP]
have "set (map snd [(p', t') \<leftarrow> ss . p'=pc+1]) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
snd ` set ss \<subseteq> A

goal (1 subgoal):
 1. set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A

goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
with x semilat Semilat_axioms
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
semilat (A, r, f)
Semilat A r f
set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A
[PROOF STEP]
have "(map snd [(p', t') \<leftarrow> ss . p'=pc+1] \<Squnion>\<^bsub>f\<^esub> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
semilat (A, r, f)
Semilat A r f
set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A

goal (1 subgoal):
 1. map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A
[PROOF STEP]
by (auto intro!: plusplus_closed)
[PROOF STATE]
proof (state)
this:
map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A

goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
with s0 x
[PROOF STATE]
proof (chain)
picking this:
snd ` set ss \<subseteq> A
x \<in> A
map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
snd ` set ss \<subseteq> A
x \<in> A
map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A

goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
by (simp add: merge_def T_A)
[PROOF STATE]
proof (state)
this:
merge c pc ss x \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SPRAY_event:
  "SPRAY x \<noteq> {} \<Longrightarrow> x \<in> \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPRAY x \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
proof (unfold SPRAY_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R \<in> \<P>. x \<in> R} \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
assume nonempty_SPRAY: "{R \<in> \<P>. x \<in> R} \<noteq> {}"
[PROOF STATE]
proof (state)
this:
{R \<in> \<P>. x \<in> R} \<noteq> {}

goal (1 subgoal):
 1. {R \<in> \<P>. x \<in> R} \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{R \<in> \<P>. x \<in> R} \<noteq> {}
[PROOF STEP]
have x_in_path_R: "\<exists>R \<in> \<P>. x \<in> R"
[PROOF STATE]
proof (prove)
using this:
{R \<in> \<P>. x \<in> R} \<noteq> {}

goal (1 subgoal):
 1. \<exists>R\<in>\<P>. x \<in> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>R\<in>\<P>. x \<in> R

goal (1 subgoal):
 1. {R \<in> \<P>. x \<in> R} \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
thus "x \<in> \<E>"
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<in>\<P>. x \<in> R

goal (1 subgoal):
 1. x \<in> \<E>
[PROOF STEP]
using in_path_event
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<in>\<P>. x \<in> R
\<lbrakk>?Q \<in> \<P>; ?a \<in> ?Q\<rbrakk> \<Longrightarrow> ?a \<in> \<E>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma or_lem: "(a=c) ==> (b=d) ==> (a | b) = (c | d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = c; b = d\<rbrakk> \<Longrightarrow> (a \<or> b) = (c \<or> d)
[PROOF STEP]
by simp


[STATEMENT]
lemma zero_vector_5:
  "zero_vector x \<longleftrightarrow> x * top = x * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_vector x = (x * top = x * bot)
[PROOF STEP]
by (metis top_right_mult_increasing zero_vector_def zero_vector_left_zero)


[STATEMENT]
lemma zero_vector_one_vector_vector:
  "zero_vector x \<Longrightarrow> one_vector x \<Longrightarrow> vector x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zero_vector x; one_vector x\<rbrakk> \<Longrightarrow> vector x
[PROOF STEP]
by (metis one_vector_def vector_1 zero_vector_0)


[STATEMENT]
lemma top_one_vector:
  "one_vector top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_vector top
[PROOF STEP]
by (simp add: one_vector_def)


[STATEMENT]
lemma not_IndP_VarP: "{IndP x, VarP x} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
obtain m::name  where "atom m \<sharp> (x,A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. atom m \<sharp> (x, A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom m \<sharp> (x, A)

goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom m \<sharp> (x, A)

goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
by  (auto simp: fresh_Pair) (blast intro: ExFalso cut_same [OF VarP_cong [THEN Iff_MP_same]])
[PROOF STATE]
proof (state)
this:
{IndP x, VarP x} \<turnstile> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_zero_representation:
  "v = 0"
  if "\<And>b. b \<in> B \<Longrightarrow> representation B v b = 0" and v: "v \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
have empty: "{b. representation B v b \<noteq> 0} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {b. representation B v b \<noteq> 0} = {}
[PROOF STEP]
using that(1) representation_ne_zero
[PROOF STATE]
proof (prove)
using this:
?b \<in> B \<Longrightarrow> representation B v ?b = 0
representation ?basis ?v ?b \<noteq> 0 \<Longrightarrow> ?b \<in> ?basis

goal (1 subgoal):
 1. {b. representation B v b \<noteq> 0} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{b. representation B v b \<noteq> 0} = {}

goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
have "v \<in> span B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> span B
[PROOF STEP]
using B v
[PROOF STATE]
proof (prove)
using this:
independent B
span B = S
v \<in> S

goal (1 subgoal):
 1. v \<in> span B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> span B

goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
from sum_nonzero_representation_eq[OF B(1) this]
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>b | representation B v b \<noteq> 0. representation B v b *\<^sub>R b) = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>b | representation B v b \<noteq> 0. representation B v b *\<^sub>R b) = v

goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
by (simp add: empty)
[PROOF STATE]
proof (state)
this:
v = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subspace_S: "subspace S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subspace S
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
independent B
span B = S

goal (1 subgoal):
 1. subspace S
[PROOF STEP]
by auto


[STATEMENT]
lemma (in pcategory) pcat_vsubset_index_pcategory:
  assumes "J \<subseteq>\<^sub>\<circ> I"
  shows "pcategory \<alpha> J \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcategory \<alpha> J \<AA>
[PROOF STEP]
proof(intro pcategoryI pcategory_psemicategoryI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja. Ja \<subseteq>\<^sub>\<circ> J \<Longrightarrow> cat_prod Ja \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 3. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>" if \<open>J' \<subseteq>\<^sub>\<circ> J\<close> for J'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
have "J' \<subseteq>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
show "cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule pcat_Obj_vsubset_Vset)
[PROOF STATE]
proof (state)
this:
cat_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?J' \<subseteq>\<^sub>\<circ> J \<Longrightarrow> cat_prod ?J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
fix A B J'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume prems:
    "J' \<subseteq>\<^sub>\<circ> J"
    "A \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>Ci\<in>\<^sub>\<circ>J'. \<AA> i)\<lparr>Obj\<rparr>"
    "B \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>Ci\<in>\<^sub>\<circ>J'. \<AA> i)\<lparr>Obj\<rparr>"
    "A \<in>\<^sub>\<circ> Vset \<alpha>"
    "B \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> J
A \<subseteq>\<^sub>\<circ> cat_prod J' \<AA>\<lparr>Obj\<rparr>
B \<subseteq>\<^sub>\<circ> cat_prod J' \<AA>\<lparr>Obj\<rparr>
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. pcategory_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> cat_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. Hom (\<Prod>\<^sub>Ci\<in>\<^sub>\<circ>J'. \<AA> i) a b) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from prems(1) assms
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
have "J' \<subseteq>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from pcat_Hom_vifunion_in_Vset[OF this prems(2-5)]
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (cat_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. pcategory_base \<alpha> J \<AA>
[PROOF STEP]
qed (rule pcat_vsubset_index_pcategory_base[OF assms])


[STATEMENT]
lemma cf_brcomp_def':
  assumes "\<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>C\<^sub>F cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
interpret \<SS>: is_functor \<alpha> \<open>\<CC> \<times>\<^sub>C \<CC>\<close> \<CC> \<SS>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cf_brcomp_def cs_intro: cat_cs_intros
      )
[PROOF STATE]
proof (state)
this:
cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cf_blcomp_is_functor:
  assumes "\<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "cf_blcomp \<SS> : \<CC> \<times>\<^sub>C\<^sub>3 \<CC> \<times>\<^sub>C\<^sub>3 \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<SS>: is_functor \<alpha> \<open>\<CC> \<times>\<^sub>C \<CC>\<close> \<CC> \<SS>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps cf_blcomp_def' cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma only_touches_opening:
  assumes \<open>only_touches i branch xs\<close> \<open>(v, v') \<in> xs\<close> \<open>branch !. v = Some (ps, a)\<close>
  shows \<open>i = a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
only_touches i branch xs
(v, v') \<in> xs
branch !. v = Some (ps, a)

goal (1 subgoal):
 1. i = a
[PROOF STEP]
unfolding only_touches_def is_at_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>xs. \<forall>ps a. branch !. v = Some (ps, a) \<longrightarrow> i = a
(v, v') \<in> xs
branch !. v = Some (ps, a)

goal (1 subgoal):
 1. i = a
[PROOF STEP]
by auto


[STATEMENT]
lemma Pdrop_valid [simp]: "valid_path (ldropn n P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (ldropn n P)
[PROOF STEP]
using valid_path_drop
[PROOF STATE]
proof (prove)
using this:
valid_path ?P \<Longrightarrow> valid_path (ldropn ?n ?P)

goal (1 subgoal):
 1. valid_path (ldropn n P)
[PROOF STEP]
by auto


[STATEMENT]
lemma "test (do {
  tmp0 \<leftarrow> slots_document . getElementById(''test_closed_closed'');
  n \<leftarrow> createTestTree(tmp0);
  tmp1 \<leftarrow> n . ''test_closed_closed'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 \<leftarrow> n . ''c1'';
  tmp3 \<leftarrow> tmp2 . assignedSlot;
  assert_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp4 \<leftarrow> n . ''s1'';
  tmp5 \<leftarrow> tmp4 . assignedSlot;
  assert_equals(tmp5, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp6 \<leftarrow> n . ''s1'';
  tmp7 \<leftarrow> tmp6 . assignedNodes();
  tmp8 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp7, [tmp8]);
  tmp9 \<leftarrow> n . ''s2'';
  tmp10 \<leftarrow> tmp9 . assignedNodes();
  tmp11 \<leftarrow> n . ''s1'';
  assert_array_equals(tmp10, [tmp11]);
  tmp12 \<leftarrow> n . ''s1'';
  tmp13 \<leftarrow> tmp12 . assignedNodes(True);
  tmp14 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp13, [tmp14]);
  tmp15 \<leftarrow> n . ''s2'';
  tmp16 \<leftarrow> tmp15 . assignedNodes(True);
  tmp17 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp16, [tmp17])
}) slots_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind slots_document . getElementById(''test_closed_closed'') (\<lambda>tmp0. Heap_Error_Monad.bind (createTestTree tmp0) (\<lambda>n. Heap_Error_Monad.bind (n . ''test_closed_closed'') (\<lambda>tmp1. Heap_Error_Monad.bind (removeWhiteSpaceOnlyTextNodes tmp1) (\<lambda>_. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp2. Heap_Error_Monad.bind tmp2 . assignedSlot (\<lambda>tmp3. Heap_Error_Monad.bind assert_array_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'') (\<lambda>_. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp4. Heap_Error_Monad.bind tmp4 . assignedSlot (\<lambda>tmp5. Heap_Error_Monad.bind assert_array_equals(tmp5, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'') (\<lambda>_. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp6. Heap_Error_Monad.bind tmp6 . assignedNodes() (\<lambda>tmp7. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp8. Heap_Error_Monad.bind assert_array_equals(tmp7, [tmp8]) (\<lambda>_. Heap_Error_Monad.bind (n . ''s2'') (\<lambda>tmp9. Heap_Error_Monad.bind tmp9 . assignedNodes() (\<lambda>tmp10. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp11. Heap_Error_Monad.bind assert_array_equals(tmp10, [tmp11]) (\<lambda>_. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp12. Heap_Error_Monad.bind tmp12 . assignedNodes(True) (\<lambda>tmp13. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp14. Heap_Error_Monad.bind assert_array_equals(tmp13, [tmp14]) (\<lambda>_. Heap_Error_Monad.bind (n . ''s2'') (\<lambda>tmp15. Heap_Error_Monad.bind tmp15 . assignedNodes(True) (\<lambda>tmp16. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp17. assert_array_equals(tmp16, [tmp17]))))))))))))))))))))))))))) slots_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma eme1p:
  "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (1 + n) mod d = 1 + n mod d" for n d :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (1 + n) mod d = 1 + n mod d
[PROOF STEP]
using emep1 [of n d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (n + 1) mod d = n mod d + 1

goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (1 + n) mod d = 1 + n mod d
[PROOF STEP]
by (simp add: ac_simps)


[STATEMENT]
lemma vec_comp_allE:
  "vec_comp_all r v w \<Longrightarrow> i < dim_vec v \<Longrightarrow> r (v $ i) (w $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vec_comp_all r v w; i < dim_vec v\<rbrakk> \<Longrightarrow> r (v $ i) (w $ i)
[PROOF STEP]
unfolding vec_comp_all_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<dim_vec v. r (v $ i) (w $ i); i < dim_vec v\<rbrakk> \<Longrightarrow> r (v $ i) (w $ i)
[PROOF STEP]
by auto


[STATEMENT]
lemma equiv_cp_cong[simp]: "Q \<triangleq> Q' \<Longrightarrow> cp Q \<triangleq> cp Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<triangleq> Q' \<Longrightarrow> cp Q \<triangleq> cp Q'
[PROOF STEP]
by (auto simp: equiv_def)


[STATEMENT]
lemma gen'_cp_intros:
  "gen' y Q G \<Longrightarrow> gen' x (Conj Q (x \<approx> y)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G)"
  "gen' y Q G \<Longrightarrow> gen' x (Conj Q (y \<approx> x)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gen' y Q G \<Longrightarrow> gen' x (Conj Q (x \<approx> y)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G)) &&& (gen' y Q G \<Longrightarrow> gen' x (Conj Q (y \<approx> x)) ((\<lambda>Q. cp (Q[y \<^bold>\<rightarrow> x])) ` G))
[PROOF STEP]
by (metis (no_types, lifting) gen'.intros(8) gen'_qp image_cong qp_cp_subst_triv,
      metis (no_types, lifting) gen'.intros(9) gen'_qp image_cong qp_cp_subst_triv)


[STATEMENT]
lemma seqI [simp]:
    assumes "arr f" and "arr g" and "dom g = cod f"
    shows "seq g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq g f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. seq g f
[PROOF STEP]
have "ide (cod f) \<and> seq (cod f) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (cod f) \<and> seq (cod f) f
[PROOF STEP]
using assms(1) has_codomain_iff_arr codomains_def cod_in_codomains ext
[PROOF STATE]
proof (prove)
using this:
arr f
(codomains ?f \<noteq> {}) = arr ?f
codomains ?f \<equiv> {b. ide b \<and> b \<cdot> ?f \<noteq> null}
codomains ?f \<noteq> {} \<Longrightarrow> cod ?f \<in> codomains ?f
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. ide (cod f) \<and> seq (cod f) f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ide (cod f) \<and> seq (cod f) f

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (cod f) \<and> seq (cod f) f

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
have "ide (cod f) \<and> seq g (cod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (cod f) \<and> seq g (cod f)
[PROOF STEP]
using assms(2-3) domains_def domains_simp ext
[PROOF STATE]
proof (prove)
using this:
arr g
local.dom g = cod f
domains ?f \<equiv> {a. ide a \<and> ?f \<cdot> a \<noteq> null}
arr ?f \<Longrightarrow> domains ?f = {local.dom ?f}
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. ide (cod f) \<and> seq g (cod f)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ide (cod f) \<and> seq g (cod f)

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (cod f) \<and> seq (cod f) f
ide (cod f) \<and> seq g (cod f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (cod f) \<and> seq (cod f) f
ide (cod f) \<and> seq g (cod f)

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
using match_4 ide_def ext
[PROOF STATE]
proof (prove)
using this:
ide (cod f) \<and> seq (cod f) f
ide (cod f) \<and> seq g (cod f)
\<lbrakk>seq ?g ?f; seq ?h ?g\<rbrakk> \<Longrightarrow> seq ?h (?g \<cdot> ?f)
ide ?a \<equiv> ?a \<cdot> ?a \<noteq> null \<and> (\<forall>f. (f \<cdot> ?a \<noteq> null \<longrightarrow> f \<cdot> ?a = f) \<and> (?a \<cdot> f \<noteq> null \<longrightarrow> ?a \<cdot> f = f))
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
seq g f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma analz_Un_implSecureSet_aux_3:
  "Enc_keys_clean (G \<union> H) \<Longrightarrow>
  analz (implSecureSet_aux Ag G \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> -payload"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz (implSecureSet_aux Ag G \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> - payload
[PROOF STEP]
by (rule subset_trans [OF analz_Un_implSecureSet_aux_2], auto)


[STATEMENT]
lemma [code]:
    "not_disjoint_intervals A B =
      (case A of (s,e) \<Rightarrow> case B of (s',e') \<Rightarrow> s \<le> e' \<and> s' \<le> e \<and> s \<le> e \<and> s' \<le> e')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_disjoint_intervals A B = (case A of (s, e) \<Rightarrow> case B of (s', e') \<Rightarrow> s \<le> e' \<and> s' \<le> e \<and> s \<le> e \<and> s' \<le> e')
[PROOF STEP]
apply(cases A, cases B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>A = (a, b); B = (aa, ba)\<rbrakk> \<Longrightarrow> not_disjoint_intervals A B = (case A of (s, e) \<Rightarrow> case B of (s', e') \<Rightarrow> s \<le> e' \<and> s' \<le> e \<and> s \<le> e \<and> s' \<le> e')
[PROOF STEP]
apply(simp add: not_disjoint_intervals_def interval_of.simps disjoint_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done