theory SIMPL_Lemmas

lemma exec_While_cong':
  assumes c: "\<And>s s'. \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>c', Normal s\<rangle> \<Rightarrow> s'"
  assumes w: "\<Gamma> \<turnstile> \<langle>v, Normal s\<rangle> \<Rightarrow> s'"
  assumes eq: "v = While S c" "v' = While S c'"
  shows      "\<Gamma> \<turnstile> \<langle>v', Normal s\<rangle> \<Rightarrow> s'" using w eq apply (induct, simp_all) apply (rule exec.intros, assumption) apply (simp add: c) apply simp apply (rule exec.intros, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>v',Normal s\<rangle> \<Rightarrow> s' proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>v,Normal s\<rangle> \<Rightarrow> s'
v = While S c
v' = While S c'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>v',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>sa b s'a t. \<lbrakk>sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>While S c,s'a\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While S c',s'a\<rangle> \<Rightarrow> t; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',Normal sa\<rangle> \<Rightarrow> t
 2. \<And>sa b. \<lbrakk>sa \<notin> S; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',Normal sa\<rangle> \<Rightarrow> Normal sa proof (prove)
goal (3 subgoals):
 1. \<And>sa b s'a t. \<lbrakk>sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>While S c,s'a\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While S c',s'a\<rangle> \<Rightarrow> t; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal sa\<rangle> \<Rightarrow> ?s'80 sa b s'a t
 2. \<And>sa b s'a t. \<lbrakk>sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>While S c,s'a\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While S c',s'a\<rangle> \<Rightarrow> t; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',?s'80 sa b s'a t\<rangle> \<Rightarrow> t
 3. \<And>sa b. \<lbrakk>sa \<notin> S; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',Normal sa\<rangle> \<Rightarrow> Normal sa proof (prove)
goal (2 subgoals):
 1. \<And>sa b s'a t. \<lbrakk>sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>While S c,s'a\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While S c',s'a\<rangle> \<Rightarrow> t; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',s'a\<rangle> \<Rightarrow> t
 2. \<And>sa b. \<lbrakk>sa \<notin> S; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',Normal sa\<rangle> \<Rightarrow> Normal sa proof (prove)
goal (1 subgoal):
 1. \<And>sa b. \<lbrakk>sa \<notin> S; b = S; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'; v = While S c; v' = While S c'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',Normal sa\<rangle> \<Rightarrow> Normal sa proof (prove)
goal:
No subgoals!