theory SALOverflowFWInst_deep = SALOverflowPlatform_deep + AuxBox2:

text {* In this theory we prove that our instantiated functions satisfy
the PCC Framework's requirements. In the very end this leads to a reuse
of the VCG Soundness theorem and thus guarantees the soundness of our platform *} 

section {* Requirements for the Safety Logic hold! *}

theorem SALSafetyLogicIns:
"SafetyLogic Conj Impl TrueF FalseF valid"
(*<*)
apply (unfold SafetyLogic_def)

--{* semConj *}
apply (rule conjI, (rule allI)+, rule iffI)
apply (erule rev_mp, induct_tac "L", (simp add: ls), (simp add: ls))+

--{* semImp *}
apply (rule conjI, (rule allI)+, (simp add: ls))

--{* TrueFSem *}
apply (rule conjI)
apply (simp add: ls)

--{* semFalseF *}
apply (simp add: ls)
(*>*)
done

section {* Auxiliary Lemmas *}

lemma checkPos_split:
"checkPos prg (l1@l2) = ((checkPos prg l1) \<and> (checkPos prg l2))"
(*<*)
apply (induct_tac l1)
apply simp
apply (simp add: checkPos.simps Let_def split_def fst_conv snd_conv bool.cases)
(*>*)
done

lemma isafe_imp_safeF:
"\<forall> prg s. valid prg s (isafe (domC prg, prg, anF prg, fst s, FalseF, Conj, Impl, safeF, succsF, wpF)) \<longrightarrow> valid prg s (safeF prg (fst s))"
(*<*)
apply (rule allI)+
apply (subgoal_tac "isafe (domC prg, prg, anF prg, (fst s), FalseF, Conj, Impl, safeF, succsF, wpF) =
(if \<not> (fst s) mem domC prg then FalseF
 else Conj ([safeF prg (fst s)]@
       (case anF prg (fst s) of
        None \<Rightarrow> (map (\<lambda>(j, B). Impl B (wpF prg (fst s) j (isafe ([a\<in>domC prg . a \<noteq> (fst s)], prg, anF prg, j, FalseF, Conj, Impl, safeF, succsF, wpF))))
                              (succsF prg (fst s)))
      | Some an_i \<Rightarrow> [an_i])))")
 prefer 2
 apply (rule isafe.simps)
apply (case_tac "(fst s)\<in> set (domC prg)")
apply (simp add: set_mem_eq del: isafe.simps)
apply (case_tac "anF prg (fst s)")
apply (simp del: isafe.simps)
apply (rule impI)
apply (simp add:  valid_def validF_validFs.simps Conj_def)

apply (simp add: valid_def validF_validFs.simps Conj_def)


--{* case: fst s notin set domC prg *}
apply (rule impI)
apply (simp add: set_mem_eq FalseF_def valid_def del: isafe.simps )
(*>*)
done

lemma isafeF_imp_safeF:
"valid prg (p,m,e) (isafeF prg p) \<Longrightarrow> valid prg (p,m,e) (safeF prg p)"
(*<*)
apply (cut_tac isafe_imp_safeF)
apply (erule_tac x="prg" in allE)
apply (erule_tac x="(p,m,e)" in allE)
apply (simp add: isafeF_def)
(*>*)
done

subsection {* Pre Safe States *}

text {* We define the set of so called pre safe states. These
are states that originate from a (previously) safe execution. *}

consts
safeP::"SALprogram \<Rightarrow> SALstate set" 

inductive "safeP prg"
intros
init: "\<lbrakk> valid prg (p,m,e) (initF prg)  \<rbrakk> \<Longrightarrow> (p,m,e) \<in> (safeP prg)"
step: "\<lbrakk> (p,m,e) \<in> (safeP prg);  
        valid prg (p,m,e) (safeF prg p);
        valid prg (p',m',e') (safeF prg p'); 
        ((p,m,e),(p',m',e')) \<in> (effS prg) \<rbrakk> 
 \<Longrightarrow> (p',m',e') \<in> (safeP prg)"

lemma isafeP_imp_safeP:
"(p,m,e) \<in> isafeP prg \<Longrightarrow> (p,m,e) \<in> safeP prg"
(*<*)
apply (simp only: isafeP_def)
apply (erule isafeP'.induct)
apply (simp only: split_paired_all)
apply (rule safeP.init)
apply simp

apply (subgoal_tac "\<exists> p m e. s = (p,m,e)")
 prefer 2
 apply (rule_tac x="fst s" in exI)
 apply (rule_tac x="fst (snd s)" in exI)
 apply (rule_tac x="snd (snd s)" in exI)
 apply simp
apply (subgoal_tac "\<exists> p' m' e'. s' = (p',m',e')")
 prefer 2
 apply (rule_tac x="fst s'" in exI)
 apply (rule_tac x="fst (snd s')" in exI)
 apply (rule_tac x="snd (snd s')" in exI)
 apply simp
apply (erule exE)+
apply (simp only:)

apply (rule_tac p="p" and m="m" and e="e" in safeP.step)
apply assumption
apply (rule  isafeF_imp_safeF)
apply simp
apply (rule  isafeF_imp_safeF)
apply simp

apply simp
(*>*)
done

section {* System Invariants *}

text {* Useful properties about states that
        originate from a safe execution. *}

subsection {* System Invariant 1 *}

consts sysinv::"SALstate \<times> SALprogram \<Rightarrow> bool"

recdef 
  sysinv  "measure (\<lambda> ((pc,m,e),prg). length (cs e))"
  "sysinv ((pc,m,e),prg) = (case (cs e) 
                            of [] \<Rightarrow> False
                            | c#css \<Rightarrow> (let (k,m)=c; (pn',i')=(h e)!k; (pn,i)=pc 
                                        in (case css 
                                            of [] \<Rightarrow> pn=0 \<and> (\<forall> i0 x. cmd prg (0,i0) \<noteq> Some (RET x))
                                            | c'#css' \<Rightarrow> (\<exists> x. cmd prg (pn',i') = Some (CALL x pn)) 
                                                         \<and> k < length (h e) 
                                                         \<and> sysinv (((pn',i'),m,e\<lparr>cs:=css,h:=take k (h e)\<rparr>),prg)
                                           )
                                        )
                            )"
(hints recdef_simp: filterreduction)

lemma sysinv_calltime:
"\<lbrakk> sysinv ((p,m,e),prg) \<rbrakk> \<Longrightarrow> 1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < (length (h e))"
(*<*)
apply (case_tac "cs e")
apply simp
apply (case_tac "list")
apply simp
apply (simp add: sysinv.simps Let_def split_def fst_conv snd_conv)
(*>*)
done

theorem sysinv_pres:
"\<And> prg p m e. \<lbrakk> wf prg ; (p,m,e) \<in> (safeP prg) \<rbrakk> \<Longrightarrow> sysinv((p,m,e),prg)"
(*<*)
apply (rule safeP.induct)
apply simp
apply (simp add: initF_def valid_def validF_validFs.simps Let_def split_def fst_conv snd_conv)
apply (case_tac "cs ea")
apply simp
apply (case_tac "list")
apply (simp add: Let_def wf_def)
apply (rule allI)+
apply (case_tac "cmd prg (0,i0)")
apply simp
apply (cut_tac "cmd_domC")
apply (erule_tac x="aa" in allE)
apply (erule_tac x="(0,i0)" in allE)
apply (erule_tac x="prg" in allE)
apply (drule mp, assumption)
apply (drule set_list_split)
apply (erule exE)+
apply (simp add: checkPos_split add: Let_def)
apply (case_tac "aa = RET x")
apply simp
apply simp

--{* case: list = aa lista *}
apply (simp add: Let_def incA_def split_def)

--{* INDUCTION CASE *}
apply (case_tac "cmd prg pa")
apply (simp add: effS_def step_def split_def Let_def)

apply (case_tac "cs ea")
apply simp

--{* induction case *}
apply (rename_tac "prg" "p" "m" "e" "e'" "e''" "m'" "m''" "p'" "p''" "a" "aa" "css")
apply (rule ssubst[OF sysinv.simps])
apply (simp add: effS_def mem_Collect_eq del: sysinv.simps)
apply (case_tac a)
--{* SET nat1 nat2 *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "cs e'")
apply simp
--{* cs e = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (case_tac css)
apply simp
--{* css = ac  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* ADD nat1 nat2 *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "cs e'")
apply simp
--{* cs e = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (case_tac css)
apply simp
--{* css = ac  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* SUB *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "cs e'")
apply simp
--{* cs e = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (case_tac css)
apply simp
--{* css = ac  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* INC *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "cs e'")
apply simp
--{* cs e = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (case_tac css)
apply simp
--{* css = ac  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* JMPEQ nat1 nat2 nat3 *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (case_tac "(\<exists>n. m' nat1 = NAT n) \<and> (\<exists>n'. m' nat2 = NAT n')")
apply simp
apply (case_tac "\<exists>n. m' nat1 = NAT n \<and> m' nat2 = NAT n")
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "css")
apply (simp add: Let_def split_def)

--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)

apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "css")
apply (simp add: Let_def split_def)

--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)

apply simp
--{* JMPL *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (case_tac "(\<exists>n. m' nat1 = NAT n) \<and> (\<exists>n'. m' nat2 = NAT n')")
apply simp
apply (case_tac "\<exists>n. m' nat1 = NAT n \<and> (\<exists>n'. m' nat2 = NAT n' \<and> n < n')")
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "css")
apply (simp add: Let_def split_def)

--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)

apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "css")
apply (simp add: Let_def split_def)

--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)

apply simp
--{* JLE nat1 nat2 nat3 *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (case_tac "(\<exists>n. m' nat1 = NAT n) \<and> (\<exists>n'. m' nat2 = NAT n')")
apply simp
apply (case_tac "\<exists>n. m' nat1 = NAT n \<and> (\<exists>n'. m' nat2 = NAT n' \<and> n \<le> n')")
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "css")
apply (simp add: Let_def split_def)

--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)

apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "css")
apply (simp add: Let_def split_def)

--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)

apply simp
--{* JMPB nat *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "cs e'")
apply simp
--{* cs e = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (case_tac css)
apply simp
--{* css = ac  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* JMPI nat *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (case_tac "m' nat")
apply (simp add: safeF_def)
prefer 2
apply (simp add: safeF_def)
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)

apply (case_tac "cs e'")
apply simp
--{* cs e = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (case_tac css)
apply simp
--{* css = ac  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* CALL *}
apply (simp add: step_def  Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv nth_append)
apply (case_tac "css")
apply (simp add: nth_append)
--{* css = ab  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp rec_upd_simp2 rec_upd_simp3 del: sysinv.simps)

--{* RET nat *}
apply (case_tac "m' nat")
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (simp only: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv option.cases instr.cases tval.cases simp_thms option.simps Pair_eq)
apply (drule_tac P="\<lambda> x. x" in subst[OF sysinv.simps])


apply (case_tac "css")
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (erule conjE)+
apply (erule_tac x="snd p'" in allE)
apply (erule_tac x="nat" in allE)
apply (subgoal_tac "(0,snd p') = p'")
 prefer 2
 apply (rule_tac P="\<lambda> t. (t,snd p') = p'" and t="0" and s="fst p'" in subst)
 apply assumption
 apply (simp (no_asm))
apply simp

--{* case : css = ab list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps validF_validFs.simps)
apply (erule conjE | erule exE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: validF_validFs.simps sysinv.simps)

apply (case_tac "list")
apply (simp add: callpc_def Let_def  callstate_def split_def incA_def)

apply (simp add: Let_def split_def fst_conv snd_conv del: validF_validFs.simps sysinv.simps)
apply (drule_tac P="\<lambda> x. x" in subst[OF sysinv.simps])
apply (simp add: Let_def split_def nth_append rec_upd_simp rec_upd_simp2 rec_upd_simp3 min_elim fst_conv snd_conv del: sysinv.simps)
apply (erule conjE |erule exE)+
apply (subgoal_tac "take (fst aa) (h e') ! fst ab = h e' ! fst ab")
 prefer 2
 apply (simp)
apply (subgoal_tac "min (fst ab) (fst aa) = fst ab")
 prefer 2
 apply (simp add: min_def)
apply (subgoal_tac "fst ab - length (h e') = 0")
 prefer 2
 apply simp
apply (simp only: take.simps nat.cases simp_thms append_Nil2)
apply (rule conjI)
apply (rule_tac x="xb" in exI)
apply (simp add: incA_def Let_def split_def fst_conv snd_conv  callpc_def callstate_def)

apply simp

--{* MOV nat1 nat2 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv  del: sysinv.simps)
apply (erule conjE)+
apply (case_tac "m' nat1")
apply simp
prefer 2
apply simp
apply (case_tac "m' nat2")
apply simp
prefer 2
apply simp
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (drule_tac t="p''" in sym)
apply (case_tac "css")
apply (simp add: Let_def split_def)
--{* css = ab  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv.simps)
--{* HALT *}
apply (simp add: step_def Let_def split_def)
(*>*)
done

lemma sysinv_pres':
"\<And> prg s. \<lbrakk> wf prg; s \<in> isafeP prg \<rbrakk> \<Longrightarrow> sysinv (s,prg)"
(*<*)
apply (simp only: split_paired_all)
apply (drule isafeP_imp_safeP)
apply (rule sysinv_pres)
apply assumption+
(*>*)
done


subsection {* System Invariant 2 *}

consts sysinv2::"SALstate \<times> SALprogram \<Rightarrow> bool"

recdef 
  sysinv2  "measure (\<lambda> ((pc,m,e),prg). length (cs e))"
  "sysinv2 ((pc,m,e),prg) = (case (cs e) 
                            of [] \<Rightarrow> False
                            | c#css \<Rightarrow> (let (k,m'')=c; (pn',i')=(h e)!k
                                        in ( case css
                                              of [] \<Rightarrow> True
                                              | c'#css' \<Rightarrow> (k < length (h e) \<and>                                                                                valid prg ((pn',i'),m'',e\<lparr> cs:=css, h:=take k (h e) \<rparr>) (isafeF prg (pn',i')) \<and>
                                               sysinv2 (((pn',i'),m'',e\<lparr> cs:=css, h:=take k (h e) \<rparr>),prg)
                                           ) 
                                         )
                              ))"
(hints recdef_simp: filterreduction)

lemma sysinv2_pres:
"\<forall> prg s.  wf prg \<longrightarrow> s \<in> (isafeP prg) \<longrightarrow> sysinv2 (s,prg)"
(*<*)
apply (rule allI)+
apply (simp only: split_paired_all)
apply (rename_tac "prg" "pn" "i" "m" "e")
apply (rule impI)
apply (rule impI)
apply (erule isafeP_induct)
--{* base case *}
apply (simp only: split_paired_all)
apply (rename_tac "prg" "pn_" "i_" "m_" "e_" "pn" "i" "m" "e")

apply (simp only: valid_def validF_validFs.simps initF_def Let_def split_def fst_conv snd_conv simp_thms eval.simps Pair_eq tval.simps del: sysinv2.simps) 
apply (erule allE)
apply (erule conjE)
apply (case_tac "cs e")
apply simp
apply simp
apply (case_tac "list")
apply (simp add: Let_def)
apply (simp add: incA_def split_def)
--{* induction step *}
apply (subgoal_tac "valid prg s (safeF prg (fst s))")
 prefer 2
 apply (simp only: split_paired_all)
 apply simp
 apply (drule isafeF_imp_safeF)
 apply assumption
apply (subgoal_tac "s' \<in> (isafeP prg)")
 prefer 2
 apply (rule isafeP_step)
 apply simp+
apply (simp add: effS_def mem_Collect_eq)
apply (simp only: split_paired_all)
apply (rename_tac "prg" "pn" "i" "m" "e" "pn'" "i'" "m''" "e''")
apply (case_tac "cmd prg (pn,i)")
apply (simp add: step_def)
--{* case: cmd prg (pn,i) = Some a *}
apply (case_tac a)
--{* SET nat1 nat2 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* ADD nat1 nat2 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* SUB nat1 nat2 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* INC nat *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* JMPEQ nat1 nat2 nat3 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (erule conjE | erule exE)+
apply (subgoal_tac "\<exists> n. m nat1 = NAT n")
 prefer 2
 apply (case_tac "m nat1")
 apply simp
 apply simp
 apply simp
apply (erule exE)
apply (subgoal_tac "\<exists> na. m nat2 = NAT na")
 prefer 2
 apply (case_tac "m nat2")
 apply simp
 apply simp
 apply simp
apply (erule exE)
apply (case_tac "n=na")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* case: n ~= na *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* JMPL nat1 nat2 nat3 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (erule conjE | erule exE)+
apply (subgoal_tac "\<exists> n. m nat1 = NAT n")
 prefer 2
 apply (case_tac "m nat1")
 apply simp
 apply simp
 apply simp
apply (erule exE)
apply (subgoal_tac "\<exists> na. m nat2 = NAT na")
 prefer 2
 apply (case_tac "m nat2")
 apply simp
 apply simp
 apply simp
apply (erule exE)
apply (case_tac "n < na")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* case not n < na *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* JLE nat1 nat2 nat3 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (erule conjE | erule exE)+
apply (subgoal_tac "\<exists> n. m nat1 = NAT n")
 prefer 2
 apply (case_tac "m nat1")
 apply simp
 apply simp
 apply simp
apply (erule exE)
apply (subgoal_tac "\<exists> na. m nat2 = NAT na")
 prefer 2
 apply (case_tac "m nat2")
 apply simp
 apply simp
 apply simp
apply (erule exE)
apply (case_tac "n \<le>  na")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* case not n <= na *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* JMPB nat *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* JMPI nat *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (case_tac "m nat")
apply simp
prefer 2
apply simp
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* CALL nat1 nat2 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp)
apply (subgoal_tac "e\<lparr>h := h e @ [(pn, i)], cs := [(length (h e), m), aa], cs := [aa], h := h e\<rparr> = e")
 prefer 2
 apply simp
