[STATEMENT]
lemma StartBallot_HInv3_p:
  "\<lbrakk> StartBallot s s' p; HInv3_L s' p q d \<rbrakk>
          \<Longrightarrow> HInv3_R s' p q d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>StartBallot s s' p; HInv3_L s' p q d\<rbrakk> \<Longrightarrow> HInv3_R s' p q d
[PROOF STEP]
by(auto simp add: StartBallot_def dest: InitPhase_HInv3_p)


[STATEMENT]
lemma resActRight:
  fixes x :: name
  and   \<alpha> :: act
  and   P :: ccs

  assumes "x \<sharp> \<alpha>"
  and     "Id \<subseteq> Rel"

  shows "\<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>(\<alpha>.(P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>\<alpha>.P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<alpha>
Id \<subseteq> Rel

goal (1 subgoal):
 1. \<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>\<alpha>.P
[PROOF STEP]
by(fastforce simp add: simulation_def elim: resCases actCases intro: Action)


[STATEMENT]
lemma WEAK[rule_format]:
  "G \<rhd> c : A \<Longrightarrow> (\<forall> H . G \<subseteq> H \<longrightarrow> H \<rhd> c :A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<rhd> c : A \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<rhd> c : A \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A
[PROOF STEP]
apply (erule VDM_proof.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>G. \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Skip : (\<lambda>a b. b = a)
 2. \<And>G x e. \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Assign x e : (\<lambda>a b. b = update a x (evalE e a))
 3. \<And>G c1 A1 c2 A2. \<lbrakk>G \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; G \<rhd> c2 : A2; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Comp c1 c2 : (\<lambda>a b. \<exists>r. A1 a r \<and> A2 r b)
 4. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 5. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 6. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 7. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 8. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>G H. G \<subseteq> H \<Longrightarrow> H \<rhd> Skip : (\<lambda>a b. b = a)
 2. \<And>G x e. \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Assign x e : (\<lambda>a b. b = update a x (evalE e a))
 3. \<And>G c1 A1 c2 A2. \<lbrakk>G \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; G \<rhd> c2 : A2; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Comp c1 c2 : (\<lambda>a b. \<exists>r. A1 a r \<and> A2 r b)
 4. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 5. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 6. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 7. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 8. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMSkip)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>G x e. \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Assign x e : (\<lambda>a b. b = update a x (evalE e a))
 2. \<And>G c1 A1 c2 A2. \<lbrakk>G \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; G \<rhd> c2 : A2; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Comp c1 c2 : (\<lambda>a b. \<exists>r. A1 a r \<and> A2 r b)
 3. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 4. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 5. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 7. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>G x e H. G \<subseteq> H \<Longrightarrow> H \<rhd> Assign x e : (\<lambda>a b. b = update a x (evalE e a))
 2. \<And>G c1 A1 c2 A2. \<lbrakk>G \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; G \<rhd> c2 : A2; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Comp c1 c2 : (\<lambda>a b. \<exists>r. A1 a r \<and> A2 r b)
 3. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 4. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 5. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 7. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMAssign)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>G c1 A1 c2 A2. \<lbrakk>G \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; G \<rhd> c2 : A2; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Comp c1 c2 : (\<lambda>a b. \<exists>r. A1 a r \<and> A2 r b)
 2. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 3. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 4. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>G c1 A1 c2 A2 H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> Comp c1 c2 : (\<lambda>a b. \<exists>r. A1 a r \<and> A2 r b)
 2. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 3. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 4. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMComp)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>G c1 A1 c2 A2 H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c1 : A1
 2. \<And>G c1 A1 c2 A2 H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c2 : A2
 3. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 4. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 5. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 7. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (erule_tac x=H in allE, simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>G c1 A1 c2 A2 H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A1; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : A2; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c2 : A2
 2. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 3. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 4. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (erule_tac x=H in allE, simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>G c1 A c2 B b. \<lbrakk>G \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; G \<rhd> c2 : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 2. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 3. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>G c1 A c2 B b H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> Iff b c1 c2 : (\<lambda>a c. (evalB b a \<longrightarrow> A a c) \<and> (\<not> evalB b a \<longrightarrow> B a c))
 2. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 3. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMIff)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>G c1 A c2 B b H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c1 : A
 2. \<And>G c1 A c2 B b H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c2 : B
 3. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 4. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (erule_tac x=H in allE, simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>G c1 A c2 B b H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c1 : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c2 : B; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c2 : B
 2. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 3. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (erule_tac x=H in allE, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>G c B b A. \<lbrakk>G \<rhd> c : B; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 2. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> While b c : (\<lambda>a c. A a c \<and> \<not> evalB b c)
 2. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMWhile)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c : ?B44 G c B b A H
 2. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s. \<not> evalB b s \<longrightarrow> A s s
 3. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s r t. evalB b s \<longrightarrow> ?B44 G c B b A H s r \<longrightarrow> A r t \<longrightarrow> A s t
 4. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 6. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (erule_tac x=H in allE, simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s. \<not> evalB b s \<longrightarrow> A s s
 2. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t
 3. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 5. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>G c B b A H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B; \<forall>s. \<not> evalB b s \<longrightarrow> A s s; \<forall>s. evalB b s \<longrightarrow> (\<forall>r. B s r \<longrightarrow> (\<forall>t. A r t \<longrightarrow> A s t)); G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s r t. evalB b s \<longrightarrow> B s r \<longrightarrow> A r t \<longrightarrow> A s t
 2. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 4. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A G. \<lbrakk>({A} \<union> G) \<rhd> body : A; \<forall>H. {A} \<union> G \<subseteq> H \<longrightarrow> H \<rhd> body : A\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 2. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A G H. \<lbrakk>\<forall>H. A \<in> H \<and> G \<subseteq> H \<longrightarrow> H \<rhd> body : A; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> Call : A
 2. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMCall)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A G H. \<lbrakk>\<forall>H. A \<in> H \<and> G \<subseteq> H \<longrightarrow> H \<rhd> body : A; G \<subseteq> H\<rbrakk> \<Longrightarrow> ({A} \<union> H) \<rhd> body : A
 2. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (erule_tac x="({A} \<union> H)" in allE, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A G H. \<lbrakk>G \<subseteq> H; G \<subseteq> insert A H \<longrightarrow> insert A H \<rhd> body : A\<rbrakk> \<Longrightarrow> insert A H \<rhd> body : A
 2. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 3. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A G. A \<in> G \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> Call : A
 2. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A G H. \<lbrakk>A \<in> G; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> Call : A
 2. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMAx)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A G H. \<lbrakk>A \<in> G; G \<subseteq> H\<rbrakk> \<Longrightarrow> A \<in> H
 2. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>G c A B. \<lbrakk>G \<rhd> c : A; \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t\<rbrakk> \<Longrightarrow> \<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>G c A B H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c : B
[PROOF STEP]
apply (rule VDMConseq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>G c A B H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t; G \<subseteq> H\<rbrakk> \<Longrightarrow> H \<rhd> c : ?A82 G c A B H
 2. \<And>G c A B H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t; G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s t. ?A82 G c A B H s t \<longrightarrow> B s t
[PROOF STEP]
apply (erule_tac x=H in allE, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>G c A B H. \<lbrakk>\<forall>s t. A s t \<longrightarrow> B s t; G \<subseteq> H; H \<rhd> c : A\<rbrakk> \<Longrightarrow> H \<rhd> c : ?A82 G c A B H
 2. \<And>G c A B H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t; G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s t. ?A82 G c A B H s t \<longrightarrow> B s t
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>G c A B H. \<lbrakk>\<forall>H. G \<subseteq> H \<longrightarrow> H \<rhd> c : A; \<forall>s t. A s t \<longrightarrow> B s t; G \<subseteq> H\<rbrakk> \<Longrightarrow> \<forall>s t. A s t \<longrightarrow> B s t
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
have "?thesis = eval_pf (Forall (Exist (Or (Eq [1, -1] 5)
    (Forall (Forall (Imp (Neg (Le [-1, 0] (- 6))) (Imp (Eq [1, 6, 0, -1] 0) (Eq [0, 1] 1)))))))) []"
    (is "_ = eval_pf ?P []")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)) = eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)) = eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)) = eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
