[STATEMENT]
lemma ABinds_lookup_fresh:
  "atom v \<sharp> \<Gamma> \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae) v = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom v \<sharp> \<Gamma> \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae) v = \<bottom>
[PROOF STEP]
by (induct \<Gamma> rule: ABinds.induct) (auto simp add: fresh_Cons fresh_Pair fup_Aexp_lookup_fresh fresh_delete)


[STATEMENT]
lemma Afix_lookup_fresh:
  assumes "atom v \<sharp> \<Gamma>"
  shows "(Afix \<Gamma>\<cdot>ae) v = ae v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Afix \<Gamma>\<cdot>ae) v = ae v
[PROOF STEP]
apply (rule below_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Afix \<Gamma>\<cdot>ae) v \<sqsubseteq> ae v
 2. ae v \<sqsubseteq> (Afix \<Gamma>\<cdot>ae) v
[PROOF STEP]
apply (subst Afix_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) v \<sqsubseteq> ae v
 2. ae v \<sqsubseteq> (Afix \<Gamma>\<cdot>ae) v
[PROOF STEP]
apply (rule fix_ind[where  P = "\<lambda> ae'. ae' v \<sqsubseteq> ae v"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. adm (\<lambda>ae'. ae' v \<sqsubseteq> ae v)
 2. \<bottom> v \<sqsubseteq> ae v
 3. \<And>x. x v \<sqsubseteq> ae v \<Longrightarrow> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x) v \<sqsubseteq> ae v
 4. ae v \<sqsubseteq> (Afix \<Gamma>\<cdot>ae) v
[PROOF STEP]
apply (auto simp add: ABinds_lookup_fresh[OF assms] fun_belowD[OF Afix_above_arg])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_comp2join_fresh:
  "atom ` (domA \<Delta>) \<sharp>* \<Gamma> \<Longrightarrow> ABinds \<Delta>\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds \<Delta>\<cdot>ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> ABinds \<Delta>\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds \<Delta>\<cdot>ae
[PROOF STEP]
proof (induct \<Delta> rule: ABinds.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. atom ` domA [] \<sharp>* \<Gamma> \<Longrightarrow> ABinds []\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds []\<cdot>ae
 2. \<And>v e binds. \<lbrakk>atom ` domA (delete v binds) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v binds)\<cdot>ae; atom ` domA ((v, e) # binds) \<sharp>* \<Gamma>\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # binds)\<cdot>ae
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
atom ` domA [] \<sharp>* \<Gamma>

goal (2 subgoals):
 1. atom ` domA [] \<sharp>* \<Gamma> \<Longrightarrow> ABinds []\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds []\<cdot>ae
 2. \<And>v e binds. \<lbrakk>atom ` domA (delete v binds) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v binds)\<cdot>ae; atom ` domA ((v, e) # binds) \<sharp>* \<Gamma>\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # binds)\<cdot>ae
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds []\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds []\<cdot>ae
[PROOF STEP]
by (simp add: Afix_above_arg del: fun_meet_simp)
[PROOF STATE]
proof (state)
this:
ABinds []\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds []\<cdot>ae

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>atom ` domA (delete v binds) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v binds)\<cdot>ae; atom ` domA ((v, e) # binds) \<sharp>* \<Gamma>\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # binds)\<cdot>ae
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>atom ` domA (delete v binds) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v binds)\<cdot>ae; atom ` domA ((v, e) # binds) \<sharp>* \<Gamma>\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # binds)\<cdot>ae
[PROOF STEP]
case (2 v e \<Delta>)
[PROOF STATE]
proof (state)
this:
atom ` domA (delete v \<Delta>) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v \<Delta>)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v \<Delta>)\<cdot>ae
atom ` domA ((v, e) # \<Delta>) \<sharp>* \<Gamma>

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>atom ` domA (delete v binds) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v binds)\<cdot>ae; atom ` domA ((v, e) # binds) \<sharp>* \<Gamma>\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # binds)\<cdot>ae
[PROOF STEP]
from 2(2)
[PROOF STATE]
proof (chain)
picking this:
atom ` domA ((v, e) # \<Delta>) \<sharp>* \<Gamma>
[PROOF STEP]
have "atom v \<sharp> \<Gamma>" and  "atom ` domA (delete v \<Delta>) \<sharp>* \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
atom ` domA ((v, e) # \<Delta>) \<sharp>* \<Gamma>

goal (1 subgoal):
 1. atom v \<sharp> \<Gamma> &&& atom ` domA (delete v \<Delta>) \<sharp>* \<Gamma>
[PROOF STEP]
by (auto simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
atom v \<sharp> \<Gamma>
atom ` domA (delete v \<Delta>) \<sharp>* \<Gamma>

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>atom ` domA (delete v binds) \<sharp>* \<Gamma> \<Longrightarrow> ABinds (delete v binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v binds)\<cdot>ae; atom ` domA ((v, e) # binds) \<sharp>* \<Gamma>\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # binds)\<cdot>ae
[PROOF STEP]
from 2(1)[OF this(2)]
[PROOF STATE]
proof (chain)
picking this:
ABinds (delete v \<Delta>)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v \<Delta>)\<cdot>ae
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ABinds (delete v \<Delta>)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds (delete v \<Delta>)\<cdot>ae

goal (1 subgoal):
 1. ABinds ((v, e) # \<Delta>)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # \<Delta>)\<cdot>ae
[PROOF STEP]
by (simp del: fun_meet_simp add: Afix_lookup_fresh[OF \<open>atom v \<sharp> \<Gamma>\<close>])
[PROOF STATE]
proof (state)
this:
ABinds ((v, e) # \<Delta>)\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds ((v, e) # \<Delta>)\<cdot>ae

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Afix_append_fresh:
  assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>"
  shows "Afix (\<Delta> @ \<Gamma>)\<cdot>ae = Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix (\<Delta> @ \<Gamma>)\<cdot>ae = Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
[PROOF STEP]
proof (rule below_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Afix (\<Delta> @ \<Gamma>)\<cdot>ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
 2. Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
show *: "Afix (\<Delta> @ \<Gamma>)\<cdot>ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix (\<Delta> @ \<Gamma>)\<cdot>ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
[PROOF STEP]
apply (rule Afix_least_below)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ABinds (\<Delta> @ \<Gamma>)\<cdot>(Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)) \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
 2. ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
[PROOF STEP]
apply (simp add: Abinds_append_disjoint[OF fresh_distinct[OF assms]] Afix_comp2join_fresh[OF assms])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ABinds \<Delta>\<cdot>(Afix \<Delta>\<cdot>ae) \<squnion> ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)) \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
 2. ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
[PROOF STEP]
apply (rule below_trans[OF join_mono[OF Abinds_Afix_below Abinds_Afix_below]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Afix \<Delta>\<cdot>ae \<squnion> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
 2. ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)
[PROOF STEP]
apply (simp_all add: Afix_above_arg  below_trans[OF Afix_above_arg Afix_above_arg])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Afix (\<Delta> @ \<Gamma>)\<cdot>ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)

goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
show "Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
proof (rule Afix_least_below)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
 2. Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
show "ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
apply (rule below_trans[OF _ Abinds_Afix_below])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> ABinds (\<Delta> @ \<Gamma>)\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae)
[PROOF STEP]
apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<squnion> ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae

goal (1 subgoal):
 1. Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
have "ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
apply (rule below_trans[OF _ Abinds_Afix_below])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> ABinds (\<Delta> @ \<Gamma>)\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae)
[PROOF STEP]
apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<squnion> ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae

goal (1 subgoal):
 1. Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
thus "Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
[PROOF STATE]
proof (prove)
using this:
ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae

goal (1 subgoal):
 1. Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
apply (rule Afix_least_below)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae
[PROOF STEP]
apply (rule Afix_above_arg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Afix_e_to_heap:
   "Afix (delete x \<Gamma>)\<cdot>(fup\<cdot>(Aexp e)\<cdot>n \<squnion> ae) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>n \<squnion> ae)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix (delete x \<Gamma>)\<cdot>(\<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<squnion> ae) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>n \<squnion> ae)
[PROOF STEP]
apply (simp add: Afix_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> xa. ae \<squnion> (\<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<squnion> ABinds (delete x \<Gamma>)\<cdot>xa)) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (rule fix_least_below, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae \<squnion> (\<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<squnion> ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (intro join_below)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ae \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
 2. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
 3. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
 2. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<sqsubseteq> ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<squnion> \<A>\<^sup>\<bottom>\<^bsub>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x\<^esub> e))
 2. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (rule below_trans[OF _ join_above2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<sqsubseteq> esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<squnion> \<A>\<^sup>\<bottom>\<^bsub>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x\<^esub> e)
 2. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (rule below_trans[OF _ join_above2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<sqsubseteq> ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<squnion> \<A>\<^sup>\<bottom>\<^bsub>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x\<^esub> e
 2. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (rule below_trans[OF _ join_above2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e \<sqsubseteq> \<A>\<^sup>\<bottom>\<^bsub>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x\<^esub> e
 2. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (rule monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x
 2. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds (delete x \<Gamma>)\<cdot>(ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<squnion> \<A>\<^sup>\<bottom>\<^bsub>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x\<^esub> e))) \<sqsubseteq> (\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e)))
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<sqsubseteq> ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) \<squnion> \<A>\<^sup>\<bottom>\<^bsub>(\<mu> xa. ae \<squnion> (esing x\<cdot>n \<squnion> (ABinds (delete x \<Gamma>)\<cdot>xa \<squnion> \<A>\<^sup>\<bottom>\<^bsub>xa x\<^esub> e))) x\<^esub> e))
[PROOF STEP]
apply (simp add: below_trans[OF _ join_above2])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_e_to_heap':
   "Afix (delete x \<Gamma>)\<cdot>(Aexp e\<cdot>n) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>(up\<cdot>n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix (delete x \<Gamma>)\<cdot>(\<A>\<^bsub>n\<^esub> e) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>(up\<cdot>n))
[PROOF STEP]
using Afix_e_to_heap[where ae = \<bottom> and n = "up\<cdot>n"]
[PROOF STATE]
proof (prove)
using this:
Afix (delete ?x ?\<Gamma>)\<cdot>(\<A>\<^sup>\<bottom>\<^bsub>up\<cdot>n\<^esub> ?e \<squnion> \<bottom>) \<sqsubseteq> Afix ((?x, ?e) # delete ?x ?\<Gamma>)\<cdot>(esing ?x\<cdot>(up\<cdot>n) \<squnion> \<bottom>)

goal (1 subgoal):
 1. Afix (delete x \<Gamma>)\<cdot>(\<A>\<^bsub>n\<^esub> e) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>(up\<cdot>n))
[PROOF STEP]
by simp


[STATEMENT]
lemma dims_unit_vec: "dims (unit_vec n i) = [n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims (unit_vec n i) = [n]
[PROOF STEP]
unfolding unit_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1::'a else (0::'a))) = [n]
[PROOF STEP]
by (simp add: tensor_from_lookup_def)


[STATEMENT]
lemma lookup_unit_vec:
assumes "j<n"
shows "lookup (unit_vec n i) [j] = (if i=j then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if i = j then 1::'a else (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if i = j then 1::'a else (0::'a))
[PROOF STEP]
have "[j] \<lhd> [n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [j] \<lhd> [n]
[PROOF STEP]
by (simp add: assms valid_index.Cons valid_index.Nil)
[PROOF STATE]
proof (state)
this:
[j] \<lhd> [n]

goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if i = j then 1::'a else (0::'a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[j] \<lhd> [n]
[PROOF STEP]
have "lookup (unit_vec n i) [j] = (\<lambda>x. if x=[i] then 1 else 0) [j]"
[PROOF STATE]
proof (prove)
using this:
[j] \<lhd> [n]

goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if [j] = [i] then 1::'b else (0::'b))
[PROOF STEP]
by (simp add: lookup_tensor_from_lookup unit_vec_def)
[PROOF STATE]
proof (state)
this:
lookup (unit_vec n i) [j] = (if [j] = [i] then 1::?'b1 else (0::?'b1))

goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if i = j then 1::'a else (0::'a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lookup (unit_vec n i) [j] = (if [j] = [i] then 1::?'b1 else (0::?'b1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (unit_vec n i) [j] = (if [j] = [i] then 1::?'b1 else (0::?'b1))

goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if i = j then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lookup (unit_vec n i) [j] = (if i = j then 1::'a else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subtensor_prod_with_unit_vec:
fixes A::"'a::ring_1 tensor"
assumes "j<n"
shows "subtensor (unit_vec n i \<otimes> A) j = (if i=j then A else (tensor0 (dims A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
have 0:"lookup (unit_vec n i) [j] = (if i=j then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (unit_vec n i) [j] = (if i = j then 1::'b else (0::'b))
[PROOF STEP]
unfolding unit_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1::'b else (0::'b))) [j] = (if i = j then 1::'b else (0::'b))
[PROOF STEP]
by (simp add: assms lookup_tensor_from_lookup valid_index.Cons valid_index.Nil)
[PROOF STATE]
proof (state)
this:
lookup (unit_vec n i) [j] = (if i = j then 1::?'b1 else (0::?'b1))

goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
have 1:"order (unit_vec n i) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (unit_vec n i) = 1
[PROOF STEP]
unfolding unit_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1::'b else (0::'b))) = 1
[PROOF STEP]
by (simp add: tensor_from_lookup_def)
[PROOF STATE]
proof (state)
this:
order (unit_vec n i) = 1

goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
j < n
[PROOF STEP]
have 2:"j < hd (dims (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1 else 0)))"
[PROOF STATE]
proof (prove)
using this:
j < n

goal (1 subgoal):
 1. j < hd (dims (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1::'b else (0::'b))))
[PROOF STEP]
by (simp add: dims_tensor_from_lookup)
[PROOF STATE]
proof (state)
this:
j < hd (dims (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1::?'b3 else (0::?'b3))))

goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
using unit_vec_def subtensor_prod_with_vec 1 2 0 smult_1 tensor_smult0
[PROOF STATE]
proof (prove)
using this:
unit_vec ?n ?i = tensor_from_lookup [?n] (\<lambda>x. if x = [?i] then 1::?'a else (0::?'a))
\<lbrakk>order ?A = 1; ?i < hd (dims ?A)\<rbrakk> \<Longrightarrow> subtensor (?A \<otimes> ?B) ?i = lookup ?A [?i] \<cdot> ?B
order (unit_vec n i) = 1
j < hd (dims (tensor_from_lookup [n] (\<lambda>x. if x = [i] then 1::?'b3 else (0::?'b3))))
lookup (unit_vec n i) [j] = (if i = j then 1::?'b1 else (0::?'b1))
?A = (1::?'a) \<cdot> ?A
(0::?'a) \<cdot> ?A = tensor0 (dims ?A)

goal (1 subgoal):
 1. subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))
[PROOF STEP]
by (metis (no_types, lifting) tensor_from_lookup_eqI)
[PROOF STATE]
proof (state)
this:
subtensor (unit_vec n i \<otimes> A) j = (if i = j then A else tensor0 (dims A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subtensor_decomposition:
assumes "dims A \<noteq> []"
shows "listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A" (is "?LS = A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
let ?f = "\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
have correct_dims:"\<And>B. B \<in> set (map ?f [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B. B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B. B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B. B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A
[PROOF STEP]
assume "B \<in> set (map ?f [0..<hd (dims A)])"
[PROOF STATE]
proof (state)
this:
B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])

goal (1 subgoal):
 1. \<And>B. B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])
[PROOF STEP]
obtain i where B:"B = ?f i" and "i<hd (dims A)"
[PROOF STATE]
proof (prove)
using this:
B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>B = unit_vec (hd (dims A)) i \<otimes> subtensor A i; i < hd (dims A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = unit_vec (hd (dims A)) i \<otimes> subtensor A i
i < hd (dims A)

goal (1 subgoal):
 1. \<And>B. B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B = unit_vec (hd (dims A)) i \<otimes> subtensor A i
i < hd (dims A)
[PROOF STEP]
have "dims (subtensor A i) = tl (dims A)"
[PROOF STATE]
proof (prove)
using this:
B = unit_vec (hd (dims A)) i \<otimes> subtensor A i
i < hd (dims A)

goal (1 subgoal):
 1. dims (subtensor A i) = tl (dims A)
[PROOF STEP]
using dims_subtensor
[PROOF STATE]
proof (prove)
using this:
B = unit_vec (hd (dims A)) i \<otimes> subtensor A i
i < hd (dims A)
\<lbrakk>dims ?A \<noteq> []; ?i < hd (dims ?A)\<rbrakk> \<Longrightarrow> dims (subtensor ?A ?i) = tl (dims ?A)

goal (1 subgoal):
 1. dims (subtensor A i) = tl (dims A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B = unit_vec (hd (dims A)) i \<otimes> subtensor A i
i < hd (dims A)
\<lbrakk>dims ?A \<noteq> []; ?i < hd (dims ?A)\<rbrakk> \<Longrightarrow> dims (subtensor ?A ?i) = tl (dims ?A)
dims A \<noteq> []

goal (1 subgoal):
 1. dims (subtensor A i) = tl (dims A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dims (subtensor A i) = tl (dims A)

goal (1 subgoal):
 1. \<And>B. B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims B = dims A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dims (subtensor A i) = tl (dims A)
[PROOF STEP]
show "dims B = dims A"
[PROOF STATE]
proof (prove)
using this:
dims (subtensor A i) = tl (dims A)

goal (1 subgoal):
 1. dims B = dims A
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
dims (subtensor A i) = tl (dims A)

goal (1 subgoal):
 1. dims (unit_vec (hd (dims A)) i \<otimes> subtensor A i) = dims A
[PROOF STEP]
by (metis append_Cons assms dims_tensor_prod dims_unit_vec list.exhaust_sel self_append_conv2)
[PROOF STATE]
proof (state)
this:
dims B = dims A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims ?B = dims A

goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
have "\<And>j. j < hd (dims A) \<Longrightarrow> subtensor ?LS j = subtensor A j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
assume "j < hd (dims A)"
[PROOF STATE]
proof (state)
this:
j < hd (dims A)

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
have 1:"subtensor ?LS j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map ?f [0..<hd (dims A)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))
[PROOF STEP]
using subtensor_listsum[of "(map (\<lambda>i. ?f i) [0..<hd (dims A)])" "dims A" j, OF correct_dims assms \<open>j < hd (dims A)\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>Aa. Aa \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> Aa \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))

goal (1 subgoal):
 1. subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
have "... = listsum (tl (dims A)) (map (\<lambda>i. subtensor (?f i) j) [0..<hd (dims A)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])
[PROOF STEP]
have "map (\<lambda>A. subtensor A j) (map ?f [0..<hd (dims A)]) = map (\<lambda>i. subtensor (?f i) j) [0..<hd (dims A)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]
[PROOF STEP]
unfolding map_map[of "(\<lambda>A. subtensor A j)" "?f" "[0..<hd (dims A)]"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((\<lambda>A. subtensor A j) \<circ> (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i)) [0..<hd (dims A)] = map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]

goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))
map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]))
map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]

goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
listsum (tl (dims A)) (map (\<lambda>A. subtensor A j) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)])

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
have "... =  map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]) = map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j
[PROOF STEP]
unfolding subtensor_prod_with_unit_vec[OF \<open>j < hd (dims A)\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)]) = map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j
[PROOF STEP]
using listsum_all_0_but_one[of j "(map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)])" "tl (dims A)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. \<lbrakk>i \<noteq> j; i < length (map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)])\<rbrakk> \<Longrightarrow> map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! i = tensor0 (tl (dims A)); dims (map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j) = tl (dims A); j < length (map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)])\<rbrakk> \<Longrightarrow> listsum (tl (dims A)) (map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)]) = map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j

goal (1 subgoal):
 1. listsum (tl (dims A)) (map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)]) = map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j
[PROOF STEP]
by (simp add: \<open>j < hd (dims A)\<close> assms)
[PROOF STATE]
proof (state)
this:
listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]) = map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
listsum (tl (dims A)) (map (\<lambda>i. subtensor (unit_vec (hd (dims A)) i \<otimes> subtensor A i) j) [0..<hd (dims A)]) = map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
have "... = subtensor A j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j = subtensor A j
[PROOF STEP]
by (simp add: \<open>j < hd (dims A)\<close>)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. if i = j then subtensor A i else tensor0 (dims (subtensor A i))) [0..<hd (dims A)] ! j = subtensor A j

goal (1 subgoal):
 1. \<And>j. j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
show "subtensor ?LS j = subtensor A j"
[PROOF STATE]
proof (prove)
using this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j

goal (1 subgoal):
 1. subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) j = subtensor A j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) ?j = subtensor A ?j

goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) ?j = subtensor A ?j

goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
have "dims ?LS = dims A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = dims A
[PROOF STEP]
using correct_dims listsum_dims
[PROOF STATE]
proof (prove)
using this:
?B \<in> set (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) \<Longrightarrow> dims ?B = dims A
(\<And>A. A \<in> set ?As \<Longrightarrow> dims A = ?ds) \<Longrightarrow> dims (listsum ?ds ?As) = ?ds

goal (1 subgoal):
 1. dims (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = dims A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dims (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = dims A

goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) ?j = subtensor A ?j
dims (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = dims A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) ?j = subtensor A ?j
dims (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = dims A

goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
using subtensor_eqI
[PROOF STATE]
proof (prove)
using this:
?j < hd (dims A) \<Longrightarrow> subtensor (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) ?j = subtensor A ?j
dims (listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)])) = dims A
\<lbrakk>dims ?A \<noteq> []; dims ?A = dims ?B; \<And>i. i < hd (dims ?A) \<Longrightarrow> subtensor ?A i = subtensor ?B i\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A
[PROOF STEP]
by (metis (no_types, lifting) assms)
[PROOF STATE]
proof (state)
this:
listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<pi>_no_tokens: "\<pi> k {} I =  limit (\<lambda> I. Complete k (Predict k I)) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k {} I = limit (\<lambda>I. Complete k (Predict k I)) I
[PROOF STEP]
by (simp add: \<pi>_def Scan_empty)


[STATEMENT]
lemma bin_elem: "x \<in> bin I k \<Longrightarrow> x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> bin I k \<Longrightarrow> x \<in> I
[PROOF STEP]
by (auto simp add: bin_def)


[STATEMENT]
lemma Gen_implies_pvalid: "x \<in> Gen P \<Longrightarrow> \<exists> p \<in> P. pvalid p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Gen P \<Longrightarrow> \<exists>p\<in>P. pvalid p x
[PROOF STEP]
by (auto simp add: Gen_def)


[STATEMENT]
lemma wellformed_init_item[simp]: "r \<in> \<RR> \<Longrightarrow> k \<le> length Doc \<Longrightarrow> wellformed_item (init_item r k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> \<RR>; k \<le> length Doc\<rbrakk> \<Longrightarrow> wellformed_item (init_item r k)
[PROOF STEP]
by (simp add: init_item_def wellformed_item_def)


[STATEMENT]
lemma init_item_origin[simp]: "item_origin (init_item r k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_origin (init_item r k) = k
[PROOF STEP]
by (auto simp add: item_origin_def init_item_def)


[STATEMENT]
lemma init_item_end[simp]: "item_end (init_item r k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end (init_item r k) = k
[PROOF STEP]
by (auto simp add: item_end_def init_item_def)


[STATEMENT]
lemma init_item_nonterminal[simp]: "item_nonterminal (init_item r k) = fst r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_nonterminal (init_item r k) = fst r
[PROOF STEP]
by (auto simp add: init_item_def item_nonterminal_def)


[STATEMENT]
lemma init_item_\<alpha>[simp]: "item_\<alpha> (init_item r k) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_\<alpha> (init_item r k) = []
[PROOF STEP]
by (auto simp add: init_item_def item_\<alpha>_def)


[STATEMENT]
lemma Predict_elem_in_Gen:
  assumes I_in_Gen_P: "I \<subseteq> Gen P"
  assumes k: "k \<le> length Doc"
  assumes x_in_Predict: "x \<in> Predict k I"
  shows "x \<in> Gen P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Gen P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Gen P
[PROOF STEP]
have "x \<in> I \<or> (\<exists> r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some(fst r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> I \<or> (\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r))
[PROOF STEP]
using x_in_Predict
[PROOF STATE]
proof (prove)
using this:
x \<in> Predict k I

goal (1 subgoal):
 1. x \<in> I \<or> (\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r))
[PROOF STEP]
by (auto simp add: Predict_def)
[PROOF STATE]
proof (state)
this:
x \<in> I \<or> (\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r))

goal (1 subgoal):
 1. x \<in> Gen P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> I \<or> (\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> I \<or> (\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r))

goal (1 subgoal):
 1. x \<in> Gen P
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> I \<Longrightarrow> x \<in> Gen P
 2. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (2 subgoals):
 1. x \<in> I \<Longrightarrow> x \<in> Gen P
 2. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. x \<in> Gen P
[PROOF STEP]
using I_in_Gen_P
[PROOF STATE]
proof (prove)
using this:
x \<in> I
I \<subseteq> Gen P

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

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)
[PROOF STEP]
obtain r y where ry: "r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and>
      next_symbol y = Some (fst r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)

goal (1 subgoal):
 1. (\<And>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)
[PROOF STEP]
have "\<exists> p \<in> P. pvalid p y"
[PROOF STATE]
proof (prove)
using this:
r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)

goal (1 subgoal):
 1. \<exists>p\<in>P. pvalid p y
[PROOF STEP]
using Gen_implies_pvalid I_in_Gen_P bin_elem subsetCE
[PROOF STATE]
proof (prove)
using this:
r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)
?x \<in> Gen ?P \<Longrightarrow> \<exists>p\<in>?P. pvalid p ?x
I \<subseteq> Gen P
?x \<in> bin ?I ?k \<Longrightarrow> ?x \<in> ?I
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>P. pvalid p y
[PROOF STEP]
obtain p where p: "p \<in> P \<and> pvalid p y"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>P. pvalid p y

goal (1 subgoal):
 1. (\<And>p. p \<in> P \<and> pvalid p y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> P \<and> pvalid p y

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
have wellformed_p: "wellformed_tokens p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_tokens p
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p \<in> P \<and> pvalid p y

goal (1 subgoal):
 1. wellformed_tokens p
[PROOF STEP]
by (auto simp add: pvalid_def)
[PROOF STATE]
proof (state)
this:
wellformed_tokens p

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
have wellformed_x: "wellformed_item x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item x
[PROOF STEP]
by (simp add: ry k)
[PROOF STATE]
proof (state)
this:
wellformed_item x

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
from ry
[PROOF STATE]
proof (chain)
picking this:
r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)
[PROOF STEP]
have "item_end y = k"
[PROOF STATE]
proof (prove)
using this:
r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r)

goal (1 subgoal):
 1. item_end y = k
[PROOF STEP]
by (auto simp add: bin_def)
[PROOF STATE]
proof (state)
this:
item_end y = k

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p \<in> P \<and> pvalid p y
item_end y = k
[PROOF STEP]
have charslength_p[simplified]: "charslength p = k"
[PROOF STATE]
proof (prove)
using this:
p \<in> P \<and> pvalid p y
item_end y = k

goal (1 subgoal):
 1. charslength p = k
[PROOF STEP]
by (auto simp add: pvalid_def)
[PROOF STATE]
proof (state)
this:
length (chars p) = k

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
have item_end_x: "item_end x = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end x = k
[PROOF STEP]
by (simp add: ry)
[PROOF STATE]
proof (state)
this:
item_end x = k

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
have pvalid_x: "pvalid p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pvalid p x
[PROOF STEP]
apply (auto simp add: pvalid_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wellformed_tokens p
 2. wellformed_item x
 3. \<exists>u\<le>length p. length (chars p) = item_end x \<and> length (chars (take u p)) = item_origin x \<and> (\<exists>\<gamma>. is_derivation (take u (terminals p) @ item_nonterminal x # \<gamma>)) \<and> derives (item_\<alpha> x) (drop u (terminals p))
[PROOF STEP]
apply (simp add: wellformed_p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wellformed_item x
 2. \<exists>u\<le>length p. length (chars p) = item_end x \<and> length (chars (take u p)) = item_origin x \<and> (\<exists>\<gamma>. is_derivation (take u (terminals p) @ item_nonterminal x # \<gamma>)) \<and> derives (item_\<alpha> x) (drop u (terminals p))
[PROOF STEP]
apply (simp add: wellformed_x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u\<le>length p. length (chars p) = item_end x \<and> length (chars (take u p)) = item_origin x \<and> (\<exists>\<gamma>. is_derivation (take u (terminals p) @ item_nonterminal x # \<gamma>)) \<and> derives (item_\<alpha> x) (drop u (terminals p))
[PROOF STEP]
apply (rule_tac x="length p" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p \<le> length p \<and> length (chars p) = item_end x \<and> length (chars (take (length p) p)) = item_origin x \<and> (\<exists>\<gamma>. is_derivation (take (length p) (terminals p) @ item_nonterminal x # \<gamma>)) \<and> derives (item_\<alpha> x) (drop (length p) (terminals p))
[PROOF STEP]
apply (auto simp add: charslength_p ry)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<gamma>. is_derivation (terminals p @ fst r # \<gamma>)
[PROOF STEP]
by (metis append_Cons next_symbol_starts_item_\<beta> p pvalid_def
        pvalid_is_derivation_terminals_item_\<beta> ry)
[PROOF STATE]
proof (state)
this:
pvalid p x

goal (1 subgoal):
 1. \<exists>r y. r \<in> \<RR> \<and> x = init_item r k \<and> y \<in> bin I k \<and> next_symbol y = Some (fst r) \<Longrightarrow> x \<in> Gen P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pvalid p x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pvalid p x

goal (1 subgoal):
 1. x \<in> Gen P
[PROOF STEP]
using Gen_def mem_Collect_eq p
[PROOF STATE]
proof (prove)
using this:
pvalid p x
Gen ?P = {uu_. \<exists>x p. uu_ = x \<and> p \<in> ?P \<and> pvalid p x}
(?a \<in> Collect ?P) = ?P ?a
p \<in> P \<and> pvalid p y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> Gen P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Predict_subset_Gen:
  assumes "I \<subseteq> Gen P"
  assumes "k \<le> length Doc"
  shows "Predict k I \<subseteq> Gen P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Predict k I \<subseteq> Gen P
[PROOF STEP]
using Predict_elem_in_Gen assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?I \<subseteq> Gen ?P; ?k \<le> length Doc; ?x \<in> Predict ?k ?I\<rbrakk> \<Longrightarrow> ?x \<in> Gen ?P
I \<subseteq> Gen P
k \<le> length Doc

goal (1 subgoal):
 1. Predict k I \<subseteq> Gen P
[PROOF STEP]
by blast


[STATEMENT]
lemma nth_superfluous_append[simp]: "i < length a \<Longrightarrow> (a@b)!i = a!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length a \<Longrightarrow> (a @ b) ! i = a ! i
[PROOF STEP]
by (simp add: nth_append)


[STATEMENT]
lemma tokens_nth_in_\<Z>:
  "p \<in> \<PP> \<Longrightarrow> \<forall> i. i < length p \<longrightarrow> (\<exists> u. p ! i \<in> \<Z> (charslength (take i p)) u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<PP> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
proof (induct rule: \<PP>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>i<length []. \<exists>u. [] ! i \<in> \<Z> (charslength (take i [])) u
 2. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
case Base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<forall>i<length []. \<exists>u. [] ! i \<in> \<Z> (charslength (take i [])) u
 2. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length []. \<exists>u. [] ! i \<in> \<Z> (charslength (take i [])) u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length []. \<exists>u. [] ! i \<in> \<Z> (charslength (take i [])) u

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
case (Induct p k u)
[PROOF STATE]
proof (state)
this:
?q \<in> \<P> k u \<Longrightarrow> \<forall>i<length ?q. \<exists>u. ?q ! i \<in> \<Z> (charslength (take i ?q)) u
p \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?q \<in> \<P> k u \<Longrightarrow> \<forall>i<length ?q. \<exists>u. ?q ! i \<in> \<Z> (charslength (take i ?q)) u
p \<in> \<P> k (Suc u)
[PROOF STEP]
have "p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)"
[PROOF STATE]
proof (prove)
using this:
?q \<in> \<P> k u \<Longrightarrow> \<forall>i<length ?q. \<exists>u. ?q ! i \<in> \<Z> (charslength (take i ?q)) u
p \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)

goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
proof (induct rule: limit_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> \<P> k u \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
 2. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> Append (\<Z> k (Suc u)) k Y\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
case (Init p)
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u

goal (2 subgoals):
 1. \<And>p. p \<in> \<P> k u \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
 2. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> Append (\<Z> k (Suc u)) k Y\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u

goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
using Induct
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
?q \<in> \<P> k u \<Longrightarrow> \<forall>i<length ?q. \<exists>u. ?q ! i \<in> \<Z> (charslength (take i ?q)) u
pa__ \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> Append (\<Z> k (Suc u)) k Y\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> Append (\<Z> k (Suc u)) k Y\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
case (Iterate p Y)
[PROOF STATE]
proof (state)
this:
?q \<in> Y \<Longrightarrow> \<forall>i<length ?q. \<exists>u. ?q ! i \<in> \<Z> (charslength (take i ?q)) u
p \<in> Append (\<Z> k (Suc u)) k Y

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> Append (\<Z> k (Suc u)) k Y\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
from Iterate(2)
[PROOF STATE]
proof (chain)
picking this:
p \<in> Append (\<Z> k (Suc u)) k Y
[PROOF STEP]
have "p \<in> Y \<or> (\<exists> q t. p = q@[t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and>
      admissible (q @ [t]))"
[PROOF STATE]
proof (prove)
using this:
p \<in> Append (\<Z> k (Suc u)) k Y

goal (1 subgoal):
 1. p \<in> Y \<or> (\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]))
[PROOF STEP]
by (auto simp add: Append_def)
[PROOF STATE]
proof (state)
this:
p \<in> Y \<or> (\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]))

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> \<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u; p \<in> Append (\<Z> k (Suc u)) k Y\<rbrakk> \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> Y \<or> (\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> Y \<or> (\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]))

goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> Y \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
 2. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p \<in> Y

goal (2 subgoals):
 1. p \<in> Y \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
 2. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> Y

goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
using Iterate(1)
[PROOF STATE]
proof (prove)
using this:
p \<in> Y
?q \<in> Y \<Longrightarrow> \<forall>i<length ?q. \<exists>u. ?q ! i \<in> \<Z> (charslength (take i ?q)) u

goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])
[PROOF STEP]
obtain q t where
        qt: "p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])"
[PROOF STATE]
proof (prove)
using this:
\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])

goal (1 subgoal):
 1. (\<And>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])
[PROOF STEP]
have q_in_Y: "q \<in> Y"
[PROOF STATE]
proof (prove)
using this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])

goal (1 subgoal):
 1. q \<in> Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> Y

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
with qt
[PROOF STATE]
proof (chain)
picking this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])
q \<in> Y
[PROOF STEP]
have k: "k = charslength q"
[PROOF STATE]
proof (prove)
using this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])
q \<in> Y

goal (1 subgoal):
 1. k = charslength q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = charslength q

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
with qt
[PROOF STATE]
proof (chain)
picking this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])
k = charslength q
[PROOF STEP]
have t: "t \<in> \<Z> k (Suc u)"
[PROOF STATE]
proof (prove)
using this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t])
k = charslength q

goal (1 subgoal):
 1. t \<in> \<Z> k (Suc u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> \<Z> k (Suc u)

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> \<Z> k (Suc u) \<and> admissible (q @ [t]) \<Longrightarrow> \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u
[PROOF STEP]
proof(auto simp add: qt)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < Suc (length q) \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < Suc (length q) \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
assume i: "i < Suc (length q)"
[PROOF STATE]
proof (state)
this:
i < Suc (length q)

goal (1 subgoal):
 1. \<And>i. i < Suc (length q) \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < Suc (length q)
[PROOF STEP]
have "i < length q \<or> i = length q"
[PROOF STATE]
proof (prove)
using this:
i < Suc (length q)

goal (1 subgoal):
 1. i < length q \<or> i = length q
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
i < length q \<or> i = length q

goal (1 subgoal):
 1. \<And>i. i < Suc (length q) \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length q \<or> i = length q
[PROOF STEP]
show "\<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u"
[PROOF STATE]
proof (prove)
using this:
i < length q \<or> i = length q

goal (1 subgoal):
 1. \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
 2. i = length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
i < length q

goal (2 subgoals):
 1. i < length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
 2. i = length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
from Iterate(1)[OF q_in_Y]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length q. \<exists>u. q ! i \<in> \<Z> (charslength (take i q)) u

goal (1 subgoal):
 1. \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
by (simp add: 1)
[PROOF STATE]
proof (state)
this:
\<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u

goal (1 subgoal):
 1. i = length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
i = length q

goal (1 subgoal):
 1. i = length q \<Longrightarrow> \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u
[PROOF STEP]
apply (auto simp add: 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. t \<in> \<Z> (length (chars q)) u
[PROOF STEP]
apply (rule_tac x="Suc u" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<Z> (length (chars q)) (Suc u)
[PROOF STEP]
using k t
[PROOF STATE]
proof (prove)
using this:
k = charslength q
t \<in> \<Z> k (Suc u)

goal (1 subgoal):
 1. t \<in> \<Z> (length (chars q)) (Suc u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. (q @ [t]) ! i \<in> \<Z> (length (chars (take i q))) u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<length p. \<exists>u. p ! i \<in> \<Z> (charslength (take i p)) u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_append_token:
  assumes p: "p \<in> \<P> k u"
  assumes t: "t \<in> \<Z> k (Suc u)"
  assumes pt: "admissible (p@[t])"
  assumes k: "charslength p = k"
  shows "p@[t] \<in> \<P> k (Suc u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ [t] \<in> \<P> k (Suc u)
[PROOF STEP]
apply (simp only: \<P>.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ [t] \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)
[PROOF STEP]
apply (rule_tac n="Suc 0" in limit_elem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ [t] \<in> funpower (Append (\<Z> k (Suc u)) k) (Suc 0) (\<P> k u)
[PROOF STEP]
using p t pt k
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
t \<in> \<Z> k (Suc u)
admissible (p @ [t])
charslength p = k

goal (1 subgoal):
 1. p @ [t] \<in> funpower (Append (\<Z> k (Suc u)) k) (Suc 0) (\<P> k u)
[PROOF STEP]
apply (auto simp only: Append_def funpower.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> (charslength p) u; t \<in> \<Z> (charslength p) (Suc u); admissible (p @ [t]); k = charslength p; p @ [t] \<notin> \<P> (charslength p) u\<rbrakk> \<Longrightarrow> \<exists>pa ta. p @ [t] = pa @ [ta] \<and> pa \<in> by_length (charslength p) (\<P> (charslength p) u) \<and> ta \<in> \<Z> (charslength p) (Suc u) \<and> admissible (pa @ [ta])
[PROOF STEP]
by fastforce


[STATEMENT]
lemma indexlt_simp: "indexlt k' u' k u = (k' < k \<or> (k' = k \<and> u' < u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indexlt k' u' k u = (k' < k \<or> k' = k \<and> u' < u)
[PROOF STEP]
by (auto simp add: indexlt_def indexlt_rel_def)


[STATEMENT]
lemma \<P>_induct[consumes 1, case_names Induct]:
  assumes "p \<in> \<P> k u"
  assumes induct: "\<And> p k u . (\<And> p' k' u'. p' \<in> \<P> k' u' \<Longrightarrow> indexlt k' u' k u \<Longrightarrow> P p' k' u')
                     \<Longrightarrow> p \<in> \<P> k u \<Longrightarrow> P p k u"
  shows "P p k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p k u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P p k u
[PROOF STEP]
let ?R = "indexlt_rel <*lex*> {}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P p k u
[PROOF STEP]
have wf_R: "wf ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (indexlt_rel <*lex*> {})
[PROOF STEP]
by (auto simp add: wf_indexlt_rel)
[PROOF STATE]
proof (state)
this:
wf (indexlt_rel <*lex*> {})

goal (1 subgoal):
 1. P p k u
[PROOF STEP]
let ?P = "\<lambda> a. snd a \<in> \<P> (fst (fst a)) (snd (fst a)) \<longrightarrow> P (snd a) (fst (fst a)) (snd (fst a))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P p k u
[PROOF STEP]
have "p \<in> \<P> k u \<longrightarrow> P p k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k u \<longrightarrow> P p k u
[PROOF STEP]
apply (rule wf_induct[OF wf_R, where P = ?P and a = "((k, u), p)", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a b ba. (((a, b), ba), x) \<in> indexlt_rel <*lex*> {} \<longrightarrow> ba \<in> \<P> a b \<longrightarrow> P ba a b \<Longrightarrow> snd x \<in> \<P> (fst (fst x)) (snd (fst x)) \<longrightarrow> P (snd x) (fst (fst x)) (snd (fst x))
[PROOF STEP]
apply (auto simp add: indexlt_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>\<forall>aa ba. indexlt aa ba a b \<longrightarrow> (\<forall>b. b \<in> \<P> aa ba \<longrightarrow> P b aa ba); ba \<in> \<P> a b\<rbrakk> \<Longrightarrow> P ba a b
[PROOF STEP]
apply (rule_tac p=ba and k=a and u=b in induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba p' k' u'. \<lbrakk>\<forall>aa ba. indexlt aa ba a b \<longrightarrow> (\<forall>b. b \<in> \<P> aa ba \<longrightarrow> P b aa ba); ba \<in> \<P> a b; p' \<in> \<P> k' u'; indexlt k' u' a b\<rbrakk> \<Longrightarrow> P p' k' u'
 2. \<And>a b ba. \<lbrakk>\<forall>aa ba. indexlt aa ba a b \<longrightarrow> (\<forall>b. b \<in> \<P> aa ba \<longrightarrow> P b aa ba); ba \<in> \<P> a b\<rbrakk> \<Longrightarrow> ba \<in> \<P> a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u \<longrightarrow> P p k u

goal (1 subgoal):
 1. P p k u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u \<longrightarrow> P p k u

goal (1 subgoal):
 1. P p k u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u \<longrightarrow> P p k u
p \<in> \<P> k u
\<lbrakk>\<And>p' k' u'. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' ?k ?u\<rbrakk> \<Longrightarrow> P p' k' u'; ?p \<in> \<P> ?k ?u\<rbrakk> \<Longrightarrow> P ?p ?k ?u

goal (1 subgoal):
 1. P p k u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P p k u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonempty_path_indices:
  assumes p: "p \<in> \<P> k u"
  assumes nonempty: "p \<noteq> []"
  shows "k > 0 \<or> u > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<or> 0 < u
[PROOF STEP]
proof (cases "u = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < k \<or> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = 0

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < k \<or> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
note u = True
[PROOF STATE]
proof (state)
this:
u = 0

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < k \<or> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
have "k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
proof (cases "k = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> 0 < k
 2. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> 0 < k
 2. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
with p u
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k u
u = 0
k = 0
[PROOF STEP]
have "p = []"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
u = 0
k = 0

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

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> 0 < k
 2. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
with nonempty
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> []
p = []
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
p = []

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

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> 0 < k
 2. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < k

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> 0 < k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 < k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < k

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < k \<or> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. 0 < k \<or> 0 < u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < k \<or> 0 < u

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> 0

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> 0 < k \<or> 0 < u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0

goal (1 subgoal):
 1. 0 < k \<or> 0 < u
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 < k \<or> 0 < u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma base_paths:
  assumes p: "p \<in> \<P> k 0"
  assumes k: "k > 0"
  shows "\<exists> u. p \<in> \<P> (k - 1) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. p \<in> \<P> (k - 1) u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. p \<in> \<P> (k - 1) u
[PROOF STEP]
from k
[PROOF STATE]
proof (chain)
picking this:
0 < k
[PROOF STEP]
have "\<exists> i. k = Suc i"
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. \<exists>i. k = Suc i
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<exists>i. k = Suc i

goal (1 subgoal):
 1. \<exists>u. p \<in> \<P> (k - 1) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. k = Suc i
[PROOF STEP]
obtain i where i: "k = Suc i"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. k = Suc i

goal (1 subgoal):
 1. (\<And>i. k = Suc i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = Suc i

goal (1 subgoal):
 1. \<exists>u. p \<in> \<P> (k - 1) u
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k 0

goal (1 subgoal):
 1. \<exists>u. p \<in> \<P> (k - 1) u
[PROOF STEP]
by (auto simp add: i natUnion_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. p \<in> \<P> (k - 1) u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma indexlt_trans: "indexlt k'' u'' k' u' \<Longrightarrow> indexlt k' u' k u \<Longrightarrow> indexlt k'' u'' k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>indexlt k'' u'' k' u'; indexlt k' u' k u\<rbrakk> \<Longrightarrow> indexlt k'' u'' k u
[PROOF STEP]
using dual_order.strict_trans indexlt_simp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b < ?a; ?c < ?b\<rbrakk> \<Longrightarrow> ?c < ?a
indexlt ?k' ?u' ?k ?u = (?k' < ?k \<or> ?k' = ?k \<and> ?u' < ?u)

goal (1 subgoal):
 1. \<lbrakk>indexlt k'' u'' k' u'; indexlt k' u' k u\<rbrakk> \<Longrightarrow> indexlt k'' u'' k u
[PROOF STEP]
by auto