apply (simp only: valid_def)
--{* case: list = ab  lista *}
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
apply (rule ssubst[OF sysinv2.simps])
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
apply (subgoal_tac "e\<lparr>h := h e @ [(pn, i)], cs := (length (h e), m) # aa # ab # lista, cs := aa # ab # lista, h:= h e\<rparr> = e")
 prefer 2
 apply simp
apply (simp only: valid_def)
apply simp
--{* RET nat *}
apply (frule_tac "sysinv_pres'")
apply assumption
apply (case_tac "m nat")
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv  del: sysinv2.simps)
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv  del: sysinv2.simps)
apply (simp only: validF_validFs.simps eval.simps step_def safeF_def valid_def Let_def split_def fst_conv snd_conv option.cases instr.cases tval.cases simp_thms option.simps Pair_eq)
apply (drule_tac P="\<lambda> x. x" in subst[OF sysinv2.simps])
apply (case_tac "cs e")
apply simp
apply (case_tac "list")
apply (simp add: Let_def)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps validF_validFs.simps)
apply (erule conjE | erule exE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def incA_def callpc_def callstate_def fst_conv snd_conv del: validF_validFs.simps sysinv.simps)

apply (case_tac "lista")
apply (simp add: callpc_def Let_def  callstate_def split_def incA_def)

apply (simp add: Let_def split_def nth_append rec_upd_simp rec_upd_simp2 rec_upd_simp3 min_elim fst_conv snd_conv del: validF_validFs.simps sysinv2.simps)
apply (erule conjE |erule exE)+
apply (subgoal_tac "take (fst aa) (h e) ! fst ab = h e ! fst ab")
 prefer 2
 apply (simp)
apply (subgoal_tac "min (fst ab) (fst aa) = fst ab")
 prefer 2
 apply (simp add: min_def)
apply (subgoal_tac "fst ab - length (h e) = 0")
 prefer 2
 apply simp
apply (simp only: take.simps nat.cases simp_thms append_Nil2)
--{* MOV nat1 nat2 *}
apply (simp add: step_def safeF_def valid_def Let_def split_def fst_conv snd_conv )
apply (erule conjE)+
apply (case_tac "m nat1")
apply simp
prefer 2
apply simp 
--{* m nat1 = NAT nat *}
apply simp
apply (case_tac "m nat2")
apply simp
prefer 2
apply simp
--{* m nat2 = NAT nata *}
apply simp
apply (erule conjE)+
apply (drule_tac t="e''" in sym)
apply (drule_tac t="m''" in sym)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "cs e")
apply simp
--{* cs e = aa  list *}
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (simp add: Let_def split_def fst_conv snd_conv del: sysinv2.simps)
apply (erule conjE)+
apply (simp add: Let_def split_def fst_conv snd_conv nth_append rec_upd_simp del: sysinv2.simps)
--{* HALT *}
apply (simp add: step_def)
(*>*)
done

lemma ex_weak: "\<exists> n n'. a = NAT n \<and> b = NAT n' \<and> n = n' \<Longrightarrow> \<exists> n n'. a = NAT n \<and> b = NAT n'"
apply auto
done

lemma ex_eq: "(\<exists>n. m nat1 = NAT n) \<and> (\<exists>n'. m nat2 = NAT n') \<Longrightarrow> \<not> (\<exists>n. m nat1 = NAT n \<and> m nat2 = NAT n) \<Longrightarrow> (\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n' \<and> n \<noteq> n')"
apply auto
done

lemma ex_less: "(\<exists>n. m nat1 = NAT n) \<and> (\<exists>n'. m nat2 = NAT n') \<Longrightarrow> \<not> (\<exists>n. m nat1 = NAT n \<and> (\<exists>n'. m nat2 = NAT n' \<and> n < n')) \<Longrightarrow> \<exists>n. m nat1 = NAT n \<and> (\<exists>n'. m nat2 = NAT n' \<and> \<not> n < n')"
apply auto
done

lemma list_length_nth:
"(la@[i,j])!(length la)=i"
(*<*)
apply (induct_tac la)
apply simp
apply simp
(*>*)
done

lemma list_length_nth2:
"(la@[i])!(length la)=i"
(*<*)
apply (induct_tac la)
apply simp
apply simp
(*>*)
done

lemma list_length_suc_nth:
"(la@[i,j])!(Suc (length la))=j"
(*<*)
apply (induct_tac la)
apply simp
apply simp
(*>*)
done


lemma path_succsF:
"\<lbrakk> l \<in> paths prg succsF; k+1<length l \<rbrakk> \<Longrightarrow> \<exists> B. (l!(k+1),B) \<in> set (succsF prg (l!k))"
(*<*)
apply (rotate_tac 1)
apply (erule rev_mp)
apply (rule_tac  prg="prg" and succsF'="succsF" in paths.induct)
apply assumption
apply simp
apply (rule impI)
apply (rule_tac x="B" in exI)
apply assumption
apply (case_tac "k= length (la)")
apply simp
apply (rule_tac x="B" in exI)
apply (rename_tac "pc''")
apply (subgoal_tac "(la@[pc,pc''])!(Suc (length la)) = pc''")
 prefer 2
 apply (rule list_length_suc_nth)
apply (subgoal_tac "(la@[pc,pc''])!(length la) = pc")
 prefer 2
 apply (rule list_length_nth)
apply simp
apply (rule impI)
apply (simp (no_asm) only: nth_append)
apply (case_tac "k + 1 = length la")
apply (simp add: list_length_nth2)
apply (simp add: nth_append)
apply (subgoal_tac "k + 1 < length (la @ [pc])")
apply simp
apply (simp only: nth_append)
apply simp
apply (subgoal_tac "k + 1 \<noteq> length (la @ [pc])")
apply simp
apply simp
(*>*)
done

lemma less_chain_simp:
"\<lbrakk> \<forall> k. length l <= k+1 \<or> l!k < l!(k+1); 1 < length (l::pos  list) \<rbrakk> \<Longrightarrow> hd l < last l"
(*<*)
apply (erule rev_mp)
apply (erule rev_mp)
apply (induct l)
apply simp
apply (case_tac list)
apply simp
apply (case_tac lista)
apply simp
apply (rule impI)
apply (erule_tac x="0" in allE)
apply simp
apply (rule impI)
apply (rule impI)
apply hypsubst
apply simp
apply (rule conjI)
apply (rule impI)
apply simp
apply (frule_tac x="0" and P="\<lambda> k. Suc (Suc 0) <= k \<or> (?Q k)" in spec)
apply simp
apply (frule_tac x="1" and P="\<lambda> k. Suc (Suc 0) <= k \<or> (?Q k)" in spec)
apply simp
apply (erule order_less_trans, assumption)
apply (rule impI)
apply simp
apply (frule_tac x="0" and P="\<lambda> k. Suc (Suc (length listb)) <= k \<or> (?Q k)" in spec)
apply simp
apply (frule_tac x="1" and P="\<lambda> k. Suc (Suc (length listb)) <= k \<or> (?Q k)" in spec)
apply simp
apply (frule_tac x="0" in spec)
apply (subgoal_tac "\<forall> k. Suc (length listb) <= k \<or> ((aa#ab#listb)!k < (ab#listb)!k)")
apply (drule mp)
apply assumption
apply simp
apply (erule order_less_trans, assumption)
apply (rule allI)
apply (case_tac k)
apply simp
apply (case_tac listb)
apply simp
apply (case_tac nat)
apply simp
apply (frule_tac x="2" and P="\<lambda> k. Suc (Suc (Suc (length list))) <= k \<or> (?Q k)" in spec)
apply simp
apply simp
apply (frule_tac x="Suc (Suc (Suc nata))" and P="\<lambda> k. Suc (Suc (Suc (length list))) <= k \<or> (?Q k)" in spec)
apply simp
(*>*)
done

lemma path_length:
"\<lbrakk> l \<in> paths prg succsF \<rbrakk> \<Longrightarrow> 1 < length l"
(*<*)
apply (rule_tac prg="prg" and succsF'="succsF" in paths.induct)
apply assumption
apply simp
apply simp
(*>*)
done

lemma loop_has_back_jump:
"\<lbrakk> l \<in> paths prg succsF; hd l = last l \<rbrakk> \<Longrightarrow> \<exists> k. (k+1)<length l \<and> l!(k+1) <= l!k"
(*<*)
apply (frule path_length)
apply (rule classical)
apply (simp only: not_ex)
apply (simp only: de_Morgan_conj)
apply (simp only: linorder_not_less)
apply (subgoal_tac "\<forall>k. length ?l \<le> k + 1 \<or> ?l ! k < ?l ! (k + 1)")
apply (drule less_chain_simp)
apply assumption
apply simp
apply (rule allI)
apply (erule_tac x="k" in allE)
apply (subgoal_tac "(\<not> l ! (k+1) <= l ! k) = (l!k < l!(k+1))")
apply simp
apply (rule_tac x="l!(k+1)" and y="l!k" in linorder_not_le)
(*>*)
done


lemma back_jumps_annotated:
" wf prg  \<Longrightarrow> \<forall> pc'' pc B. (pc'',B) \<in> set (succsF prg pc) \<longrightarrow> pc''<=pc \<longrightarrow> ((anF prg pc'') \<noteq> None \<or> (anF prg pc \<noteq> None))"
(*<*)
apply (rule allI)+
apply (simp only: split_paired_all)
apply (rename_tac "pn'" "i'" "pn" "i" "B")
apply (rule impI)+
apply (subgoal_tac "\<exists> ins. cmd prg (pn,i) = Some ins")
apply (erule exE)
apply (simp only: wf_def)
apply (frule domC_split)
apply (erule exE)+
apply (simp only: checkPos_split)
apply (erule conjE)+
apply (simp add: checkPos_split Let_def split_def fst_conv snd_conv option.cases succsF_def)
apply (case_tac ins)
--{* SET nat1 nat2 *}
apply simp
apply (erule leq_pairE)
apply simp
apply simp
--{* ADD nat1 nat2 *}
apply simp
apply (erule leq_pairE)
apply simp
apply simp
--{* SUB nat1 nat2 *}
apply simp
apply (erule leq_pairE)
apply simp
apply simp
--{* INC nat *}
apply simp
apply (erule leq_pairE)
apply simp
apply simp
--{* JMPEQ nat1 nat2 nat3 *}
apply simp
apply (case_tac "i'=Suc i")
apply simp
apply (erule leq_pairE)
apply simp
apply simp
apply (case_tac "nat3 = 0")
apply simp
apply (erule conjE)+
apply (case_tac "\<exists>y. anF prg (pn, i) = Some y")
apply assumption
apply simp
apply simp
apply (erule conjE)+
apply (erule leq_pairE)
apply simp
apply simp
--{* JMPL nat1 nat2 nat3 *}
apply simp
apply (case_tac "i'=Suc i")
apply simp
apply (erule leq_pairE)
apply simp
apply simp
apply (case_tac "nat3 = 0")
apply simp
apply (erule conjE)+
apply (case_tac "\<exists>y. anF prg (pn, i) = Some y")
apply assumption
apply simp
apply simp
apply (erule conjE)+
apply (erule leq_pairE)
apply simp
apply simp
--{* JLE nat1 nat2 nat3 *}
apply simp
apply (case_tac "i'=Suc i")
apply simp
apply (erule leq_pairE)
apply simp
apply simp
apply (case_tac "nat3 = 0")
apply simp
apply (erule conjE)+
apply (case_tac "\<exists>y. anF prg (pn, i) = Some y")
apply assumption
apply simp
apply simp
apply (erule conjE)+
apply (erule leq_pairE)
apply simp
apply simp
--{* JMPB nat *}
apply simp
apply (case_tac "\<exists>y. anF prg (pn, i - nat) = Some y")
apply simp
apply simp
--{* JMPI nat *}
apply simp
apply (case_tac "\<exists>y. anF prg (pn, i) = Some y")
apply simp
apply simp
--{* CALL nat 1 nat2 *}
apply simp
apply (case_tac "\<exists>y. anF prg (nat2, 0) = Some y")
apply simp
apply simp
--{* RET nat *}
apply simp
apply (drule set_list_split)
apply (erule exE)+
apply (case_tac "list_all (\<lambda>(pc, B). \<exists>y. anF prg pc = Some y) (ret_succs prg (pn,i)  nat (callpoints prg pn))")
apply simp
apply (simp only: if_not_P if_False)

--{* MOV nat1 nat2 *}
apply simp
apply (erule leq_pairE)
apply simp
apply simp
--{* HALT *}
apply simp

apply (case_tac "cmd prg (pn,i)")
apply (simp add: succsF_def Let_def option.cases)
apply simp

(*>*)
done


lemma isafeP_isafeF_initF:
"s \<in> (isafeP prg) \<Longrightarrow>  valid prg s (initF prg) \<or> valid prg s (isafeF prg (fst s))"
apply (erule isafeP_elims)
apply simp+
done


lemma lookup_changedvars:
"mp ? (V v) = Some e \<Longrightarrow> (changedvars mp) ? v = Some e"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (case_tac "fst a")
apply simp
apply (case_tac "nat = v")
apply simp
apply simp
apply simp+
(*>*)
done

lemma lookup_changedvars_neg:
"mp ? (V v) = None \<Longrightarrow> (changedvars mp) ? v = None"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (case_tac "fst a")
apply simp
apply (case_tac "nat = v")
apply simp
apply simp
apply simp+
(*<*)
done


lemma nojunk_changedvars:
"nojunk mp \<Longrightarrow> nojunk (changedvars mp)"
(*<*)
apply (induct mp)
apply simp

apply simp
apply (case_tac "list ? (fst a)")
prefer 2
apply simp

apply simp
apply (case_tac "fst a")
apply simp
apply (case_tac "changedvars list ? nat")
apply simp

apply (drule lookup_changedvars_neg)
apply simp

apply simp+
(*>*)
done

lemma changedvars_ran:
"\<lbrakk> nojunk em; x \<in> set (ran (changedvars em)) \<rbrakk> \<Longrightarrow> x \<in> set (ran (em))"
(*<*)
apply (erule rev_mp)+
apply (induct_tac em)
apply (simp add: ran_def dom_def)
apply (rule impI)+
apply (frule nojunk_range)
apply (simp del: ran_def nojunk.simps)
apply (subgoal_tac "nojunk list")
 prefer 2
 apply simp
 apply (case_tac "list ? (fst a)")
 apply simp
 apply simp
apply (case_tac "fst a")
apply (simp del: nojunk.simps)
apply (drule nojunk_changedvars)
apply (drule_tac mp="changedvars (a # list)" in nojunk_range)
apply simp
apply (erule disjE)
apply simp
apply simp

apply simp+
(*>*)
done

lemma changedvars_map:
"changedvars (map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) em) = (map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) (changedvars em))"   
(*<*)
apply (induct em)
apply simp
apply (simp only: map.simps changedvars.simps)
apply (simp only: split_paired_all)
apply simp
apply (case_tac a)
apply simp+
(*>*)
done


lemma changedvars_append:
"changedvars (mp@mp') = (changedvars mp) @ (changedvars mp')"
(*<*)
apply (induct mp)
apply simp

apply simp
(*>*)
done

lemma lookup_evalmap_None:
"em ? x = None \<Longrightarrow> map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) em ? x = None"
(*<*)
apply (induct em)
apply simp
apply (simp add: Let_def split_paired_all split_def fst_conv snd_conv)
apply (case_tac "a = x")
apply simp
apply simp
(*>*)
done

lemma lookup_evalmap_Some:
"em ? x = Some x' \<Longrightarrow> map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) em ? x = Some (C (eval I (p,m,e) x'))"
(*<*)
apply (induct em)
apply simp
apply (simp add: Let_def split_paired_all split_def fst_conv snd_conv)
apply (case_tac "a = x")
apply simp
apply simp
(*>*)
done

lemma foldl_induct:
"\<And> r r' g g' f. \<lbrakk> P r = Q r'; (P r = Q r') \<longrightarrow> (P g = Q g'); (P g = Q g') \<longrightarrow> (\<forall> a\<in> set L. \<forall> x y. P x = Q y \<longrightarrow> P (f g x a) = Q (f g' y a)) \<rbrakk> \<Longrightarrow> P (foldl (f g) r L) = Q (foldl (f g') r' L)"
(*<*)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (induct L)
apply simp

apply (rule allI)+
apply (rule impI)+
apply simp
(*>*)
done

lemma foldl_induct2:
"\<And> r r' g g' f L L'. \<lbrakk> P r = Q r'; (P r = Q r') \<longrightarrow> (P g = Q g'); L = map fst G ; L' = map snd G; (P g = Q g') \<longrightarrow> L = map fst G \<longrightarrow> L' = map snd G \<longrightarrow> (\<forall> i. i < length L \<longrightarrow> (\<forall> x y. P x = Q y \<longrightarrow> P (f g x (L ! i)) = Q (f g' y (L' ! i)))) \<rbrakk> \<Longrightarrow> P (foldl (f g) r L) = Q (foldl (f g') r' L')"
(*<*)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (induct G)
apply simp

apply (rule allI)+
apply (rule impI)+
apply simp
apply (erule_tac x="f g r (fst a)" in allE)
apply (erule_tac x="f g' r' (snd a)" in allE)
apply (erule_tac x="g" in allE)
apply (erule_tac x="g'" in allE)
apply (erule_tac x="f" in allE)
apply simp
apply (subgoal_tac "(\<forall>i<length list. \<forall>x y. P x = Q y \<longrightarrow> P (f g x (fst (list ! i))) = Q (f g' y (snd (list ! i))))")
 prefer 2
 apply (rule allI)
 apply (rule impI)
 apply (erule_tac x="Suc i" in allE)
 apply simp
apply (drule mp, assumption)
apply (erule_tac x="0" in allE)
apply simp
(*>*)
done

lemma zip_fst:
"\<And> L'. length L = length L' \<Longrightarrow> L = map fst (zip L L')"
(*<*)
apply (induct L)
apply simp

apply simp
apply atomize
apply (case_tac "L'")
apply simp
apply (erule_tac x="lista" in allE)
apply simp
done
(*>*)

lemma zip_snd:
"\<And> L. length L = length L' \<Longrightarrow> L' = map snd (zip L L')"
(*<*)
apply (induct L')
apply simp

apply simp
apply atomize
apply (case_tac "L")
apply simp
apply (erule_tac x="lista" in allE)
apply simp
done
(*>*)

lemma foldl_induct2':
"\<And> r r' g g' f L L'. \<lbrakk> P r = Q r'; (P r = Q r') \<longrightarrow> (P g = Q g'); length L = length L'; (P g = Q g') \<longrightarrow> (length L = length L') \<longrightarrow> (\<forall> i. i < length L \<longrightarrow> (\<forall> x y. P x = Q y \<longrightarrow> P (f g x (L ! i)) = Q (f g' y (L' ! i)))) \<rbrakk> \<Longrightarrow> P (foldl (f g) r L) = Q (foldl (f g') r' L')"
(*<*)
apply (rule_tac G="zip L L'" in foldl_induct2)
apply simp+
apply (erule_tac P="length L = length L'" in rev_mp)
apply (induct_tac L)
apply simp
apply (case_tac "L'")
apply simp
apply simp

apply (rule impI, rule zip_fst, assumption)

apply (rule zip_snd, assumption)
apply simp
done
(*>*)

lemma list_split_at_i:
"\<And> L. i < length L \<Longrightarrow> \<exists> as a as'. L=as@a#as' \<and> length as = i"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct i)
apply simp
apply (rule allI)
apply (rule impI)
apply (simp add: neq_Nil_conv)
apply (rule allI)
apply (rule impI)
apply (case_tac "n = length L")
apply simp
apply (subgoal_tac "n < length L")
 prefer 2
 apply simp
apply (erule_tac x="L" in allE)
apply simp
apply (erule exE | erule conjE)+
apply (case_tac "as'")
apply simp
apply (rule_tac x="as@[a]" in exI)
apply simp
(*>*)
done


lemma substE_eval:
"eval I (p,m,e) (substE NoPt em ex) = eval I (p,m,e) (substE NoPt (map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) em) ex)"
(*<*)
apply (induct ex)
--{* subgoal: V nat *}
apply (simp add: mode.cases)
apply (simp add: id_lookup_def)
apply (case_tac "em ? (V nat)")
apply (simp add: Let_def lookup_map_None)

apply (simp add: Let_def lookup_map_Some)
--{* subgoal: Lv v *}
apply simp
--{* subgoal: C tval *}
apply (simp add: id_lookup_def)
--{* subgoal: Pc *}
apply (simp add: id_lookup_def)
apply (case_tac "em ? Pc")
apply (simp add: lookup_evalmap_None)
apply (simp add: lookup_evalmap_Some)
--{* subgoal: Rp *}
apply (simp add: id_lookup_def)
apply (case_tac "em ? Rp")
apply (simp add: lookup_evalmap_None)
apply (simp add: lookup_evalmap_Some)
--{* subgoal: Tm *}
apply (simp add: id_lookup_def)
apply (case_tac "em ? Tm")
apply (simp add: lookup_evalmap_None)
apply (simp add: lookup_evalmap_Some)
--{* subgoal: Add expr1 expr2*}
apply simp
--{* subgoal: Sub expr1 expr2) *}
apply simp
--{* subgoal: Mult expr1 expr2) *}
apply simp
--{* subgoal: Deref expr *}
apply (simp add: mode.cases Let_def)
apply (simp only: changedvars_map)
apply (rule_tac L="changedvars em" and L'="(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) (changedvars em))" in  foldl_induct2')
apply simp
apply simp
apply simp
apply simp
apply (rule allI)
apply (rule impI)
apply (drule list_split_at_i)
apply (erule exE | erule conjE)+
apply (simp add: nth_append)
apply (rule allI)+
apply (rule impI)+
apply (simp add: split_def fst_conv snd_conv)
apply (case_tac "eval I (p, m, e) (substE NoPt (map (\<lambda>u. (fst u, C (eval I (p, m, e) (snd u)))) em) expr) = NAT (fst a)")
apply simp
apply simp

