theory SIMPL_Lemmas

lemma hoarep_revert:
  "Gamm \<turnstile> P (call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s))) Q,R
     \<Longrightarrow> Gamm \<turnstile> P (Call fnname) Q,R" apply (rule hoare_complete) apply (drule hoare_sound) apply (simp add: cvalid_def HoarePartialDef.valid_def) apply (erule allEI)+ apply (rule impI, drule mp) apply (erule exec.cases, simp_all)[1] apply (case_tac ta, simp_all)[1] apply (erule exec_call) apply simp apply (rule exec.intros) apply (erule exec_callAbrupt, simp_all)[1] apply (erule exec_callFault, simp_all)[1] apply (erule exec_callStuck, simp_all)[1] apply (erule exec_callUndefined) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Gamm\<turnstile> P call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s)) Q,R \<Longrightarrow> Gamm\<turnstile> P Call fnname Q,R proof (prove)
goal (1 subgoal):
 1. Gamm\<turnstile> P call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s)) Q,R \<Longrightarrow> Gamm\<Turnstile>\<^bsub>/{}\<^esub> P Call fnname Q,R proof (prove)
goal (1 subgoal):
 1. Gamm,{}\<Turnstile>\<^bsub>/{}\<^esub> P call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s)) Q,R \<Longrightarrow> Gamm\<Turnstile>\<^bsub>/{}\<^esub> P Call fnname Q,R proof (prove)
goal (1 subgoal):
 1. \<forall>s t. Gamm\<turnstile> \<langle>call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s)),s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R \<Longrightarrow> \<forall>s t. Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (1 subgoal):
 1. \<And>s t. Gamm\<turnstile> \<langle>call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s)),s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R \<Longrightarrow> Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (2 subgoals):
 1. \<And>s t. Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t \<Longrightarrow> Gamm\<turnstile> \<langle>call (\<lambda>s. s) fnname (\<lambda>a b. b) (\<lambda>i t. Basic (\<lambda>s. s)),s\<rangle> \<Rightarrow> t
 2. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (3 subgoals):
 1. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = ta; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> ta
 2. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 3. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (6 subgoals):
 1. \<And>s t p bdy sa ta x1. \<lbrakk>fnname = p; s = Normal sa; t = Normal x1; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Normal x1; ta = Normal x1\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Normal x1
 2. \<And>s t p bdy sa ta x2. \<lbrakk>fnname = p; s = Normal sa; t = Abrupt x2; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt x2; ta = Abrupt x2\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Abrupt x2
 3. \<And>s t p bdy sa ta x3. \<lbrakk>fnname = p; s = Normal sa; t = Fault x3; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Fault x3; ta = Fault x3\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Fault x3
 4. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Stuck; ta = Stuck\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 5. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 6. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (7 subgoals):
 1. \<And>s t p bdy sa ta x1. \<lbrakk>fnname = p; s = Normal sa; t = Normal x1; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Normal x1; ta = Normal x1\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Normal (?t56 s t p bdy sa ta x1)
 2. \<And>s t p bdy sa ta x1. \<lbrakk>fnname = p; s = Normal sa; t = Normal x1; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Normal x1; ta = Normal x1\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>Basic (\<lambda>s. s),Normal (?t56 s t p bdy sa ta x1)\<rangle> \<Rightarrow> Normal x1
 3. \<And>s t p bdy sa ta x2. \<lbrakk>fnname = p; s = Normal sa; t = Abrupt x2; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt x2; ta = Abrupt x2\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Abrupt x2
 4. \<And>s t p bdy sa ta x3. \<lbrakk>fnname = p; s = Normal sa; t = Fault x3; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Fault x3; ta = Fault x3\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Fault x3
 5. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Stuck; ta = Stuck\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 6. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 7. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (6 subgoals):
 1. \<And>s t p bdy sa ta x1. \<lbrakk>fnname = p; s = Normal sa; t = Normal x1; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Normal x1; ta = Normal x1\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>Basic (\<lambda>s. s),Normal x1\<rangle> \<Rightarrow> Normal x1
 2. \<And>s t p bdy sa ta x2. \<lbrakk>fnname = p; s = Normal sa; t = Abrupt x2; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt x2; ta = Abrupt x2\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Abrupt x2
 3. \<And>s t p bdy sa ta x3. \<lbrakk>fnname = p; s = Normal sa; t = Fault x3; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Fault x3; ta = Fault x3\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Fault x3
 4. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Stuck; ta = Stuck\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 5. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 6. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (5 subgoals):
 1. \<And>s t p bdy sa ta x2. \<lbrakk>fnname = p; s = Normal sa; t = Abrupt x2; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt x2; ta = Abrupt x2\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Abrupt x2
 2. \<And>s t p bdy sa ta x3. \<lbrakk>fnname = p; s = Normal sa; t = Fault x3; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Fault x3; ta = Fault x3\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Fault x3
 3. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Stuck; ta = Stuck\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 4. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 5. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (4 subgoals):
 1. \<And>s t p bdy sa ta x3. \<lbrakk>fnname = p; s = Normal sa; t = Fault x3; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Fault x3; ta = Fault x3\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Fault x3
 2. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Stuck; ta = Stuck\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 3. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 4. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (3 subgoals):
 1. \<And>s t p bdy sa ta. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = Some bdy; Gamm\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Stuck; ta = Stuck\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 2. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 3. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (2 subgoals):
 1. \<And>s t p sa. \<lbrakk>fnname = p; s = Normal sa; t = Stuck; Gamm p = None\<rbrakk> \<Longrightarrow> Gamm\<turnstile> \<langle>CALL p(),Normal sa\<rangle> \<Rightarrow> Stuck
 2. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>Gamm\<turnstile> \<langle>Call fnname,s\<rangle> \<Rightarrow> t; s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R\<rbrakk> \<Longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` R proof (prove)
goal:
No subgoals!