[STATEMENT]
lemma WhileRule:
 "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<subseteq> i; Valid (i \<inter> b) c (A 0) i; i \<inter> - b \<subseteq> q\<rbrakk> \<Longrightarrow> Valid p (While b c) (Awhile i v A) q
[PROOF STEP]
apply (clarsimp simp:Valid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; Sem (While b c) s s'; s \<in> p\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply(drule While_aux)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p\<rbrakk> \<Longrightarrow> \<forall>sa s'a. Sem c sa s'a \<longrightarrow> sa \<in> ?I9 s s' \<and> sa \<in> b \<longrightarrow> s'a \<in> ?I9 s s'
 2. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p\<rbrakk> \<Longrightarrow> s \<in> ?I9 s s'
 3. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p; s' \<in> ?I9 s s' \<and> s' \<notin> b\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p\<rbrakk> \<Longrightarrow> s \<in> i
 2. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p; s' \<in> i \<and> s' \<notin> b\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p; s' \<in> i \<and> s' \<notin> b\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done