Theory execSVMBalanced_lemmas

(*  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. execSVMBalanced property *}

theory execSVMBalanced_lemmas
imports Main "../CoreSafe/SafeRASemantics" SVMSemantics CoreSafeToSVM CertifSafeToSVM_definitions
                                           basic_properties
begin



lemma identityEnvironment_Val:
  "[|  (E1,E2) \<Join>  (rho,S); E1 x = Some v; length rho > 0|]  
  ==>  S!+(rho |> x) = Val v"
apply (unfold identityEnvironment.simps)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
 apply (case_tac " S !+(rho |> x) = Val v",simp,simp)
by (simp add: dom_def)


lemma identityEnvironment_Reg:
  "[| (E1,E2) \<Join> (rho,S); E2 x = Some r; length rho > 0|] 
  ==> S!+(rho |> x) = Reg r"
apply (frule_tac r="r" in identityEnvironment_good, elim conjE)
apply (unfold identityEnvironment.simps)
apply (elim conjE)
apply (erule_tac x="x" and A="dom E2" in ballE)
 apply (case_tac " S !+ (rho |> x) = Reg r", simp, simp)
by (simp add: dom_def)

lemma restrictToRegion_monotone:
"(h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k = (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)"
apply (unfold restrictToRegion.simps, unfold Let_def, auto)
apply (subgoal_tac
"{p ∈ dom h'. fst (the (h' p)) ≤ k ∧ fst (the ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}) p)) ≤ k} = 
 {p ∈ dom h'. fst (the (h' p)) ≤ k}")
apply (simp, auto)
apply (subgoal_tac "x ∈ dom h'", clarsimp)
by (simp add: dom_def)


declare envSearch.simps [simp del]
declare identityEnvironment.simps [simp del] 


lemma execSVMBalanced_IntT:
  "[|(q, ls, is, cs1) = trE p' funm fname rho (ConstE (LitN i) a);
    cs = concat codes;
   (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs; 
    drop j is' = is; 
    P = ((cs, contm), p, ct, st); 
    td = topDepth rho; 
    S' = drop td S;
    s0 = ((h, k), k0, (q, j), S);
    E \<Join> (rho,S)|]
   ==> P\<turnstile>s0 , td#tds -svm-> ((h, k) \<down> k0, k0, (q, Suc (Suc (Suc j))), Val (IntT i) # S') #
                          [((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)] , Suc 0#tds ∧ fst (the (map_of cs q)) ! Suc (Suc (Suc j)) = POPCONT"
apply simp
apply (subgoal_tac "topDepth rho < length S")
prefer 2 apply (rule lengthS_topDepth,assumption)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) p'))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (subgoal_tac "(Suc  j) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="Suc j" in j_length)
apply (frule_tac i="Suc j" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  j)) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc j))" in j_length)
apply (frule_tac i="(Suc (Suc j))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc  j))) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc j)))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc j)))" in  nth_drop',simp) 
apply (elim conjE)
apply (simp add: Let_def, split split_if_asm, simp)
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def)
apply (simp add: Let_def, rule conjI, simp, simp)
apply (simp add: Let_def, rule conjI, simp, simp) 
apply (simp, simp add: Let_def)
apply (rule conjI, simp, simp)
apply (simp add: extendsL_def add: extends_def)
by clarsimp