--{* subgoal: Ifeq *}
apply simp
apply (case_tac "eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr1) =
                eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr2)")
apply simp
apply simp
--{* subgoal: Old *}
apply simp
(*>*)
done


lemma substE_var_simp: 
"\<And> I p m e rm em v tv. \<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv'); nojunk ((V v,C tv)#em) \<rbrakk> \<Longrightarrow>  
eval I (p,m,e) (substE NoPt ((V v,C tv)#em) ex) = (eval I (p,m[v::=tv],e) (substE NoPt em ex))"
(*<*)
apply (erule rev_mp)+
apply (induct ex)

--{* subgoal 1: ex = V nat *}
apply (rule impI)+
apply (simp add: id_lookup_def)
apply (case_tac "v = nat")
apply (simp add: del_lookup_eq Let_def update_def)
apply (case_tac "em ? (V nat)")
apply (simp add: Let_def)

apply simp

--{* v ~= nat *}
apply simp
apply (case_tac "em ? (V nat)")
apply (simp add: Let_def update_def)

apply (erule_tac x="a" in ballE)
apply (erule exE)
apply (simp add: eval.simps)

apply (drule_tac mp="em" and a="V nat" in some_lookup_range)
apply simp
--{* ex = Lv nat *}
apply simp
--{* ex = C tval *}
apply (rule impI)+
apply simp
--{* ex = Pc *}
apply (rule impI)+
apply (simp add: id_lookup_def)
apply (case_tac "em ? Pc")
apply (simp add: Let_def)

apply (simp add: Let_def update_def)
apply (subgoal_tac "\<exists> tv'. a = C tv'")
 prefer 2
 apply (erule_tac x="a" in ballE)
 apply assumption
 apply (drule some_lookup_range)
 apply simp
apply (erule exE)
apply simp

--{* ex = Rp *}
apply (rule impI)+
apply (simp add: id_lookup_def)
apply (case_tac "em ? Rp")
apply (simp add: Let_def)

apply (simp add: Let_def update_def)
apply (subgoal_tac "\<exists> tv'. a = C tv'")
 prefer 2
 apply (erule_tac x="a" in ballE)
 apply assumption
 apply (drule some_lookup_range)
 apply simp
apply (erule exE)
apply simp

--{* subgoal: Tm *}
apply (rule impI)+
apply (simp add: id_lookup_def)
apply (case_tac "em ? Tm")
apply (simp add: Let_def)

apply (simp add: Let_def update_def)
apply (subgoal_tac "\<exists> tv'. a = C tv'")
 prefer 2
 apply (erule_tac x="a" in ballE)
 apply assumption
 apply (drule some_lookup_range)
 apply simp
apply (erule exE)
apply simp

--{* subgoal: Add expr1 expr2 *}
apply simp
--{* subgoal: Sub expr1 expr2 *}
apply simp
--{* subgoal: Muld expr1 expr2 *}
apply simp
--{* subgoal: Deref expr *}
apply atomize
apply (rule impI)+
apply (simp add: substE.simps Let_def)
apply (rule_tac L="changedvars em" in  foldl_induct)
apply simp
apply (case_tac "eval I (p, m[v ::= tv], e) (substE NoPt em expr)")
apply simp
apply simp
apply (case_tac "nat = v")
apply (simp add: Let_def update_def)

apply (simp add: Let_def update_def)

apply simp

apply simp

apply simp

apply (rule ballI)
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "nojunk em")
 prefer 2
 apply (case_tac "em ? V v" )
 apply simp
 apply simp
apply (frule nojunk_changedvars)
apply (drule_tac mp="changedvars em" in set_lookup)
apply simp
apply (drule some_lookup_range)
apply (drule changedvars_ran)
apply simp
apply (erule_tac x="em" in allE)
apply simp
apply (erule_tac x="v" in allE)
apply simp
apply (erule_tac x="tv" in allE)
apply (erule_tac x="snd a" in ballE)
apply (erule exE)
apply (simp add: split_def )
apply (case_tac "eval I (p, m[v ::= tv], e) (substE NoPt em expr) = NAT (fst a)")
apply simp

apply simp

apply simp

--{* subgoal: Ifeq *}
apply (rule impI)+
apply simp
apply (case_tac "eval I (p, m[v ::= tv], e) (substE NoPt em expr1) = eval I (p, m[v ::= tv], e) (substE NoPt em expr2)")
apply simp
apply simp
--{* subgoal: Old expr *}
apply (simp add: split_paired_all Let_def)
(*>*)
done

subsection {* Substituting Pc in Expressions *}

lemma substE_Pc:
"\<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv') ; nojunk ((Pc,C (POS p2))#em) \<rbrakk> \<Longrightarrow> 
eval I (p,m,e) (substE md ((Pc,C (POS p2))#em) ex) = eval I (p2,m,e) (substE md em ex)"
(*<*)
apply (induct ex)
--{* ex = V nat *}
apply (simp add: eval.simps substE.simps)
apply (subgoal_tac "V nat \<noteq> Pc")
 prefer 2
 apply simp
apply (frule_tac as="em" and a="Pc" and b="C (POS p2)" in id_lookup_red)
apply (simp only: ) 
apply (case_tac md)
--{* md = NoPt *}
apply (case_tac "em ? (V nat)")
apply (simp add: id_lookup_def Let_def)

apply (erule_tac x="a" in ballE)
apply (erule exE)
apply (simp add: id_lookup_def)

apply (drule some_lookup_range)
apply simp
--{* md = Mv nat1 nat2 *}
apply (simp add: Let_def)
apply (case_tac "m nat2 = NAT nat")
apply (simp add: Let_def)
apply (case_tac "m nat1")
apply simp

apply (simp add: Let_def)

apply simp

apply simp
apply (case_tac "em ? (V nat)")
apply (simp add: id_lookup_def Let_def)

apply (erule_tac x="a" in ballE)
apply (erule exE)
apply (simp add: id_lookup_def)

apply (drule some_lookup_range)
apply simp
--{* ex = Lv nat *}
apply simp
--{* ex = C tval *}
apply simp

--{* subgoal: Pc *}
apply simp
apply (case_tac "em ? Pc")
prefer 2
apply simp

apply (simp add: id_lookup_def Let_def)
--{* subgoal: Rp *}
apply simp
apply (subgoal_tac "(((Pc, C (POS p2)) # em)?\<^sub>=Rp) = (em ?\<^sub>= Rp)")
 prefer 2
 apply (simp only: id_lookup_def lookup.simps fst_conv)
 apply (subgoal_tac "Pc \<noteq> Rp")
  prefer 2
  apply simp
 apply simp
apply simp
apply (simp only: id_lookup_def)
apply (case_tac "em ? Rp")
apply (simp add: Let_def)
apply simp
apply (erule_tac x="a" in ballE)
apply (erule exE)
apply simp
apply (drule_tac a="Rp" in some_lookup_range)
apply simp
--{* subgoal: Tm *}
apply simp
apply (subgoal_tac "(((Pc, C (POS p2)) # em)?\<^sub>= Tm) = (em ?\<^sub>= Tm)")
 prefer 2
 apply (simp only: id_lookup_def lookup.simps fst_conv)
 apply (subgoal_tac "Pc \<noteq> Tm")
  prefer 2
  apply simp
 apply simp
apply simp
apply (simp only: id_lookup_def)
apply (case_tac "em ? Tm")
apply (simp add: Let_def)
apply simp
apply (erule_tac x="a" in ballE)
apply (erule exE)
apply simp
apply (drule_tac a="Tm" in some_lookup_range)
apply simp
--{* subgoal: Add expr1 expr2 *}
apply simp
--{* subgoal: Minus expr1 expr2 *}
apply simp
--{* subgoal: Mult expr1 expr2 *}
apply simp
--{* subgoal: Deref expr *}
apply (simp add: Let_def)
apply (case_tac md)
apply simp
apply (rule foldl_induct)
apply simp
apply (case_tac " eval I (p2, m, e) (substE NoPt em expr)")
apply simp

apply (simp add: Let_def)

apply simp

apply simp

apply (rule impI)
apply (rule ballI)
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "nojunk em")
 prefer 2
 apply (case_tac "em ? Pc" )
 apply simp
 apply simp
apply (frule nojunk_changedvars)
apply (drule_tac mp="changedvars em" in set_lookup)
apply simp
apply (drule some_lookup_range)
apply (drule changedvars_ran)
apply simp
apply (erule_tac x="snd a" in ballE)
apply (erule exE)
apply (simp add: split_def )
apply (case_tac "eval I (p2, m, e) (substE NoPt em expr) = NAT (fst a)")
apply simp

apply simp

apply simp

--{* md = Mv nat1 nat2 *}
apply (simp add: Let_def)
apply (case_tac "m nat2 = eval I (p2, m, e) (substE (Mv nat1 nat2) em expr)")
apply (simp add: Let_def)
apply (case_tac "m nat1")
apply simp
apply (simp add: Let_def)
apply simp

apply simp
apply (rule foldl_induct)
apply simp
apply (case_tac " eval I (p2, m, e) (substE (Mv nat1 nat2) em expr)")
apply simp

apply (simp add: Let_def)

apply simp

apply simp

apply (rule impI)
apply (rule ballI)
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "nojunk em")
 prefer 2
 apply (case_tac "em ? Pc" )
 apply simp
 apply simp
apply (frule nojunk_changedvars)
apply (drule_tac mp="changedvars em" in set_lookup)
apply simp
apply (drule some_lookup_range)
apply (drule changedvars_ran)
apply simp
apply (erule_tac x="snd a" in ballE)
apply (erule exE)
apply (simp add: split_def )
apply (case_tac "eval I (p2, m, e) (substE (Mv nat1 nat2) em expr) = NAT (fst a)")
apply simp

apply simp

apply simp


--{* IF expr1 = expr2 THEN expr3 ELSE expr4 *}
apply simp
apply (case_tac "eval I (p2, m, e) (substE md em expr1) = eval I (p2, m, e) (substE md em expr2)")
apply simp
apply simp

--{* Old expr *}
apply (simp add: Let_def split_def fst_conv snd_conv)
(*>*)
done

subsection {* Substituting  Tm in expressions *}

lemma substE_Tm:
"\<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv') ; nojunk ((Tm,Add Tm (C (NAT 1)))#em);
   1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < length (h e)
\<rbrakk> \<Longrightarrow> eval I (p,m,e) (substE md ((Tm,Add Tm (C (NAT 1)))#em) ex) = eval I (p,m,e\<lparr>h:=(h e)@[p]\<rparr>) (substE md em ex)"
(*<*)
apply (induct ex)
apply (simp add: eval.simps substE.simps)
apply (subgoal_tac "V nat \<noteq> Tm")
 prefer 2
 apply simp
apply (frule_tac as="em" and a="Tm" and b="Add Tm (C (NAT 1))" in id_lookup_red)
apply simp 
apply (case_tac md)
--{* md = NoPt *}
apply (case_tac "em ? (V nat)")
apply (simp add: id_lookup_def Let_def)

apply (erule_tac x="a" in ballE)
apply (erule exE)
apply (simp add: id_lookup_def)

apply (drule some_lookup_range)
apply simp
--{* md = Mv nat1 nat2 *}
apply (simp add: Let_def)
apply (case_tac "m nat2 = NAT nat")
apply (simp add: Let_def)
apply (case_tac "m nat1")
apply simp

apply (simp add: Let_def)

apply simp

apply simp
apply (case_tac "em ? (V nat)")
apply (simp add: id_lookup_def Let_def)

apply (erule_tac x="a" in ballE)
apply (erule exE)
apply (simp add: id_lookup_def)

apply (drule some_lookup_range)
apply simp
--{* Lv nat *}
apply simp
--{* ex = C tval *}
apply simp

--{* subgoal: Pc *}
apply (simp add: id_lookup_def)
apply (case_tac "em ? Pc")
apply (simp add: Let_def)
apply simp
apply (erule_tac x="a" in ballE)
apply (erule exE)
apply simp
apply (drule_tac a="Pc" in some_lookup_range)
apply simp

--{* subgoal: Rp *}
apply simp
apply (subgoal_tac "(((Tm,Add Tm (C (NAT 1))) # em)?\<^sub>=Rp) = (em ?\<^sub>= Rp)")
 prefer 2
 apply (simp only: id_lookup_def lookup.simps fst_conv)
 apply (subgoal_tac "Tm \<noteq> Rp")
  prefer 2
  apply simp
 apply simp
apply simp
apply (simp only: id_lookup_def)
apply (case_tac "em ? Rp")
apply (simp add: Let_def)
apply (case_tac "cs e")
apply simp
--{* cs e = a list *}
apply (case_tac "list")
apply simp
--{* hier wird benoetigt: 1 < cs e - - > fst (hd (cs e)) < length (h e) *}
apply (simp add: callstate_def callpc_def nth_append split_def) 

apply simp
apply (erule_tac x="a" in ballE)
apply (erule exE)
apply simp
apply (drule_tac a="Rp" in some_lookup_range)
apply simp
--{* subgoal: Tm *}
apply (simp add: id_lookup_def)
apply (case_tac "em ? Tm")
apply (simp add: Let_def lift_def)
apply simp

--{* subgoal: Add expr1 expr2 *}
apply simp
--{* subgoal: Minus expr1 expr2 *}
apply simp
--{* subgoal: Mult expr1 expr2 *}
apply simp
--{* subgoal: Deref expr *}
apply (simp add: Let_def)
apply (case_tac md)
apply simp
apply (rule foldl_induct)
apply simp
apply (case_tac " eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr)")
apply simp

apply (simp add: Let_def)

apply simp

apply simp

apply (rule impI)
apply (rule ballI)
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "nojunk em")
 prefer 2
 apply (case_tac "em ? Tm" )
 apply simp
 apply simp
apply (frule nojunk_changedvars)
apply (drule_tac mp="changedvars em" in set_lookup)
apply simp
apply (drule some_lookup_range)
apply (drule changedvars_ran)
apply simp
apply (erule_tac x="snd a" in ballE)
apply (erule exE)
apply (simp add: split_def )
apply (case_tac "eval I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr) = NAT (fst a)")
apply simp

apply simp

apply simp

--{* md = Mv nat1 nat2 *}
apply (simp add: Let_def)
apply (case_tac "m nat2 = eval I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substE (Mv nat1 nat2) em expr)")
apply (simp add: Let_def)
apply (case_tac "m nat1")
apply simp
apply (simp add: Let_def)
apply simp

apply simp
apply (rule foldl_induct)
apply simp
apply (case_tac " eval I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substE (Mv nat1 nat2) em expr)")
apply simp

apply (simp add: Let_def)

apply simp

apply simp

apply (rule impI)
apply (rule ballI)
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "nojunk em")
 prefer 2
 apply (case_tac "em ? Tm" )
 apply simp
 apply simp
apply (frule nojunk_changedvars)
apply (drule_tac mp="changedvars em" in set_lookup)
apply simp
apply (drule some_lookup_range)
apply (drule changedvars_ran)
apply simp
apply (erule_tac x="snd a" in ballE)
apply (erule exE)
apply (simp add: split_def )
apply (case_tac "eval I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substE (Mv nat1 nat2) em expr) = NAT (fst a)")
apply simp

apply simp

apply simp


--{* IF expr1 = expr2 THEN expr3 ELSE expr4 *}
apply simp
apply (case_tac "eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE md em expr1) = eval I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substE md em expr2)")
apply simp
apply simp

--{* Old expr *}
apply (simp add: Let_def split_def fst_conv snd_conv callstate_def)
apply (case_tac "cs e")
apply simp
apply simp
apply (case_tac "list")
apply (simp add: split_def)
apply (simp add: nth_append split_def rec_upd_simp)
(*>*)
done

subsection {* Substituting Rp in expressions *}

lemma substE_Rp:
"\<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv'); nojunk ((Tm,Add Tm (C (NAT 1)))#(Rp,(C (POS (incA p))))#em);
   1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < length (h e); cs e \<noteq> []
\<rbrakk> \<Longrightarrow> eval I (p,m,e) (contextDnE (substE NoPt ((Tm,Add Tm (C (NAT 1)))#(Rp,(C (POS (incA p))))#em) ex)) = 
      eval I (p,m,e\<lparr>cs:=(length (h e),m)#(cs e), h:=(h e)@[p]\<rparr>) (substE NoPt em ex)"
(*<*)
apply (induct ex)
apply (simp add: eval.simps substE.simps)
apply (subgoal_tac "V nat \<noteq> Tm")
 prefer 2
 apply simp
apply (frule_tac as="(Rp,C (POS (incA p)))#em" and a="Tm" and b="Add Tm (C (NAT 1))" in id_lookup_red)
apply simp
apply (subgoal_tac "V nat \<noteq> Rp")
 prefer 2
 apply simp
apply (frule_tac as="em" and a="Rp" and b="(C (POS (incA p)))" in id_lookup_red)
apply simp
apply (case_tac "em ? (V nat)")
apply (simp add: id_lookup_def Let_def)
apply (erule_tac x="a" in ballE)
apply (erule exE)
apply (simp add: id_lookup_def)
apply (drule some_lookup_range)
apply simp
--{* subgoal: Lv nat *}
apply simp
--{* subgoal: C tval *}
apply simp
--{* subgoal: Pc *}
apply simp
apply (subgoal_tac "(((Tm,Add Tm (C (NAT 1)))#(Rp,C (POS (incA p)))# em)?\<^sub>= Pc) = (em ?\<^sub>= Pc)")
 prefer 2
 apply (simp only: id_lookup_def lookup.simps fst_conv)
 apply (subgoal_tac "Tm \<noteq> Pc")
  prefer 2
  apply simp
 apply (subgoal_tac "Rp \<noteq> Pc")
  prefer 2
  apply simp
 apply simp
apply simp
apply (simp only: id_lookup_def)
apply (case_tac "em ? Pc")
apply (simp add: Let_def)

apply simp
apply (erule_tac x="a" in ballE)
apply (erule exE)
apply simp
apply (drule_tac a="Pc" in some_lookup_range)
apply simp

--{* subgoal: Rp *}
apply simp
apply (subgoal_tac "(((Tm,Add Tm (C (NAT 1)))#(Rp,C (POS (incA p)))# em)?\<^sub>=Rp) = C (POS (incA p))")
 prefer 2
 apply (simp only: id_lookup_def lookup.simps fst_conv)
 apply (subgoal_tac "Tm \<noteq> Rp")
  prefer 2
  apply simp
 apply simp
apply simp
apply (simp only: id_lookup_def)
apply (case_tac "em ? Rp")
apply (simp add: Let_def)
apply (case_tac "cs e")
apply simp
--{* cs e = a list *}
apply (simp add: callpc_def callstate_def nth_append)
apply (case_tac "em ? Tm")
apply simp
apply simp

--{* subgoal: Tm *}
apply (simp add: id_lookup_def lookup.simps)
apply (case_tac "em ? Tm")
apply (simp add: Let_def split_def fst_conv snd_conv lift_def)
apply simp
--{* subgoal: Add expr1 expr2 *}
apply simp
--{* subgoal: Minus expr1 expr2 *}
apply simp
--{* subgoal: Mult expr1 expr2 *}
apply simp
--{* subgoal: Deref expr *}
apply (simp add: Let_def)
apply (rule_tac L="changedvars em" in foldl_induct)
apply simp
apply (case_tac "eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr)")
apply simp

apply (simp add: Let_def)

apply simp

apply simp

apply (rule impI)
apply (rule ballI)
apply (rule allI)+
apply (rule impI)

apply (simp add: split_def)
apply (case_tac "eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr) = NAT (fst a)")
apply simp

apply (subgoal_tac "nojunk em")
 prefer 2
 apply (case_tac "em ? Tm" )
 apply simp
 apply (case_tac "em ? Rp")
 apply simp
 apply simp
 apply simp
apply (frule nojunk_changedvars)
apply (drule_tac mp="changedvars em" in set_lookup)
apply simp
apply (drule some_lookup_range)
apply (drule changedvars_ran)
apply simp
apply (erule_tac x="snd a" in ballE)
apply (erule exE)
apply simp

apply simp

apply simp

--{* IF expr1 = expr2 THEN expr3 ELSE expr4 *}
apply simp
apply (case_tac "eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr1) = eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr2)")
apply simp
apply simp

--{* Old expr *}
apply (simp add: Let_def split_def fst_conv snd_conv callstate_def)
apply (case_tac "cs e")
apply simp
apply simp
apply (simp add: nth_append split_def rec_upd_simp)
apply (drule_tac s="cs e" in sym)
apply simp
apply (simp only: rec_upd_simp3)
apply (subgoal_tac "e\<lparr>cs := cs e, h := h e\<rparr> = e")
 prefer 2
 apply simp
apply (simp only:)
(*>*)
done

subsection {* Effect of contextOldUp on expressions *}


lemma substE_ContextOldUp:
"\<lbrakk> (cs e) = (k',m')#(k'',m'')#css; k' < length (h e); css \<noteq> [] \<longrightarrow> k'' < length (take k' (h e)) \<rbrakk> \<Longrightarrow> 
 eval I (p,m,e) (contextOldUpE ex) = eval I (p,m,e\<lparr>cs:=tl (cs e)\<rparr>) ex"
(*<*)
apply (induct ex)
--{* subgoal: V nat *}
apply (simp add: eval.simps substE.simps Let_def)
--{* subgoal: Lv nat *}
apply simp
--{* subgoal: C tval *}
apply (simp add: eval.simps substE.simps Let_def)
--{* subgoal: Pc *}
apply (simp add: eval.simps substE.simps Let_def)
--{* subgoal: Rp *}
apply (simp add: eval.simps substE.simps Let_def split_def callstate_def callpc_def initialState_def)
apply (case_tac "css")
apply simp
apply (simp add: split_def callpc_def callstate_def)
--{* subgoal: Tm *} 
apply (simp add: eval.simps substE.simps Let_def)
--{* subgoal: Add expr1 expr2 *}
apply simp
--{* subgoal: Minus expr1 expr2 *}
apply simp
--{* subgoal: Mult expr1 expr2 *}
apply simp
--{* subgoal: Deref expr *}
apply (simp add: eval.simps substE.simps Let_def)
apply (case_tac "eval I (p, m, e\<lparr>cs := (k'', m'') # css\<rparr>) expr")
apply simp
apply (simp add: Let_def)
apply simp
--{* IF expr1 = expr2 THEN expr3 ELSE expr4 *}
apply simp
apply (case_tac "eval I (p, m, e\<lparr>cs := (k'', m'') # css\<rparr>) expr1 =
                eval I (p, m, e\<lparr>cs := (k'', m'') # css\<rparr>) expr2")
apply simp
apply simp
--{* Old expr *}
apply (simp add: Let_def split_def fst_conv snd_conv callstate_def)
apply (case_tac "css")
apply simp
apply simp
apply (erule conjE)+
apply (subgoal_tac "min k'' k' = k''")
 prefer 2
 apply (simp add: min_def)
apply (simp add: nth_append split_def rec_upd_simp rec_upd_simp3)
done


section {* Substitutions on formulae *}

lemma substE_empty:
"substE NoPt [] ex = ex"
(*<*)
apply (induct ex)
apply (simp add: id_lookup_def Let_def)+
(*>*)
done

lemma tval_V_C_noteq:
"(V x = C tv) = False"
(*<*)
apply simp
(*>*)
done

lemma tval_C_V_noteq:
"(C tv = V x) = False"
(*<*)
apply simp
(*>*)
done

lemma sizeF_substF:
"\<And> rm. sizeF (substF md em f) = sizeF f"
(*<*)

apply (induct f)
apply (simp add: sizeF_sizeFs.simps substF_substFL.simps)+
(*>*)
done


lemma substF_var_simp: 
"\<And> p m e em v tv I. \<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv'); nojunk ((V v,C tv)#em) \<rbrakk> \<Longrightarrow>
validF I (p,m,e) (substF NoPt ((V v,C tv)#em) f) = (validF I (p,m[v::=tv],e) (substF NoPt em f))"
(*<*)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (induct f)
--{* T *}
apply (simp add: valid_def validF_validFs.simps)
--{* F *}
apply (simp add: valid_def validF_validFs.simps)
--{* And list *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e em v tv I. (\<forall>ex'\<in>set (FiniteMap.ran em). \<exists>tv'. ex' = C tv') \<longrightarrow>   nojunk ((V v, C tv) # em) \<longrightarrow> (validF I (p,m,e) (And (substFL NoPt ((V v, C tv)#em) l))) = (validF I (p,m[v ::= tv],e) (And (substFL NoPt em l)))) list" in asm_rl)
apply (rule allI)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="tv" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: valid_def validF_validFs.simps)
prefer 10
apply simp
prefer 9
apply simp
--{* Impl form1 form2 *}
apply (simp add: valid_def validF_validFs.simps)
--{* Neg form *}
apply (simp add: valid_def validF_validFs.simps)
--{* expr1 = expr2 *}
apply (simp add: validF_validFs.simps del: nojunk.simps)
apply (rule impI)+
apply (rule allI)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr1)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr2)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply simp
--{*  Leq expr1 expr2 *}
apply (simp add: validF_validFs.simps del: nojunk.simps)
apply (rule impI)+
apply (rule allI)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr1)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr2)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply simp
--{* Less expr1 expr2 *}
apply (simp add: validF_validFs.simps del: nojunk.simps)
apply (rule impI)+
apply (rule allI)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr1)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr2)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply simp
--{* Ty expr vtype *}
apply (simp add: validF_validFs.simps del: nojunk.simps)
apply (rule impI)+
apply (rule allI)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply simp
--{* Forall nat. form *}
apply (rule allI)
apply (rule impI)+
apply simp
--{* Yields *}
apply (simp add: validF_validFs.simps del: nojunk.simps)
apply (rule impI)+
apply (rule allI)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((V v, C tv) # em) expr)) = (eval I (p, m[v ::= tv], e) (substE NoPt em expr))")
 prefer 2
 apply (rule substE_var_simp)
 apply assumption+
apply simp
(*>*)
done

lemma substF_empty:
"substF NoPt [] f = f"
(*<*)
apply (induct f)
apply simp
apply simp
apply (drule_tac psi="(\<lambda> (l::form list). (substFL NoPt [] l) = l) list" in asm_rl)
apply (simp add: substE_empty)+
(*>*)
done

lemma substF_Pc:
"\<And> p m e em p2 md I. \<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv'); nojunk ((Pc,C (POS p2))#em) \<rbrakk> \<Longrightarrow> 
 validF I (p,m,e) (substF md ((Pc,C (POS p2))#em) f) = (validF I (p2,m,e) (substF md em f))"
(*<*)
apply (induct f)
--{* T *}
apply (simp add: valid_def validF_validFs.simps)
--{* F *}
apply (simp add: valid_def validF_validFs.simps)
--{* And list *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e em p2 md I. (\<forall>ex'\<in>set (FiniteMap.ran em). \<exists>tv'. ex' = C tv') \<longrightarrow>   nojunk ((Pc, C (POS p2)) # em) \<longrightarrow> (validF I (p,m,e) (And (substFL md ((Pc, C (POS p2))#em) l))) = (validF I (p2,m,e) (And (substFL md em l)))) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em"  in allE)
apply (erule_tac x="p2" in allE)
apply (erule_tac x="md" in allE)
apply (erule_tac x="I" in allE)
apply simp

prefer 10
apply simp
prefer 9
apply simp

--{* Impl form1 form2 *}
apply (simp add: valid_def validF_validFs.simps)
--{* Neg form *}
apply (simp add: valid_def validF_validFs.simps)
--{* expr1 = expr2 *}
apply (simp add: substE_Pc valid_def validF_validFs.simps del: nojunk.simps)
--{* expr1 <= expr2 *}
apply (simp add: substE_Pc valid_def validF_validFs.simps del: nojunk.simps)
--{* expr1 < expr2 *}
apply (simp add: substE_Pc valid_def validF_validFs.simps del: nojunk.simps)
--{* Ty *}
apply (simp add: substE_Pc valid_def validF_validFs.simps del: nojunk.simps)
--{* Forall nat. form *}
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps Let_def split_def fst_conv snd_conv)
--{* Yields *}
apply (simp add: substE_Pc valid_def validF_validFs.simps del: nojunk.simps)
done

lemma substF_Tm_NoPt:
"\<And> p m e em I. \<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv') ; nojunk ((Tm, Tm \<oplus> C (NAT 1))#em);
 1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < length (h e)  \<rbrakk> \<Longrightarrow> validF I (p,m,e) (substF NoPt ((Tm, Tm \<oplus> C (NAT 1))#em) f) = validF I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt em f)"
apply (induct f)
--{* T *}
apply (simp add: valid_def validF_validFs.simps)
--{* F *}
apply (simp add: valid_def validF_validFs.simps)
--{* And list *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e em I. (\<forall>ex'\<in>set (FiniteMap.ran em). \<exists>tv'. ex' = C tv') \<longrightarrow>   nojunk ((Tm, Tm \<oplus> C (NAT 1)) # em) \<longrightarrow> (1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < length (h e)) \<longrightarrow> validF I (p,m,e) (And (substFL NoPt ((Tm, Tm \<oplus> C (NAT 1))#em) l)) = validF I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (And (substFL NoPt em l))) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em"  in allE)
apply (erule_tac x="I" in allE)
apply simp

prefer 10
apply simp
prefer 9
apply simp

--{* Impl form1 form2 *}
apply (simp add: valid_def validF_validFs.simps)
--{* Neg form *}
apply (simp add: valid_def validF_validFs.simps)
--{* expr1 = expr2 *}
apply (simp add: valid_def validF_validFs.simps del: nojunk.simps)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr1)) = (eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr2)) = (eval I (p,m, e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply simp
--{* expr1 <= expr2 *}
apply (simp add: valid_def validF_validFs.simps del: nojunk.simps)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr1)) = (eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr2)) = (eval I (p,m, e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply simp
--{* expr1 < expr2 *}
apply (simp add: valid_def validF_validFs.simps del: nojunk.simps)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr1)) = (eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr2)) = (eval I (p,m, e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply simp
--{* Ty *}
apply (simp add: valid_def validF_validFs.simps del: nojunk.simps)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr)) = (eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply simp
--{* Forall nat. form *}
apply (simp only: substF_substFL.simps valid_def validF_validFs.simps Let_def split_def fst_conv snd_conv)
--{* Yields *}
apply (simp add: valid_def validF_validFs.simps del: nojunk.simps)
apply (subgoal_tac "(eval I (p, m, e) (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) #em) expr)) = (eval I (p,m,e\<lparr>h := h e @ [p]\<rparr>) (substE NoPt em expr))")
 prefer 2
 apply (rule substE_Tm)
 apply assumption
 apply simp
 apply (simp add: nat_number)
apply simp
(*>*)
done

lemma eval_intvar:
"\<And> I s. intVarsE ex = [] \<Longrightarrow> eval I s ex = eval I' s ex"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct ex)
--{* V nat *}
apply simp
--{* Lv nat *}
apply simp
--{* C tval*}
apply simp
--{* Pc *}
apply simp
--{* Rp *}
apply simp
--{* Tm *}
apply simp
--{* Add *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: intVarsE.simps)
--{* Minus *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: intVarsE.simps)
--{* Mult *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (simp add: intVarsE.simps)
--{* Deref *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply simp
--{* Ifeq *}
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="I" in allE)
apply (rule allI)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (simp add: intVarsE.simps)
apply (case_tac " eval I' s expr1 = eval I' s expr2")
apply simp
apply simp
--{* Old expr *}
apply (rule allI)+
apply (erule_tac x="I" in allE)
apply (erule_tac x="callstate (snd (snd s))" in allE)
apply (simp add: Let_def split_def)
(*>*)
done

lemma substF_eval:
"\<And> p m e em I. \<lbrakk> \<forall> ex \<in> set (ran em). intVarsE ex = []; nojunk em \<rbrakk> \<Longrightarrow> validF I (p,m,e) (substF NoPt em f) = validF I (p,m,e) (substF NoPt (map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) em) f)"
(*<*)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (induct f)
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e em I. (\<forall> ex \<in> set (ran em). intVarsE ex = []) \<longrightarrow> nojunk em \<longrightarrow> validF I (p,m,e) (And (substFL NoPt em l)) = validF I (p,m,e) (And (substFL NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) l))) list" in asm_rl)
apply (rule allI)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em" in allE)
apply (erule_tac x="I" in allE)
apply simp
prefer 10
apply simp
prefer 9
apply simp

--{* Impl *}
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
--{* Neg *}
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
--{* Eq expr1 expr2 *}
apply (rule allI, (rule impI)+)
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr1) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr1))")
 prefer 2
 apply (rule substE_eval)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr2) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr2))")
 prefer 2
 apply (rule substE_eval)
