Theory maxFreshCells_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. maxFreshCells property *}

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

declare sizeH.simps [simp del]


lemma sizeH_monotone:
  "finite  (dom h) ==>
   sizeH (h |` {p ∈ dom h. fst (the (h p)) ≤ k0}, k0) - sizeH (h, k) <= 0"
apply (simp add: sizeH.simps)
apply (subgoal_tac "dom h ∩ {p ∈ dom h. fst (the (h p)) ≤ k0} ⊆ dom h")
 apply (frule card_mono, simp,clarsimp)
by blast 


lemma sizeH_add_loc:
  "[| finite (dom h); fresh pa h; (h(pa \<mapsto> (j, C, map (atom2val E1) as)), k) = (h', k) \<down> k0|]
    ==> sizeH ((h', k) \<down> k0) - sizeH (h, k) = 1"
apply (drule_tac t="(h', k) \<down> k0" in sym)
by (simp add: fresh_def add: sizeH.simps)

lemma sizeH_restrictToRegion_monotone:
  "finite  (dom h) ==>
   sizeH ((h, k) \<down> k0) <= sizeH (h, k0)"
apply (unfold restrictToRegion.simps, unfold Let_def)
apply (simp add: sizeH.simps)
apply (subgoal_tac "dom h ∩ {p ∈ dom h. fst (the (h p)) ≤ k0} ⊆ dom h")
 apply (frule card_mono, simp,clarsimp)
by blast




lemma sizeH_upd_same:
"[|h pa = Some c;
 finite (dom h); 
 SafeHeap.fresh q h |] 
 ==> sizeH (h(pa := None)(q \<mapsto> c), k) = sizeH (h, k')"
apply (simp add: sizeH.simps)
apply (simp add: SafeHeap.fresh_def)
apply (subgoal_tac "h pa = Some c ==> pa ∈ dom h")
apply (rule card_Suc_Diff1, assumption+)
by auto


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)

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


(* Lemmas for max *)
lemma max_assoc:
  "max (max (x::int) (y::int)) (z::int) =  max (x::int) (max (y::int) (z::int))"
by simp

lemma max_assoc_2:
  "max (x::int) (max (y::int) (z::int))  =  max (max (x::int) (y::int)) (z::int)"
by simp

lemma max_sym:
  "max (x::int) (y::int)  =  max (y::int) (x::int)"
by simp

lemma max_sub:
 "max ((x::int)-(z::int)) ((y::int)-(z::int)) = max (x::int) (y::int) - (z::int)"
by auto

lemma max_sub_2:
  "max (max (x::int) (y::int)) (z::int) = max (max (z::int) (x::int)) (y::int)"
by auto


(* Lemmas for foldl & max *)

lemma foldl_max_assoc:
  "foldl max (max (x::int) (y::int)) xs = max (x::int) (foldl max (y::int) xs)"
by (induct xs arbitrary: y)  (simp_all add: max_assoc)

lemma foldl_max_assoc_2:
  "foldl max (max (x::int) (y::int)) xs = max (y::int) (foldl max (x::int) xs)"
by (induct xs arbitrary: y)  (simp_all add: max_assoc)

lemma foldl_max_absorb0:
shows "max (x::int) (foldl max (y::int) zs) = foldl max (y::int) ((x::int)#zs)"
by (induct zs) (simp_all add:foldl_max_assoc)


lemma maximum_map_sub_sizeH:
  "maximum (map (λ(h, r, pc, s). sizeH h - sizeH x) (y#ys)) = 
  (maximum (map (λ(h, r, pc, s). sizeH h) (y#ys))) - sizeH x"
apply (induct ys)
 apply (unfold maximum.simps, case_tac y, case_tac b, case_tac ba, simp)
apply (case_tac y, case_tac b, case_tac ba, rename_tac hy bay ry bayy pcy sy, simp)
 apply (case_tac a, case_tac b, case_tac ba, rename_tac ha ba ra baa pca sa, simp)
apply (subst foldl_max_assoc_2)
apply (subst foldl_max_assoc_2)
by simp

lemma maximum_map_sub_sizeST:
  "maximum (map (λ(h, r, pc, w). sizeST w - sizeST x) (y#ys)) = 
  (maximum (map (λ(h, r, pc, w). sizeST w) (y#ys))) - sizeST x"
apply (induct ys)
 apply (unfold maximum.simps, case_tac y, case_tac b, case_tac ba, simp)
apply (case_tac y, case_tac b, case_tac ba, rename_tac hy bay ry bayy pcy sy, simp)
 apply (case_tac a, case_tac b, case_tac ba, rename_tac ha ba ra baa pca sa, simp)
apply (subst foldl_max_assoc_2)
apply (subst foldl_max_assoc_2)
by simp


lemma max_maximum_sub:
  "max ((maximum (map f (x#xs))) - z) ((maximum (map f (y#ys))) - z) = maximum  (map f ((x#xs) @ (y#ys))) - z"
apply (induct xs ys rule:list_induct2')
 apply (simp add:  maximum.simps)

 apply (simp  add: maximum.simps)

 apply (simp  add: maximum.simps)
 apply (subst max_sub, subst foldl_max_absorb0)
 apply (simp, subst max_sub_2)
 apply (simp add: maximum.simps)

 apply (simp add: maximum.simps)
 apply (subst foldl_max_assoc_2 [where y="(f xa)"])
 apply (subst max_sub, subst max_assoc , subst foldl_max_assoc_2)
 apply (subst max_assoc_2 [where y="f ya"])
 apply (subst max_sym [where y="f ya"])
 apply (subst max_assoc, subst max_assoc_2)

 apply (subst foldl_max_assoc_2 [where y="f ya"]) 
 apply (subst foldl_max_assoc_2 [where y=" f xa"])
 apply (subst max_assoc [where x="f xa" and z="f y"])
 apply (subst foldl_max_assoc [where x=" f xa"])
 apply (subst max_assoc_2 [where y="f xa"])
 apply (subst max_sym)
by auto

lemma maximum_map_append:
 "maximum (map f (xs @ x # x # ys)) = maximum (map f (xs @ x # ys))"
apply (induct xs ys rule:list_induct2')
by (simp add: maximum.simps)+

declare map.simps [simp del]
declare maxFreshCells.simps [simp del]
declare maximum.simps [simp del]

lemma maxFreshCells2_P:
  "maxFreshCells (ss1 @ [s]  @ ss2) = 
        max (maxFreshCells (ss1 @ [s]))
            ((maxFreshCells ([s] @ ss2)) + sizeSVMStateH s - sizeSVMStateH (hd (ss1 @ [s])))"
apply (case_tac s, case_tac b, case_tac ba) apply (rename_tac hi bi ri bai pci si)
apply (induct ss1 ss2 rule:list_induct2')

 apply (simp add: maxFreshCells.simps)

 apply (simp add: maxFreshCells.simps)
 apply (simp add: maximum.simps)
 apply (case_tac x, case_tac b, case_tac ba) apply  (rename_tac hx bx rx bax pcx sx) apply simp
 apply (simp add: maxFreshCells.simps add: maximum.simps add: map.simps)

 apply (simp, simp add: maxFreshCells.simps add: maximum.simps add: map.simps)
 apply (subst foldl_max_absorb0)
 apply (subgoal_tac "0 = sizeH hi - sizeH hi",simp)
 apply (subst max_assoc, subst max_sym [of _ 0])
 apply (subst max_assoc_2, simp,simp)

 apply simp
 apply (case_tac x, case_tac b, case_tac ba) apply  (rename_tac hx bx rx bax pcx sx) apply simp
 apply (simp add: maxFreshCells.simps)
 apply (case_tac y, case_tac b, case_tac ba) apply  (rename_tac hy bby ry bay pcy sy) apply simp
 apply (subgoal_tac "0 = sizeH hx - sizeH hx") prefer 2 apply simp
 apply (subst maximum_map_sub_sizeH [where ys="xs @ (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys"])
 apply (subst maximum_map_sub_sizeH [where ys="xs @ [(hi, ri, pci, si)]"])
 apply (subst maximum_map_sub_sizeH [where ys="(hy, ry, pcy, sy) # ys"])
 apply (simp,subst max_maximum_sub,simp,rule sym)
 apply (subgoal_tac
  "maximum ((map (λ(h, r, pc, s). sizeH h) (((hx, rx, pcx, sx) # xs) @ (hi, ri, pci, si) # 
                                           ((hi, ri, pci, si) # (hy, ry, pcy, sy) # ys)))) = 
   maximum ((map (λ(h, r, pc, s). sizeH h) (((hx, rx, pcx, sx) # xs) @ 
                                            ((hi, ri, pci, si) # (hy, ry, pcy, sy) # ys))))",simp)
by (rule maximum_map_append)


lemma maxFreshCells_P_rev:
  "maxFreshCells (rev (ss2 @ [s]  @ ss1)) = 
        max (maxFreshCells (rev ([s] @ ss1)))
            ((maxFreshCells (rev (ss2 @ [s]))) + sizeSVMStateH s - sizeSVMStateH (hd (rev ([s] @ ss1))))"
apply (case_tac s, case_tac b, case_tac ba) apply (rename_tac hi bi ri bai pci si, simp)
apply (induct "(rev ss1)" "(rev ss2)" rule:list_induct2')

 apply (simp add: maxFreshCells.simps)

 apply (simp add: maxFreshCells.simps)
 apply (simp add: maximum.simps)
 apply (case_tac x, case_tac b, case_tac ba) apply  (rename_tac hx bx rx bax pcx sx) apply simp
 apply (simp add: maxFreshCells.simps add: maximum.simps add: map.simps)

 apply (simp, simp add: maxFreshCells.simps add: maximum.simps add: map.simps)
 apply (subst foldl_max_absorb0)
 apply (subgoal_tac "0 = sizeH hi - sizeH hi",simp)
 apply (subst max_assoc, subst max_sym [of _ 0])
 apply (subst max_assoc_2, simp,simp)

 apply simp
 apply (case_tac x, case_tac b, case_tac ba) apply  (rename_tac hx bx rx bax pcx sx) apply simp
 apply (simp add: maxFreshCells.simps)
 apply (case_tac y, case_tac b, case_tac ba) apply  (rename_tac hy bby ry bay pcy sy) apply simp
 apply (subgoal_tac "0 = sizeH hx - sizeH hx") prefer 2 apply simp
 apply (subst maximum_map_sub_sizeH [where ys="xs @ (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys"])
 apply (subst maximum_map_sub_sizeH [where ys="xs @ [(hi, ri, pci, si)]"])
 apply (subst maximum_map_sub_sizeH [where ys="(hy, ry, pcy, sy) # ys"])
 apply (simp,subst max_maximum_sub,simp,rule sym)
 apply (subgoal_tac
  "maximum ((map (λ(h, r, pc, s). sizeH h) (((hx, rx, pcx, sx) # xs) @ (hi, ri, pci, si) # 
                                           ((hi, ri, pci, si) # (hy, ry, pcy, sy) # ys)))) = 
   maximum ((map (λ(h, r, pc, s). sizeH h) (((hx, rx, pcx, sx) # xs) @ 
                                            ((hi, ri, pci, si) # (hy, ry, pcy, sy) # ys))))",simp)
by (rule maximum_map_append)


lemma maxFreshCells_IntT:
  "[|finite (dom h); 
    s0 = ((h, k), k0, (q, j), S)|]  
   ==> 0 = maxFreshCells
          (rev (((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)]))"
apply (simp add: maxFreshCells.simps)
apply (simp add: Let_def add: map.simps add: maximum.simps)
apply (subgoal_tac "sizeH (h |` {p ∈ dom h. fst (the (h p)) ≤ k0}, k0) - sizeH (h, k) <= 0")
 apply simp