lemma execSVMBalanced_BoolT:
  "[|(q, ls, is, cs1) = trE p' funm fname rho (ConstE (LitB b) a);  
    cs = concat codes;
   (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs; 
    drop j is' = is; 
    P = ((cs, contm), p, ct, st); 
    td = topDepth rho; 
    S' = drop td S;
    s0 = ((h, k), k0, (q, j), S);
    E \<Join> (rho,S)|]
   ==> P\<turnstile>s0 , td#tds -svm-> ((h, k) \<down> k0, k0, (q, Suc (Suc (Suc j))), Val (BoolT b) # S') #
                          [((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)] , Suc 0#tds ∧ fst (the (map_of cs q)) ! Suc (Suc (Suc j)) = POPCONT"
apply simp
apply (subgoal_tac "topDepth rho < length S")
prefer 2 apply (rule lengthS_topDepth,assumption)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) p'))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (subgoal_tac "(Suc  j) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="Suc j" in j_length)
apply (frule_tac i="Suc j" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  j)) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc j))" in j_length)
apply (frule_tac i="(Suc (Suc j))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc  j))) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc j)))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc j)))" in  nth_drop',simp) 
apply (elim conjE)
apply (simp add: Let_def, split split_if_asm, simp)
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def)
apply (simp add: Let_def, rule conjI, simp, simp)
apply (simp add: Let_def, rule conjI, simp, simp) 
apply (simp, simp add: Let_def)
apply (rule conjI, simp, simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp


lemma execSVMBalanced_VarE:
  "[|E1 x = Some (Loc pa);
    (q, ls, is, cs1) = trE p' funm fname rho (VarE x a); 
    cs = concat codes;
   (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs; 
    drop j is' = is; 
    P = ((cs, contm), p, ct, st); 
    td = topDepth rho; 
    S' = drop td S;
    (E1,E2) \<Join> (rho,S);
    length rho > 0;
    topDepth rho < length S;
    s0 = ((h, k), k0, (q, j), S)|]
   ==> P\<turnstile>s0 , td#tds -svm-> ((h, k) \<down> k0, k0, (q, Suc (Suc (Suc j))), Val (Loc pa) # S') #
                          [((h, k), k0, (q, j + 2), Val (Loc pa) # drop (topDepth rho) S),
                           ((h, k), k0, (q, j + 1), Val (Loc pa) # S), 
                           ((h, k), k0, (q, j), S)] , Suc 0#tds ∧ fst (the (map_of cs q)) ! Suc (Suc (Suc j)) = POPCONT"
apply simp
apply (subgoal_tac "is' = fst (the (map_of (concat codes) p'))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (subgoal_tac "(Suc  j) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="Suc j" in j_length)
apply (frule_tac i="Suc j" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  j)) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc j))" in j_length)
apply (frule_tac i="(Suc (Suc j))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc  j))) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc j)))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc j)))" in  nth_drop',simp)
apply (elim conjE)
apply (simp add: Let_def, split split_if_asm, simp)
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def)
apply (simp add: Let_def) 
apply (rule identityEnvironment_Val, assumption+, simp)
apply (rule conjI, simp, simp)
apply (simp add: Let_def, rule conjI, simp, simp)
apply (simp add: Let_def, rule conjI, simp, simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp

lemma execSVMBalanced_CopyE:
"  [|E1 x = Some (Loc pa); 
    E2 r = Some j; 
    j ≤ k; 0 < m; 
    SafeHeap.copy (h, k) j pa = ((h', k), p'); 
    (q, ls, is, cs1) = trE p'a funm fname rho (x @ r a);
    (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs; cs = concat codes;
    drop ja is' = is; 
    P = ((cs, contm), p, ct, st); 
    (E1, E2) \<Join> ( rho ,  S) ; 
    td = topDepth rho; k0' ≤ k;
     S' = drop td S;
    length rho > 0;
    topDepth rho < length S;
     s0 = ((h, k), k0', (q, ja), S)|]
       ==> P\<turnstile>s0 , td#tds -svm-> [((h', k) \<down> k0', k0', (q, Suc (Suc (Suc (Suc ja)))), Val (Loc p') # S'),
                           ((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)] , Suc 0#tds
          ∧  fst (the (map_of cs q)) ! Suc (Suc (Suc (Suc ja))) = POPCONT"
apply simp
apply (subgoal_tac "is' = fst (the (map_of (concat codes) p'a))") 
apply (subgoal_tac "ja < length (fst (the (map_of (concat codes) p'a)))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="ja" in  nth_drop',simp)
apply (subgoal_tac "(Suc  ja) < length (fst (the (map_of (concat codes) p'a)))") 
 prefer 2 apply (rule_tac j="Suc ja" in j_length)
apply (frule_tac i="Suc ja" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  ja)) < length (fst (the (map_of (concat codes) p'a)))") 
 prefer 2 apply (rule_tac j="(Suc (Suc ja))" in j_length)
apply (frule_tac i="(Suc (Suc ja))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc  ja))) < length (fst (the (map_of (concat codes) p'a)))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc ja)))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc ja)))" in  nth_drop',simp)
apply (subgoal_tac "(Suc (Suc (Suc (Suc  ja)))) < length (fst (the (map_of (concat codes) p'a)))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc (Suc ja))))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc (Suc ja))))" in  nth_drop',simp)
apply (elim conjE)
apply (simp add: Let_def, split split_if_asm, simp)
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def)
apply (simp add: Let_def)
apply (rule conjI) apply (frule identityEnvironment_Val, assumption+, simp, assumption)
apply (frule identityEnvironment_Reg, assumption+, simp, assumption)
apply (rule conjI, simp, simp)
apply (simp, rule conjI, simp, simp)
apply (simp, rule conjI, simp, simp)
apply (simp, simp add: Let_def)
apply (rule conjI, simp, simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp


declare restrictToRegion.simps [simp del]

lemma execSVMBalanced_ReuseE:
" [|E1 x = Some (Loc pa); 
  h pa = Some c; 
  SafeHeap.fresh q h;
  (qa, ls, is, cs1) = trE p' funm fname rho (ReuseE x a); 
  (cs1 @ [(qa, is', fname)]) \<sqsubseteq> cs; 
  cs = concat codes; 
  drop j is' = is; 
  P = ((cs, contm), p, ct, st); finite (dom h);
  td = topDepth rho; 
  k0 ≤ k; 
 (E1, E2) \<Join> ( rho ,  S) ;
  length rho > 0;
  topDepth rho < length S;
  S' = drop td S; 
  s0 = ((h, k), k0, (qa, j), S)|]
       ==> P\<turnstile>s0 , td#tds -svm-> [((h(pa := None)(q \<mapsto> c), k) \<down> k0, k0, (qa, Suc (Suc (Suc (Suc j)))), Val (Loc q) # S'),
                           ((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)] , Suc 0#tds
           ∧ fst (the (map_of cs qa)) ! Suc (Suc (Suc (Suc j))) = POPCONT"
apply simp
apply (subgoal_tac "is' = fst (the (map_of (concat codes) qa))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) qa)))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (subgoal_tac "(Suc  j) < length (fst (the (map_of (concat codes) qa)))") 
 prefer 2 apply (rule_tac j="Suc j" in j_length)
apply (frule_tac i="Suc j" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  j)) < length (fst (the (map_of (concat codes) qa)))") 
 prefer 2 apply (rule_tac j="(Suc (Suc j))" in j_length)
apply (frule_tac i="(Suc (Suc j))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc  j))) < length (fst (the (map_of (concat codes) qa)))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc j)))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc j)))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc (Suc  j)))) < length (fst (the (map_of (concat codes) qa)))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc (Suc j))))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc (Suc j))))" in  nth_drop',simp)
apply (elim conjE)
apply (simp add: Let_def, split split_if_asm, simp)
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.step, simp_all)
apply (rule execSVMBalanced.step, simp_all) 
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def)
apply (simp add: Let_def)
apply (rule identityEnvironment_Val, assumption+)
apply simp apply (rule conjI, simp, simp)
apply (unfold Let_def)
apply (simp add: Let_def)
apply (rule conjI)
apply (frule getFresh_fresh) apply simp
apply (erule getFresh_fresh)
apply (rule conjI, simp, simp)
apply simp apply (rule conjI, simp, simp)
apply (simp add: Let_def)
apply (rule conjI, simp, simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp


declare restrictToRegion.simps [simp del]



lemma execSVMBalanced_Let1:
  "[|x1 ∉ dom E1; e1 ≠ ConstrE C as r1 a'; 
    closureCalled (Let x1 = e1 In e2 a) defs ⊆ definedFuns defs; 
    ((p, funm, contm), codes) = mapAccumL trF (1, empty, []) defs;
    cs = concat codes; 
    P = ((cs, contm), p, ct, st);
    (q, ls, is, cs1) = trE p' funm fname rho (Let x1 = e1 In e2 a); 
    (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);
     (q1, ls1, is1, cs1') = trE (q2 + 1) funm fname (rho ++) e1; 
     (q2, ls2, is2, cs2) = trE p' funm fname (rho + [(x1, 1)]) e2;
     cs1 = cs2 @ (q2, is2, fname) # cs1'; q = q1; ls = q2 # ls1 @ ls2; is = PUSHCONT q2 # is1;
     P\<turnstile>((h, k), k, (q1, j + 1), Cont (k0, q2) # S) , 0#td#tds -svm-> s # ss , Suc 0#td#tds;
     P\<turnstile> ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S), (td+1)#tds -svm-> sa # ssa , Suc 0#tds;
      s = ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)\<down> k, k, (q', i), Val v1 # drop 0 (Cont (k0, q2) # S));
     sa = ((h'', k) \<down> k0, k0, (q'a, ia), Val v2 # S'); 
     fst (the (map_of cs q')) ! i = POPCONT;
     fst (the (map_of cs q'a)) ! ia = POPCONT|]
       ==> P\<turnstile>s0 , td#tds -svm-> sa # ssa @ s #
                                     ss @ [((h, k), k0, (q1, j), S)] , Suc 0#tds"
apply (subgoal_tac "fst (the (map_of cs q1)) ! j = PUSHCONT q2")
prefer 2
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q1))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) q1)))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (frule_tac ?cs2.0="cs2" and cs1'="cs1'" in codestore_let_disjoint, assumption+)
apply (simp add: disjointList_def)
apply (simp add: extendsL_def add: extends_def) 
apply clarsimp
apply (rule execSVMBalanced_n_step) prefer 3 apply simp
prefer 2 apply simp (* e2 *) 
apply (rule execSVMBalanced.step)
(* e1 *)
apply (rule_tac s''="((h, k), k, (q1, j + 1), Cont (k0, q2) # S)" in execSVMBalanced_n_step)
apply simp
apply (rule execSVMBalanced.step)
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def)
apply (unfold Let_def) apply (simp) apply simp apply simp apply simp apply (rule conjI, simp, simp)
apply simp apply simp
apply simp
apply (rule restrictToRegion_monotone) 
apply simp apply simp
apply simp
apply (rule conjI) apply simp apply simp
done

lemma head_execSVMBalanced:
 " P\<turnstile>s0 , n -svm-> s # ss, m ==> s0 = last (s#ss)"
by (erule execSVMBalanced.induct, simp_all)

lemma head_cons_execSVMBalanced:
  "[| ss≠[]; s0 = last ss|] ==> ∃ ss'. ss = ss' @ [s0]"
by (rule_tac x="butlast ss" in exI, simp)


declare identityEnvironment.simps [simp del]


lemma exec_let2_3 [rule_format]:
  "(E1,E2) \<Join> (rho,S) 
   --> fvs as ⊆ dom E1
   --> (∀a∈ set as. atom a)
   --> map (item2Val S) (map (atom2item rho) as) = map (atom2val E1) as"
apply (induct as, simp, clarsimp)
apply (case_tac a,simp_all)
apply (rename_tac a as x n) 
apply (case_tac x,simp_all) 
apply (rename_tac a as x n)
apply (simp add: identityEnvironment.simps)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
by (case_tac "S !+ (rho |> x)",simp_all) 


lemma execSVMBalanced_Let2:
  "[|E2 r = Some j; j ≤ k; fresh pa h; x1 ∉ dom E1; r ≠ self; length rho > 0;
    cs = concat codes; P = ((cs, contm), p, ct, st); finite (dom h);
    fv (Let x1 = ConstrE C as r a' In e2 a) ⊆ dom (fst (E1,E2));
   (∀ a ∈ set as. atom a); x1 ∉ fvs as;
    finite (dom (h(pa \<mapsto> (j, C, map (atom2val E1) as))));
    (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs; drop ja is' = is;
    (q2,ls2,is2,cs2) = trE p' funm fname (rho+[(x1,1)]) e2;
    ((p, funm, contm), codes) = mapAccumL trF (1, empty, []) defs;
    (E1, E2) \<Join> ( rho ,  S) ; td = topDepth rho; k0 ≤ k; S' = drop td S; s0 = ((h, k), k0, (q, ja), S);
    items = map (atom2item rho) as; item = region2item rho r; q = q2;
    ls = ls2; is = BUILDCLS C items item # is2; cs1 = cs2;
    P\<turnstile>((h(pa \<mapsto> (j, C, map (atom2val E1) as)), k), k0, (q, Suc ja), Val (Loc pa) # S) , (td + 1)#tds -svm-> sa # ss , Suc 0#tds;
    sa = ((h', k) \<down> k0, k0, (q', i), Val v2 # S')|]
    ==> P\<turnstile>s0 , td#tds -svm-> sa # ss @ [((h, k), k0, (q, ja), S)] , Suc 0#tds"
apply (subgoal_tac "fst (the (map_of (concat codes) q2)) ! ja =  BUILDCLS C (map (atom2item rho) as) (ItemVar (rho |> r))")
prefer 2
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q2))") 
apply (subgoal_tac "ja < length (fst (the (map_of (concat codes) q2)))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="ja" in  nth_drop',simp) 
apply (frule codestore_let2_disjoint)
apply (simp add: extendsL_def add: extends_def) 
apply clarsimp
apply (rule_tac s''="((h(pa \<mapsto> (j, C, map (atom2val E1) as)), k), k0, (q, Suc ja), Val (Loc pa) # S)" in  execSVMBalanced_n_step) 
prefer 3 apply simp
prefer 2 apply simp
apply (rule execSVMBalanced.step)
apply (simp, rule execSVMBalanced.init)
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (unfold execSVM_def)
apply (unfold Let_def)
apply simp
apply (frule identityEnvironment_Reg, assumption+, simp)
apply simp
apply (simp add: Let_def)
apply (frule getFresh_fresh)
apply simp
apply (subgoal_tac "map (item2Val S) (map (atom2item rho) as) = map (atom2val E1) as", simp)
apply (subgoal_tac "∃h'. h'  = h(pa \<mapsto> (j, C, map (atom2val E1) as))") prefer 2 apply simp 
apply (erule exE)
apply (subgoal_tac 
  "h'a = h(pa \<mapsto> (j, C, map (atom2val E1) as)) -->
   h'a pa = Some (j, C, map (atom2val E1) as)")
prefer 2 apply simp 
apply (frule exec_let2_3, blast)
by (erule_tac x="x" and A="set as" in ballE,simp,simp,simp) 


lemma execSVMBalanced_Case:
" [| cs = concat codes; P = ((cs, contm), p, ct, st); 
   E1 x = Some (Loc pa);  h pa = Some (j, C, vs);
   nr = int (length vs); 
   (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a'); 
   i < length alts;
   alts!i = (pati, ei);
   pati = ConstrP C ps ms;
   xs = map pat2var ps;
   (qs ! i, lss !i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei;
   (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs;  drop ja is' = is; (E1, E2) \<Join> ( rho ,  S) ;  td = topDepth rho; 
   k0 ≤ k; S' = drop td S;  s0 = ((h, k), k0, (q, ja), S);
   (q, rss) = trAlts p' funm fname rho alts; (lss, qs, css) = unzip3 rss; ls = concat lss; is = [MATCH (rho |> x) qs];
   cs1 = concat css; 
   map_of ct C = Some (q1,r,q2);
   P\<turnstile>((h, k), k0, (qs!r, 0), ( map Val vs) @ S) , nat (int td + nr)#tds -svm-> sa # ss , Suc 0#tds;
   length rho > 0;
   sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop (nat (int td + nr)) (map Val vs @ S));
   fst (the (map_of cs q')) ! ia = POPCONT|]
   ==> P\<turnstile>s0 , td#tds -svm-> sa # ss @ [((h, k), k0, (q, ja), S)] , Suc 0#tds"
apply (frule codestore_case_alts_disjoint,rule disjI1,rule refl, assumption+)
apply (rule execSVMBalanced_n_step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.init)
apply (simp add: execSVM_def)
apply (simp add: Let_def)
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! ja = MATCH (rho |> x) qs",simp)
apply (subgoal_tac "S !+ (rho |> x) = Val (Loc pa)",simp)
apply (rule identityEnvironment_Val, assumption+) apply simp
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "ja < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="ja" in  nth_drop',simp)
apply (simp add: extendsL_def add: extends_def) 
apply clarsimp
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! ja = MATCH (rho |> x) qs",simp)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "ja < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="ja" in  nth_drop',simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp


lemma execSVMBalanced_Case_1_1:
" [| cs = concat codes; P = ((cs, contm), p, ct, st); (E1,E2) \<Join> (rho,S); 0 < length rho;
   E1 x = Some (IntT n);
   i < length alts;
   alts!i = (pati, ei);
   (qs ! i, lss !i, isi, csi) = trE p' funm fname rho ei;
   (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a'); 
   (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, rss) = trAlts p' funm fname rho alts; (lss, qs, css) = unzip3 rss; ls = concat lss; is =  [MATCHN (rho |> x) v' m' qs];
   cs1 = concat css; 
   P\<turnstile>((h, k), k0, (qs ! i, 0), S) , td # tds -svm-> sa # ss , Suc 0 # tds;
   length rho > 0;
   sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop td S);
   fst (the (map_of cs q')) ! ia = POPCONT|]
   ==> P\<turnstile>s0 , td # tds -svm-> sa # ss @ [((h, k), k0, (q, j), S)] , Suc 0 # tds"
apply (frule codestore_caseL_alts_disjoint, assumption+)
apply simp apply (unfold Let_def) 
apply (rule execSVMBalanced_n_step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.init)
apply (simp add: execSVM_def)
apply (simp add: Let_def)
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! j = MATCHN (rho |> x) v' m' qs",simp)
apply (subgoal_tac "S !+ (rho |> x) = Val (IntT n)",simp)
apply (simp add: Let_def)
apply (frule SVM_Semantic_branch_Nat_consistent,assumption+,simp)
apply (rule identityEnvironment_Val,assumption+,simp)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp) 
apply (simp add: extendsL_def add: extends_def) 
apply clarsimp
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! j = MATCHN (rho |> x) v' m' qs",simp)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp



lemma execSVMBalanced_Case_1_2:
" [| cs = concat codes; P = ((cs, contm), p, ct, st); (E1,E2) \<Join> (rho,S); 0 < length rho; 
   i < length alts;
   alts!i = (pati, ei);
   E1 x = Some (BoolT b); 
   (q, ls, is, cs1) = trE p' funm fname rho (Case VarE x a Of alts a'); 
   (qs ! i, lss !i, isi, csi) = trE p' funm fname rho ei;
   (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, rss) = trAlts p' funm fname rho alts; (lss, qs, css) = unzip3 rss; ls = concat lss; is =  [MATCHN (rho |> x) 0 2 qs];
   cs1 = concat css; 
   P\<turnstile>((h, k), k0, (qs ! i, 0), S) , td # tds -svm-> sa # ss , Suc 0 # tds;
   length rho > 0;
   sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop td S);
   fst (the (map_of cs q')) ! ia = POPCONT|]
   ==> P\<turnstile>s0 , td # tds -svm-> sa # ss @ [((h, k), k0, (q, j), S)] , Suc 0 # tds"
apply (frule codestore_caseL_alts_disjoint, assumption+)
apply simp apply (unfold Let_def)
apply (rule execSVMBalanced_n_step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.init)
apply (simp add: execSVM_def)
apply (simp add: Let_def)
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! j = MATCHN (rho |> x) 0 2 qs",simp)
apply (subgoal_tac "S !+ (rho |> x) = Val (BoolT b)",simp)
apply (simp add: Let_def)
apply (frule SVM_Semantic_branch_Bool_consistent,assumption+)
apply (rule identityEnvironment_Val,assumption+,simp)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp) 
apply (simp add: extendsL_def add: extends_def) 
apply clarsimp
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! j = MATCHN (rho |> x) 0 2 qs",simp)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp


lemma execSVMBalanced_CaseD:
" [| cs = concat codes; P = ((cs, contm), p, ct, st); 
   E1 x = Some (Loc pa);  h pa = Some (j, C, vs);
   i < length alts;
   alts!i = (pati, ei);
   pati = ConstrP C ps ms;
   xs = map pat2var ps;
   (qs ! i, lss !i, isi, csi) = trE p' funm fname (rho + zip xs (decreasing (length xs))) ei;
   nr = int (length vs); 
   (q, ls, is, cs1) = trE p' funm fname rho (CaseD VarE x a Of alts a'); 
   (cs1 @ [(q, is', fname)]) \<sqsubseteq> cs;  drop ja is' = is; (E1, E2) \<Join> ( rho ,  S) ;  td = topDepth rho; 
   k0 ≤ k; S' = drop td S;  s0 = ((h, k), k0, (q, ja), S);
   (q, rss) = trAlts p' funm fname rho alts; (lss, qs, css) = unzip3 rss; ls = concat lss; is = [MATCHD (rho |> x) qs];
   cs1 = concat css; 
   map_of ct C = Some (q1,r,q2);
   P\<turnstile>((h(pa := None), k), k0, (qs!r, 0), ( map Val vs) @ S) , nat (int td + nr)#tds -svm-> sa # ss , Suc 0#tds;
   length rho > 0;
   sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop (nat (int td + nr)) (map Val vs @ S));
   fst (the (map_of cs q')) ! ia = POPCONT|]
   ==> P\<turnstile>s0 , td#tds -svm-> sa # ss @ [((h, k), k0, (q, ja), S)] , Suc 0#tds"
apply (frule codestore_case_alts_disjoint, rule disjI2, rule refl, assumption+)
apply (rule execSVMBalanced_n_step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.init)
apply (simp add: execSVM_def)
apply (simp add: Let_def)
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! ja = MATCHD (rho |> x) qs",simp)
apply (subgoal_tac "S !+ (rho |> x) = Val (Loc pa)",simp)
apply (simp add: Let_def)
apply (rule identityEnvironment_Val, assumption+) apply simp
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "ja < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="ja" in  nth_drop',simp)
apply (simp add: extendsL_def add: extends_def) 
apply clarsimp
apply (subgoal_tac "fst (the (map_of (concat codes) q)) ! ja = MATCHD (rho |> x) qs",simp)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) q))") 
apply (subgoal_tac "ja < length (fst (the (map_of (concat codes) q)))")
 prefer 2 apply (rule j_length)
apply (frule_tac i="ja" in  nth_drop',simp)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp

 

lemma execSVMBalanced_App:
  " [|n = length xs; l = length rs; primops f = None; length as = length xs; length rr = length rs;
    qf = the (funm f);
    cs = concat codes; P = ((cs, contm), p, ct, st); finite (dom h); (q, ls, is, cs1) = trE p' funm fname rho (AppE f as rr a);
   (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); topDepth rho < length S;
   P\<turnstile>((h, Suc k), k0, (qf, 0), 
     append (map (item2Stack k S) (map (atom2item rho) as)) 
             (append (map (item2Stack k S) (map (region2item rho) rr)) (drop td S))) , (n + l)#tds -svm-> sa # ss , Suc 0#tds;
    sa = ((h', Suc k) \<down> k0, k0, (q', i), Val v # (drop td S)); fst (the (map_of cs q')) ! i = POPCONT|]
       ==> P\<turnstile>s0 , td#tds -svm-> sa # 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)] , Suc 0#tds"
apply simp
apply (subgoal_tac "is' = fst (the (map_of (concat codes) p'))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (subgoal_tac "(Suc  j) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="Suc j" in j_length)
apply (frule_tac i="Suc j" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  j)) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc j))" in j_length)
apply (frule_tac i="(Suc (Suc j))" in  nth_drop',simp) 
apply (simp add: Let_def) apply (elim conjE)
apply (rule execSVMBalanced_n_step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.step) apply simp_all
apply (rule execSVMBalanced.init)
apply (simp add: execSVM_def)
apply (rule conjI) apply simp apply simp
apply (simp add: execSVM_def)
apply (rule conjI) apply simp apply simp
apply (simp add: execSVM_def) apply (simp add: Let_def)
apply (simp add: Let_def, elim conjE)
apply (simp add: extendsL_def add: extends_def) 
by clarsimp

declare identityEnvironment.simps [simp del] 



lemma identityEnvironment_item_val [rule_format]:
  "(E1,E2) \<Join> (rho,S) 
   --> fv a ⊆ dom E1
   --> atom a
   --> item2Stack k S (atom2item rho a) = Val (atom2val E1 a)"
apply (case_tac a,simp_all)
apply (rename_tac n a') 
apply (case_tac n, simp_all)
apply (rename_tac x a')
apply (rule impI)
by (simp add: identityEnvironment.simps)


lemma execSVMBalanced_App_primops:
  " [|primops f = Some oper; v1 = atom2val E1 a1; v2 = atom2val E1 a2; v = execOp oper v1 v2;
     fv (AppE f [a1, a2] [] a)  ⊆ dom (fst (E1, E2));
     ∀ a ∈ set [a1, a2]. atom a;
     cs = concat codes; P = ((cs, contm), p, ct, st); finite (dom h); (q, ls, is, cs1) = trE p' funm fname rho (AppE f [a1, a2] [] a);
     (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)|]
     ==> P\<turnstile>s0 , td # tds -svm-> 
          [((h, k) \<down> k0, k0, (q, Suc (Suc (Suc (Suc j)))), Val (execOp oper (atom2val E1 a1) (atom2val E1 a2)) # drop (topDepth rho) S),
           ((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)] , Suc 0 # tds  ∧ fst (the (map_of cs q)) ! Suc (Suc (Suc (Suc j))) = POPCONT"
apply simp apply (simp add: Let_def) apply (elim conjE)
apply (subgoal_tac "topDepth rho < length S")
prefer 2 apply (rule lengthS_topDepth,assumption)
apply (subgoal_tac "is' = fst (the (map_of (concat codes) p'))") 
apply (subgoal_tac "j < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule j_length)
apply (frule_tac i="j" in  nth_drop',simp)
apply (subgoal_tac "(Suc  j) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="Suc j" in j_length)
apply (frule_tac i="Suc j" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc  j)) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc j))" in j_length)
apply (frule_tac i="(Suc (Suc j))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc  j))) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc j)))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc j)))" in  nth_drop',simp) 
apply (subgoal_tac "(Suc (Suc (Suc (Suc  j)))) < length (fst (the (map_of (concat codes) p')))") 
 prefer 2 apply (rule_tac j="(Suc (Suc (Suc (Suc j))))" in j_length)
apply (frule_tac i="(Suc (Suc (Suc (Suc j))))" in  nth_drop',simp) 
apply (elim conjE)
apply (split split_if_asm, simp)
apply (rule execSVMBalanced.step)
apply (rule execSVMBalanced.step)
apply (rule execSVMBalanced.step)
apply (rule execSVMBalanced.step)
apply (rule execSVMBalanced.init)
apply (unfold execSVM_def) apply (simp add: Let_def)
apply simp apply simp apply simp 
apply (rule conjI) apply simp apply simp

apply (simp add: Let_def)
apply (frule_tac a="a1" and k="k" in identityEnvironment_item_val,assumption+)
apply (case_tac  "item2Stack k S (atom2item rho a1) = Val v1") apply simp
apply (frule_tac a="a2" and k="k" in identityEnvironment_item_val,assumption+)
apply (case_tac "item2Stack k S (atom2item rho a2) = Val v2") apply simp
apply (simp add: Let_def) apply simp apply simp
apply simp apply simp apply simp
apply (rule conjI) apply simp apply simp

apply (simp add: Let_def)
apply simp apply simp apply simp
apply (rule conjI) apply simp apply simp

apply (simp add: Let_def)
apply simp apply simp apply simp
apply (rule conjI) apply (rule impI)
apply simp apply simp apply simp
apply (simp add: extendsL_def add: extends_def) 
by clarsimp



end