apply (simp only:)
--{* Leq expr1 expr2 *}
apply (rule allI, (rule impI)+)
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr1) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr1))")
 prefer 2
 apply (rule substE_eval)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr2) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr2))")
 prefer 2
 apply (rule substE_eval)
apply (simp only:)

--{* Less expr1 expr2 *}
apply (rule allI, (rule impI)+)
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr1) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr1))")
 prefer 2
 apply (rule substE_eval)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr2) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr2))")
 prefer 2
 apply (rule substE_eval)
apply (simp only:)
--{* Ty expr vtype *}
apply (rule allI, (rule impI)+)
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr))")
 prefer 2
 apply (rule substE_eval)
apply (simp only:)
--{* Forall nat. form *}
apply (rule allI, (rule impI)+)
apply (simp add: substF_substFL.simps Let_def split_def)
apply (rule doubleAllI)
apply (rule allI)
apply (subgoal_tac "(map (\<lambda>pa. (fst pa, C (eval (I[nat ::= tv]) (p, m, e) (snd pa)))) em) =
                    (map (\<lambda>pa. (fst pa, C (eval I (p, m, e) (snd pa)))) em)")
 prefer 2
 apply (erule thin_rl)
 apply (erule rev_mp)+
 apply (induct_tac "em")
 apply simp
 
 apply (simp del: nojunk.simps)
 apply (rule impI)+
 apply (rule conjI)
 apply (erule_tac x="snd a" in ballE)
 apply (rule eval_intvar)
 apply assumption
 apply (drule nojunk_range)
 apply simp
 
 apply (subgoal_tac "(\<forall>ex\<in>set (FiniteMap.ran list). intVarsE ex = [])")
  prefer 2
  apply (rule ballI)
  apply (erule_tac x="ex" in ballE)
  apply assumption
  apply (drule nojunk_range)
  apply simp
 apply (drule mp, assumption)
 apply (subgoal_tac "nojunk list")
  prefer 2
  apply simp
  apply (case_tac "list ? fst a")
  apply simp
  apply simp
apply simp
apply (simp only:)
--{* Yields *}
apply (rule allI, (rule impI)+)
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt em expr) =
                 (eval I (p, m, e) (substE NoPt (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em) expr))")
 prefer 2
 apply (rule substE_eval)
