header {* 
  \isaheader{Jinja Assertion Language} 
*}

theory Form = FiniteMap + Value:

section {* Syntax of formulae *}

types var = nat

types 
--{* The position (C,M,n) identifies the n'th 
instruction in method M of class C. *}
pos = "cname \<times> mname \<times> nat"



datatype expr = Rg var | St var | Lv var | Cn val |                               
                NewA nat | Gf vname cname expr | FrNr |                           
                Num expr num_op expr | Rel expr rel_op expr |                     
                Ite expr expr expr  | Eq expr expr |                              
                Neg expr | Imp expr expr | And "expr list" | Forall var expr |    
                Ty expr "ty" | Pos pos |                   
                Call expr | Catch cname expr                                      


syntax Add_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<oplus>" 65)
translations "Add_ e1 e2" == "Num e1 Add e2"
syntax Sub_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<ominus>" 65)
translations "Sub_ e1 e2" == "Num e1 Sub e2" 
syntax Mult_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<otimes>" 65)
translations "Mult_ e1 e2" == "Num e1 Mult e2" 
syntax Ite_ ::"expr \<Rightarrow> expr \<Rightarrow> expr \<Rightarrow> expr" ( "(IF _ THEN _ ELSE _)" [60,60,60]60)
translations "Ite_ e1 e2 e3" == "Ite e1 e2 e3"
syntax Eq_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<doteq>" 65)
translations "Eq_ e1 e2" == "Eq e1 e2" 
syntax Imp_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<supset>" 65)
translations "Imp_ e1 e2" == "Imp e1 e2" 
syntax Leq_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<preceq>" 65)
translations "Leq_ e1 e2" == "Rel e1 Leq e2" 
syntax Less_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<prec>" 65)
translations "Less_ e1 e2" == "Rel e1 Less e2"
syntax Req_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<triangleq>" 65)
translations "Req_ e1 e2" == "Rel e1 Eql e2" 
syntax (latex) Geq_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<succeq>" 65)
translations "Geq_ e1 e2" == "Rel e1 Geq e2" 
syntax (latex) Grtr_ :: "expr \<Rightarrow> expr \<Rightarrow> expr" (infix "\<succ>" 65)
translations "Grtr_ e1 e2" == "Rel e1 Grtr e2"  
syntax TT :: "expr"
translations "TT" == "Cn (Bool True)"
syntax FF :: "expr"
translations "FF" == "Cn (Bool False)"

text {* Abbreviations *}

constdefs Or::"expr list \<Rightarrow> expr"
"Or exs \<equiv> Neg (And (map Neg exs))"

(*
constdefs
none::"expr"
"none \<equiv> Num (Cn (Intg 0)) Add (Cn (Bool True))" *)

--{* A wrong typed expression evaluating to None *}
syntax none :: "expr"
translations "none" == "Num (Cn (Intg 0)) Add (Cn (Bool True))"

--{* Note: Before we turned none into a syntax translation, we
modelled it as a constant and none_def was used in proofs. We
do not want to remove none_def from proofs, because we may need
to go back to the old definition of none in case syntax translations
turn out to be too inefficient. For the meantime none_def becomes
a dummy lemma. *}
  
lemma none_def:
"none \<noteq> Num (Cn (Intg 1)) Add (Cn (Bool True))"
(*<*) by simp (*>*)

constdefs not_none::"expr \<Rightarrow> expr"
"not_none ex \<equiv> Neg (Eq ex none)"

text {* \clearpage *}
section {* Extracting information from expressions *}

consts
foldE::"(expr \<times> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> expr \<Rightarrow> 'a"
foldEs::"(expr \<times> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> expr list \<Rightarrow> 'a"

