[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