apply (simp only:)
(*>*)
done

lemma map_map_Tm: 
"(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm, te) # map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) =
 (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm, te) # em))"
(*<*)
apply (induct em)
apply simp
apply (simp only: map.simps)
apply simp
apply (simp (no_asm) add: split_def)
(*>*)
done

lemma substF_eval_exTm:
"\<And> p m e em te I. \<lbrakk> nojunk ((Tm,te)#em);  \<forall> ex \<in> set (ran em). intVarsE ex = [] \<rbrakk> \<Longrightarrow> validF I (p,m,e) (substF NoPt ((Tm,te)#em) f) = validF I (p,m,e) (substF NoPt ((Tm,te)#(map (\<lambda> (a,b). (a, C (eval I (p,m,e) b))) em)) f)"
(*<*)
apply (induct f)
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e em te I. nojunk  ((Tm,te)#em) \<longrightarrow> (\<forall> ex \<in> set (ran em). intVarsE ex = []) \<longrightarrow> validF I (p,m,e) (And (substFL NoPt ((Tm,te)#em) l)) = validF I (p,m,e) (And (substFL NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b)))) em) l))) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em" in allE)
apply (erule_tac x="te" in allE)
apply (erule_tac x="I" in allE)
apply simp
prefer 10
apply simp
prefer 9
apply simp
--{* Impl *}
apply simp
--{* Neg *}
apply simp
--{* Eq expr1 expr2 *}
apply simp
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr1) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr1))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr1) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr1))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr2) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr2))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr2) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr2))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply (simp only:)
--{* Leq expr1 expr2 *}
apply simp
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr1) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr1))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr1) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr1))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr2) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr2))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr2) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr2))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply (simp only:)
--{* Less expr1 expr2 *}
apply simp
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr1) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr1))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr1) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr1))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr2) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr2))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr2) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr2))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply (simp only:)
--{* Ty expr vtype *}
apply simp
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply simp
--{* Forall nat. form *}
apply atomize
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em" in allE)
apply (erule_tac x="te" in allE)
apply (simp add: substF_substFL.simps Let_def split_def del: nojunk.simps)
apply (rule doubleAllI)
apply (rule allI)
apply (subgoal_tac "(map (\<lambda>pa. (fst pa, C (eval (I[nat ::= tv]) (p, m, e) (snd pa)))) em) =
                    (map (\<lambda>pa. (fst pa, C (eval I (p, m, e) (snd pa)))) em)")
 prefer 2
 apply (erule_tac V="\<forall>I. ?P I" in thin_rl)
 apply (subgoal_tac "nojunk em") 
  prefer 2
  apply simp
  apply (case_tac "em ? Tm")
  apply simp
  apply simp
 apply (erule_tac V="nojunk ((Tm,te) # em)" in thin_rl)
 apply (erule rev_mp)+
 apply (induct_tac "em")
 apply simp
 
 apply (simp del: nojunk.simps)
 apply (rule impI)+
 apply (rule conjI)
 apply (drule nojunk_range)
 apply simp
 apply (erule conjE)+
 apply (rule eval_intvar)
 apply assumption

 apply (subgoal_tac "nojunk list")
  prefer 2
  apply simp
  apply (case_tac "list ? fst a")
  apply simp
  apply simp
 apply (subgoal_tac "(\<forall>ex\<in>set (FiniteMap.ran list). intVarsE ex = [])")
  prefer 2
  apply (drule nojunk_range)
  apply simp
 apply simp

apply (simp (no_asm_simp) only: substF_substFL.simps Let_def split_def)
--{* Yields *}
apply simp
apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm,te)#em) expr) =
                 (eval I (p, m, e) (substE NoPt ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr))")
 prefer 2
 apply (subgoal_tac "eval I (p, m, e) (substE NoPt ((Tm, te) # (map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)) expr) = (eval I (p, m, e) (substE NoPt ((map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) ((Tm,te)#(map (\<lambda>(a, b). (a, C (eval I (p, m, e) b))) em)))) expr))")
  prefer 2
  apply (rule substE_eval)
 apply (simp only: map_map_Tm)
 apply (rule substE_eval)
apply simp
(*>*)
done

lemma substE_Mv_NoPt:
"\<And>p m e n1 n2 nv1 nv2 em.
\<lbrakk> em = [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS p'))]; m n2 = NAT nv2; m n1 = NAT nv1 \<rbrakk> \<Longrightarrow> 
eval I (p, m, e) (substE (Mv n1 n2) em expr) =
eval I (p, m[nv2 ::= m nv1], e) (substE NoPt em expr)"
(*<*)
apply (induct expr)
--{* V nat *}
apply simp
apply (subgoal_tac "em ? V nat = None")
 prefer 2
 apply simp
apply (simp add: Let_def id_lookup_def)
apply (case_tac "nv2 = nat")
apply (simp add: Let_def update_def)
--{* case: nv2 ~= nat *}
apply (simp add: Let_def update_def id_lookup_def)
--{* Lv nat *}
apply simp
--{* C tval *}
apply simp
--{* Pc *}
apply (simp add: substE.simps eval.simps id_lookup_def)
--{* Rp *}
apply (simp add: substE.simps eval.simps id_lookup_def Let_def)
--{* Tm *}
apply (simp add: substE.simps eval.simps id_lookup_def Let_def)
--{* Add expr1 expr2 *}
apply (simp add: substE.simps eval.simps id_lookup_def)
--{* Sub expr1 expr2 *}
apply (simp add: substE.simps eval.simps id_lookup_def)
--{* Mult expr1 expr2 *}
apply (simp add: substE.simps eval.simps id_lookup_def)
--{* Deref *}
apply (simp add: substE.simps eval.simps id_lookup_def Let_def)
apply (case_tac "eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr) = NAT nv2")
apply (simp add: Let_def update_def)

apply (drule_tac s="NAT nv2" in not_sym)
apply (simp add: Let_def)
apply (case_tac " eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr)")
apply simp
prefer 2
apply simp

apply (simp add: Let_def update_def)
--{*  Ifeq *}
apply (simp add: substE.simps eval.simps id_lookup_def)
apply (case_tac "eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1) =
                eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2)")
apply simp
apply simp

--{* Old *}
apply (simp add: substE.simps eval.simps id_lookup_def Let_def)
(*>*)
done

lemma substF_Mv_NoPt:
"\<And> p m e n1 n2 nv1 nv2 em I. \<lbrakk> m n1 = NAT nv1; m n2 = NAT nv2;  em = [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS p'))]  \<rbrakk> \<Longrightarrow> 
validF I (p,m,e) (substF (Mv n1 n2) em f) = validF I (p,m[nv2 ::= m nv1],e) (substF NoPt em f)"
(*<*)
apply (induct f)
--{* T *}
apply (simp add: valid_def validF_validFs.simps)
--{* F *}
apply (simp add: valid_def validF_validFs.simps)
--{* And *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e n1 n2 nv1 nv2 em I. (m n1 = NAT nv1) \<longrightarrow> (m n2 = NAT nv2) \<longrightarrow> (em = [(Tm,Add Tm (C (NAT 1))),(Pc,C (POS p'))]) \<longrightarrow> validF I (p,m,e) (And (substFL (Mv n1 n2) em l)) = validF I (p,m[nv2 ::= m nv1],e) (And (substFL NoPt em l))) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="n1" in allE)
apply (erule_tac x="n2" in allE)
apply (erule_tac x="nv1" in allE)
apply (erule_tac x="nv2" in allE)
apply (erule_tac x="em" in allE)
apply (erule_tac x="I" in allE)
apply simp
prefer 10
apply simp
prefer 9
apply simp
--{* Impl *}
apply simp
--{* Neg *}
apply simp
--{* Eq expr1 expr2 *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply simp
--{* Leq expr1 expr2 *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply simp
--{* Less expr1 expr2 *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr1))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr2))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply simp
--{* Ty expr *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply simp
--{* Forall *}
apply simp
--{* Yields *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (substE (Mv n1 n2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr)) =
(eval I (p, m[nv2 ::= m nv1], e) (substE NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS p'))] expr))")
 prefer 2
 apply (rule substE_Mv_NoPt)
 apply simp
 apply simp
 apply simp
apply simp
(*>*)
done




lemma sizeF_contextDn:
"sizeF (contextDn f) = sizeF f"
(*<*)
apply (induct f)
apply simp+
(*>*)
done

lemma substF_Rp:
"\<And> p m e em I. \<lbrakk> (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv') ; nojunk ((Tm,Add Tm (C (NAT 1)))#(Rp,(C (POS (incA p))))#em);
   1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < length (h e); cs e \<noteq> []
\<rbrakk> \<Longrightarrow> validF I (p,m,e) (contextDn (substF NoPt ((Tm,Add Tm (C (NAT 1)))#(Rp,(C (POS (incA p))))#em) f)) = validF I (p,m,e\<lparr>cs:=(length (h e),m)#(cs e), h:=(h e)@[p]\<rparr>) (substF NoPt em f)"
(*<*)
apply (induct f)
--{* T *}
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps) 
--{* F *}
apply (simp add: substF_substFL.simps valid_def validF_validFs.simps)
--{* And *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e em I. (\<forall> ex'\<in>(set (ran em)). \<exists> tv'. ex'=C tv') \<longrightarrow> nojunk  ((Tm,Add Tm (C (NAT 1)))#(Rp, (C (POS (incA p))))#em) \<longrightarrow> ( 1 < length (cs e) \<longrightarrow> fst (hd (cs e)) < length (h e))  \<longrightarrow>  (cs e \<noteq> []) \<longrightarrow> validF I (p,m,e) (contextDn (And (substFL NoPt ((Tm,Add Tm (C (NAT 1)))#(Rp, (C (POS (incA p))))#em) l))) = validF I (p,m,e\<lparr>cs:=(length (h e),m)#(cs e), h:=(h e)@[p]\<rparr>) (And (substFL NoPt em l))) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="em" in allE)
apply (erule_tac x="I" in allE)
apply simp
prefer 10
apply simp
prefer 9
apply simp
--{* Impl *}
apply simp
--{* Neg *}
apply simp
--{* Eq expr1 expr2 *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr1))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr2))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply simp
--{* Leq expr1 expr2 *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr1))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr2))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply simp
--{* Less expr1 expr2 *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr1))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr1))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr2))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr2))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply simp
--{* Ty expr vtype *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply simp
--{* Forall *}
apply simp
--{* Yields *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextDnE (substE NoPt ((Tm, Tm \<oplus> C (NAT 1)) # (Rp, C (POS (incA p))) # em) expr))) =
(eval I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) (substE NoPt em expr))")
 prefer 2
 apply (rule substE_Rp)
 apply simp
 apply simp
 apply simp
 apply assumption
apply simp
(*>*)
done

lemma varsE_contextOldUp:
"intVarsE (contextOldUpE expr) = intVarsE expr"
(*<*)
apply (induct expr)
apply simp +
(*>*)
done

lemma freeVars_contextOldUp: 
"freeIntVars (contextOldUp form) = freeIntVars form"
(*<*)
apply (induct form)
apply (simp add: varsE_contextOldUp) +
(*>*)
done


lemma substF_ContextOldUp:
"\<And> p m e k' m' k'' m'' css I. \<lbrakk> (cs e) = (k',m')#(k'',m'')#css;  k' < length (h e); css \<noteq> [] \<longrightarrow> k'' < length (take k' (h e))
\<rbrakk> \<Longrightarrow> validF I (p,m,e) (contextOldUp f) = validF I (p,m,e\<lparr>cs:=tl (cs e)\<rparr>) f"
(*<*)
apply (induct f)
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e k' m' k'' m'' css I. (cs e) = (k',m')#(k'',m'')#css \<longrightarrow> k' < length (h e) \<longrightarrow> (css \<noteq> [] \<longrightarrow> k'' < length (take k' (h e))) \<longrightarrow>  validFs I (p,m,e) (contextOldUpL l) = validFs I (p,m,e\<lparr>cs:=tl (cs e)\<rparr>) l) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I" in allE)
apply simp
prefer 10
apply (rule allI)+
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I" in allE)
apply simp
apply (rule impI)+
apply (drule mp, assumption)+
apply atomize
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I" in allE)
apply (drule mp, assumption)+
apply simp
prefer 9
apply simp
--{* Impl *}
apply simp
apply atomize
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I" in allE)
apply simp
--{* Neg *}
apply simp
apply atomize
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I" in allE)
apply simp
--{* Eq *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr1)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr1)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr1" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr2)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr2)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr2" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply simp
--{* Leq *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr1)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr1)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr1" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr2)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr2)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr2" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply simp
--{* Less *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr1)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr1)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr1" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr2)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr2)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr2" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply simp
--{* Ty *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply simp
--{* Forall *}
apply simp
apply (rule doubleAllI)
apply (rule allI)
apply atomize
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="k'" in allE)
apply (erule_tac x="m'" in allE)
apply (erule_tac x="k''" in allE)
apply (erule_tac x="m''" in allE)
apply (erule_tac x="css" in allE)
apply (erule_tac x="I[nat ::= tv]" in allE)
apply simp
--{* Yields *}
apply simp
apply (subgoal_tac "(eval I (p, m, e) (contextOldUpE expr)) = (eval I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) expr)")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and k'="k'" and m'="m'" and k''="k''" and m''="m''" and css="css" and ex="expr" in  substE_ContextOldUp)
 apply simp
 apply simp
 apply simp
apply simp
done

subsection {* Verifying wpF *}