primrec
"foldEs f c a [] = a"
"foldEs f c a (ex#exs) = c (foldE f c a ex) (foldEs f c a exs)"
"foldE f c a (And exs) = f (And exs, foldEs f c a exs)"
"foldE f c a (Rg k) = f (Rg k, a)"
"foldE f c a (St k) = f (St k, a)"
"foldE f c a (Lv k) = f (Lv k, a)"
"foldE f c a (Cn v) = f (Cn v, a)"
"foldE f c a (NewA n) = f (NewA n, a)"
"foldE f c a (Gf F C ex) = f (Gf F C ex, foldE f c a ex)"
"foldE f c a FrNr = f (FrNr,a)"
"foldE f c a (Num e no e')= f (Num e no e', c (foldE f c a e) (foldE f c a e'))"
"foldE f c a (Rel e1 ro e2) = f (Rel e1 ro e2, c (foldE f c a e1) (foldE f c a e2))"
"foldE f c a (Eq e1 e2) = f (Eq e1 e2, c (foldE f c a e1) (foldE f c a e2))"
"foldE f c a (Neg ex) = f (Neg ex,foldE f c a ex)"
"foldE f c a (Imp e1 e2) = f (Imp e1 e2,c (foldE f c a e1) (foldE f c a e2))"
"foldE f c a (Forall v ex) = f (Forall v ex, foldE f c a ex)"
"foldE f c a (Ite e1 e2 e3) =  f (Ite e1 e2 e3, c (c (foldE f c a e1) (foldE f c a e2)) (foldE f c a e3))"
"foldE f c a (Ty ex tp) = f (Ty ex tp,foldE f c a ex)"
"foldE f c a (Pos p) = f (Pos p, a)"
"foldE f c a (Call ex) = f (Call ex, foldE f c a ex)"
"foldE f c a (Catch cn ex) = f (Catch cn ex, foldE f c a ex)"


consts noCC::"expr \<times> 'a list \<Rightarrow> 'a list"

recdef noCC "{}"
"noCC (Call ex, as) = []"
"noCC (Catch cn ex, as) = []"
"noCC (oth, as) = as"

consts stkId::"(expr \<times> var list) \<Rightarrow> var list"
recdef stkId "{}"
"stkId (St k, as) = [k]"
"stkId (oth, as) = as"

constdefs
stkIds::"expr \<Rightarrow> var list"
"stkIds ex \<equiv> foldE (\<lambda>(ex,as). noCC (ex,stkId (ex,as))) (op @) [] ex"

consts rgId::"(expr \<times> var list) \<Rightarrow> var list"
recdef rgId "{}"
"rgId (Rg k, as) = [k]"
"rgId (oth, as) = as"

constdefs
rgIds::"expr \<Rightarrow> nat list"
"rgIds ex \<equiv> foldE (\<lambda>(ex,as). noCC (ex,rgId (ex,as))) (op @) [] ex"

consts gfEx::"(vname \<times> cname \<times> expr) \<Rightarrow> expr list"

recdef gfEx "{}"
"gfEx (F,C,Gf F' C' ex) = (if F=F' \<and> C=C' then [ex] else [])"
"gfEx (F,C,oth) = []"

constdefs
getGfEx::"vname \<Rightarrow> cname \<Rightarrow> expr \<Rightarrow> expr list"
"getGfEx F C ex \<equiv> foldE (\<lambda>(ex,as). as @ gfEx(F,C,ex)) (op @) [] ex"

consts newEx::"expr \<Rightarrow> nat list"

recdef newEx "{}"
"newEx (NewA n) = [n]"
"newEx oth = []"

constdefs 
getNewEx::"expr \<Rightarrow> nat list"
"getNewEx ex \<equiv> foldE (\<lambda>(ex,as). newEx ex @ as) (op @) [] ex"

consts callEx::"expr \<Rightarrow> expr list"
recdef callEx "{}"
"callEx (Call ex) = [ex]"
"callEx oth = []"

constdefs
getCallEx::"expr \<Rightarrow> expr list"
"getCallEx ex \<equiv> foldE (\<lambda>(ex,as). callEx ex @ noCC (ex,as)) (op @) [] ex"

consts catchEx::"expr \<Rightarrow> (cname \<times> expr) list"
recdef catchEx "{}"
"catchEx (Catch cn ex) = [(cn,ex)]"
"catchEx oth = []"

constdefs
getCatchEx::"expr \<Rightarrow> (cname \<times> expr) list"
"getCatchEx ex \<equiv> foldE (\<lambda>(ex,as). catchEx ex @ noCC (ex,as)) (op @) [] ex"

consts posEx::"expr \<Rightarrow> pos list"
recdef posEx "{}"
"posEx (Pos p) = [p]"
"posEx oth = []"

