Theory CertifSafeToSVM

(*  Title:      Certificate Safe to SVM
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  June 2008, Universidad Complutense de Madrid
*)



header {* Certification of the translation CoreSafe to SVM *}

theory CertifSafeToSVM
imports Main "../CoreSafe/SafeRASemantics" SVMSemantics CoreSafeToSVM CertifSafeToSVM_definitions
        execSVMBalanced_lemmas diff_lemmas maxFreshCells_lemmas maxFreshWords_lemmas
        identityEnvironment_lemmas basic_properties
begin



subsection {* Big-step semantics enriched with resource consumption *}

declare envAdd.simps [simp del]
declare envSearch.simps [simp del]
declare decreasing.simps [simp del]
declare addEnv_good.simps [simp del]
declare rho_good.simps [simp del]


(* Lemmas for closureCalled *)

lemma closureCalled_e1:
  "closureCalled e1 defs ⊆ closureCalled (Let x1 = e1 In e2 a) defs"
apply (rule subsetI)
apply (erule closureCalled.induct)
 apply (rule closureCalled.init,simp)
by (simp, rule closureCalled.step, assumption+,simp)  


lemma closureCalled_e2:
  "closureCalled e2 defs ⊆ closureCalled (Let x1 = e1 In e2 a) defs"
apply (rule subsetI)
apply (erule closureCalled.induct)
 apply (rule closureCalled.init,simp)
by (simp, rule closureCalled.step, assumption+,simp) 

lemma closureCalled_case_aux [rule_format]:
  "i < length alts -->  alts ! i = (p, ei)  --> f ∈ called ei --> f ∈ calledList alts"
apply (induct alts arbitrary: i,simp)
apply (rule impI)+
apply simp
apply (case_tac i)
 apply (rule disjI1,simp)
by (rule disjI2,simp)

lemma closureCalled_case:
  "[|i < length alts; 
   alts ! i =  (ConstrP C ps ms, ei) |]
   ==> closureCalled ei defs ⊆ closureCalled (Case VarE x a Of alts a') defs"
apply (rule subsetI)
apply (erule closureCalled.induct)
 apply (rule closureCalled.init,simp)
 apply (rule closureCalled_case_aux,assumption+)
by (simp, rule closureCalled.step, assumption+,simp)  

lemma closureCalled_case_1_x:
  "[|i < length alts; 
   alts ! i =  (ConstP p, ei) |]
   ==> closureCalled ei defs ⊆ closureCalled (Case VarE x a Of alts a') defs"
apply (rule subsetI)
apply (erule closureCalled.induct)
 apply (rule closureCalled.init,simp)
 apply (rule closureCalled_case_aux,assumption+)
by (simp, rule closureCalled.step, assumption+,simp) 


lemma closureCalled_cased_aux [rule_format]:
  "i < length alts -->  alts ! i = (p, ei)  --> f ∈ called ei --> f ∈ calledList' alts"
apply (induct alts arbitrary: i,simp)
apply (rule impI)+
apply simp
apply (case_tac i)
 apply (rule disjI1,simp)
by (rule disjI2,simp)

lemma closureCalled_cased:
  "[|i < length alts; 
   alts ! i =  (ConstrP C ps ms, ei) |]
   ==> closureCalled ei defs ⊆ closureCalled (CaseD VarE x a Of alts a') defs"
apply (rule subsetI)
apply (erule closureCalled.induct)
 apply (rule closureCalled.init,simp)
 apply (rule closureCalled_cased_aux,assumption+)
by (simp, rule closureCalled.step, assumption+,simp)  


(* Lemmas for extendsL *)

lemma disjointDomain:
  "p ∉ dom m ==> ((n ++ m) p) = (n p)"
apply (unfold map_add_def)
by (case_tac "(m p)", simp, simp add: dom_def)


lemma extendsL_append:
  "disjointList c c' ==> extendsL (c @ c') cs = (extendsL c cs ∧ extendsL c' cs)"
apply (simp add: extendsL_def add: extends_def add: disjointList_def, auto)
apply (erule_tac x="x" in ballE, simp, simp add: dom_def)
apply (erule_tac x="x" in ballE)
apply (subgoal_tac "x ∉ dom (map_of c)") 
apply (frule_tac n="(map_of c')" in  disjointDomain, simp)
apply (blast,simp)
apply (erule conjE, simp add: dom_def)
apply (erule_tac x="x" in ballE, simp) defer
apply (erule_tac x="x" in ballE)
apply (erule_tac x="x" in ballE, simp, simp add: dom_def)
apply (erule_tac x="x" in ballE, simp)
by (frule_tac n="map_of c'" in disjointDomain, simp, clarsimp, clarsimp)


lemma extendsL_e1:
  "[|disjointList (cs2 @ [(q2, is2, fname)])  (cs1' @ [(q1, is', fname)]);
   (cs2 @ (q2, is2, fname) # cs1' @ [(q1, is', fname)]) \<sqsubseteq> cs|] 
   ==> (cs1' @ [(q1, is', fname)]) \<sqsubseteq> cs"
by (frule_tac cs="cs" in extendsL_append, simp)