have "\<dots> = dfa_accepts (dfa_of_pf 0 ?P) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) [] = dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []
[PROOF STEP]
by (simp add: dfa_of_pf_correctness del: dfa_of_pf.simps)
[PROOF STATE]
proof (state)
this:
eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) [] = dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_pf (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1)))))))) [] = dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
have "\<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
dfa_accepts (dfa_of_pf 0 (Forall (Exist (Or (Eq [1, - 1] 5) (Forall (Forall (Imp (Neg (Le [- 1, 0] (- 6))) (Imp (Eq [1, 6, 0, - 1] 0) (Eq [0, 1] 1))))))))) []

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)

goal (1 subgoal):
 1. \<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<exists>xa. int xa - int x = 5) \<or> (\<forall>xa xb. \<not> 6 \<le> int xb \<longrightarrow> int xb + (6 * int xa - int x) = 0 \<longrightarrow> int xa = 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reach2:
  "\<not> s\<turnstile> l reachable_from x \<Longrightarrow> \<not> s\<langle>l:=y\<rangle>\<turnstile> l reachable_from x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> s\<turnstile> l reachable_from x \<Longrightarrow> \<not> s\<langle>l := y\<rangle>\<turnstile> l reachable_from x
[PROOF STEP]
by (simp)


[STATEMENT]
lemma pop_list_current [simp]: "\<lbrakk>invar small; 0 < size small; Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow> x # list_current small' = list_current small"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar small; 0 < size small; Small.pop small = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current small
[PROOF STEP]
proof(induction small arbitrary: x rule: pop.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>state x. \<lbrakk>invar (Common state); 0 < size (Common state); Small.pop (Common state) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Common state)
 2. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 3. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
case (1 state)
[PROOF STATE]
proof (state)
this:
invar (Common state)
0 < size (Common state)
Small.pop (Common state) = (x, small')

goal (3 subgoals):
 1. \<And>state x. \<lbrakk>invar (Common state); 0 < size (Common state); Small.pop (Common state) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Common state)
 2. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 3. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Common state)