constdefs
getPosEx::"expr \<Rightarrow> pos list"
"getPosEx ex \<equiv> foldE (\<lambda>(ex,as). posEx ex @ noCC (ex,as)) (op @) [] ex"

constdefs
subExpr::"expr \<Rightarrow> expr list"
"subExpr ex \<equiv> foldE (\<lambda>(ex,as). ex#noCC(ex,as)) (op @) [] ex"

consts logV::"expr \<Rightarrow> var list"
recdef logV "{}"
"logV (Lv k) = [k]"
"logV (Forall k ex) = [k]"
"logV oth = []"

constdefs
logVarsE :: "expr \<Rightarrow> var list"
"logVarsE ex \<equiv> foldE (\<lambda>(ex,as). logV ex @ as) (op @) [] ex"

consts
bindsVar ::"expr \<Rightarrow> var option"

recdef bindsVar "{}"
"bindsVar (Forall v ex) = Some v"
"bindsVar oth = None"

constdefs
freeLvs:: "expr \<Rightarrow> var list"
"freeLvs ex \<equiv> foldE (\<lambda>(ex,as). (case bindsVar ex of None \<Rightarrow> as@(logV ex)
                                                 | Some v \<Rightarrow> [x\<in>as. x\<noteq>v])) (op @) [] ex"

consts
extractEq::"(expr \<times> expr) \<Rightarrow> expr option"

recdef extractEq "measure (\<lambda> (ex,ex'). size ex)"
"extractEq (And [],ex) = None"
"extractEq (And (ex'#exs),ex) = (case extractEq (ex',ex) 
 of None \<Rightarrow> extractEq (And exs,ex) | Some ex'' \<Rightarrow> Some ex'')"
"extractEq (Eq ex' ex'',ex) = (if ex'=ex then Some ex'' else None)" 
"extractEq (ex',ex) = None"

consts
isNegTy::"(expr \<times> expr) \<Rightarrow> bool"

recdef isNegTy "measure (\<lambda> (ex',ex). size ex')"
"isNegTy (Neg (Ty ex tp),ex') = (ex = ex')"
"isNegTy (oth,ex') = False"

consts
extractTy::"(expr \<times> expr) \<Rightarrow> ty list"

--{* extractTy (ex,ex') lists the possible types of ex' in a state that satisfies ex *}

recdef extractTy "measure (\<lambda> (ex',ex). size ex')"
"extractTy (And [],ex) = []"
"extractTy (And (ex'#exs),ex) = extractTy (ex',ex) @ extractTy (And exs,ex)"
"extractTy (Ty ex' tp,ex) = (if ex'=ex then [tp] else [])" 
"extractTy (Neg (And []),ex) = []"
"extractTy (Neg (And (Neg ex'#exs)),ex) = (if (list_all (\<lambda> ex''. isNegTy (ex'',ex)) (Neg ex'#exs)) then (extractTy (ex',ex) @ extractTy (Neg (And exs),ex)) else [])"
"extractTy (oth, ex) = []"
(hints cong del:  option.weak_case_cong)

constdefs eqExMps::"(expr ~~> expr) \<Rightarrow> (expr ~~> expr) \<Rightarrow> expr \<Rightarrow> bool"
"eqExMps em em' ex \<equiv> foldE (\<lambda>(ex,a). em ? ex = em' ? ex \<and> list_all (\<lambda>x. x) (noCC (ex,[a]))) (op \<and>) True ex"

datatype heapexpr = GF vname cname expr | TY expr "ty"

consts heapEx::"expr \<Rightarrow> heapexpr list"

recdef heapEx "{}"
"heapEx (Gf F C ex) = [GF F C ex]"
"heapEx (Ty ex ty) = [TY ex ty]"
"heapEx oth        = []"

constdefs
getHeapEx::"expr \<Rightarrow> heapexpr list"
"getHeapEx ex \<equiv> foldE (\<lambda>(ex,as). as @ heapEx ex) (op @) [] ex"

text {* \clearpage *}
section {* Substitution Function *}

consts 
substE::"(expr ~~> expr) \<Rightarrow> expr \<Rightarrow> expr"
substEs::"(expr ~~> expr) \<Rightarrow> expr list  \<Rightarrow> expr list"

primrec 
substEs_Nil: "substEs em [] = []"
substEs_Cons: "substEs em (ex#exs) = (substE em ex)#(substEs em exs)"

substE_Rg: "substE em (Rg k) = em ?\<^sub>= (Rg k)"
substE_St: "substE em (St k) = em ?\<^sub>= (St k)"
substE_Lv: "substE em (Lv k) = em ?\<^sub>= (Lv k)"
substE_Cn: "substE em (Cn tv) = em ?\<^sub>= (Cn tv)"
substE_NewA: "substE em (NewA n) = em ?\<^sub>= (NewA n)"
substE_Gf: "substE em (Gf F C ex) = (case em ? (Gf F C ex) 
                          of None \<Rightarrow> Gf F C (substE em ex)
                          | Some ex' \<Rightarrow> ex')"