lemma correctWpF:
"\<lbrakk> wf prg ; (p,m,e)\<in> safeP prg ; ((p, m, e), p', m',e') \<in> effS prg ; prg,(p,m,e) \<Turnstile> wpF prg p p' Q \<rbrakk> \<Longrightarrow> (prg,(p', m',e') \<Turnstile> Q)"
(*<*)
apply (simp only: valid_def)
apply (rule allI)
apply (erule_tac x="I" in allE)
apply (erule_tac P="validF I (p,m,e) (wpF prg p p' Q)" in rev_mp)
apply (erule_tac P="((p, m, e), p', m',e') \<in> effS prg" in rev_mp)
apply (erule_tac P="(p,m,e)\<in> safeP prg" in rev_mp)
apply (erule_tac P="wf prg" in rev_mp)
apply (case_tac "cmd prg p")
apply (simp add: effS_def step_def option.cases split_def)
apply (rule impI)+
apply (case_tac "a")
apply (simp add: effS_def step_def wpF_def split_def Let_def)
apply (subgoal_tac "C (NAT (Suc 0)) = (C (NAT 1))")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "(validF I (p, m, e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p')), (V nat1, C (NAT nat2))] Q)) =
(validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p')), (V nat1, C (NAT nat2))] Q))")  
 prefer 2
 apply (rule substF_Tm_NoPt)
 apply (rule ballI)
 apply (simp only: ran_del fst_conv snd_conv del_def filter.simps split_def expr.simps)
 apply (subgoal_tac " V nat1 \<noteq> Pc ")
  prefer 2
  apply (simp (no_asm))
 apply (simp only: if_True simp_thms)
 apply (simp only: ran_del fst_conv snd_conv del_def filter.simps split_def expr.simps)
 apply (simp only: ran_def dom_def  map.simps set.simps)
 apply (erule_tac P="ex' \<in> ?a" in rev_mp)
 apply (simp (no_asm))
 
 apply (simp (no_asm) add: nojunk.simps)

 apply (simp (no_asm) add: dom_def)
 apply (drule sysinv_pres)
 apply assumption
 apply (case_tac "cs e")
 apply (erule_tac P="cs e= []" in rev_mp)
 apply (simp (no_asm))
 apply (case_tac "list")
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (erule_tac P="list =[]" in rev_mp)
 apply (simp (no_asm))
 apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
 apply (erule_tac P="list = ab # lista" in rev_mp)
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (simp (no_asm))
 apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
 apply (rule impI)+
 apply (erule conjE)+
 apply assumption
apply (simp only:)

apply (subgoal_tac "validF I (p, m, e') (substF NoPt [(Pc, C (POS p')), (V nat1, C (NAT nat2))] Q) =
                    (validF I (p', m, e') (substF NoPt [(V nat1, C (NAT nat2))] Q))")
 prefer 2
 apply (rule substF_Pc)
 apply (simp add: ran_def dom_def)
 apply simp
apply (simp only:)

apply (subgoal_tac "validF I (p', m, e') (substF NoPt [(V nat1, C (NAT nat2))] Q) =
                    (validF I (p', m[nat1 ::= NAT nat2], e') (substF NoPt [] Q))")
 prefer 2
 apply (rule substF_var_simp) 
 apply (simp (no_asm) add: ran_def dom_def)
 apply (simp (no_asm) add: ran_def dom_def)
apply (simp only: substF_empty)
--{* ADD nat1 nat2 *}
apply (simp add: effS_def step_def wpF_def split_def Let_def)
apply (subgoal_tac "C (NAT (Suc 0)) = (C (NAT 1))")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p')), (V nat1, V nat1 \<oplus> V nat2)]")
 prefer 2
 apply (simp (no_asm) add: nojunk.simps)
apply (drule_tac I="I" and p="p" and m="m" and e="e" and f="Q"  in substF_eval_exTm)
apply (simp (no_asm) add: ran_def dom_def intVarsE.simps)
apply (simp only: map.simps split_def fst_conv snd_conv)
apply (subgoal_tac "
(validF I (p, m,e) (substF NoPt ((Tm, Tm \<oplus> C (NAT 1))#[(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat1, C (eval I (p, m, e) (V nat1 \<oplus> V nat2)))]) Q)) =
(validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat1, C (eval I (p, m, e) (V nat1 \<oplus> V nat2)))] Q))")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and f="Q" in substF_Tm_NoPt)
 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))
 
 apply (drule sysinv_pres)
 apply assumption
 apply (case_tac "cs e")
 apply (erule_tac P="cs e= []" in rev_mp)
 apply (simp (no_asm))
 apply (case_tac "list")
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (erule_tac P="list =[]" in rev_mp)
 apply (simp (no_asm))

 apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
 apply (erule_tac P="list = ab # lista" in rev_mp)
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (simp (no_asm))
 apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
 apply (rule impI)+
 apply (erule conjE)+
 apply assumption
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e') (substF NoPt [(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat1, C (eval I (p, m, e) (V nat1 \<oplus> V nat2)))] Q) =
 validF I (p', m, e') (substF NoPt [(V nat1, C (eval I (p, m, e) (V nat1 \<oplus> V nat2)))] Q)")
 prefer 2
 apply (simp (no_asm) only: eval.simps)
 apply  (rule substF_Pc)
 
 apply (rule ballI)
 apply (erule_tac P="ex' \<in> ?P" in rev_mp)
 apply (simp (no_asm) add: ran_del del_def filter.simps)
 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))

apply (simp only:)

apply (subgoal_tac "validF I (p', m, e') (substF NoPt [(V nat1, C (eval I (p, m, e) (V nat1 \<oplus> V nat2)))] Q) =
                    validF I (p', m[nat1 ::= (eval I (p, m, e) (V nat1 \<oplus> V nat2))], e') (substF NoPt [] Q)")
 prefer 2
 apply (rule substF_var_simp)

 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))

apply (simp only: substF_empty eval.simps Let_def split_def fst_conv snd_conv)
--{* SUB nat1 nat2 *}
apply (simp add: effS_def step_def wpF_def split_def Let_def)
apply (subgoal_tac "C (NAT (Suc 0)) = (C (NAT 1))")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p')), (V nat1, V nat1 \<ominus> V nat2)]")
 prefer 2
 apply (simp (no_asm) add: nojunk.simps)
apply (drule_tac I="I" and p="p" and m="m" and e="e" and f="Q"  in substF_eval_exTm)
apply (simp (no_asm) add: ran_def dom_def intVarsE.simps)
apply (simp only: map.simps split_def fst_conv snd_conv)
apply (subgoal_tac "
(validF I (p, m,e) (substF NoPt ((Tm, Tm \<oplus> C (NAT 1))#[(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat1, C (eval I (p, m, e) (V nat1 \<ominus>  V nat2)))]) Q)) =
(validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat1, C (eval I (p, m, e) (V nat1 \<ominus> V nat2)))] Q))")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and f="Q" in substF_Tm_NoPt)
 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))
 
 apply (drule sysinv_pres)
 apply assumption
 apply (case_tac "cs e")
 apply (erule_tac P="cs e= []" in rev_mp)
 apply (simp (no_asm))
 apply (case_tac "list")
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (erule_tac P="list =[]" in rev_mp)
 apply (simp (no_asm))

 apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
 apply (erule_tac P="list = ab # lista" in rev_mp)
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (simp (no_asm))
 apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
 apply (rule impI)+
 apply (erule conjE)+
 apply assumption
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e') (substF NoPt [(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat1, C (eval I (p, m, e) (V nat1 \<ominus> V nat2)))] Q) =
 validF I (p', m, e') (substF NoPt [(V nat1, C (eval I (p, m, e) (V nat1 \<ominus> V nat2)))] Q)")
 prefer 2
 apply (simp (no_asm) only: eval.simps)
 apply  (rule substF_Pc)
 
 apply (rule ballI)
 apply (erule_tac P="ex' \<in> ?P" in rev_mp)
 apply (simp (no_asm) add: ran_del del_def filter.simps)
 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))

apply (simp only:)

apply (subgoal_tac "validF I (p', m, e') (substF NoPt [(V nat1, C (eval I (p, m, e) (V nat1 \<ominus> V nat2)))] Q) =
                    validF I (p', m[nat1 ::= (eval I (p, m, e) (V nat1 \<ominus> V nat2))], e') (substF NoPt [] Q)")
 prefer 2
 apply (rule substF_var_simp)

 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))

apply (simp only: substF_empty eval.simps Let_def split_def fst_conv snd_conv)

--{* INC nat *}
apply (simp add: effS_def step_def wpF_def split_def Let_def)
apply (subgoal_tac "C (NAT (Suc 0)) = (C (NAT 1))")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p')), (V nat, Add (V nat) (C (NAT 1)))]")
 prefer 2
 apply (simp (no_asm) add: nojunk.simps)
apply (drule_tac I="I" and p="p" and m="m" and e="e" and f="Q"  in substF_eval_exTm)
apply (simp (no_asm) add: ran_def dom_def intVarsE.simps)
apply (simp only: map.simps split_def fst_conv snd_conv)
apply (subgoal_tac "
(validF I (p, m,e) (substF NoPt ((Tm, Tm \<oplus> C (NAT 1))#[(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat, C (eval I (p, m, e) (Add (V nat) (C (NAT 1))) ))]) Q)) =
(validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (eval I (p, m, e) (C (POS p')))),  (V nat, C (eval I (p, m, e) (Add (V nat) (C (NAT 1))) ))] Q))")
 prefer 2
 apply (rule_tac I="I" and p="p" and m="m" and e="e" and f="Q" in substF_Tm_NoPt)
 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))
 
 apply (drule sysinv_pres)
 apply assumption
 apply (case_tac "cs e")
 apply (erule_tac P="cs e= []" in rev_mp)
 apply (simp (no_asm))
 apply (case_tac "list")
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (erule_tac P="list =[]" in rev_mp)
 apply (simp (no_asm))

 apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
 apply (erule_tac P="list = ab # lista" in rev_mp)
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (simp (no_asm))
 apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
 apply (rule impI)+
 apply (erule conjE)+
 apply assumption
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e') (substF NoPt [(Pc, C (eval I (p, m, e) (C (POS p')))), (V nat, C (eval I (p, m, e) (Add (V nat) (C (NAT 1)))))] Q) =
 validF I (p', m, e') (substF NoPt [(V nat, C (eval I (p, m, e) (Add (V nat) (C (NAT 1)))))] Q)")
 prefer 2
 apply (simp (no_asm) only: eval.simps)
 apply  (rule substF_Pc)
 
 apply (rule ballI)
 apply (erule_tac P="ex' \<in> ?P" in rev_mp)
 apply (simp (no_asm) add: ran_del del_def filter.simps)
 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))

apply (simp only:)