0 < size (Common state)
Small.pop (Common state) = (x, small')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Common state)
0 < size (Common state)
Small.pop (Common state) = (x, small')

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Common state)
[PROOF STEP]
by(auto simp: pop_list_current split: prod.splits)
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Common state)

goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
case (2 current small auxS)
[PROOF STATE]
proof (state)
this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')

goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')
[PROOF STEP]
have "invar current"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')

goal (1 subgoal):
 1. invar current
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
invar current

goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')
invar current
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')
invar current

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)

goal (1 subgoal):
 1. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
case (3 current auxS big newS count)
[PROOF STATE]
proof (state)
this:
invar (Reverse2 current auxS big newS count)
0 < size (Reverse2 current auxS big newS count)
Small.pop (Reverse2 current auxS big newS count) = (x, small')

goal (1 subgoal):
 1. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 current auxS big newS count)
0 < size (Reverse2 current auxS big newS count)
Small.pop (Reverse2 current auxS big newS count) = (x, small')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 current auxS big newS count)
0 < size (Reverse2 current auxS big newS count)
Small.pop (Reverse2 current auxS big newS count) = (x, small')

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
proof(induction current rule: Current.pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Reverse2 (Current [] added old remained) auxS big newS count); 0 < size (Reverse2 (Current [] added old remained) auxS big newS count); Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
 2. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
case (1 added old remained)
[PROOF STATE]
proof (state)
this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Reverse2 (Current [] added old remained) auxS big newS count); 0 < size (Reverse2 (Current [] added old remained) auxS big newS count); Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
 2. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')
[PROOF STEP]
have "\<not>is_empty old"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')

goal (1 subgoal):
 1. \<not> is_empty old
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty)
[PROOF STATE]
proof (state)
this:
\<not> is_empty old

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Reverse2 (Current [] added old remained) auxS big newS count); 0 < size (Reverse2 (Current [] added old remained) auxS big newS count); Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
 2. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')