substE_FrNr: "substE em FrNr = em ?\<^sub>= FrNr"
substE_Num: "substE em (Num e1 no e2) = (case em ? (Num e1 no e2) 
                             of None \<Rightarrow> Num (substE em e1) no (substE em e2)
                             | Some ex' \<Rightarrow> ex')"

substE_Rel: "substE em (Rel e1 ro e2) = (case em ? (Rel e1 ro e2) 
                             of None \<Rightarrow> Rel (substE em e1) ro (substE em e2)
                             | Some ex' \<Rightarrow> ex')"

substE_Ite: "substE em (Ite b t e) = (case em ? (Ite b t e)
 of None \<Rightarrow> Ite (substE em b) (substE em t) (substE em e) 
| Some ex' \<Rightarrow> ex')"

substE_Eq: "substE em (Eq e1 e2) = (case em ? (Eq e1 e2)
                         of None \<Rightarrow> Eq (substE em e1) (substE em e2)
                         | Some ex' \<Rightarrow> ex')"

substE_Neg: "substE em (Neg ex) = (case em ? (Neg ex)
                         of None \<Rightarrow> Neg (substE em ex)
                         | Some ex' \<Rightarrow> ex')"

substE_Imp: "substE em (Imp e1 e2) = (case em ? (Imp e1 e2)
                         of None \<Rightarrow> Imp (substE em e1) (substE em e2)
                         | Some ex' \<Rightarrow> ex')"

substE_And: "substE em (And exs) = And (substEs em exs)"

substE_Forall: "substE em (Forall v ex) = (case em ? (Forall v ex)
                            of None \<Rightarrow> Forall v (substE em ex)
                            | Some ex' \<Rightarrow> ex')"

substE_Ty: "substE em (Ty ex tp) = (case em ? (Ty ex tp)
                            of None \<Rightarrow> Ty (substE em ex) tp
                            | Some ex' \<Rightarrow> ex')"

substE_Pos: "substE em (Pos p) =  em ?\<^sub>= (Pos p)"

substE_Call: "substE em (Call ex) = em ?\<^sub>= (Call ex)"

substE_Catch: "substE em (Catch cn ex) = em ?\<^sub>= (Catch cn ex)"

section {* Auxiliary Lemmas *}


lemma expr_induct: 
"\<lbrakk>\<And>nat. P1 (Rg nat); 
  \<And>nat. P1 (St nat); 
  \<And>nat. P1 (Lv nat); 
  \<And>val. P1 (Cn val); 
  \<And> n. P1 (NewA n);
  \<And>list1 list2 expr. P1 expr \<Longrightarrow> P1 (Gf list1 list2 expr); 
  P1 FrNr;
  \<And>expr1 num_op expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (Num expr1 num_op expr2);
  \<And>expr1 rel_op expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (Rel expr1 rel_op expr2);
  \<And>expr1 expr2 expr3. \<lbrakk>P1 expr1; P1 expr2; P1 expr3\<rbrakk> \<Longrightarrow> 
    P1 (IF expr1 THEN expr2 ELSE expr3);
  \<And>expr1 expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (expr1 \<doteq> expr2); 
  \<And>expr. P1 expr \<Longrightarrow> P1 (Neg expr);
  \<And>expr1 expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (expr1 \<supset> expr2); 
  \<And>nat expr. P1 expr \<Longrightarrow> P1 (Forall nat expr); 
  \<And>expr ty. P1 expr \<Longrightarrow> P1 (Ty expr ty); 
  \<And>x. P1 (Pos x);
  \<And>expr. P1 expr \<Longrightarrow> P1 (Call expr); 
  \<And>list expr. P1 expr \<Longrightarrow> P1 (Catch list expr);
  \<And>expr es. \<lbrakk>\<forall>ex \<in> set es. P1 ex\<rbrakk> \<Longrightarrow> P1 (And es)\<rbrakk>