apply (subgoal_tac "validF I (p', m, e') (substF NoPt [(V nat, C (eval I (p, m, e) (Add (V nat) (C (NAT 1)))))] Q) =
                    validF I (p', m[nat ::= (eval I (p, m, e) (Add (V nat) (C (NAT 1))))], e') (substF NoPt [] Q)")
 prefer 2
 apply (rule substF_var_simp)

 apply (simp (no_asm) add: ran_def dom_def)

 apply (simp (no_asm))

apply (simp only:)
apply (erule conjE)+
apply (simp only: substF_empty)
apply (drule_tac t="m'" in sym)
apply (subgoal_tac "Suc 0 = 1")
 prefer 2
 apply (simp (no_asm))
apply (simp only: eval.simps Let_def split_def fst_conv snd_conv)

--{* JMPEQ *}
apply (simp add: wpF_def split_def Let_def)
apply (subgoal_tac "Suc 0 =  1")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q) =
                    validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")  
 prefer 2
 apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))]")
  prefer 2
  apply (simp (no_asm) add: nojunk.simps)
 apply (simp only: substF_eval_exTm map.simps split_def fst_conv snd_conv)

 apply (subgoal_tac "validF I (p, m,e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)),(Pc, C (POS p'))] Q) =
validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")
  prefer 2
  apply (rule substF_Tm_NoPt)
  apply (rule_tac ballI)
  apply (erule_tac P="ex' \<in> ?A" in rev_mp)
  apply (simp (no_asm) add: ran_del del_def filter.simps)
  apply (simp (no_asm) add: ran_def dom_def)

  apply (simp (no_asm))
  apply (simp (no_asm) add: dom_def)

  apply (drule sysinv_pres)
  apply assumption
  apply (case_tac "cs e")
  apply (erule_tac P="cs e= []" in rev_mp)
  apply (simp (no_asm))
  apply (case_tac "list")
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (erule_tac P="list =[]" in rev_mp)
  apply (simp (no_asm))

  apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
  apply (erule_tac P="list = ab # lista" in rev_mp)
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (simp (no_asm))
  apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
  apply (rule impI)+
  apply (erule conjE)+
  apply assumption
 apply (simp only:)  
apply (subgoal_tac "validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, (C (POS p')))] Q) =
validF I (p', m,  e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply  (rule substF_Pc)
 apply (simp (no_asm) add: ran_def dom_def)
 
 apply (simp (no_asm))
apply (simp only: substF_empty)

apply (simp add: effS_def step_def split_def Let_def fst_conv snd_conv)
apply (case_tac "(\<exists>n. m nat1 = NAT n) \<and> (\<exists>n'. m nat2 = NAT n')")
apply simp
apply (case_tac "\<exists>n. m nat1 = NAT n \<and> m nat2 = NAT n")
apply simp

apply simp

apply simp
--{* JMPL nat1 nat2 nat3 *}
apply (simp add: wpF_def split_def Let_def)
apply (subgoal_tac "Suc 0 =  1")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q) =
                    validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")  
 prefer 2
 apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))]")
  prefer 2
  apply (simp (no_asm) add: nojunk.simps)
 apply (simp only: substF_eval_exTm map.simps split_def fst_conv snd_conv)

 apply (subgoal_tac "validF I (p, m,e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)),(Pc, C (POS p'))] Q) =
validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")
  prefer 2
  apply (rule substF_Tm_NoPt)
  apply (rule_tac ballI)
  apply (erule_tac P="ex' \<in> ?A" in rev_mp)
  apply (simp (no_asm) add: ran_del del_def filter.simps)
  apply (simp (no_asm) add: ran_def dom_def)

  apply (simp (no_asm))
  apply (simp (no_asm) add: dom_def)

  apply (drule sysinv_pres)
  apply assumption
  apply (case_tac "cs e")
  apply (erule_tac P="cs e= []" in rev_mp)
  apply (simp (no_asm))
  apply (case_tac "list")
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (erule_tac P="list =[]" in rev_mp)
  apply (simp (no_asm))

  apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
  apply (erule_tac P="list = ab # lista" in rev_mp)
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (simp (no_asm))
  apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
  apply (rule impI)+
  apply (erule conjE)+
  apply assumption
 apply (simp only:)  
apply (subgoal_tac "validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, (C (POS p')))] Q) =
validF I (p', m,  e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply  (rule substF_Pc)
 apply (simp (no_asm) add: ran_def dom_def)
 
 apply (simp (no_asm))
apply (simp only: substF_empty)

apply (simp add: effS_def step_def split_def Let_def fst_conv snd_conv)
apply (case_tac "(\<exists>n. m nat1 = NAT n) \<and> (\<exists>n'. m nat2 = NAT n')")
apply simp
apply (case_tac " \<exists>n. m nat1 = NAT n \<and> (\<exists>n'. m nat2 = NAT n' \<and> n < n')")
apply simp

apply simp

apply simp
--{* JLE *}
apply (simp add: wpF_def split_def Let_def)
apply (subgoal_tac "Suc 0 =  1")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q) =
                    validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")  
 prefer 2
 apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))]")
  prefer 2
  apply (simp (no_asm) add: nojunk.simps)
 apply (simp only: substF_eval_exTm map.simps split_def fst_conv snd_conv)

 apply (subgoal_tac "validF I (p, m,e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)),(Pc, C (POS p'))] Q) =
validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")
  prefer 2
  apply (rule substF_Tm_NoPt)
  apply (rule_tac ballI)
  apply (erule_tac P="ex' \<in> ?A" in rev_mp)
  apply (simp (no_asm) add: ran_del del_def filter.simps)
  apply (simp (no_asm) add: ran_def dom_def)

  apply (simp (no_asm))
  apply (simp (no_asm) add: dom_def)

  apply (drule sysinv_pres)
  apply assumption
  apply (case_tac "cs e")
  apply (erule_tac P="cs e= []" in rev_mp)
  apply (simp (no_asm))
  apply (case_tac "list")
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (erule_tac P="list =[]" in rev_mp)
  apply (simp (no_asm))

  apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
  apply (erule_tac P="list = ab # lista" in rev_mp)
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (simp (no_asm))
  apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
  apply (rule impI)+
  apply (erule conjE)+
  apply assumption
 apply (simp only:)  
apply (subgoal_tac "validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, (C (POS p')))] Q) =
validF I (p', m,  e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply  (rule substF_Pc)
 apply (simp (no_asm) add: ran_def dom_def)
 
 apply (simp (no_asm))
apply (simp only: substF_empty)

apply (simp add: effS_def step_def split_def Let_def fst_conv snd_conv)
apply (case_tac "(\<exists>n. m nat1 = NAT n) \<and> (\<exists>n'. m nat2 = NAT n')")
apply simp
apply (case_tac " \<exists>n. m nat1 = NAT n \<and> (\<exists>n'. m nat2 = NAT n' \<and> n \<le> n')")
apply simp

apply simp

apply simp
--{* JMPB *}
apply (simp add: wpF_def split_def Let_def)
apply (subgoal_tac "Suc 0 =  1")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q) =
                    validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")  
 prefer 2
 apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))]")
  prefer 2
  apply (simp (no_asm) add: nojunk.simps)
 apply (simp only: substF_eval_exTm map.simps split_def fst_conv snd_conv)

 apply (subgoal_tac "validF I (p, m,e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)),(Pc, C (POS p'))] Q) =
validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")
  prefer 2
  apply (rule substF_Tm_NoPt)
  apply (rule_tac ballI)
  apply (erule_tac P="ex' \<in> ?A" in rev_mp)
  apply (simp (no_asm) add: ran_del del_def filter.simps)
  apply (simp (no_asm) add: ran_def dom_def)

  apply (simp (no_asm))
  apply (simp (no_asm) add: dom_def)

  apply (drule sysinv_pres)
  apply assumption
  apply (case_tac "cs e")
  apply (erule_tac P="cs e= []" in rev_mp)
  apply (simp (no_asm))
  apply (case_tac "list")
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (erule_tac P="list =[]" in rev_mp)
  apply (simp (no_asm))

  apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
  apply (erule_tac P="list = ab # lista" in rev_mp)
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (simp (no_asm))
  apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
  apply (rule impI)+
  apply (erule conjE)+
  apply assumption
 apply (simp only:)  
apply (subgoal_tac "validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, (C (POS p')))] Q) =
validF I (p', m,  e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply  (rule substF_Pc)
 apply (simp (no_asm) add: ran_def dom_def)
 
 apply (simp (no_asm))
apply (simp only: substF_empty)

apply (simp add: effS_def step_def split_def Let_def fst_conv snd_conv)
--{* JMPI *}
apply (simp add: wpF_def split_def Let_def)
apply (subgoal_tac "Suc 0 =  1")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q) =
                    validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")  
 prefer 2
 apply (subgoal_tac "nojunk [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))]")
  prefer 2
  apply (simp (no_asm) add: nojunk.simps)
thm substF_eval_exTm
 apply (simp only: substF_eval_exTm map.simps split_def fst_conv snd_conv)

 apply (subgoal_tac "validF I (p, m,e) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)),(Pc, C (POS p'))] Q) =
validF I (p, m,e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")
  prefer 2
  apply (rule substF_Tm_NoPt)
  apply (rule_tac ballI)
  apply (erule_tac P="ex' \<in> ?A" in rev_mp)
  apply (simp (no_asm) add: ran_del del_def filter.simps)
  apply (simp (no_asm) add: ran_def dom_def)

  apply (simp (no_asm))
  apply (simp (no_asm) add: dom_def)

  apply (drule sysinv_pres)
  apply assumption
  apply (case_tac "cs e")
  apply (erule_tac P="cs e= []" in rev_mp)
  apply (simp (no_asm))
  apply (case_tac "list")
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (erule_tac P="list =[]" in rev_mp)
  apply (simp (no_asm))

  apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
  apply (erule_tac P="list = ab # lista" in rev_mp)
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (simp (no_asm))
  apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
  apply (rule impI)+
  apply (erule conjE)+
  apply assumption
 apply (simp only:)  
apply (subgoal_tac "validF I (p, m, e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, (C (POS p')))] Q) =
validF I (p', m,  e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply  (rule substF_Pc)
 apply (simp (no_asm) add: ran_def dom_def)
 
 apply (simp (no_asm))
apply (simp only: substF_empty)
apply (simp add: effS_def step_def split_def Let_def fst_conv snd_conv)
apply (case_tac "m nat")
apply simp
prefer 2
apply simp
apply simp
--{* CALL nat1 nat2 *}
apply (simp add: wpF_def split_def Let_def effS_def step_def)
apply (subgoal_tac "Suc 0 =  1")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (contextDn
                     (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Rp, C (POS (incA p))),
                        (Pc, C (POS p')), (V nat1, C (POS (fst p, Suc (snd p))))]
                       Q)) =  
validF I (p, m, e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr>) 
                     (substF NoPt [(Pc, C (POS p')), (V nat1, C (POS (fst p, Suc (snd p))))]
                       Q)")
 prefer 2
 apply (rule substF_Rp)
 
 apply (rule ballI)
 apply (subgoal_tac "V nat1 \<noteq> Pc")
  prefer 2
  apply (simp (no_asm))
 apply (simp only:  ran_del del_def filter.simps split_def fst_conv snd_conv simp_thms if_True set.simps)
 apply (simp only: ran_def dom_def map.simps set.simps)
 apply (simp only: mem_simps simp_thms)
 apply (erule disjE)
 apply (rule_tac x="(POS p')" in exI)
 apply (simp (no_asm))
 apply (rule_tac x="POS (fst p, Suc (snd p))" in exI)
 apply (simp (no_asm))

 apply (simp (no_asm))

 apply (case_tac "cs e")
 apply (erule_tac P="cs e = []" in rev_mp)
 apply (simp (no_asm))
 apply (case_tac "list")
 apply (erule_tac P="list = []" in rev_mp)
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (simp (no_asm))
 apply (drule sysinv_pres)
 apply assumption
 apply (erule_tac P="sysinv ?a" in rev_mp)
 apply (erule_tac P="list = ab # lista" in rev_mp)
 apply (erule_tac P="cs e = aa # list" in rev_mp)
 apply (simp (no_asm) add: Let_def split_def)
 apply (rule classical)
 apply (drule sysinv_pres)
 apply (assumption)
 apply (erule_tac P="sysinv ?a" in rev_mp)
 apply (erule_tac P="\<not> cs e \<noteq> []" in rev_mp)
 apply (simp (no_asm) )
apply (simp only: incA_def split_def fst_conv snd_conv simp_thms)
apply (subgoal_tac "validF I (p, m, e
               \<lparr>cs := (length (h e), m) # cs e,
                  h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS p')), (V nat1, C (POS (fst p, Suc (snd p))))] Q) =
         validF I (p', m, e
               \<lparr>cs := (length (h e), m) # cs e,
                  h := h e @ [p]\<rparr>) (substF NoPt [(V nat1, C (POS (fst p, Suc (snd p))))] Q)")
 prefer 2
 apply (rule substF_Pc)
 apply (rule ballI)
 apply (simp only: ran_del del_def filter.simps snd_conv fst_conv)
 apply (simp only: ran_def dom_def map.simps set.simps mem_simps simp_thms) 
 apply (rule_tac x="(POS (fst p, Suc (snd p)))" in exI)
 apply (simp (no_asm))
 
 apply (simp (no_asm))
apply (simp only:)
apply (subgoal_tac "  validF I (p', m, e
               \<lparr>cs := (length (h e), m) # cs e,
                  h := h e @ [p]\<rparr>) (substF NoPt [(V nat1, C (POS (fst p, Suc (snd p))))] Q) =
 validF I (p', m[nat1 ::= (POS (fst p, Suc (snd p)))], e
               \<lparr>cs := (length (h e), m) # cs e,
                  h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply (rule substF_var_simp)
 apply (simp (no_asm) add: dom_def ran_def)

 apply (simp (no_asm))
apply (simp only:)
apply (simp only: substF_empty simp_thms)
apply (erule conjE)+
apply (drule_tac t="p'" in sym)
apply (drule_tac t="m'" in sym)
apply (drule_tac t="e'" in sym)
apply (subgoal_tac "e\<lparr>cs := (length (h e), m) # cs e, h := h e @ [p]\<rparr> = e\<lparr>h := h e @ [p], cs := (length (h e), m) # cs e\<rparr>")
 prefer 2
 apply (simp (no_asm))
apply (simp only:)
--{* RET nat *}
apply (simp add: wpF_def split_def Let_def effS_def step_def)
apply (case_tac "m nat")
apply simp
apply simp
apply simp
apply (frule sysinv_pres)
apply assumption
apply (case_tac "cs e")
apply simp
 
apply (case_tac "list")
apply (simp add: Let_def split_def fst_conv snd_conv)
apply (erule conjE)+
apply (erule_tac x="snd p" in allE)
apply (erule_tac x="nat" in allE)
apply (subgoal_tac "(fst p,snd p) = p")
 prefer 2
 apply (simp (no_asm))
 apply simp

apply (simp add: Let_def split_def fst_conv snd_conv)
apply (erule conjE)+
apply (subgoal_tac "validF I (p, m, e) (contextOldUp (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q)) =
                    validF I (p, m, e\<lparr>cs := tl (cs e)\<rparr>) (substF NoPt [(Tm, Tm \<oplus> C (NAT 1)), (Pc, C (POS p'))] Q)")
 prefer 2
 apply (rule_tac k'="fst aa" and m'="snd aa" and k''="fst ab" and m''="snd ab" and css="lista" in substF_ContextOldUp)
 apply simp
 apply simp
 apply (rule impI)
 apply (case_tac "lista")
 apply simp
 apply simp
apply (subgoal_tac "NAT (Suc 0) = NAT  1")
  prefer 2
  apply simp
apply (simp only: simp_thms)
apply (subgoal_tac "validF I (p, m', e\<lparr>cs := tl (aa # ab # lista)\<rparr>) (substF NoPt ((Tm, Tm \<oplus> C (NAT 1))#[(Pc, C (POS p'))]) Q) = validF I (p, m', (e\<lparr>cs := tl (aa # ab # lista)\<rparr>)\<lparr>h:= (h (e\<lparr>cs := tl (aa # ab # lista)\<rparr>))@[p]\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q)")
 prefer 2
 apply (erule_tac V="NAT (Suc 0) = NAT 1" in thin_rl)
 apply (rule substF_Tm_NoPt)
 apply (rule ballI)
 apply (simp only: ran_del del_def filter.simps map.simps  mem_simps simp_thms)
 apply (simp only: ran_def dom_def snd_conv map.simps mem_simps set.simps simp_thms)
 apply (rule_tac x="POS p'" in exI)
 apply (simp (no_asm))

 apply (simp (no_asm))

 apply (simp (no_asm))
 apply (rule impI)
 apply (case_tac "lista")
 apply simp
 apply simp
apply (simp only: simp_thms)
apply (subgoal_tac "e\<lparr>cs := tl (aa # ab # lista),h := h (e\<lparr>cs := tl (aa # ab # lista)\<rparr>) @ [p]\<rparr> = 
e\<lparr>h := h e @ [p], cs := tl (aa # ab # lista)\<rparr>")
 prefer 2
 apply (simp (no_asm))
apply (simp only:)
apply (subgoal_tac "validF I (p, m', e\<lparr>h := h e @ [p], cs := tl (aa # ab # lista)\<rparr>) (substF NoPt [(Pc, C (POS p'))] Q) =
validF I (p', m', e\<lparr>h := h e @ [p], cs := tl (aa # ab # lista)\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply (rule substF_Pc)
 apply (simp (no_asm) add: ran_def dom_def)
 
 apply (simp (no_asm))

apply (simp only: substF_empty)
apply (drule_tac t="e'" in sym)
apply (drule_tac t="p'" in sym)
apply (drule_tac t="m'" in sym)
apply (simp only: tl.simps)
--{* MOV nat1 nat2 *}
apply (simp add: effS_def step_def wpF_def split_def Let_def)
apply (case_tac "m nat1")
apply simp
prefer 2
apply simp
--{* case m nat1 = NAT nat *}
apply simp
apply (case_tac "m nat2")
apply simp
prefer 2
apply simp
--{* case m nat2 = NAT nata *}
apply simp
apply (erule conjE)+
apply (drule_tac t="e'" in sym)
apply (drule_tac t="p'" in sym)
apply (drule_tac t="m'" in sym)
apply (simp only:)
apply (subgoal_tac "validF I (p, m, e) (substF (Mv nat1 nat2) [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS (fst p, Suc (snd p))))] Q) = 
validF I (p, m[nata ::= m nat], e) (substF NoPt [(Tm, Tm \<oplus> C (NAT (Suc 0))), (Pc, C (POS (fst p, Suc (snd p))))] Q)")
 prefer 2
 apply (rule substF_Mv_NoPt)
 apply assumption+
 apply (simp (no_asm))
apply (simp only:)
apply (subgoal_tac "validF I (p, m[nata ::= m nat], e) (substF NoPt ((Tm, Tm \<oplus> C (NAT 1))# [(Pc, C (POS (fst p, Suc (snd p))))]) Q) =
validF I (p, m[nata ::= m nat], e\<lparr> h:=(h e)@[p] \<rparr> ) (substF NoPt [(Pc, C (POS (fst p, Suc (snd p))))] Q)") 
 prefer 2
 apply (rule substF_Tm_NoPt)
  apply (rule_tac ballI)
  apply (erule_tac P="ex' \<in> ?A" in rev_mp)
  apply (simp (no_asm) add: ran_del del_def filter.simps)
  apply (simp (no_asm) add: ran_def dom_def)

  apply (simp (no_asm))

  apply (drule sysinv_pres)
  apply assumption
  apply (case_tac "cs e")
  apply (erule_tac P="cs e= []" in rev_mp)
  apply (simp (no_asm))
  apply (case_tac "list")
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (erule_tac P="list =[]" in rev_mp)
  apply (simp (no_asm))

  apply (erule_tac P="sysinv ((p,m,e),prg)" in rev_mp)
  apply (erule_tac P="list = ab # lista" in rev_mp)
  apply (erule_tac P="cs e = aa # list" in rev_mp)
  apply (simp (no_asm))
  apply (simp (no_asm) only: Let_def split_def fst_conv snd_conv)
  apply (rule impI)+
  apply (erule conjE)+
  apply assumption
apply simp

apply (subgoal_tac "validF I (p, m[nata ::= m nat], e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [(Pc, C (POS (fst p, Suc (snd p))))] Q) =
validF I ((fst p, Suc (snd p)), m[nata ::= m nat], e\<lparr>h := h e @ [p]\<rparr>) (substF NoPt [] Q)")
 prefer 2
 apply  (rule substF_Pc)
 
 apply (simp (no_asm) add: ran_def dom_def)
 apply (simp (no_asm) add: ran_del del_def filter.simps)
apply (simp only: substF_empty)
--{* HALT *}
apply (simp add: effS_def step_def split_def Let_def)
(*>*)
done

subsection {* Verifying succsF *}


lemma substE_contextUp_switch:
"substE NoPt [] (contextUpE ex) = contextUpE (substE NoPt [] ex)"
(*<*)
apply (simp only: substE_empty)
(*>*)
done

lemma intVarsE_contextUp:
"intVarsE (contextUpE expr) = intVarsE expr"
(*<*)
apply (induct expr)
apply (simp add: contextUpE_def) +
(*>*)
done

lemma freeIntVars_contextUp: 
"freeIntVars (contextUp form) = freeIntVars form"
(*<*)
apply (induct form)
apply (simp add: intVarsE_contextUp) +
(*>*)
done

lemma substF_contextUp_switch:
"substF NoPt [] (contextUp f) = contextUp (substF NoPt [] f)"
(*<*)
apply (simp add: substF_empty)
(*>*)
done

lemma eval_contextUpE:
"eval I (p, m, e) (contextUpE expr) = eval I (callstate e) expr"
(*<*)
apply (induct expr)
apply (simp add: contextUpE_def Let_def)+
(*>*)
done

lemma validF_contextUp:
"\<And> p m e I. validF I (p, m, e) (contextUp f) = validF I (callstate e) f"
(*<*)
apply (induct f)
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (drule_tac psi="(\<lambda> (l::form list). \<forall> p m e I. (validFs I (p,m,e) (contextUpL l)) = (validFs I (callstate e) l)) list" in asm_rl)
apply (erule_tac x="p" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="e" in allE)
apply (erule_tac x="I" in allE)
apply simp
prefer 10
apply simp
prefer 9
apply simp
--{* Impl *}
apply simp
--{* Neg *}
apply simp
--{* Eq expr1 expr2 *}
apply (simp add: eval_contextUpE)
--{* Leq expr1 expr2 *}
apply (simp add: eval_contextUpE)
--{* Less expr1 expr2 *}
apply (simp add: eval_contextUpE)
--{* Ty expr *}
apply (simp add: eval_contextUpE)
--{* Forall *}
apply simp
--{* Yields *}
apply (simp add: eval_contextUpE)
(*>*)
done

lemma jumptargets_valid:
"\<And> jt. \<lbrakk> validF I ((pn,i),m,e) A; m x = NAT n; jt = jumptargets pn x A; jt \<noteq> [] \<rbrakk> \<Longrightarrow> (pn,n) \<in> set jt" 
apply (induct A)
--{* T *}
apply simp
--{* F *}
apply simp
--{* And *}
apply (drule_tac psi="(\<lambda> l. \<forall> jt. validF I ((pn,i),m,e) (And l) \<longrightarrow> m x = NAT n \<longrightarrow> jt = jumptargets pn x (And l) \<longrightarrow> jt \<noteq> [] \<longrightarrow> (pn,n) \<in> set jt) list" in asm_rl)
apply simp
prefer 10
apply (simp add: Let_def)
apply (atomize)
apply (rule impI)+
apply (case_tac "jumptargets pn x form = []")
apply simp
--{* ~= [] *}
apply (erule_tac x="jumptargets pn x form" in allE)
apply simp

prefer 9
apply simp
--{* Imp *}
apply simp
--{* Neg *}
apply simp
--{* Eq *}
apply simp
--{* Leq *}
apply simp
--{* Less *}
apply simp
--{* Ty *}
apply simp
--{* Forall *}
apply simp
--{* Yields *}
apply simp
apply (case_tac "expr" )
apply simp
apply (case_tac "x = nat")
apply simp
apply (subgoal_tac "(pn,n) = (pn, nv (NAT n))")
 prefer 2
 apply (simp add: nv_def)
apply (simp only:)
apply (rule imageI)
apply (simp add: Let_def)
apply simp+
done


lemma succsF_complete:
"\<And> prg s s'. \<lbrakk> wf prg ; s \<in> (isafeP prg) ; (s,s') \<in> (effS prg) \<rbrakk> \<Longrightarrow> (\<exists> B. (fst s',B) \<in> set (succsF prg (fst s)) \<and> valid prg s B)"
(*<*)
apply (simp only: split_paired_all)
apply (rename_tac "prg" "pn" "i" "m" "e" "pn'" "i'" "m'" "e'")
apply (simp add: effS_def mem_Collect_eq)
apply (case_tac "cmd prg (pn,i)")
apply (simp add: step_def) 
--{* case: cmd prg (pn,i) = Some a *}
apply (case_tac "a")
--{* SET nat1 nat2 *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, i + 1), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: step_def del:cmd.simps)
apply (simp add: TrueF_def Let_def valid_def)
--{* ADD nat1 nat2 *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, i + 1), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: step_def del:cmd.simps)
apply (simp add: TrueF_def Let_def valid_def)
--{* SUB nat1 nat2 *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, i + 1), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: step_def del:cmd.simps)
apply (simp add: TrueF_def Let_def valid_def)
--{* INC nat *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, i + 1), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: step_def del:cmd.simps)
apply (simp add: TrueF_def Let_def valid_def)
--{* JMPEQ nat1 nat2 nat3 *}
apply (subgoal_tac "(succsF prg (pn,i)) =  [((pn, i + nat3), And [ (Ty (V nat1) Nat), (Ty (V nat2) Nat), (Eq (V nat1) (V nat2)), (Eq Pc (C (POS (pn,i))))]), ((pn, i + 1), And [ (Ty (V nat1) Nat), (Ty (V nat2) Nat), (Neg (Eq (V nat1) (V nat2))), (Eq Pc (C (POS (pn,i))))])
                     ]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv )
apply (case_tac "(\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n')")
apply (case_tac "(\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n' \<and> n = n')")
apply (rule_tac x="And [ (Ty (V nat1) Nat), (Ty (V nat2) Nat), (Eq (V nat1) (V nat2)), (Eq Pc (C (POS (pn,i))))]" in exI)
apply (erule conjE | erule exE)+
apply (simp add: valid_def Let_def step_def del:cmd.simps)
apply (rule_tac x=" And [ (Ty (V nat1) Nat), (Ty (V nat2) Nat), (Neg (Eq (V nat1) (V nat2))), (Eq Pc (C (POS (pn,i))))]" in exI)
apply (erule conjE | erule exE)+
apply (simp add: valid_def Let_def  step_def del:cmd.simps del: not_ex de_Morgan_conj)
apply (simp add: valid_def step_def del:cmd.simps del: not_ex de_Morgan_conj)
--{* JMPL nat1 nat2 nat3 *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, i + nat3), And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Less (V nat1) (V nat2)), (Eq  Pc (C (POS (pn,i))))]), ((pn, i + 1), And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Neg (Less (V nat1) (V nat2))), (Eq Pc (C (POS (pn,i))))])
                    ]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv )
apply (case_tac "(\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n')")
apply (case_tac "(\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n' \<and> n < n')")
apply (erule conjE | erule exE)+
apply (rule_tac x="And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Less (V nat1) (V nat2)), (Eq  Pc (C (POS (pn,i))))]" in exI)
apply (simp add: valid_def Let_def step_def nv_def del:cmd.simps)
apply (rule_tac x=" And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Neg (Less (V nat1) (V nat2))), (Eq Pc (C (POS (pn,i))))]" in exI)
apply (erule conjE | erule exE)+
apply (simp add: valid_def Let_def nv_def step_def del:cmd.simps del: not_ex de_Morgan_conj)
apply (simp add: valid_def step_def del:cmd.simps del: not_ex de_Morgan_conj)
--{* JLE nat1 nat2 nat3 *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, i + nat3), And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Leq (V nat1) (V nat2)), (Eq  Pc (C (POS (pn,i))))]), ((pn, i + 1), And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Neg (Leq (V nat1) (V nat2))), (Eq Pc (C (POS (pn,i))))])
                    ]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv )
apply (case_tac "(\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n')")
apply (case_tac "(\<exists>n n'. m nat1 = NAT n \<and> m nat2 = NAT n' \<and> n \<le>  n')")
apply (erule conjE | erule exE)+
apply (rule_tac x="And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Leq (V nat1) (V nat2)), (Eq  Pc (C (POS (pn,i))))]" in exI)
apply (simp add: valid_def Let_def step_def nv_def del:cmd.simps)
apply (rule_tac x=" And [(Ty (V nat1) Nat), (Ty (V nat2) Nat), (Neg (Leq (V nat1) (V nat2))), (Eq Pc (C (POS (pn,i))))]" in exI)
apply (erule conjE | erule exE)+
apply (simp add: valid_def Let_def nv_def step_def del:cmd.simps del: not_ex de_Morgan_conj)
apply (simp add: valid_def step_def del:cmd.simps del: not_ex de_Morgan_conj)
--{* JMPB nat *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn, (i::nat) - nat), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: TrueF_def Let_def valid_def step_def del:cmd.simps)
--{* JMPI nat *}
apply (simp add: step_def)
apply (case_tac "m nat")
apply simp
prefer 2
apply simp
apply simp
apply (subgoal_tac "((pn,nata), Eq (V nat) (C (NAT nata))) \<in> set (succsF prg (pn,i))")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
 apply (case_tac "anF prg (pn,i)")
 apply (simp add: wf_def)
 apply (frule domC_split)
 apply (erule exE)+
 apply (simp add: checkPos_split Let_def)
 --{* Some aa *}
 apply simp
 apply (erule_tac isafeP_elims)
 --{* initF case *}
 apply (drule_tac t="s'" in sym)
 apply (simp add: initF_def valid_def validF_validFs.simps Let_def split_def fst_conv snd_conv)
 apply (erule conjE)+
 apply (erule_tac x="I" in allE)
 apply (erule conjE)+
 apply (erule_tac x="NAT nat" in allE)
 apply (simp add: update_def Let_def)
 --{* isafeF case *}
 apply (simp add: isafeF_def)
 apply (case_tac "fst s'' mem domC prg")
 apply (drule_tac t="s''" in sym)
 apply (simp add: valid_def validF_validFs.simps Conj_def)
 apply (erule_tac x="I" in allE)+
 apply (erule conjE)+
 apply (subgoal_tac "(pn,nata) \<in> set (jumptargets pn nat aa)")
  prefer 2
  apply (rule_tac I="I" and A="aa" and jt="jumptargets pn nat aa" in jumptargets_valid)
  apply simp
  apply simp
  apply simp
  apply (simp add: wf_def)
  apply (frule domC_split, (erule exE)+)
  apply (simp only: checkPos_split Let_def)
  apply (erule conjE)+
  apply (simp add: checkPos.simps Let_def)
  apply (rule classical)
  apply simp
 apply simp
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply simp

 apply (simp add: valid_def FalseF_def)

apply (rule_tac x="V nat \<doteq> C (NAT nata)" in exI)
apply (simp add: valid_def validF_validFs.simps Let_def)

--{* CALL nat1 nat2 *}
apply (subgoal_tac "(succsF prg (pn,i)) = [((nat2, 0), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv )
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: TrueF_def  Let_def valid_def step_def del: cmd.simps)
--{* RET nat *}
--{* Proof Outline: 1) Show that sysinv and sysinv2 hold for the current state. Then we know that
                       program counter of the topmost callframe points to a call 
                       instruction for the current procedure (CALL x pn) and that the
                       the recorded call state is reachable from the initial state.
                    2) Show that safeS holds for the current state. Then we know
                       that the return address in register x conforms with the call
                       address we record in the callstack (cs e). 
                    3) From 1) and 2) we can conclude, that 
                       the static successor address (pn',i') is the return address
                       stored in register x. Hence the dynamic and static sucessor
                       are the same and the first part of B holds. 
                    4) Show that sysinv2 holds. Then we know that the current state is
                       reachble in n2 steps form the recorded call state, which is
                       reachable in n1 steps from the initial state s0, where n1 + n2 
                       = n. 
                    5) From 4) we conclude that the recorded call state satisfies
                       preF. This means it also satisfies the annotation attached to
                       this callpoint, which is the second condition of B. *} 