\<not> is_empty old
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')
\<not> is_empty old

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
[PROOF STEP]
by(auto simp: rev_take drop_Suc drop_tl)
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
invar (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
0 < size (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
Small.pop (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count) = (x, small')

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
0 < size (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
Small.pop (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count) = (x, small')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
0 < size (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
Small.pop (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count) = (x, small')

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iprev_inext: "
  n \<noteq> Max I \<or> infinite I \<Longrightarrow> iprev (inext n I) I = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> Max I \<or> infinite I \<Longrightarrow> iprev (inext n I) I = n
[PROOF STEP]
by (blast intro: iprev_inext_infin iprev_inext_fin)


[STATEMENT]
lemma fun_upd2_comm:
assumes "a' = a \<and> b' = b \<longrightarrow> c' = c"
shows "fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a' = a \<and> b' = b \<longrightarrow> c' = c

goal (1 subgoal):
 1. fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c
[PROOF STEP]
unfolding fun_upd2_def
[PROOF STATE]
proof (prove)
using this:
a' = a \<and> b' = b \<longrightarrow> c' = c

goal (1 subgoal):
 1. (\<lambda>a'a b'a. if a' = a'a \<and> b' = b'a then c' else if a = a'a \<and> b = b'a then c else f a'a b'a) = (\<lambda>a'a b'a. if a = a'a \<and> b = b'a then c else if a' = a'a \<and> b' = b'a then c' else f a'a b'a)
[PROOF STEP]
by (intro ext) auto


[STATEMENT]
lemma reflects_iso:
    assumes "\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>" and "B.iso (F f)"
    shows "A.iso f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)
[PROOF STEP]
obtain g' where g': "B.inverse_arrows (F f) g'"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)

goal (1 subgoal):
 1. (\<And>g'. B.inverse_arrows (F f) g' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B.inverse_arrows (F f) g'

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
have 1: "\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
[PROOF STEP]
using assms g'
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)
B.inverse_arrows (F f) g'

goal (1 subgoal):
 1. \<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
[PROOF STEP]
by (metis B.inv_in_hom B.inverse_unique preserves_hom)
[PROOF STATE]
proof (state)
this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
[PROOF STEP]
obtain g where g: "\<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g'"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>

goal (1 subgoal):
 1. (\<And>g. \<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) is_full
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
\<lbrakk>A.ide ?a; A.ide ?a'; \<guillemotleft>?g : F ?a' \<rightarrow>\<^sub>B F ?a\<guillemotright>\<rbrakk> \<Longrightarrow> \<exists>f. \<guillemotleft>f : ?a' \<rightarrow>\<^sub>A ?a\<guillemotright> \<and> F f = ?g

goal (1 subgoal):
 1. (\<And>g. \<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis A.arrI A.ide_cod A.ide_dom A.in_homE)
[PROOF STATE]
proof (state)
this:
\<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g'

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
have "A.inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.inverse_arrows f g
[PROOF STEP]
using assms 1 g g' A.inverse_arrowsI
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
\<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g'
B.inverse_arrows (F f) g'
\<lbrakk>A.ide (A ?g ?f); A.ide (A ?f ?g)\<rbrakk> \<Longrightarrow> A.inverse_arrows ?f ?g

goal (1 subgoal):
 1. A.inverse_arrows f g
[PROOF STEP]
by (metis A.arr_iff_in_hom A.dom_comp A.in_homE A.seqI' B.inverse_arrowsE
            A.cod_comp locally_reflects_ide preserves_comp)
[PROOF STATE]
proof (state)
this:
A.inverse_arrows f g

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A.inverse_arrows f g

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma H_cons: "\<tt>\<tt> p \<le> \<tt>\<tt> p' \<Longrightarrow> \<tt>\<tt> q' \<le> \<tt>\<tt> q \<Longrightarrow> H p' x q' \<Longrightarrow> H p x q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tt>\<tt> p \<le> \<tt>\<tt> p'; \<tt>\<tt> q' \<le> \<tt>\<tt> q; H p' x q'\<rbrakk> \<Longrightarrow> H p x q
[PROOF STEP]
by (simp add: H_consl H_consr)

\<comment> \<open> Skip \<close>


[STATEMENT]
lemma next_upto_generator [simp]:
  "list.next upto_generator n = (n, n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.next local.upto_generator n = (n, n + 1)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma beforex_beforex\<^sub>0_eq:
 "P,C,M \<rhd> xt / I,d \<equiv> \<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 P C M d I xt xt\<^sub>0 xt\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,C,M \<rhd> xt / I,d \<equiv> \<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 P C M d I xt xt\<^sub>0 xt\<^sub>1
[PROOF STEP]
using beforex_def
[PROOF STATE]
proof (prove)
using this:
(?P,?C,?M \<rhd> ?xt / ?I,?d) = (\<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 ?P ?C ?M ?d ?I ?xt xt\<^sub>0 xt\<^sub>1)

goal (1 subgoal):
 1. P,C,M \<rhd> xt / I,d \<equiv> \<exists>xt\<^sub>0 xt\<^sub>1. beforex\<^sub>0 P C M d I xt xt\<^sub>0 xt\<^sub>1
[PROOF STEP]
by auto


[STATEMENT]
lemma pat_rule:
  "\<lbrakk> p\<equiv>p'; ID p' t' T \<rbrakk> \<Longrightarrow> ID p t' T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<equiv> p'; ID p' t' T\<rbrakk> \<Longrightarrow> ID p t' T
[PROOF STEP]
by simp


[STATEMENT]
lemma mkt_stocks_assets:
  shows "stk_strict_subs (stocks Mkt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk_strict_subs (stocks Mkt)
[PROOF STEP]
unfolding stocks_def prices_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk_strict_subs (fst (Rep_discrete_market Mkt))
[PROOF STEP]
by (metis Rep_discrete_market mem_Collect_eq split_beta')


[STATEMENT]
lemma self_finance_init:
  assumes "\<forall>w. prices Mkt asset 0 w \<noteq> 0"
  and "portfolio pf"
shows "val_process Mkt (self_finance Mkt v pf asset) 0 w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
define scp where "scp = qty_single asset (remaining_qty Mkt v pf asset)"
[PROOF STATE]
proof (state)
this:
scp = qty_single asset (remaining_qty Mkt v pf asset)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "val_process Mkt (self_finance Mkt v pf asset) 0 w =
    val_process Mkt pf 0 w +
    val_process Mkt scp 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt scp 0 w
[PROOF STEP]
unfolding scp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) 0 w
[PROOF STEP]
using assms single_comp_portfolio[of asset]
    sum_val_process[of pf "qty_single asset (remaining_qty Mkt v pf asset)" Mkt]
[PROOF STATE]
proof (prove)
using this:
\<forall>w. prices Mkt asset 0 w \<noteq> 0
portfolio pf
portfolio (qty_single asset ?qty)
\<lbrakk>portfolio pf; portfolio (qty_single asset (remaining_qty Mkt v pf asset))\<rbrakk> \<Longrightarrow> \<forall>n w. val_process Mkt (qty_sum pf (qty_single asset (remaining_qty Mkt v pf asset))) n w = val_process Mkt pf n w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) n w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) 0 w
[PROOF STEP]
by (simp add: \<open>\<And>qty. portfolio (qty_single asset qty)\<close> self_finance_def)
[PROOF STATE]
proof (state)
this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt scp 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt scp 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w +
    (sum (\<lambda>x. ((prices Mkt) x 0 w) * (scp x (Suc 0) w)) {asset})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)
[PROOF STEP]
using subset_val_process'[of "{asset}" scp]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {asset}; support_set scp \<subseteq> {asset}\<rbrakk> \<Longrightarrow> val_process ?Mkt scp ?n ?w = (\<Sum>x\<in>{asset}. prices ?Mkt x ?n ?w * scp x (Suc ?n) ?w)

goal (1 subgoal):
 1. val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)
[PROOF STEP]
unfolding scp_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {asset}; support_set (qty_single asset (remaining_qty Mkt v pf asset)) \<subseteq> {asset}\<rbrakk> \<Longrightarrow> val_process ?Mkt (qty_single asset (remaining_qty Mkt v pf asset)) ?n ?w = (\<Sum>x\<in>{asset}. prices ?Mkt x ?n ?w * qty_single asset (remaining_qty Mkt v pf asset) x (Suc ?n) ?w)

goal (1 subgoal):
 1. val_process Mkt pf 0 w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * qty_single asset (remaining_qty Mkt v pf asset) x (Suc 0) w)
[PROOF STEP]
by (auto simp add:  single_comp_support)
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w) = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w) = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w) = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + prices Mkt asset 0 w * (remaining_qty Mkt v pf asset) (Suc 0) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w
[PROOF STEP]
unfolding scp_def qty_single_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * (qty_empty(asset := remaining_qty Mkt v pf asset)) asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w)/(prices Mkt asset 0 w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w. prices Mkt asset 0 w \<noteq> 0
portfolio pf

goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w) = v

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = v

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma first_tail_second: "first(tail s) = second s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. first (tail s) = second s
[PROOF STEP]
by (simp add: first_def second_def tail_def suffix_def)