lemma extendsL_e2:
  "[| disjointList (cs2 @ [(q2, is2, fname)])  (cs1' @ [(q1, is', fname)]); 
   (cs2 @ (q2, is2, fname) # cs1' @ [(q1, is', fname)]) \<sqsubseteq> cs|] 
   ==> (cs2 @ [(q2, is2, fname)]) \<sqsubseteq> cs"
by (frule_tac cs="cs" in extendsL_append, simp)


lemma extendsL_case:
  "[| subList (csi @ [(qs ! i, isi, fname)]) cs1; q ∉ dom (map_of cs1);
    i < length alts; qs!i ∉ dom (map_of cs1);
    (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs|] 
   ==> (csi @ [(qs ! i, isi, fname)]) \<sqsubseteq> cs"
apply (simp add: subList.simps, elim exE)
apply (subgoal_tac "disjointList cs1 [(q, is', fname)]",simp)
by (simp add: disjointList_def)


(* Lemmas for rho *)

lemma rho1:
  "length rho > 0 ==> topDepth (rho++) = 0"
by (induct rho, simp, simp add: envPlusPlus.simps, auto)

lemma rho2:
 " 0 < length rho ==>  0 < length (rho ++)"
by (induct rho, simp, simp add: envPlusPlus.simps, auto)


lemma rho3 [rule_format]:
  " 0 < length rho --> td = topDepth rho --> rho_good rho
   -->  td + 1 = topDepth (rho + [(x1, 1)])"
apply (induct rho, simp, clarsimp)
by (simp add: rho_good.simps add: envAdd.simps add: envSearch.simps)

lemma rho_case [rule_format]:
  "0 < length rho -->  td = topDepth rho --> rho_good rho -->  nr = int (length xs) 
   --> nat (int td + nr) =  topDepth (rho + zip xs (decreasing (length xs)))"
apply (induct rho xs rule: list_induct2',simp_all)
apply clarsimp
apply (simp add: rho_good.simps add: envAdd.simps add: envSearch.simps)
apply clarsimp
apply (simp add: rho_good.simps add: envAdd.simps add: envSearch.simps)
apply (simp add: Let_def)
apply (subgoal_tac "length (decreasing (Suc (length ys))) = Suc (length ys)",simp)
apply (induct_tac ys, simp)
by (subst decreasing.simps,simp)+


lemma length_decreasing_add_assoc:
"length (decreasing (length xs + length rs)) = length xs + length rs"
apply (induct xs rs rule:list_induct2', simp_all)
   apply (subst decreasing.simps,simp)
  apply (subst decreasing.simps, simp, subst length_decreasing_eq_length, simp)
 apply (subst decreasing.simps, simp, subst length_decreasing_eq_length, simp)
by (subst decreasing.simps,simp)+



(* Lemmas for drop *)

lemma drop_general:
  "drop n xs = y#ys ==> drop (Suc n) xs = ys"
apply (induct xs arbitrary: n)
apply simp
apply (simp add:drop_Cons)
apply (simp split:nat.splits)
done

lemma nth_drop':
  "i < length xs ==> drop i xs = xs ! i # drop (Suc i) xs"
apply (induct i arbitrary: xs)
apply (simp add: neq_Nil_conv)
apply (erule exE)+
apply simp
apply (case_tac xs)
apply simp_all
done

lemma equals_dom_map_upd_none: 
  "dom (λa. if a = x then None else m a) = dom (m(x := None))"
by (auto, split split_if_asm, simp, simp)

lemma dom_map_insert:
 "dom (λa. if a = x then Some z else m a) = insert x (dom m)"
by(auto simp add:dom_def)


declare envPlusPlus.simps [simp del]
declare envAdd.simps [simp del]
declare restrictToRegion.simps [simp del]
declare sizeST.simps [simp del]
declare maxFreshCells.simps [simp del]
declare maxFreshWords.simps [simp del]



lemma correctness [rule_format]:
 "(E1,E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r  --> 
  finite (dom h') -->
  (∀ x∈ varProg e. x≠ self) -->
  fvReg e ⊆ dom (snd (E1,E2)) -->
  fv e ⊆ dom (fst (E1,E2)) -->
  self ∈ dom (snd (E1,E2)) -->
  boundVar e ∩ dom (snd (E1,E2)) = {} -->
    (closureCalled e defs ⊆ definedFuns defs
  ∧ ((p, funm, contm), codes) = mapAccumL trF (1, empty, []) defs
  ∧ cs = concat codes 
  ∧ P = ((cs, contm),p,ct,st)
  ∧ finite (dom h) 
  -->
          (∀ rho S S' k0 s0 p' q ls is is' cs1 j tds.
            (q, ls, is, cs1) = trE p' funm fname rho e 
          ∧ (append cs1  [(q,is',fname)]) \<sqsubseteq> cs 
          ∧ drop j is' = is
          ∧  (E1,E2) \<Join> (rho,S)
          ∧ td = topDepth rho 
          ∧ k0 ≤ k 
          ∧ S' = drop td S 
          ∧ s0 = ((h, k), k0, (q, j), S) 
          -->
              (∃ q' i s ss δ m w. 
                     P\<turnstile>s0 , td#tds -svm-> s # ss, Suc 0#tds 
              ∧ s = ((h', k) \<down> k0, k0, (q', i), Val v # S')
              ∧ fst (the (map_of cs q'))!i = POPCONT
              ∧ r = (δ,m,w)
              ∧ δ = diff k (h,k) (h',k)
              ∧ m = maxFreshCells (rev (s#ss))
              ∧ w = maxFreshWords (rev (s#ss)))))"
apply (rule impI)
apply (erule SafeRASem.induct)


(* (ConstE (LitN i) a) *)
apply (rule impI)+
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (rule_tac x=q in exI)
apply (rule_tac x="Suc (Suc (Suc j))" in exI)
apply (rule_tac x="((h, k) \<down> k0, k0, (q, Suc (Suc (Suc j))), Val (IntT i) # S')" in exI)
apply (rule_tac x="[((h, k), k0, (q, j+2), Val (IntT i) # drop (topDepth rho) S),
                    ((h, k), k0, (q, j+1), Val (IntT i) # S),
                    ((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="[]k" in exI)
apply (rule_tac x="0" in exI)
apply (rule_tac x="1" in exI)
apply (frule execSVMBalanced_IntT) apply (assumption+) apply (erule conjE)
apply (rule conjI, simp)
apply (rule conjI, simp)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_IntT)
apply (rule conjI, rule maxFreshCells_IntT, assumption+)
apply (frule lengthS_topDepth)
apply (rule maxFreshWords_IntT) apply (assumption+, simp)


(* (ConstE (LitB b) a) *)
apply (rule impI)+
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (rule_tac x=q in exI)
apply (rule_tac x="Suc (Suc (Suc j))" in exI)
apply (rule_tac x="((h, k) \<down> k0, k0, (q, Suc (Suc (Suc j))), Val (BoolT b) # S')" in exI)
apply (rule_tac x="[((h, k), k0, (q, j+2), Val (BoolT b) # drop (topDepth rho) S),
                    ((h, k), k0, (q, j+1), Val (BoolT b) # S),
                    ((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="[]k" in exI)
apply (rule_tac x="0" in exI)
apply (rule_tac x="1" in exI)
apply (frule execSVMBalanced_BoolT, assumption+, erule conjE)
apply (rule conjI, assumption)
apply (rule conjI, simp)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_BoolT)
apply (rule conjI, rule maxFreshCells_BoolT, assumption+)
apply (frule lengthS_topDepth)
apply (rule maxFreshWords_BoolT,assumption+, simp)


(*  (VarE x a) *)
apply (rule impI)+
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (rule_tac x=q in exI)
apply (rule_tac x="Suc (Suc (Suc j))" in exI)
apply (rule_tac x="((h, k) \<down> k0, k0, (q, Suc (Suc (Suc j))), Val (Val.Loc pa) # S')" in exI)
 apply (rule_tac x="[((h, k), k0, (q, j+2), Val (Val.Loc pa) # drop (topDepth rho) S),
                     ((h, k), k0, (q, j+1), Val (Val.Loc pa) # S),
                     ((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="[]k" in exI)
apply (rule_tac x="0" in exI)
apply (rule_tac x="1" in exI)
apply (frule rho_good, elim conjE)
apply (frule lengthS_topDepth)
apply (frule execSVMBalanced_VarE, assumption+, erule conjE)
apply (rule conjI, assumption)
apply (rule conjI, simp)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_VarE)
apply (rule conjI, rule maxFreshCells_VarE, assumption+)
apply (frule lengthS_topDepth)
apply (rule maxFreshWords_VarE,assumption+, simp)


(* (x @ r a) *)
apply (rule impI)+
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule A7)
apply (elim conjE)
apply (rule_tac x=q in exI)
apply (rule_tac x="(Suc (Suc (Suc (Suc ja))))" in exI)
apply (rule_tac x="((h', k) \<down> k0, k0, (q, (Suc (Suc (Suc (Suc ja))))), Val (Val.Loc p') # S')" in exI)
 apply (rule_tac x="[((h', k), k0, (q, Suc (Suc (Suc ja))), Val (Loc p') # drop (topDepth rho) S),
                           ((h', k), k0, (q, Suc (Suc ja)), Val (Loc p') # S),
                           ((h, k), k0, (q, Suc ja), Val (Loc pa) # Reg j #  S),
                           ((h, k), k0, (q, ja), S)]" in exI)
apply (rule_tac x="[j \<mapsto> m]" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="2" in exI)
apply (frule rho_good, elim conjE)
apply (frule lengthS_topDepth)
apply (frule_tac k0'="k0" in execSVMBalanced_CopyE, assumption+, erule conjE)
apply (rule conjI, assumption)
apply (rule conjI, simp)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_CopyE, assumption+)
apply (rule conjI, rule maxFreshCells_CopyE, assumption+)
apply (frule lengthS_topDepth)
apply (rule maxFreshWords_CopyE,assumption+, simp)


(* (ReuseE x a) *)
apply (rule impI)+
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (rule_tac x=qa in exI)
apply (rule_tac x="(Suc (Suc (Suc (Suc j))))" in exI)
apply (rule_tac x="(((h(pa:=None))(q\<mapsto>c), k) \<down> k0, k0, (qa, Suc (Suc (Suc (Suc j)))), Val (Loc q) # S')" in exI)
apply (rule_tac x="[(((h(pa:=None))(q\<mapsto>c), k), k0, (qa, Suc (Suc (Suc j))), Val (Loc q) # drop (topDepth rho) S),
                      (((h(pa:=None))(q\<mapsto>c), k), k0, (qa, Suc (Suc j)), Val (Loc q) # S), 
                      ((h, k), k0, (qa, Suc j), Val (Loc pa) # S),
                      ((h, k), k0, (qa, j), S)]" in exI)
apply (rule_tac x="[]k" in exI)
apply (rule_tac x="0" in exI)
apply (rule_tac x="1" in exI)
apply (frule rho_good, elim conjE)
apply (frule lengthS_topDepth)
apply (frule execSVMBalanced_ReuseE, assumption+, erule conjE)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_ReuseE, assumption+)
apply (rule conjI, rule maxFreshCells_ReuseE, assumption+)
apply (frule lengthS_topDepth)
apply (rule maxFreshWords_ReuseE,simp,assumption)


(* Let 1 *)
apply (rule impI)+ apply(elim conjE)
apply (rule allI)+ apply (rule impI, elim conjE)
apply (frule trE_let, simp, elim exE)

apply (erule_tac x="C" in allE)
 apply (erule_tac x=" h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}" in allE)
apply (erule_tac x="as" in allE)
 apply (erule_tac x="v1" in allE)
apply (erule_tac x="r1" in allE)
apply (erule_tac x="a'" in allE)
apply (elim conjE)


apply (frule_tac e="e1" in finite_dom_h,elim conjE) 
apply (frule_tac e="e2" in finite_dom_h,elim conjE)
apply (frule finite_dom_h') apply assumption
 apply (drule mp,assumption)+
 apply (drule mp, rule x_not_self, rule all_exp_core)+
 apply (drule mp,simp)+
 apply (subst dom_map_insert, assumption)
 apply (drule mp,simp)+
 apply (subgoal_tac "closureCalled e1 defs ⊆ closureCalled (Let x1 = e1 In e2 a) defs") 
  prefer 2 apply (rule closureCalled_e1) 
 apply (erule subset_trans, assumption)
apply (drule mp, simp)
 apply (subgoal_tac "closureCalled e2 defs ⊆ closureCalled (Let x1 = e1 In e2 a) defs") 
  prefer 2 apply (rule closureCalled_e2)
 apply (erule subset_trans, assumption)


apply (erule_tac x="(rho++)" in allE)         (* rho de e1 *)
 apply (erule_tac x="(rho+[(x1,1)])" in allE) (* rho de e2 *)

apply (erule_tac x=" Cont (k0,q2) # S" in allE)  (* S de e1 *)
apply (erule_tac x="(Val v1#S)" in allE)         (* S de e2 *) 

apply (erule_tac x="drop 0 (Cont (k0,q2) # S)" in allE)  (* S' de e1 *)
apply (erule_tac x="S'" in allE) (* S' de e2 *)  

apply (erule_tac x="k" in allE)   (* k0 de e1 *)
apply (erule_tac x="k0" in allE)  (* K0 de e2 *)

apply (erule_tac x="((h, k), k, (q1, j+1), Cont (k0,q2) # S)" in allE)  (* s0 de e1 *)
apply (erule_tac x="(( h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S)" in allE)

apply (erule_tac x="(q2+1)" in allE)  
apply (erule_tac x="p'" in allE) 

apply (erule_tac x="q1" in allE)
apply (erule_tac x="q2" in allE)

apply (erule_tac x="ls1" in allE)
apply (erule_tac x="ls2" in allE)

apply (erule_tac x="is1" in allE)
apply (erule_tac x="is2" in allE)

apply (erule_tac x="is'" in allE)
apply (erule_tac x="is2" in allE)

apply (erule_tac x="cs1'" in allE)
apply (erule_tac x="cs2" in allE)

apply (erule_tac x="j+1" in allE)
apply (erule_tac x="0" in allE)

apply (erule_tac x="td#tds" in allE)
apply (erule_tac x="tds" in allE)


apply (drule mp) (* HI e1 *)
apply (frule rho_good, elim conjE)
 apply (rule conjI) apply assumption 
 apply (rule conjI) apply (frule_tac ?cs2.0="cs2" and cs1'="cs1'" in codestore_let_disjoint, assumption+)
                    apply (simp, elim conjE, erule extendsL_e1, assumption+) 
 apply (rule conjI) apply (simp, erule drop_general) 
 apply (rule conjI) apply (erule identityEnvironment_e1, assumption+)
 apply (rule conjI) apply (rule sym, erule rho1)
 apply (rule conjI) apply simp
 apply (rule conjI) apply simp 
 apply simp

apply (drule mp) (* HI e2 *)
apply (frule rho_good, elim conjE)
 apply (rule conjI) apply assumption
 apply (rule conjI) apply (frule_tac ?cs2.0="cs2" and cs1'="cs1'" in codestore_let_disjoint, assumption+)
                    apply (simp, elim conjE, erule extendsL_e2, assumption+) 
 apply (rule conjI) apply simp 
 apply (rule conjI) apply (erule identityEnvironment_e2,assumption+,clarsimp,assumption+,simp)
 apply (rule conjI) apply (erule rho3,assumption+)
 apply (rule conjI) apply assumption
 apply (rule conjI) apply simp
 apply (rule refl)


(* Demostracion por hipotesis *)
apply (elim exE)
apply (elim conjE)

apply (rule_tac x="q'a" in exI)
apply (rule_tac x="ia" in exI)

(* Estado final *)
apply (rule_tac x="sa" in exI)

(* Estados intermedios *)
apply (rule_tac x=" ssa @
                    ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # drop 0 (Cont (k0,q2) # S)) # ss @
                    [((h,k),k0,(q,j), S)]" in exI)
apply (rule_tac x="δ1 ⊕ δ2" in exI)
apply (rule_tac x=" max m1 (m2 + \<parallel> δ1 \<parallel>)" in exI)
apply (rule_tac x=" max (s1 + 2) (s2 + 1)" in exI)
apply (rule conjI, frule execSVMBalanced_Let1, assumption+, simp)
apply (rule conjI, assumption) 
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_Let1, assumption+)
apply (frule_tac v="v1" in resources_gre_0) apply (elim exE, elim conjE)
apply (frule_tac v="v2" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI, rule maxFreshCells_Let1, assumption+, simp, simp, simp)
apply (rule maxFreshWords_Let1,assumption+, simp)




(* Let2 *)
apply (rule impI)+ apply (elim conjE)
apply (rule allI)+ apply (rule impI, elim conjE)
apply (frule trE_let2, elim exE)

apply (frule_tac e="e2" in finite_dom_h,elim conjE)
apply (drule mp, rule finite_dom_h', assumption, simp)
apply (drule mp, rule x_not_self, rule all_exp_core)
apply (drule mp, simp)+
apply (subst dom_map_insert, assumption)
apply (drule mp, simp)
apply (drule mp, simp)
apply (drule mp)
apply (rule conjI)
 apply (subgoal_tac "closureCalled e2 defs ⊆ closureCalled (Let x1 = ConstrE C as r a' In e2 a) defs") 
  prefer 2 apply (rule closureCalled_e2)
 apply (erule subset_trans, assumption) 
apply (frule finite_dom_h) apply (erule conjI)+ 
apply (elim conjE,assumption)

apply (erule_tac x="(rho+[(x1,1)])" in allE) (* rho de e2 *)
apply (erule_tac x="( Val (Loc pa) #S)" in allE)         (* S de e2 *) 
apply (erule_tac x="S'" in allE) (* S' de e2 *)  
apply (erule_tac x="k0" in allE)  (* K0 de e2 *)
apply (erule_tac x="((h(pa \<mapsto> (j, C, map (atom2val E1) as)), k), k0, (q, Suc ja), Val (Loc pa) # S)" in allE)  (* s0 de e2 *)

apply (erule_tac x="p'" in allE) 


apply (erule_tac x="q" in allE)
apply (erule_tac x="ls2" in allE)
apply (erule_tac x="is2" in allE)
apply (erule_tac x="is'" in allE)
apply (erule_tac x="cs2" in allE)
apply (erule_tac x="Suc ja" in allE)
apply (erule_tac x="tds" in allE)


apply (drule mp) (* HI e2 *)
apply (frule rho_good, elim conjE)
 apply (rule conjI) apply simp
 apply (rule conjI) apply simp 
 apply (rule conjI) apply simp
                    apply (rule drop_general,assumption)
 apply (rule conjI) apply (erule identityEnvironment_e2_let2,assumption+,simp,assumption+,simp)
 apply (rule conjI) apply (erule rho3,assumption+)
 apply (rule conjI) apply assumption
 apply (rule conjI) apply simp   
 apply (rule refl)
 apply (elim exE)
 apply (elim conjE)

apply (rule_tac x="q'" in exI)
apply (rule_tac x="i" in exI)

apply (rule_tac x="sa" in exI)
apply (rule_tac x=" ss @ [((h, k), k0, (q, ja), S)]" in exI)
apply (rule_tac x="δ ⊕ [j \<mapsto> 1]" in exI)
apply (rule_tac x=" m + 1" in exI)
apply (rule_tac x="s+1" in exI)

apply (frule rho_good, elim conjE)
apply (frule finite_dom_h) apply (elim conjE)
apply (subgoal_tac "core (Let x1 = ConstrE C as r a' In e2 a)")
prefer 2 apply (rule all_exp_core)
apply (frule let_atoms,elim conjE)
apply (rule conjI, rule execSVMBalanced_Let2,assumption+) 
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, rule diff_Let2,assumption+)
apply (frule_tac v="v2" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI, rule maxFreshCells_Let2, assumption+, simp, simp)
apply (rule maxFreshWords_Let2,assumption+,simp)



(* (Case VarE x a Of alts a') *)
apply (rule impI)+
apply (elim conjE)

apply (rule allI)+
apply (rule impI, elim conjE)

apply (erule_tac x="pa" in allE)
apply (erule_tac x="extend E1 xs vs" in allE)
apply (erule_tac x="xs" in allE)
apply (erule_tac x="vs" in allE)
apply (erule_tac x="j" in allE)
apply (erule_tac x="C" in allE)
apply (elim conjE)

apply (frule trE_case, assumption+)
apply (elim exE, elim conjE) 

apply (frule finite_dom_h,elim conjE)
apply (drule mp, simp) 
apply (drule mp, simp) apply (rule x_not_self, rule all_exp_core)
apply (drule mp, simp)+ 
 apply (subgoal_tac "closureCalled ei defs ⊆ closureCalled (Case VarE x a Of alts a') defs") 
  prefer 2 apply (rule closureCalled_case,assumption+) 
 apply (erule subset_trans, assumption)

apply (frule case_constructor_good,assumption+)

apply (erule_tac x="rho + zip xs (decreasing (length xs))" in allE) (* rho de ei *)
apply (erule_tac x="map Val vs @ S" in allE)       (* S de ei. *) 
apply (erule_tac x="drop (nat (int td + nr)) (map Val vs @ S)" in allE) (* S' *)
apply (erule_tac x="k0" in allE)  (* K0 de ei *)
apply (erule_tac x="((h, k), k0, (qs!i, 0), ( map Val vs) @ S)" in allE)  (* s0 de ei *)

apply (erule_tac x="p'" in allE) 
apply (erule_tac x="qs!i" in allE) (* antes q *)
apply (erule_tac x="lss!i" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="csi" in allE)
apply (erule_tac x="0" in allE)
apply (erule_tac x="tds" in allE)


apply (drule mp) (* HI ei *)
apply (frule rho_good, elim conjE)
apply (frule codestore_case_alts_disjoint, rule disjI1, rule refl, assumption+, elim conjE) 
 apply (rule conjI) apply simp (* traduccion *)
 apply (rule conjI) apply (rule extendsL_case, assumption+,simp,assumption+,simp,assumption)
 apply (rule conjI) apply simp
 apply (rule conjI) apply (rule identityEnvironment_case,simp,assumption+)
                    apply (rule addEnv_rho_good, assumption+,simp)
 apply (rule conjI) apply (rule rho_case, assumption+, simp, unfold def_extend_def, elim conjE, simp)
 apply (rule conjI) apply assumption
 apply (rule conjI) apply (rule refl)
 apply (rule refl)


 apply (elim exE)
 apply (elim conjE)

apply (rule_tac x="q'" in exI)
apply (rule_tac x="ia" in exI)

apply (rule_tac x="sa" in exI)
apply (rule_tac x=" ss @ [((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="δ" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="s+nr" in exI)


apply (rule conjI) apply (frule rho_good, elim conjE)
                   apply (rule execSVMBalanced_Case ,assumption+)
apply (erule_tac V="(qs ! i, lss ! i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei" in thin_rl)
apply (rule conjI) apply (subgoal_tac "(nat (int td + int (length vs)) - length vs) =
                    (nat (int td + int (length vs) - int (length vs)))",simp,simp)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, simp)
apply (frule_tac v="v" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI) apply (rule maxFreshCells_Case, assumption+, simp)
apply (rule maxFreshWords_Case,assumption+,simp,assumption)



(* (Case VarE x a Of alts a') (LitN n) *)
apply (rule impI)+
apply (elim conjE)

apply (erule_tac x="n" in allE)
apply (elim conjE)

apply (rule allI)+
apply (rule impI, elim conjE)

apply (frule trE_case_1_1, assumption+)
apply (elim exE, elim conjE) 
apply (frule finite_dom_h,elim conjE)
apply (drule mp, simp) 
apply (drule mp, simp, rule x_not_self, rule all_exp_core)
apply (drule mp, simp)+
 apply (subgoal_tac "closureCalled ei defs ⊆ closureCalled (Case VarE x a Of alts a') defs") 
  prefer 2 apply (rule closureCalled_case_1_x,assumption+) 
 apply (erule subset_trans, assumption)

apply (erule_tac x="rho" in allE) (* rho de ei *)
apply (erule_tac x="S" in allE)       (* S de ei. *) 
apply (erule_tac x="drop td S" in allE) (* S' *)
apply (erule_tac x="k0" in allE)  (* K0 de ei *)
apply (erule_tac x="((h, k), k0, (qs!i, 0),  S)" in allE)  (* s0 de ei *)

apply (erule_tac x="p'" in allE) 
apply (erule_tac x="qs!i" in allE) (* antes q *)
apply (erule_tac x="lss!i" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="csi" in allE)
apply (erule_tac x="0" in allE)
apply (erule_tac x="tds" in allE)


apply (drule mp) (* HI ei *)
apply (frule codestore_caseL_alts_disjoint, assumption+, elim conjE)
 apply (rule conjI) apply assumption (* traduccion *)
 apply (rule conjI) apply (rule extendsL_case, assumption+,simp,assumption+,simp,assumption) 
 apply (rule conjI) apply simp 
 apply (rule conjI) apply assumption 
 apply (rule conjI) apply assumption
 apply (rule conjI) apply assumption
 apply (rule conjI) apply (rule refl)
 apply (rule refl)
 apply (elim exE)
 apply (elim conjE)

apply (rule_tac x="q'" in exI)
apply (rule_tac x="ia" in exI)

apply (rule_tac x="sa" in exI)
apply (rule_tac x=" ss @ [((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="δ" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="s" in exI)

apply (rule conjI) apply (frule rho_good, elim conjE)
                   apply (rule execSVMBalanced_Case_1_1, assumption+) 
apply (rule conjI) apply simp 
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, simp)
apply (frule_tac v="v" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI) apply (rule maxFreshCells_Case_1_x, assumption+,simp)
apply (rule maxFreshWords_Case_1_x, assumption+,simp,assumption)



(* (Case VarE x a Of alts a') (LitB b) *)
apply (rule impI)+
apply (elim conjE)

apply (erule_tac x="b" in allE)
apply (elim conjE)

apply (rule allI)+
apply (rule impI, elim conjE)

apply (frule trE_case_1_2, assumption+)
apply (elim exE, elim conjE) 

apply (frule finite_dom_h,elim conjE)
apply (drule mp, simp)
apply (drule mp, simp, rule x_not_self, rule all_exp_core)
apply (drule mp, simp)+
 apply (subgoal_tac "closureCalled ei defs ⊆ closureCalled (Case VarE x a Of alts a') defs") 
  prefer 2 apply (rule closureCalled_case_1_x,assumption+) 
 apply (erule subset_trans, assumption)

apply (erule_tac x="rho" in allE) (* rho de ei *)
apply (erule_tac x="S" in allE)       (* S de ei. *) 
apply (erule_tac x="drop td S" in allE) (* S' *)
apply (erule_tac x="k0" in allE)  (* K0 de ei *)
apply (erule_tac x="((h, k), k0, (qs!i, 0),  S)" in allE)  (* s0 de ei *)

apply (erule_tac x="p'" in allE) 
apply (erule_tac x="qs!i" in allE) (* antes q *)
apply (erule_tac x="lss!i" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="csi" in allE)
apply (erule_tac x="0" in allE)
apply (erule_tac x="tds" in allE)

apply (drule mp) (* HI ei *)
apply (frule codestore_caseL_alts_disjoint, assumption+, elim conjE)
 apply (rule conjI) apply assumption (* traduccion *)
 apply (rule conjI) apply (rule extendsL_case, assumption+,simp,assumption+,simp,assumption) 
 apply (rule conjI) apply simp 
 apply (rule conjI) apply assumption 
 apply (rule conjI) apply assumption
 apply (rule conjI) apply assumption
 apply (rule conjI) apply (rule refl)
 apply (rule refl)
 apply (elim exE)
 apply (elim conjE)

apply (rule_tac x="q'" in exI)
apply (rule_tac x="ia" in exI)

apply (rule_tac x="sa" in exI)
apply (rule_tac x=" ss @ [((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="δ" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="s" in exI)

apply (rule conjI) apply (frule rho_good, elim conjE)
                   apply (rule execSVMBalanced_Case_1_2, assumption+) 
apply (rule conjI) apply simp 
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI, simp)
apply (frule_tac v="v" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI) apply (rule maxFreshCells_Case_1_x, assumption+,simp)
apply (rule maxFreshWords_Case_1_x, assumption+,simp,assumption)



(* (CaseD VarE x a Of alts a') *)
apply (rule impI)+
apply (elim conjE)

apply (rule allI)+
apply (rule impI, elim conjE)

apply (erule_tac x="pa" in allE)
apply (erule_tac x="extend E1 xs vs" in allE)
apply (erule_tac x="xs" in allE)
apply (erule_tac x="vs" in allE)
apply (erule_tac x="j" in allE)
apply (erule_tac x="C" in allE)
apply (elim conjE)

apply (frule trE_cased, assumption+)
apply (elim exE, elim conjE) 

apply (frule finite_dom_h,elim conjE)
apply (drule mp, simp)
apply (drule mp, simp, rule x_not_self, rule all_exp_core)
apply (drule mp, simp)+
 apply (subgoal_tac "finite (dom (h(pa := None)))") prefer 2 apply simp  
 apply (subgoal_tac "closureCalled ei defs ⊆ closureCalled (CaseD VarE x a Of alts a') defs") 
  prefer 2 apply (rule closureCalled_cased,assumption+) 
 apply (rule conjI) apply (erule subset_trans, assumption)
 apply (subst equals_dom_map_upd_none, assumption)

apply (frule cased_constructor_good,assumption+)

apply (erule_tac x="rho + zip xs (decreasing (length xs))" in allE) (* rho de ei *)
apply (erule_tac x="map Val vs @ S" in allE)       (* S de ei. *) 
apply (erule_tac x="drop (nat (int td + nr)) (map Val vs @ S)" in allE) (* S' *)
apply (erule_tac x="k0" in allE)  (* K0 de ei *)
apply (erule_tac x="((h(pa := None), k), k0, (qs!i, 0), ( map Val vs) @ S)" in allE)  (* s0 de ei *)

apply (erule_tac x="p'" in allE) 
apply (erule_tac x="qs!i" in allE) 
apply (erule_tac x="lss!i" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="isi" in allE)
apply (erule_tac x="csi" in allE)
apply (erule_tac x="0" in allE)
apply (erule_tac x="tds" in allE)

apply (drule mp) (* HI ei *)
apply (frule rho_good, elim conjE)
apply (frule codestore_case_alts_disjoint, rule disjI2, rule refl, assumption+, elim conjE)
 apply (rule conjI) apply assumption (* traduccion *)
 apply (rule conjI) apply (rule extendsL_case, assumption+,simp,assumption+,simp,assumption)
 apply (rule conjI) apply simp 
 apply (rule conjI) apply (rule identityEnvironment_cased,simp,assumption+)
                    apply (rule addEnv_rho_good, assumption+,simp,simp add: def_extend_def, simp, assumption+, simp)
 apply (rule conjI) apply (rule rho_case,assumption+,simp)
 apply (rule conjI) apply assumption
 apply (rule conjI) apply (rule refl)
 apply (rule refl)
 apply (elim exE)
 apply (elim conjE)

apply (rule_tac x="q'" in exI)
apply (rule_tac x="ia" in exI)

apply (rule_tac x="sa" in exI)
apply (rule_tac x=" ss @ [((h, k), k0, (q, ja), S)]" in exI)
apply (rule_tac x="δ ⊕ [j \<mapsto> -1]" in exI)
apply (rule_tac x="max 0 (m - 1)" in exI)
apply (rule_tac x="s+nr" in exI)

apply (rule conjI) apply (frule rho_good, elim conjE)
                   apply (rule execSVMBalanced_CaseD ,assumption+)
apply (erule_tac V="(qs ! i, lss ! i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei" in thin_rl)
apply (rule conjI) apply (subgoal_tac "(nat (int td + int (length vs)) - length vs) =
                    (nat (int td + int (length vs) - int (length vs)))",simp,simp)
apply (rule conjI, assumption)
apply (rule conjI, rule refl)
apply (rule conjI) apply (rule diff_CaseD, assumption+)
apply (frule_tac v="v" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI) apply (rule maxFreshCells_CaseD, assumption+,simp)
apply (rule maxFreshWords_CaseD,assumption+,simp,assumption)


(* (AppE f [a1, a2] [] a) primops *)
apply (rule impI)+
apply (elim conjE)

apply (rule allI)+
apply (rule impI, elim conjE)

apply (rule_tac x="q" in exI)
apply (rule_tac x=" Suc (Suc (Suc (Suc j)))" in exI)

apply (rule_tac x="((h, k) \<down> k0, k0, (q, Suc (Suc (Suc (Suc j)))), Val (execOp oper (atom2val E1 a1) (atom2val E1 a2)) # S')" in exI)
apply (rule_tac x="[((h, k), k0, (q, Suc (Suc (Suc j))), Val (execOp oper (atom2val E1 a1) (atom2val E1 a2)) # drop (topDepth rho) S), 
             ((h, k), k0, (q,  Suc (Suc j)), Val v # S), 
             ((h, k), k0, (q, Suc j), (map (item2Stack k S) [atom2item rho a1, atom2item rho a2]) @ S),
             ((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="[]k" in exI)
apply (rule_tac x="0" in exI)
apply (rule_tac x="2" in exI)
apply (subgoal_tac "core (AppE f [a1, a2] [] a)")
prefer 2 apply (rule all_exp_core)
apply (frule app_atoms)
apply (frule execSVMBalanced_App_primops, assumption+, erule conjE)
apply (rule conjI) apply simp  
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply assumption
apply (rule conjI) apply (rule refl)
apply (rule conjI) apply (rule empty_diff)
apply (rule conjI) apply (rule maxFreshCells_App_primops, assumption+)
apply (frule lengthS_topDepth)
apply (rule maxFreshWords_App_primops, assumption+)


(* (AppE f as rr a) *)
apply (rule impI)+
apply (elim conjE)

apply (rule allI)+
apply (rule impI, elim conjE)

apply (frule trE_app, assumption+)
apply (elim exE, elim conjE) 

apply (frule finite_dom_h,elim conjE)
apply (drule mp) apply (erule finite_dom_h', assumption)
apply (drule mp, simp, rule x_not_self, rule all_exp_core)
apply (drule mp, simp)+
apply (subst dom_map_insert, assumption)
apply (drule mp, simp)+ apply clarsimp
apply (drule mp, simp)+ apply (subst dom_map_insert) apply (elim conjE) apply clarsimp
apply (drule mp)
 apply (subgoal_tac "closureCalled e defs ⊆ closureCalled (AppE f as rr a) defs") 
  prefer 2 apply (rule closureCalled_app)
apply (simp,erule subset_trans,assumption)
 
apply (erule_tac x="[(empty,0,0)] + (zip (xs @ rs) (decreasing (length xs + length rs)))" in allE) (* rho de e. *)
apply (erule_tac x="map (item2Stack k S) (map (atom2item rho) as) @ 
                    map (item2Stack k S) (map (region2item rho) rr) @ drop td  S" in allE)       (* S de e *) 
apply (erule_tac x=" drop td S" in allE) (* S'. *)
apply (erule_tac x="k0" in allE)  (* K0 de e *)
apply (erule_tac x="((h, Suc k), k0, (qf, 0), map (item2Stack k S) (map (atom2item rho) as) @ 
                                              map (item2Stack k S) (map (region2item rho) rr) @ drop td  S)" in allE)  (* s0 de e *)

apply (erule_tac x="p'" in allE) 
apply (erule_tac x="qf" in allE)
apply (erule_tac x="lsf" in allE)
apply (erule_tac x="is" in allE)
apply (erule_tac x="is" in allE)
apply (erule_tac x="csf" in allE)
apply (erule_tac x="0" in allE)
apply (erule_tac x="tds" in allE)


apply (drule mp) (* HI ei *)
 apply (rule conjI) apply assumption 
 apply (rule conjI) apply (rule codestore_extend,assumption+)
 apply (rule conjI) apply simp 
 apply (rule conjI) apply (frule rho_good, elim conjE)
                    apply (frule app_distinct_boundVar,elim conjE)
                    apply (subgoal_tac "core (AppE f as rr a)")
                    prefer 2 apply (rule all_exp_core)
                    apply (frule app_arguments_good,assumption+,elim conjE)
                    apply (frule app_atoms)
                    apply (rule identityEnvironment_App,simp,assumption+,rule sym, simp, rule sym, simp,assumption+)
 apply (rule conjI) apply (simp add: envAdd.simps) apply (simp add: Let_def)
                    apply (subst length_decreasing_add_assoc,simp)
 apply (rule conjI) apply simp
 apply (rule conjI) apply (subgoal_tac "core (AppE f as rr a)")
                    prefer 2 apply (rule all_exp_core)
                    apply (frule app_arguments_good, assumption+,elim conjE)
                    apply simp
 apply (rule refl)


 apply (elim exE)
 apply (elim conjE)

apply (rule_tac x="q'" in exI)
apply (rule_tac x="i" in exI)

apply (rule_tac x="sa" in exI)
apply (rule_tac x=" ss @ 
        [((h, k), k0, (q, Suc (Suc j)), append (append (map (item2Stack k S) (map (atom2item rho) as)) 
                                                       (map (item2Stack k S) (map (region2item rho) rr))) (drop td S)),
         ((h, k), k0, (q, Suc j), append (append (map (item2Stack k S) (map (atom2item rho) as)) 
                                                 (map (item2Stack k S) (map (region2item rho) rr))) S),
         ((h, k), k0, (q, j), S)]" in exI)
apply (rule_tac x="δ(k + 1 := None)" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="max (int n + int l) (s + int n + int l - int td)" in exI)

apply (subgoal_tac "core (AppE f as rr a)")
prefer 2 apply (rule all_exp_core)

apply (rule conjI) apply (frule lengthS_topDepth)
                   apply (frule app_arguments_good,assumption+,elim conjE)
                   apply (rule_tac l="l" in execSVMBalanced_App,assumption+,rule sym,simp,rule sym,simp,assumption+)
apply (rule conjI) apply (simp, rule restrictToRegion_monotone_Suc_k, assumption)
apply (rule conjI, assumption)
apply (rule conjI) apply (rule refl) 
apply (rule conjI) apply (rule diff_App, assumption+,simp)
apply (frule_tac v="v" in resources_gre_0, elim exE, elim conjE)
apply (rule conjI) apply (rule maxFreshCells_App, assumption+, simp)
apply (frule app_arguments_good,assumption+)
apply (frule lengthS_topDepth)
apply (frule_tac v="v" in resources_gre_0, elim exE, elim conjE)
by (rule maxFreshWords_App,assumption+, simp, rule sym, simp, assumption+, simp)


(*

lemma correctness_b:
 "(E1,E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r  --> 
    core e -->
    (closureCalled e defs ⊆ definedFuns defs
  ∧ ((p, funm, contm), codes) = mapAccumL trF (1, empty, []) defs
  ∧ cs = concat codes 
  ∧ P = ((cs, contm),p,ct,st)
  ∧ finite (dom h) 
  -->
          (∀ rho S S' k0 s0 p' q ls is is' cs1 j tds.
            (q, ls, is, cs1) = trE p' funm fname rho e 
          ∧ (append cs1  [(q,is',fname)]) \<sqsubseteq> cs 
          ∧ drop j is' = is
          ∧  (E1,E2) \<Join> (rho,S)
          ∧ td = topDepth rho 
          ∧ k0 ≤ k 
          ∧ S' = drop td S 
          ∧ s0 = ((h, k), k0, (q, j), S) 
          -->
              (∃ q' i s ss δ m w. 
                     P\<turnstile>s0 , td#tds -svm-> s # ss, Suc 0#tds 
              ∧ s = ((h', k) \<down> k0, k0, (q', i), Val v # S')
              ∧ fst (the (map_of cs q'))!i = POPCONT
              ∧ r = (δ,m,w)
              ∧ δ = diff k (h,k) (h',k)
              ∧ m = maxFreshCells (rev (s#ss))
              ∧ w = maxFreshWords (rev (s#ss)))))"
apply (rule impI)
apply (rule impI)
apply (frule finite_dom_h,elim conjE) 
apply (frule finite_dom_h',assumption)
apply (frule x_not_self)

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

oops
(*by (rule correctness,assumption+)*)
*)

end