\<Longrightarrow> P1 expr"
(*<*)
apply (subgoal_tac "P1 expr \<and> (\<forall>ex\<in>set []. P1 ex)")
 prefer 2
 apply (rule_tac ?P1.0="P1" and ?P2.0="\<lambda>l. (\<forall>ex \<in> set l. P1 ex)" in expr.induct)
 apply simp+
done
(*>*)


lemma expr_induct': 
"\<lbrakk>\<And>nat. P1 (Rg nat); 
  \<And>nat. P1 (St nat); 
  \<And>nat. P1 (Lv nat); 
  \<And>val. P1 (Cn val); 
  \<And> n. P1 (NewA n);
  \<And>list1 list2 expr. P1 expr \<Longrightarrow> P1 (Gf list1 list2 expr); 
  P1 FrNr;
  \<And>expr1 num_op expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (Num expr1 num_op expr2);
  \<And>expr1 rel_op expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (Rel expr1 rel_op expr2);
  \<And>expr1 expr2 expr3. \<lbrakk>P1 expr1; P1 expr2; P1 expr3\<rbrakk> \<Longrightarrow> P1 (IF expr1 THEN expr2 ELSE expr3);
  \<And>expr1 expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (expr1 \<doteq> expr2); 
  \<And>expr. P1 expr \<Longrightarrow> P1 (Neg expr);
  \<And>expr1 expr2. \<lbrakk>P1 expr1; P1 expr2\<rbrakk> \<Longrightarrow> P1 (expr1 \<supset> expr2); 
  \<And>nat expr. P1 expr \<Longrightarrow> P1 (Forall nat expr); 
  \<And>expr ty. P1 expr \<Longrightarrow> P1 (Ty expr ty); 
  \<And>x. P1 (Pos x);
  \<And>expr. P1 expr \<Longrightarrow> P1 (Call expr); 
  \<And>list expr. P1 expr \<Longrightarrow> P1 (Catch list expr);
  \<And>expr ex es. \<lbrakk> P1 ex; P1 (And es)\<rbrakk> \<Longrightarrow> P1 (And (ex#es)); 
  P1 (And [])\<rbrakk>
\<Longrightarrow> P1 expr"
(*<*)
apply (subgoal_tac "P1 expr \<and> (P1 (And []))")
 prefer 2
 apply (rule_tac ?P1.0="P1" and ?P2.0="\<lambda>l. P1 (And l)" in expr.induct)
 apply simp+
done
(*>*)


consts parts::"expr \<Rightarrow> expr list"
primrec
"parts (Rg k) = []"
"parts (St k) = []"
"parts (Lv k) = []"
"parts (Cn v) = []"
"parts (NewA n)  = []"
"parts (Gf F C ex) = [ex]"
"parts FrNr   = []"
"parts (Num e1 no e2) = [e1,e2]"
"parts (Rel e1 ro e2) = [e1,e2]"
"parts (Ite e1 e2 e3) = [e1,e2,e3]"
"parts (Eq e1 e2)     = [e1,e2]"
"parts (Neg ex)       = [ex]"
"parts (Imp e1 e2)    = [e1,e2]"
"parts (And es)       = es"
"parts (Forall k ex)  = [ex]"
"parts (Ty ex tp)     = [ex]"
"parts (Pos p)        = []"
"parts (Call ex)      = []"
"parts (Catch X ex)   = []"

lemma getExpr_refl: "ex \<in> set (subExpr ex)"
(*<*)
apply (rule expr_induct)
apply (simp add: subExpr_def)+
done
(*>*)


lemma subExpr_And_cons:
"subExpr (And (ex#es)) = 
 [And (ex#es)] @ (subExpr ex @ (tl (subExpr (And es))))"
(*<*)
apply (simp add: subExpr_def)
done
(*>*)


lemma subExpr_And_in_list:
"ex \<in> set es \<Longrightarrow> ex \<in> set (tl (subExpr (And es)))"
(*<*)
apply (erule rev_mp)
apply (induct_tac "es")
apply simp

apply (rule impI)
apply (simp only: subExpr_And_cons)
apply simp
apply (erule disjE)
apply (simp add: getExpr_refl)

apply simp
done
(*>*)


lemma subExpr_And_map:
"subExpr (And es) = And es # (concat (map subExpr es))"
(*<*)
apply (induct_tac es)
apply (simp add: subExpr_def)

apply (simp only: subExpr_And_cons)
apply simp
done
(*>*)

lemma subExpr_Gf:
"\<And> ex' ex''. \<lbrakk> ex' \<in> set (subExpr ex); ex'' \<in> set (parts ex') \<rbrakk> 
 \<Longrightarrow> ex'' \<in> set (subExpr ex)"
(*<*)
apply (erule_tac P="ex'' \<in> set (parts ex')" in rev_mp)
apply (erule rev_mp)
apply (rule_tac expr="ex" in  expr_induct)
--{* Rg *}
apply (simp add: subExpr_def)
--{* St *}
apply (simp add: subExpr_def)
--{* Lv *}
apply (simp add: subExpr_def)
--{* Cn *}
apply (simp add: subExpr_def)
--{* NewA *}
apply (simp add: subExpr_def)
--{* Gf list1 list2 expr *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (erule disjE)
apply (cut_tac ex="expr" in getExpr_refl)
apply (simp add: subExpr_def parts.simps)

apply (simp add: subExpr_def parts.simps)
--{* FrNr *}
apply (simp add: subExpr_def parts.simps)
--{* Num expr1 numop expr2 *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)+
apply (simp add: parts.simps)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply (simp add: getExpr_refl)

apply (erule disjE)
apply simp

apply simp
--{* Rel expr1 relop expr2 *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)+
apply (simp add: parts.simps)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply (simp add: getExpr_refl)

apply (erule disjE)
apply simp

apply simp
--{* IF expr1 THEN expr2 ELSE expr3 *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)+
apply (simp add: parts.simps)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply (erule disjE)
apply (simp add: getExpr_refl)

apply (simp add: getExpr_refl)

apply (erule disjE)+
apply simp

apply (erule disjE)
apply simp

apply simp
--{* Eq expr1 expr2 *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)+
apply (simp add: parts.simps)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply (simp add: getExpr_refl)

apply (erule disjE)
apply simp

apply simp
--{* Neg expr *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply simp
--{* Imp expr1 expr2 *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)+
apply (simp add: parts.simps)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply (simp add: getExpr_refl)

apply (erule disjE)
apply simp

apply simp
--{* Forall nat expr *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply simp
--{* Ty expr ty *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
apply (fold subExpr_def)
apply (erule disjE)
apply (simp add: getExpr_refl)

apply simp
--{* Pos *}
apply (simp add: subExpr_def)
--{* Call *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
--{* Catch list expr *}
apply (rule impI)+
apply (simp add: subExpr_def parts.simps)
--{* And list *}
apply (rule impI)+
apply (simp only: subExpr_And_map)
apply simp
apply (erule disjE)

apply (simp add: parts.simps)

apply (erule_tac x="ex''" in ballE)

apply (rule disjI2)
apply (rule_tac x="ex''" in bexI)
apply (simp add: getExpr_refl)

apply assumption
apply simp

apply (erule bexE)
apply (erule_tac x="a" in ballE)
apply (rule disjI2)
apply (rule_tac x="a" in bexI)
apply simp
apply assumption
apply simp
done
(*>*)


lemma subExpr_rgIds: 
"Rg k \<in> set (subExpr ex) \<Longrightarrow> k \<in> set (rgIds ex)"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def rgIds_def | fastsimp)+
done
(*>*)


lemma subExpr_stkIds: 
"St k \<in> set (subExpr ex) \<Longrightarrow> k \<in> set (stkIds ex)"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def stkIds_def | fastsimp)+
done
(*>*)


lemma subExpr_NewEx: 
"NewA n \<in> set (subExpr ex) \<Longrightarrow> n \<in> set (getNewEx ex)"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: getNewEx_def subExpr_def | fastsimp)+
done
(*>*)


lemma subExpr_getCatchEx: 
"Catch X ex \<in> set (subExpr ex') \<Longrightarrow> (X,ex) \<in> set (getCatchEx ex')"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def getCatchEx_def | fastsimp)+
done
(*>*)


lemma subExpr_getCallEx: 
"Call ex \<in> set (subExpr ex') \<Longrightarrow> ex \<in> set (getCallEx ex')"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def getCallEx_def | fastsimp)+
done
(*>*)


lemma subExpr_getGfEx: 
"Gf F C ex  \<in> set (subExpr ex') \<Longrightarrow> ex \<in> set (getGfEx F C ex')"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def getGfEx_def | fastsimp)+
done
(*>*)


lemma subExpr_getHeapEx: 
"Gf F C ex  \<in> set (subExpr ex') \<Longrightarrow> GF F C ex \<in> set (getHeapEx ex')"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def getHeapEx_def | fastsimp)+
done
(*>*)


lemma subExpr_getHeapEx_TY:
"Ty ex ty \<in> set (subExpr ex') \<Longrightarrow> TY ex ty \<in> set (getHeapEx ex')"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def getHeapEx_def | fastsimp)+
done
(*>*)


lemma eqExMps_Call:
"eqExMps em em' (Call ex) = (em ? (Call ex) = em' ? (Call ex))"
(*<*)
apply (simp add: eqExMps_def)
done
(*>*)


lemma eqExMps_Catch:
"eqExMps em em' (Catch X ex) = (em ? (Catch X ex) = em' ? (Catch X ex))"
(*<*)
apply (simp add: eqExMps_def)
done
(*>*)


lemma eqExMps_And':
"eqExMps em em' (And es) = ((em ? (And es) = em' ? (And es)) \<and> 
 (\<forall>ex \<in> set es. eqExMps em em' ex))"
(*<*)
apply (simp add: eqExMps_def simp_thms)
apply (case_tac "em ? And es = em' ? And es")
prefer 2
apply simp

apply simp

apply (induct_tac "es")
apply simp

apply simp
done
(*>*)

lemma substE_empty:
"substE [] ex = ex"
(*<*)
apply (induct ex rule: expr_induct)
apply (simp add: id_lookup_def del_def)+
apply (erule rev_mp)
apply (induct_tac es)
apply simp
apply simp
done
(*>*)


lemma substEs_map:
"substEs em es = map (substE em) es"
(*<*)
apply (induct_tac es)
apply simp
apply simp
done
(*>*)


lemma foldEs_append:
"\<lbrakk> \<forall>ex. c a ex = ex; \<forall> ex ex' ex''. c ex (c ex' ex'') = c (c ex ex') ex'' \<rbrakk>
\<Longrightarrow> (foldEs f c a (es@es')) = c (foldEs f c a es) (foldEs f c a es')"
(*<*)
apply (induct_tac es)
apply simp

apply simp
done
(*>*)


lemma substE_eq:
"eqExMps em em' ex \<Longrightarrow> substE em ex = substE em' ex" 
(*<*)
apply (erule rev_mp)
apply (rule_tac expr="ex" in expr_induct)
apply (simp add: eqExMps_def substE_substEs.simps id_lookup_def)+

apply (rule impI)
apply (simp add: substEs_map)

--{* And case *}
apply (rule ballI)
apply (erule_tac x="x" in ballE)
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: foldE_foldEs.simps)
apply (subgoal_tac "\<forall>ex. (op \<and>) True ex = ex")
 prefer 2
 apply simp
apply (subgoal_tac "\<forall> ex ex' ex''. (op \<and>) ex ((op \<and>) ex' ex'') = (op \<and>) ((op \<and>) ex ex') ex''")
 prefer 2
 apply simp
apply (drule_tac es="ys" and es'="x # zs" and f="(\<lambda>(ex, a). em ? ex = em' ? ex \<and> list_all (\<lambda>x. x) (noCC (ex, [a])))" in foldEs_append)
apply simp
apply (erule conjE)
apply (simp only: foldE_foldEs.simps)
apply (simp only: simp_thms)

apply simp
done
(*>*)


lemma eqExMps_ren:
"\<lbrakk> ex = ex'; eqExMps em em' ex'\<rbrakk> \<Longrightarrow> eqExMps em em' ex"
(*<*)
by simp
(*>*)

end