[STATEMENT]
lemma wt_ge_0[simp]:
assumes "proper c" and "i < brn c"
shows "0 \<le> wt c s i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> wt c s i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proper c
i < brn c

goal (1 subgoal):
 1. 0 \<le> wt c s i
[PROOF STEP]
proof (induct c arbitrary: i s rule: proper_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>ch c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (Ch ch c1 c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Ch ch c1 c2) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 7. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
case (Ch ch c1 c2)
[PROOF STATE]
proof (state)
this:
?i < brn c1 \<Longrightarrow> 0 \<le> wt c1 ?s ?i
?i < brn c2 \<Longrightarrow> 0 \<le> wt c2 ?s ?i
i < brn (Ch ch c1 c2)

goal (7 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>ch c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (Ch ch c1 c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Ch ch c1 c2) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 7. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?i < brn c1 \<Longrightarrow> 0 \<le> wt c1 ?s ?i
?i < brn c2 \<Longrightarrow> 0 \<le> wt c2 ?s ?i
i < brn (Ch ch c1 c2)

goal (1 subgoal):
 1. 0 \<le> wt (Ch ch c1 c2) s i
[PROOF STEP]
using properCh
[PROOF STATE]
proof (prove)
using this:
?i < brn c1 \<Longrightarrow> 0 \<le> wt c1 ?s ?i
?i < brn c2 \<Longrightarrow> 0 \<le> wt c2 ?s ?i
i < brn (Ch ch c1 c2)
0 \<le> cval ?ch ?s \<and> cval ?ch ?s \<le> 1

goal (1 subgoal):
 1. 0 \<le> wt (Ch ch c1 c2) s i
[PROOF STEP]
by (cases i) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
0 \<le> wt (Ch ch c1 c2) s i

goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
case (Par cl ii)
[PROOF STATE]
proof (state)
this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (Par cl)

goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
have "properL cl" and "ii < brnL cl (length cl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
using Par
[PROOF STATE]
proof (prove)
using this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (Par cl)

goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properL cl
ii < brnL cl (length cl)

goal (6 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (Par cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s i
 6. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
properL cl
ii < brnL cl (length cl)

goal (1 subgoal):
 1. 0 \<le> wt (Par cl) s ii
[PROOF STEP]
apply (cases rule: brnL_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s ii
[PROOF STEP]
using Par
[PROOF STATE]
proof (prove)
using this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (Par cl)

goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (Par cl) s ii
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> wt (Par cl) s ii

goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
case (ParT cl ii)
[PROOF STATE]
proof (state)
this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
have "properL cl" and "ii < brnL cl (length cl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
using ParT
[PROOF STATE]
proof (prove)
using this:
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (1 subgoal):
 1. properL cl &&& ii < brnL cl (length cl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properL cl
ii < brnL cl (length cl)

goal (5 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
 5. \<And>cl i s. \<lbrakk>properL cl; \<And>c i s. \<lbrakk>c \<in> set cl; i < brn c\<rbrakk> \<Longrightarrow> 0 \<le> wt c s i; i < brn (ParT cl)\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
properL cl
ii < brnL cl (length cl)

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
proof(cases rule: brnL_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
case (Local n i)
[PROOF STATE]
proof (state)
this:
n < length cl
i < brn (cl ! n)
ii = brnL cl n + i

goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n < length cl; i < brn (cl ! n); ii = brnL cl n + i\<rbrakk> \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
proof (cases "WtFT cl = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. WtFT cl = 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
 2. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
WtFT cl = 1

goal (2 subgoals):
 1. WtFT cl = 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
 2. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
WtFT cl = 1

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
using Local ParT
[PROOF STATE]
proof (prove)
using this:
WtFT cl = 1
n < length cl
i < brn (cl ! n)
ii = brnL cl n + i
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
by (cases "n = pickFT cl \<and> i = 0") auto
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal (1 subgoal):
 1. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
WtFT cl \<noteq> 1

goal (1 subgoal):
 1. WtFT cl \<noteq> 1 \<Longrightarrow> 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
WtFT cl \<noteq> 1

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
using Local ParT
[PROOF STATE]
proof (prove)
using this:
WtFT cl \<noteq> 1
n < length cl
i < brn (cl ! n)
ii = brnL cl n + i
properL cl
\<lbrakk>?c \<in> set cl; ?i < brn ?c\<rbrakk> \<Longrightarrow> 0 \<le> wt ?c ?s ?i
ii < brn (ParT cl)

goal (1 subgoal):
 1. 0 \<le> wt (ParT cl) s ii
[PROOF STEP]
by (cases "finished (cl ! n)") auto
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> wt (ParT cl) s ii

goal (4 subgoals):
 1. \<And>i s. i < brn Done \<Longrightarrow> 0 \<le> wt Done s i
 2. \<And>atm i s. i < brn (Atm atm) \<Longrightarrow> 0 \<le> wt (Atm atm) s i
 3. \<And>c1 c2 i s. \<lbrakk>\<And>i s. i < brn c1 \<Longrightarrow> 0 \<le> wt c1 s i; \<And>i s. i < brn c2 \<Longrightarrow> 0 \<le> wt c2 s i; i < brn (c1 ;; c2)\<rbrakk> \<Longrightarrow> 0 \<le> wt (c1 ;; c2) s i
 4. \<And>tst c i s. \<lbrakk>\<And>i s. i < brn c \<Longrightarrow> 0 \<le> wt c s i; i < brn (While tst c)\<rbrakk> \<Longrightarrow> 0 \<le> wt (While tst c) s i
[PROOF STEP]
qed auto


[STATEMENT]
lemma less_is_non_zero_p1:
  fixes a :: "'a :: len word"
  shows "a < k \<Longrightarrow> a + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < k \<Longrightarrow> a + 1 \<noteq> 0
[PROOF STEP]
apply (erule contrapos_pn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + 1 = 0 \<Longrightarrow> \<not> a < k
[PROOF STEP]
apply (drule max_word_wrap)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = - 1 \<Longrightarrow> \<not> a < k
[PROOF STEP]
apply (simp add: not_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma test_bit_rcat:
  "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> bit rc n =
    (n < size rc \<and> n div sw < size wl \<and> bit ((rev wl) ! (n div sw)) (n mod sw))"
  for wl :: "'a::len word list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = size (hd wl); rc = word_rcat wl\<rbrakk> \<Longrightarrow> bit rc n = (n < size rc \<and> n div sw < length wl \<and> bit (rev wl ! (n div sw)) (n mod sw))
[PROOF STEP]
by (simp add: word_size word_rcat_def rev_map bit_horner_sum_uint_exp_iff bit_simps not_le)


[STATEMENT]
lemma and_neq_0_is_nth:
  \<open>x AND y \<noteq> 0 \<longleftrightarrow> bit x n\<close> if \<open>y = 2 ^ n\<close> for x y :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x AND y \<noteq> 0) = bit x n
[PROOF STEP]
apply (simp add: bit_eq_iff bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>n<LENGTH('a). bit x n \<and> bit y n) = bit x n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y = 2 ^ n

goal (1 subgoal):
 1. (\<exists>n<LENGTH('a). bit x n \<and> bit y n) = bit x n
[PROOF STEP]
apply (simp add: bit_simps not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = 2 ^ n \<Longrightarrow> (n < LENGTH('a) \<and> bit x n \<and> n < LENGTH('a)) = bit x n
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y n x. take_bit LENGTH('a) y = take_bit LENGTH('a) (2 ^ n) \<Longrightarrow> (n < LENGTH('a) \<and> (n < LENGTH('a) \<and> bit x n) \<and> n < LENGTH('a)) = (n < LENGTH('a) \<and> bit x n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SeqAppendP_fresh_iff [simp]:
  "a \<sharp> SeqAppendP f1 k1 f2 k2 g \<longleftrightarrow> a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
obtain g1::name and g2::name
    where "atom g1 \<sharp> (g2,f1,k1,f2,k2,g)" "atom g2 \<sharp> (f1,k1,f2,k2,g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g1 g2. \<lbrakk>atom g1 \<sharp> (g2, f1, k1, f2, k2, g); atom g2 \<sharp> (f1, k1, f2, k2, g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom g1 \<sharp> (g2, f1, k1, f2, k2, g)
atom g2 \<sharp> (f1, k1, f2, k2, g)

goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom g1 \<sharp> (g2, f1, k1, f2, k2, g)
atom g2 \<sharp> (f1, k1, f2, k2, g)

goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem AbstFormP_Neg: "{AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
obtain k1::name and s1::name and k::name and s::name
    where "atom s1 \<sharp> (v,i,x,x')"        "atom k1 \<sharp> (v,i,x,x',s1)"
      "atom s  \<sharp> (v,i,x,x',k1,s1)"  "atom k  \<sharp> (v,i,x,x',s,k1,s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 k1 s k. \<lbrakk>atom s1 \<sharp> (v, i, x, x'); atom k1 \<sharp> (v, i, x, x', s1); atom s \<sharp> (v, i, x, x', k1, s1); atom k \<sharp> (v, i, x, x', s, k1, s1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom s1 \<sharp> (v, i, x, x')
atom k1 \<sharp> (v, i, x, x', s1)
atom s \<sharp> (v, i, x, x', k1, s1)
atom k \<sharp> (v, i, x, x', s, k1, s1)

goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom s1 \<sharp> (v, i, x, x')
atom k1 \<sharp> (v, i, x, x', s1)
atom s \<sharp> (v, i, x, x', k1, s1)
atom k \<sharp> (v, i, x, x', s, k1, s1)

goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
by (force simp: AbstFormP.simps [of s v i "Q_Neg x" _ k] AbstFormP.simps [of s1 v i x x' k1]
        intro: SeqAbstFormP_Neg [THEN cut3])
[PROOF STATE]
proof (state)
this:
{AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_golomb_encoding: "is_encoding N\<^sub>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
have "is_encoding (\<lambda>n. N\<^sub>e n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
unfolding N\<^sub>e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_encoding (\<lambda>n. Ng\<^sub>e (n + 1))
[PROOF STEP]
by (intro encoding_compose_2[where g="(\<lambda>n. n + 1)"] elias_gamma_encoding, auto)
[PROOF STATE]
proof (state)
this:
is_encoding N\<^sub>e

goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_encoding N\<^sub>e

goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_encoding N\<^sub>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma devBC_some[simp]: assumes "\<parallel>nid\<parallel>\<^bsub>t n\<^esub>" shows "devBC t n nid n = Some nid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<parallel>nid\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
have "(n, nid)\<in> his t n nid"
[PROOF STATE]
proof (prove)
using this:
\<parallel>nid\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. (n, nid) \<in> his t n nid
[PROOF STEP]
using his.intros(1)
[PROOF STATE]
proof (prove)
using this:
\<parallel>nid\<parallel>\<^bsub>t n\<^esub>
\<parallel>?nid\<parallel>\<^bsub>?t ?n\<^esub> \<Longrightarrow> (?n, ?nid) \<in> his ?t ?n ?nid

goal (1 subgoal):
 1. (n, nid) \<in> his t n nid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
hence "devBC t n nid n = (Some (THE nid'. (n, nid')\<in>his t n nid))"
[PROOF STATE]
proof (prove)
using this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
[PROOF STEP]
using devBC_def
[PROOF STATE]
proof (prove)
using this:
(n, nid) \<in> his t n nid
devBC ?t ?n ?nid ?n' \<equiv> if \<exists>nid'. (?n', nid') \<in> his ?t ?n ?nid then Some (THE nid'. (?n', nid') \<in> his ?t ?n ?nid) else None

goal (1 subgoal):
 1. devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
have "(THE nid'. (n, nid')\<in>his t n nid) = nid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE nid'. (n, nid') \<in> his t n nid) = nid
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (n, nid) \<in> his t n nid
 2. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
from \<open>(n, nid)\<in> his t n nid\<close>
[PROOF STATE]
proof (chain)
picking this:
(n, nid) \<in> his t n nid
[PROOF STEP]
show "(n, nid)\<in> his t n nid"
[PROOF STATE]
proof (prove)
using this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. (n, nid) \<in> his t n nid
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
fix nid'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
assume "(n, nid') \<in> his t n nid"
[PROOF STATE]
proof (state)
this:
(n, nid') \<in> his t n nid

goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
thus "nid' = nid"
[PROOF STATE]
proof (prove)
using this:
(n, nid') \<in> his t n nid

goal (1 subgoal):
 1. nid' = nid
[PROOF STEP]
using his_determ_base
[PROOF STATE]
proof (prove)
using this:
(n, nid') \<in> his t n nid
(?n, ?nid') \<in> his ?t ?n ?nid \<Longrightarrow> ?nid' = ?nid

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(THE nid'. (n, nid') \<in> his t n nid) = nid

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
(THE nid'. (n, nid') \<in> his t n nid) = nid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
(THE nid'. (n, nid') \<in> his t n nid) = nid

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
devBC t n nid n = Some nid

goal:
No subgoals!
[PROOF STEP]
qed