apply (subgoal_tac "sysinv(((pn,i),m,e),prg)")      
 prefer 2
 apply (rule sysinv_pres')
 apply assumption
 apply assumption

apply (subgoal_tac "\<exists> k' m' k'' m'' lista. cs e = (k',m')#(k'',m'')#lista")
 prefer 2
 apply (case_tac "cs e")
 apply simp
 --{* cs e = aa list *}
 apply (case_tac "list")
 apply (simp add: Let_def)
 --{* cs e = aa ab list *}
 apply (rule_tac x="fst aa" in exI)
 apply (rule_tac x="snd aa" in exI)
 apply (rule_tac x="fst ab" in exI)
 apply (rule_tac x="snd ab" in exI)
 apply (rule_tac x="lista" in exI)
 apply simp
apply (erule exE)+

apply (subgoal_tac "valid prg ((pn,i),m,e) (safeF prg (pn,i))")
 prefer 2
 apply (drule isafeP_elim)
 apply simp

 apply (case_tac "(pn,i) mem (domC prg)")
 apply (simp add: isafeF_def valid_def validF_validFs.simps Conj_def)

 apply (simp add: isafeF_def valid_def validF_validFs.simps FalseF_def)

apply (subgoal_tac "valid prg (\<pc> e,\<m> e,\<e> e) (isafeF prg (\<pc> e))")
 prefer 2
  apply (cut_tac sysinv2_pres)
  apply (erule_tac x="prg" in allE)
  apply (erule_tac x="((pn,i),m,e)" in allE)
  apply (drule mp, assumption)+
  apply (drule_tac P="\<lambda> s. s" in subst[OF sysinv2.simps]) 
  apply (simp add: safeF_def Let_def split_def fst_conv snd_conv callpc_def callmem_def callenv_def callstate_def del: sysinv.simps sysinv2.simps )

--{* main proof for RET *}
apply (simp add: step_def safeF_def sysinv.simps Let_def fst_conv snd_conv split_def)

apply (case_tac "m nat")
apply simp
apply simp
--{* m nat = POS x *}
apply simp
apply (erule conjE | erule exE)+
apply (simp add: callpc_def callmem_def callenv_def callstate_def Let_def split_def fst_conv snd_conv succsF_def valid_def validF_validFs.simps)


apply (drule_tac s="(pn',i')" and t="incA ((h e)! k')" in sym)
apply simp

apply (subgoal_tac "(h e) ! k' \<in> set (domC prg)")
 prefer 2
  --{* cmd domC instantiieren *} 
 apply (cut_tac cmd_domC)
 apply (erule_tac x="(CALL xa pn)" in allE)
 apply (erule_tac x="(h e) ! k'" in allE)
 apply (erule_tac x="prg" in allE)
 apply (drule mp, assumption)
 apply assumption

apply (subgoal_tac "(h e) ! k' \<in>set (callpoints prg pn)")
 prefer 2
 apply (simp only: callpoints_def)
 apply (simp only: set_filter mem_Collect_eq)
 apply (simp add: isCall_def)
apply (rule_tac x="let anF=(case (anF prg (h e ! k'))
                            of None \<Rightarrow> TrueF
                            | Some f \<Rightarrow> (contextUp f)
                           ) 
                    in (Conj [Eq (V nat) (C (POS (pn', i'))),(Eq Pc (C (POS (pn,i)))),anF])" in exI)
apply (rule conjI)
apply (subgoal_tac "\<exists> ys zs. (callpoints prg pn) = ys@(h e ! k')#zs")
 prefer 2
 apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: ret_succs_split Let_def split_def fst_conv snd_conv incA_def)
--{* second conjunct *}
apply (simp add: Let_def Conj_def del: sysinv2.simps sysinv.simps domC.simps isafe.simps anF.simps cmd.simps valid_def)
apply (case_tac "anF prg (h e ! k')" )
apply (simp add: TrueF_def)
apply (simp add: Let_def split_def fst_conv snd_conv isafeF_def isafe.simps set_mem_eq valid_def Conj_def)
apply (subgoal_tac "valid prg ((pn, i), m', e) (contextUp aa) = valid prg (callstate e) aa")
 prefer 2
 apply (simp only: valid_def)
 apply (rule doubleAllI)
 apply (rule allI)
 apply (rule validF_contextUp)
apply (simp add: valid_def callstate_def)
--{* MOV nat1 nat2 *}
apply (case_tac "m nat1")
apply (simp add: step_def)
prefer 2
apply (simp add: step_def)
apply (case_tac "m nat2")
apply (simp add: step_def)
prefer 2
apply (simp add: step_def)
apply (subgoal_tac "(succsF prg (pn,i)) = [((pn,i+1), Eq Pc (C (POS (pn,i))))]")
 prefer 2
 apply (simp add: succsF_def Let_def split_def fst_conv snd_conv)
apply (rule_tac x="Eq Pc (C (POS (pn,i)))" in exI)
apply (simp add: step_def Let_def valid_def validF_validFs.simps del:cmd.simps)
--{* HALT *}
apply (simp add: step_def)
(*>*)
done


subsection {* Instantianting the VCG Framework *}

--{* Show that this platform's safety logic agrees with the constraints the PCCFramework demands. *}

theorem SALAnnotationLogicIns:
"VerificationConditionGenerator Conj Impl TrueF FalseF valid provable effS wpF succsF initF ipc safeF anF domC wf"
(*<*)
apply (unfold VerificationConditionGenerator_def)
--{* SafetyLogic *}
apply (rule conjI)
apply (rule SALSafetyLogicIns)
--{* VerificationConditionGenerator *}
apply (unfold VerificationConditionGenerator_axioms_def)
apply (rule conjI)
--{* correctIpc *}
apply (rule allI)+
apply (simp add: valid_def initF_def ipc_def Let_def split_def fst_conv snd_conv)

apply (rule conjI)
--{* correctWpF *}
apply (rule allI)+
apply (rule impI)+
apply (simp only: split_paired_all)
apply (rule_tac prg="prg" and p="(a,b)" and m="aa" and e="ba" and Q="Q" in correctWpF)
apply assumption
apply (rule isafeP_imp_safeP)
apply (simp only: isafeP_def isafeF_def split_def)
apply (subgoal_tac "  (\<lambda>prg pc. isafe (fst (domC prg, prg, pc), fst (snd (domC prg, prg, pc)), anF (fst (snd (domC prg, prg, pc))),
                              snd (snd (domC prg, prg, pc)), \<FalseF>, Conj, Impl, safeF, succsF, wpF)) = isafeF")
 prefer 2
 apply (rule ext)
 apply (rule ext)
 apply (simp add: isafeF_def)
apply (simp only:)
apply assumption
apply assumption

apply (rule conjI)
--{* succsFcomplete *}
apply (rule allI)+
apply (rule impI)+
apply (rule succsF_complete)
apply assumption 
apply (simp only: isafeP_def isafeF_def split_def)
apply (subgoal_tac "  (\<lambda>prg pc. isafe (fst (domC prg, prg, pc), fst (snd (domC prg, prg, pc)), anF (fst (snd (domC prg, prg, pc))),
                              snd (snd (domC prg, prg, pc)), \<FalseF>, Conj, Impl, safeF, succsF, wpF)) = isafeF")
 prefer 2
 apply (rule ext)
 apply (rule ext)
 apply (simp add: isafeF_def)
apply (simp only:)
apply assumption

apply (rule conjI)
--{* correct Safety Logic *}
apply ((rule allI)+, (rule impI)+)
apply (rule correctSafetyLogic)
apply (simp add: provable_def)
apply (subgoal_tac "  (\<lambda>prg pc. isafe (fst (domC prg, prg, pc), fst (snd (domC prg, prg, pc)), anF (fst (snd (domC prg, prg, pc))),
                              snd (snd (domC prg, prg, pc)), \<FalseF>, Conj, Impl, safeF, succsF, wpF)) = isafeF")
 prefer 2
 apply (rule ext)
 apply (rule ext)
 apply (simp add: isafeF_def)
apply (simp only: isafeP_def fst_conv snd_conv split_def)

--{* correct_wf *}
apply (rule allI)
apply (rule impI)
apply (drule back_jumps_annotated)
apply (simp only: enoughAn_def isLoop_def noAnn_def)
apply (rule allI)
apply (rule impI)
apply clarify

apply (frule loop_has_back_jump)
apply assumption
apply (erule exE)
apply (erule conjE)
apply (frule_tac l="l" and prg="prg" and k="k" in path_succsF)
apply assumption
apply (erule exE)

apply (erule_tac x="(l!(k+1))" in allE)
apply (frule_tac x="l!(k+1)" in allE)
apply simp
apply (rotate_tac 3)
apply (erule_tac x="l!k" in allE)
apply (erule_tac x="B" in allE)
apply (subgoal_tac "l!(k+1) \<in> set l")
 prefer 2
 apply simp
apply clarify
apply (erule disjE)
apply (erule_tac x="(l ! (k + 1))" in allE)
apply simp
apply (erule_tac x="l ! k" in allE)
apply simp
(*>*)
done


section {* Platform Soundness *}

constdefs isSafe::"SALprogram \<Rightarrow> bool"
"isSafe \<equiv> \<lambda> prg. \<forall> s s'. prg,s \<Turnstile> initF prg \<and> (s,s') \<in> (effS prg)\<^sup>* \<longrightarrow> prg,s' \<Turnstile> safeF prg (fst s')" 

theorem platform_soundness:
"\<lbrakk> wf prg; provable prg (vcgSALDeep prg) \<rbrakk> \<Longrightarrow> isSafe prg"
(*<*)
apply (subgoal_tac "VerificationConditionGenerator Conj Impl TrueF FalseF valid provable effS wpF succsF initF ipc safeF anF domC wf")
 prefer 2
 apply (rule SALAnnotationLogicIns)
apply (drule_tac prg="prg" and anF="anF" in VerificationConditionGenerator.vcg_soundness)
apply assumption
apply (simp only: vcgSALDeep_def domA_def vcG_def)
apply (simp add: isSafe_def)
(*>*)
done

text {* Establish System Invariants *}

lemma vc_proof_startup:
"\<And> s. \<lbrakk> wf prg; s \<in> isafeP prg \<rbrakk> \<Longrightarrow> sysinv (s,prg) \<and> sysinv2 (s,prg) \<and> (\<exists> c css. cs (snd (snd s)) = c#css)"
(*<*)
apply (rule context_conjI)
 apply (rule sysinv_pres')
 apply assumption
 apply assumption
apply (rule context_conjI)
 apply (cut_tac sysinv2_pres)
 apply (erule_tac x="prg" in allE)
 apply (erule_tac x="s" in allE)
 apply (drule mp, assumption)+
 apply assumption
apply (case_tac "cs (snd (snd s))")
apply (simp add: sysinv.simps split_paired_all)
apply (rule_tac x="a" in exI)
apply (rule_tac x="list" in exI)
apply (case_tac "list")
apply (simp add: sysinv.simps Let_def split_def fst_conv snd_conv split_paired_all)
apply fastsimp
(*>*)
done



end