by (erule sizeH_monotone)

lemma maxFreshCells_BoolT:
  "[|finite (dom h); 
    s0 = ((h, k), k0, (q, j), S)|]  
   ==> 0 = maxFreshCells
          (rev (((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)]))"
apply (simp add: maxFreshCells.simps)
apply (simp add: Let_def add: map.simps add: maximum.simps)
apply (subgoal_tac "sizeH (h |` {p ∈ dom h. fst (the (h p)) ≤ k0}, k0) - sizeH (h, k) <= 0")
 apply simp
by (erule sizeH_monotone)

lemma maxFreshCells_VarE:
  "[|finite (dom h); 
    s0 = ((h, k), k0, (q, j), S)|]  
   ==> 0 = maxFreshCells
           (rev (((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)]))"
apply (simp add: maxFreshCells.simps)
apply (simp add: Let_def add: map.simps add: maximum.simps)
apply (subgoal_tac "sizeH (h |` {p ∈ dom h. fst (the (h p)) ≤ k0}, k0) - sizeH (h, k) <= 0")
 apply simp
by (erule sizeH_monotone)


declare restrictToRegion.simps [simp del]

lemma maxFreshCells_CopyE:
  "[|E1 x = Some (Loc pa); E2 r = Some j; j ≤ k;
    0 < m; SafeHeap.copy (h, k) j pa = ((h', k), p'); m = SafeRASemantics.size h pa;
    finite (dom h);  finite (dom h');
    extends h h'; SafeRASemantics.size h' p' = SafeRASemantics.size h pa;
    sizeH (h', k) - sizeH (h, k) = SafeRASemantics.size h' p'|]
    ==> m = maxFreshCells
             (rev [((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)]) "
apply (simp add: maxFreshCells.simps)
apply (simp add: map.simps add: maximum.simps)
apply (subgoal_tac "sizeH ((h', k) \<down> k0) <= sizeH (h', k0)")
 apply (subgoal_tac "sizeH (h', k0) = sizeH (h', k)",simp)
 apply (simp add: sizeH.simps)
by (rule sizeH_restrictToRegion_monotone,assumption+)


lemma maxFreshCells_ReuseE:
  "[|h pa = Some c;
    finite (dom h); 
    SafeHeap.fresh q h |] 
   ==> 0 = maxFreshCells
               (rev [((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)])"
apply (subgoal_tac "sizeH (h(pa := None)(q \<mapsto> c), k) = sizeH (h, k)")
 apply (simp add: maxFreshCells.simps add: map.simps add: maximum.simps)
  apply (subgoal_tac "sizeH ((h(pa := None)(q \<mapsto> c), k) \<down> k0) <= sizeH (h(pa := None)(q \<mapsto> c), k0)")
   apply (subgoal_tac "sizeH (h(pa := None)(q \<mapsto> c), k0) = sizeH (h, k)",auto)
  apply (rule sizeH_upd_same, assumption+)
 apply (subgoal_tac "finite (dom (h(pa := None)(q \<mapsto> c)))")
  apply (rule sizeH_restrictToRegion_monotone,assumption+)
 apply (simp add: SafeHeap.fresh_def)
by (rule sizeH_upd_same,assumption+)


lemma cons_append_assoc:
  "x#(xs @ ys) = (x#xs) @ ys"
by simp

lemma cons_append_assoc_2:
  "(x#xs) @ ys = x#(xs @ ys)"
by simp

lemma cons_append:
  "x#xs = [x] @ xs"
by simp

lemma cons_append_2:
  "[x] @ xs = x # xs"
by simp


lemma append_assoc_2:
 "(xs @  ys) @ zs = xs @ (ys @ zs)"
by (induct xs) auto

lemma cons_cons_append:
 "[x,y] = [x] @ [y]"
by simp

declare rev.simps [simp del]

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)



lemma let1_1:
 "[| P\<turnstile>((h, k), k, (q1, j + 1), Cont (k0, q2) # S) , 0#td#tds -svm-> s # ss , Suc 0#td#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));
    (δ1, m1, s1) = (δ, m, w); 
    m = maxFreshCells (rev (s # ss));
    m >= 0|] 
   ==> maxFreshCells
                (rev ([((((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)]))) = m1"
apply (frule_tac s="s" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp,simp)
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym)
apply (rule_tac t="ss" and s="ss' @ [((h, k), k, (q1, Suc j), Cont (k0, q2) # S)]" in ssubst,assumption)
apply (subst append_assoc_2)
apply (subst cons_append_assoc [of _ "ss'"])
apply (subst maxFreshCells_P_rev, simp)
apply (unfold rev.simps, simp)
by (unfold maxFreshCells.simps maximum.simps map.simps,simp)





lemma let1_2:
 "[| 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;
    sa = ((h'', k) \<down> k0, k0, (q'a, ia), Val v2 # S'); 
    (δ1, m1, s1) = (δ, m, w);
    (δ2, m2, s2) = (δ', ma, wa); ma >= 0;
    δ = diff k (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k);
    ma = maxFreshCells (rev (sa # ssa))|] 
   ==> maxFreshCells (rev (sa # ssa @ 
                 [((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # drop 0 (Cont (k0, q2) # S))])) + 
       sizeSVMStateH (((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # drop 0 (Cont (k0, q2) # S))) - 
       sizeSVMStateH (((h, k), k0, (q, j), S)) = 
        m2 +  \<parallel> δ1 \<parallel>"
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ssa=[]",simp) apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
 apply (elim conjE)
 apply (drule_tac t=" (h'', k) \<down> k0" in sym, simp)
 apply (subgoal_tac 
  "sizeH (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) - sizeH ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k) = 0",simp)
 apply (subst restrictToRegion_monotone [of  _ k])
 apply (rule let1_3, simp)
 apply (rule sym)
 apply (subgoal_tac "(h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k = (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)",simp)
 apply (rule restrictToRegion_monotone)
apply simp
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ssa" in sym)
apply (rule_tac t="ssa" and s=" ss' @ [((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S)]" in ssubst,assumption)
apply (rename_tac ssa') apply simp
apply (subst cons_append_assoc [of _ "ssa'"])
apply (subst cons_cons_append [of "(((h' |` {p ∈ (dom h'). ((fst (the (h' p))) ≤ k)}), k), k0, (q2, 0), ((Val v1) # S))"])
apply (subst maxFreshCells_P_rev, simp)
apply (unfold rev.simps, simp)
apply (unfold maxFreshCells.simps maximum.simps map.simps, simp)
apply (subgoal_tac
  "(h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k = (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)")
prefer 2 apply (rule restrictToRegion_monotone)
apply simp
apply (subgoal_tac
 "sizeH ((h' |` {p ∈ (dom h'). ((fst (the (h' p))) ≤ k)}), k) - (sizeH (h, k)) = 
    \<parallel> diff k (h,k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<parallel>")
apply simp
by (rule let1_3)


lemma maxFreshCells_Let1:
  "[|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'); 
    (δ1, m1, s1) = (δ, m, w); 
    (δ2, m2, s2) = (δ', ma, wa);
    δ = diff k (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k);
    m = maxFreshCells (rev (s # ss)); m >= 0;
    ma = maxFreshCells (rev (sa # ssa)); ma >= 0|] 
   ==> max m1 (m2 + \<parallel> δ1 \<parallel>) =
          maxFreshCells
           (rev (sa # 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)]))"
apply (subst cons_append_assoc)
apply (subst cons_append [of _ "ss @ [((h, k), k0, (q, j), S)]"])
apply (subst maxFreshCells_P_rev)
apply (subst let1_1,assumption+) 
apply (subst cons_append_2)
apply (subst rev.simps(2) [where xs="ss @ [((h, k), k0, (q, j), S)]"])
apply (subst rev_append [of "ss"])
apply (subst rev.simps)
apply (subst rev.simps)
apply (unfold append_Nil)
apply (subst cons_append_2)
apply (subst cons_append_assoc_2 [of "((h, k), k0, (q, j), S)"])
apply (unfold hd.simps)
apply (subst cons_append_assoc_2)
apply (subst let1_2 [where ma="ma"],assumption+)
by (rule refl)



lemma maxFreshCells_Let2:
  "[|finite (dom h); 
    fresh pa h;
     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'); 
    (δ, m, s) = (δ', ma, w); ma >= 0;
    ma = maxFreshCells (rev (sa # ss))|]
    ==> m + 1 = maxFreshCells (rev (sa # ss @ [((h, k'), k0, (q, ja), S)]))"
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp) apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
apply (elim conjE)
apply (drule_tac t="(h', k) \<down> k0" in sym)
apply (subgoal_tac 
  "sizeH (h(pa \<mapsto> (j, C, map (atom2val E1) as)), k) - sizeH (h, k') = 1")
prefer 2 apply (simp add: sizeH.simps add: fresh_def) apply clarsimp
apply simp
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym)
apply (rule_tac t="ss" and s=" ss' @ [((h(pa \<mapsto> (j, C, map (atom2val E1) as)), k), k0, (q, Suc ja), Val (Loc pa) # S)]" 
                in ssubst,assumption)
apply (subst cons_append_assoc)
apply simp
apply (subst cons_append_assoc [where xs="ss'"])
apply (subst cons_append_assoc [where xs="ss'"])
apply (subst cons_cons_append)
apply (subst maxFreshCells_P_rev)
apply (simp add: rev.simps add: hd.simps)
apply (simp add: maxFreshCells.simps add: maximum.simps add: map.simps)
apply (subgoal_tac 
  "sizeH (h(pa \<mapsto> (j, C, map (atom2val E1) as)), k) - sizeH (h, k') = 1")
prefer 2 apply (simp add: sizeH.simps add: fresh_def)
by auto


lemma maxFreshCells_Case:
  "[| finite (dom h); i < length alts; E1 x = Some (Loc pa); h pa = Some (j, C, vs);
     nr = int (length vs); 
     s0 = ((h, k), k0, (q, ja), S); 
     P\<turnstile>((h, k), k0, (qs ! i, 0), map Val vs @ S) , nat (int td + nr)#tds -svm-> sa # ss , Suc 0#tds;
     sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop (nat (int td + nr)) (map Val vs @ S));
     (δ, m, s) = (δ', ma, w);
      ma = maxFreshCells (rev (sa # ss)); ma >= 0|]
      ==> m = maxFreshCells (rev (sa # ss @ [((h, k), k0, (q, ja), S)]))"
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp)
apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps, simp) 
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym, simp)
apply (subst cons_append_assoc [where ys=" [((h, k), k0, ((qs ! i), 0), ((map Val vs) @ S)), ((h, k), k0, (q, ja), S)]"])
apply (subst cons_cons_append)
apply (subst maxFreshCells_P_rev, simp)
by (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)


lemma maxFreshCells_Case_1_x:
  "[| s0 = ((h, k), k0, (q, ja), S); 
     P\<turnstile>((h, k), k0, (qs ! i, 0), S) , td # tds -svm-> sa # ss , Suc 0 # tds;
    sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop td S);
     (δ, m, s) = (δ', ma, w);
      ma = maxFreshCells (rev (sa # ss)); ma >= 0|]
      ==> m = maxFreshCells (rev (sa # ss @ [((h, k), k0, (q, ja), S)]))"
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp)
apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps, simp) 
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym, simp)
apply (subst cons_append_assoc [where ys=" [((h, k), k0, ((qs ! i), 0), S), ((h, k), k0, (q, ja), S)]"])
apply (subst cons_cons_append)
apply (subst maxFreshCells_P_rev, simp)
by (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)

lemma maxFreshCells_CaseD:
  "[| finite (dom h); i < length alts; E1 x = Some (Loc pa); h pa = Some (j, C, vs);
     nr = int (length vs); 
     s0 = ((h, k), k0, (q, ja), S); 
     P\<turnstile>((h(pa := None), k), k0, (qs ! i, 0), map Val vs @ S) , nat (int td + nr)#tds -svm-> sa # ss , Suc 0#tds;
     sa = ((h', k) \<down> k0, k0, (q', ia), Val v # drop (nat (int td + nr)) (map Val vs @ S));
     (δ, m, s) = (δ', ma, w);
      ma = maxFreshCells (rev (sa # ss)); ma >= 0|]
      ==> max 0 (m - 1) = maxFreshCells (rev (sa # ss @ [((h, k), k0, (q, ja), S)]))"
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp)
apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
 apply (elim conjE)
 apply (drule_tac t="(h', k) \<down> k0" in sym)
 apply (subgoal_tac "sizeH (h(pa := None), k) - sizeH (h, k) < 0",simp)
 apply (subgoal_tac "pa ∈ dom h")
 apply (subgoal_tac "card (dom h) >= 1")
 apply (simp add: sizeH.simps) 
 apply (subgoal_tac "card (dom h) >= 1", arith)
 apply (subgoal_tac "∃h'. h=h'(pa:=Some (j, C, vs)) ∧ pa ∉ dom h'")
 apply (erule exE, simp)
 apply (rule_tac x="h(pa:=None)" in exI, simp)
 apply (rule sym, rule map_upd_triv, assumption)
 apply (simp add: dom_def)
apply simp
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym, simp)
apply (subst cons_append_assoc [where ys=" [((h(pa := None), k), k0, ((qs ! i), 0), ((map Val vs) @ S)), ((h, k), k0, (q, ja), S)]"])
apply (subst cons_cons_append)
apply (subst maxFreshCells_P_rev, simp)
apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
apply (subgoal_tac "sizeH (h(pa := None), k) - sizeH (h, k) = -1",simp)
apply (simp add: sizeH.simps)
apply (subgoal_tac "pa ∈ dom h")
 apply (subst card_Diff_singleton,assumption+)
 apply (subgoal_tac "card (dom h) >= 1", arith)
 apply (subgoal_tac "∃h'. h=h'(pa:=Some (j, C, vs)) ∧ pa ∉ dom h'")
 apply (erule exE, simp)
 apply (rule_tac x="h(pa:=None)" in exI, simp)
 apply (rule sym, rule map_upd_triv, assumption)
by (simp add: dom_def)


lemma maxFreshCells_App:
  " [|Σ f = Some (xs, rs, e); E1' = map_of (zip xs (map (atom2val E1) as)); n = length xs; l = length rs;
     E2' = map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k);
     finite (dom h); 
     s0 = ((h, k), k0, (q, j), 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); 
     (δ, m, s) = (δ', ma, w);
     ma = maxFreshCells (rev (sa # ss)); ma >= 0|]
       ==>  m = maxFreshCells
               (rev (sa # ss @ [((h, k), k0, (q, Suc (Suc j)),
                                      (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),
                                      (map (item2Stack k S) (map (atom2item rho) as) @ map (item2Stack k S) (map (region2item rho) rr)) @
                                      S),
                                     ((h, k), k0, (q, j), S)]))"
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp)
apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
 apply (elim conjE)
 apply (drule_tac t="(h', Suc k) \<down> k0" in sym)
 apply (simp add: sizeH.simps)
apply simp
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym, simp)
apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
apply (subgoal_tac "sizeH (h, Suc k) - sizeH (h, k) = 0",simp)
by (simp add: sizeH.simps)



lemma maxFreshCells_App_primops:
  " [|finite (dom h)|]
       ==> 0 = maxFreshCells
               (rev [((h, k) \<down> k0, k0, (q, Suc (Suc (Suc (Suc j)))), Val (execOp oper (atom2val E1 a1) (atom2val E1 a2)) # 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)])"
apply (simp add: maxFreshCells.simps)
apply (subgoal_tac "sizeH ((h, k) \<down> k0) <= sizeH (h, k)")
 apply (simp add: rev.simps add: maxFreshCells.simps add: maximum.simps add: map.simps)
apply (unfold restrictToRegion.simps, unfold Let_def)
apply (simp add: sizeH.simps)
apply (subgoal_tac "dom h ∩ {p ∈ dom h. fst (the (h p)) ≤ k0} ⊆ dom h")
 apply (frule card_mono, simp,clarsimp)
by blast


end