Theory maxFreshWords_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. maxFreshWords property *}

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


declare sizeST.simps [simp del]


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
apply simp_all
done

lemma maxFreshWords_1 [rule_format]:
"length S > td --> sizeST (drop td S) - sizeST S <= 0"
apply (induct td,simp,auto)
apply (subgoal_tac "drop td S = S ! td # drop (Suc td) S",simp)
apply (case_tac "S!td")
apply (simp add: sizeST.simps)+
by (rule nth_drop',simp) 

(* 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 maxFreshWords.simps [simp del]
declare maximum.simps [simp del]

lemma maxFreshWords_P:
  "maxFreshWords (ss1 @ [s]  @ ss2) = 
        max (maxFreshWords (ss1 @ [s]))
            ((maxFreshWords ([s] @ ss2)) + sizeSVMStateST s - sizeSVMStateST (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: maxFreshWords.simps)

 apply (simp add: maxFreshWords.simps 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: maxFreshWords.simps add: maximum.simps add: map.simps)

 apply (simp, simp add: maxFreshWords.simps add: maximum.simps add: map.simps)
 apply (subst foldl_max_absorb0)
 apply (subgoal_tac "0 = sizeST si - sizeST si",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: maxFreshWords.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 = sizeST sx - sizeST sx") prefer 2 apply simp
 apply (subst maximum_map_sub_sizeST [where ys="xs @ (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys"])
 apply (subst maximum_map_sub_sizeST [where ys="xs @ [(hi, ri, pci, si)]"])
 apply (subst maximum_map_sub_sizeST [where ys="(hy, ry, pcy, sy) # ys"])
 apply (simp, subst max_maximum_sub, simp, rule sym)
 apply (subgoal_tac
  "maximum (map (λ(h, r, pc, y). sizeST y) (((hx, rx, pcx, sx) # xs) @ (hi, ri, pci, si) # (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys)) =
   maximum (map (λ(h, r, pc, y). sizeST y) (((hx, rx, pcx, sx) # xs) @ (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys))", simp)
by (rule maximum_map_append)


lemma maxFreshWords_P_rev:
  "maxFreshWords (rev (ss2 @ [s]  @ ss1)) = 
        max (maxFreshWords (rev ([s] @ ss1)))
            ((maxFreshWords (rev (ss2 @ [s]))) + sizeSVMStateST s - sizeSVMStateST (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: maxFreshWords.simps)

 apply (simp add: maxFreshWords.simps 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: maxFreshWords.simps add: maximum.simps add: map.simps)

 apply (simp, simp add: maxFreshWords.simps add: maximum.simps add: map.simps)
 apply (subst foldl_max_absorb0)
 apply (subgoal_tac "0 = sizeST si - sizeST si",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: maxFreshWords.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 = sizeST sx - sizeST sx") prefer 2 apply simp
 apply (subst maximum_map_sub_sizeST [where ys="xs @ (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys"])
 apply (subst maximum_map_sub_sizeST [where ys="xs @ [(hi, ri, pci, si)]"])
 apply (subst maximum_map_sub_sizeST [where ys="(hy, ry, pcy, sy) # ys"])
 apply (simp, subst max_maximum_sub, simp, rule sym)
 apply (subgoal_tac
  "maximum (map (λ(h, r, pc, y). sizeST y) (((hx, rx, pcx, sx) # xs) @ (hi, ri, pci, si) # (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys)) =
   maximum (map (λ(h, r, pc, y). sizeST y) (((hx, rx, pcx, sx) # xs) @ (hi, ri, pci, si) # (hy, ry, pcy, sy) # ys))", simp)
by (rule maximum_map_append)



lemma maxFreshWords_IntT:
  "[|s0 = ((h, k), k0, (q, j), S);
   length S > topDepth rho;
   S' = drop (topDepth rho) S|]   
   ==> 1 = maxFreshWords
       (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: maxFreshWords.simps)
apply (simp add: map.simps add: maximum.simps)
apply (simp add: sizeST.simps)
apply (subgoal_tac "sizeST (drop (topDepth rho) S) - sizeST S <= 0")
 apply simp
by (rule maxFreshWords_1)


lemma maxFreshWords_BoolT:
  "[|s0 = ((h, k), k0, (q, j), S);
   length S > topDepth rho;
   S' = drop (topDepth rho) S|]   
   ==> 1 = maxFreshWords
       (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: maxFreshWords.simps)
apply (simp add: map.simps add: maximum.simps)
apply (simp add: sizeST.simps)
apply (subgoal_tac "sizeST (drop (topDepth rho) S) - sizeST S <= 0")
 apply simp
by (rule maxFreshWords_1)


lemma maxFreshWords_VarE:
  "[|s0 = ((h, k), k0, (q, j), S);
   length S > topDepth rho;
   S' = drop (topDepth rho) S|]   
   ==> 1 = maxFreshWords
          (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: maxFreshWords.simps)
apply (simp add: map.simps add: maximum.simps)
apply (simp add: sizeST.simps)
apply (subgoal_tac "sizeST (drop (topDepth rho) S) - sizeST S <= 0")
 apply simp
by (rule maxFreshWords_1)


lemma maxFreshWords_CopyE:
  "[|s0 = ((h, k), k0, (q, ja), S);
   length S > topDepth rho;
   S' = drop (topDepth rho) S|]   
   ==> 2 = maxFreshWords
           (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: maxFreshWords.simps)
apply (simp add: map.simps add: maximum.simps)
apply (simp add: sizeST.simps)
apply (subgoal_tac "sizeST (drop (topDepth rho) S) - sizeST S <= 0")
 apply simp
by (rule maxFreshWords_1)


lemma maxFreshWords_ReuseE:
  "[| S' = drop (topDepth rho) S;
   length S > topDepth rho|] 
   ==> 1 = maxFreshWords
               (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 (simp add: maxFreshWords.simps)
apply (simp add: map.simps add: maximum.simps)
apply (simp add: sizeST.simps)
apply (subgoal_tac "sizeST (drop (topDepth rho) S) - sizeST S <= 0")
 apply simp
by (rule maxFreshWords_1)

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 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

lemma append_Nil3:
  "xs = xs @ []"
by simp

declare rev.simps [simp del]

declare restrictToRegion.simps [simp del]

lemma let1_1:
  "[|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);
    P\<turnstile>((h, k), k, (q1, j + 1), Cont (k0, q2) # S) , 0#td#tds -svm-> s # ss , Suc 0#td#tds;
    w = maxFreshWords (rev (s # ss));
    0 < w |] 
   ==> (maxFreshWords
                    (rev ([((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S)] @
                          ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # Cont (k0, q2) # S) #
                          ss @ [((h, k), k0, (q, j), S)]))) = s1+2"
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 simp
(* c2 *)
apply (subst cons_append [of "((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S)"])
apply (subst cons_append [of "((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # Cont (k0, q2) # S)"])
apply (subst maxFreshWords_P_rev)
(* c1 *)
apply (subst append_assoc_2)
apply (subst cons_cons_append)
apply (subst maxFreshWords_P_rev)
apply (simp add: rev.simps add: map.simps add: maxFreshWords.simps add: sizeSVMStateST.simps)
by (simp add: sizeST.simps add: maximum.simps)



lemma let1_2:
  "[|sa = ((h'', k) \<down> k0, k0, (q'a, ia), Val v2 # S'); 
   (δ2, m2, s2) = (δ', ma, wa);
    wa = maxFreshWords (rev (sa # ssa));
    ssa = ssa' @ [((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S)]|] 
  ==> (maxFreshWords
                 (rev (((h'', k) \<down> k0, k0, (q'a, ia), Val v2 # S') #
                       ssa' @ [((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S)])) +
                sizeST (Val v1 # S) -
                sizeSVMStateST
                 (hd (rev (((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k), k0, (q2, 0), Val v1 # S) #
                           ((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # Cont (k0, q2) # S) #
                           ss @ [((h, k), k0, (q, j), S)])))) = s2 + 1"
apply (simp add: rev.simps add: map.simps add: maxFreshWords.simps add: sizeSVMStateST.simps)
apply (simp add: sizeST.simps) 
done


lemma maxFreshWords_Let1:
  "[|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);
   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;
   w = maxFreshWords (rev (s # ss)); ma = maxFreshCells (rev (sa # ssa)); wa = maxFreshWords (rev (sa # ssa)); 0 < w|]
   ==> max (s1 + 2) (s2 + 1) =
          maxFreshWords
           (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 (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ssa=[]") defer
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)
apply (subst cons_append_assoc)
apply (subst cons_append [where xs ="((h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) \<down> k, k, (q', i), Val v1 # Cont (k0, q2) # S) #
                     ss @ [((h, k), k0, (q, j), S)]"])
apply (subst maxFreshWords_P_rev)
apply (subst let1_1,simp_all)  
apply (subst let1_2,simp_all) 
apply (rule conjI,simp)+
apply (rule refl)
apply (frule_tac s="(((h'', k) \<down> k0) \<down> k, k, (q', i), Val v2 # Cont (k0, q'a) # S')" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp) 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, k), k, (q1, Suc j), Cont (k0, q'a) # S')]" in ssubst,assumption)
apply (subst append_assoc)
apply (subst cons_append_assoc [of _ _ "([((h, k), k, (q1, (Suc j)), ((Cont (k0, q'a)) # S'))] @ [((h, k), k0, (q, j), S')])"])
apply (subst cons_append_assoc [of "((h'', k) \<down> k0, k0, (q'a, 0), Val v2 # S')"])
apply (subst maxFreshWords_P_rev)
apply (simp add: rev.simps add: map.simps add: maxFreshWords.simps add: sizeSVMStateST.simps)
apply (simp add: sizeST.simps add: maximum.simps)
done


lemma maxFreshWords_Let2:
  "[|sa = ((h', k) \<down> k0, k0, (q', i), Val v2 # S'); 
    P\<turnstile>((h(pa \<mapsto> (j, C, b)), k), k0, (q, Suc ja), Val (Loc pa) # S) , (td + 1)#tds -svm-> sa # ss , Suc 0#tds;
   (δ, m, s) = (δ', ma, w);
    w = maxFreshWords (rev (sa # ss)); 0 < w|]
    ==> s + 1 = maxFreshWords (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: maxFreshWords.simps add: maximum.simps add: map.simps)
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, b)), k), k0, (q, Suc ja), Val (Loc pa) # S)]" in ssubst,assumption)
apply simp
apply (subst cons_append_assoc)
apply (subst cons_append_assoc)
apply (subst cons_cons_append)
apply (subst maxFreshWords_P_rev)
apply (simp add: rev.simps add: map.simps add: maxFreshWords.simps add: sizeSVMStateST.simps)
apply (simp add: sizeST.simps) apply (simp add: maximum.simps)
done

lemma max_1:
  "[| max 0 a = a; max c b > 0 |]  ==>  max (c) (b) + a = max (max (0::int) (a::int)) (max (c) (b) + a)"
by simp
     
lemma max_2:
  "(a::int) > (b::int) ==> (max f c + a - b) = (max f c) + (a - b)"
by simp

lemma sizeST_Val_vs_length_vs:
"int (length vs) = sizeST (map Val vs @ S) - sizeST S"
apply (induct vs arbitrary: S)
 apply (simp add: map.simps)
by (simp add: map.simps add: sizeST.simps)


lemma maxFreshWords_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); w > 0; 
     w = maxFreshWords (rev (sa # ss))|]
      ==> 
     s + nr = maxFreshWords (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: maxFreshWords.simps add: maximum.simps add: map.simps) 
apply clarsimp
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 maxFreshWords_P_rev, simp)
apply (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps)
apply (case_tac vs,simp)
 apply (subgoal_tac "sizeST (map Val [] @ S) - sizeST S = 0",simp)
 apply (simp add: map.simps)
apply simp
apply (subgoal_tac "int (length vs) > 0") prefer 2 apply simp
apply (subgoal_tac "int (length vs) = sizeST (map Val vs @ S) - sizeST S",simp) 
apply (subgoal_tac "sizeST (map Val vs @ S) > sizeST S") 
apply (subgoal_tac "max 0 (sizeST (map Val vs @ S) - sizeST S) = sizeST (map Val vs @ S) - sizeST S",simp)
apply (subst max_1,simp+)
apply (subst max_2,simp) 
apply (simp, simp, simp)
by (rule sizeST_Val_vs_length_vs)

lemma maxFreshWords_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); w > 0;
     w = maxFreshWords (rev (sa # ss))|]
      ==> 
     s  = maxFreshWords (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: maxFreshWords.simps add: maximum.simps add: map.simps) 
apply clarsimp
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 maxFreshWords_P_rev, simp)
by (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps)


lemma maxFreshWords_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); w > 0; 
     w = maxFreshWords (rev (sa # ss))|]
      ==> 
     s + nr = maxFreshWords (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: maxFreshWords.simps add: maximum.simps add: map.simps) 
apply clarsimp
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 maxFreshWords_P_rev, simp)
apply (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps)
apply (case_tac vs,simp)
 apply (subgoal_tac "sizeST (map Val [] @ S) - sizeST S = 0",simp)
 apply (simp add: map.simps)
apply simp
apply (subgoal_tac "int (length vs) > 0") prefer 2 apply simp
apply (subgoal_tac "int (length vs) = sizeST (map Val vs @ S) - sizeST S",simp) 
apply (subgoal_tac "sizeST (map Val vs @ S) > sizeST S") 
apply (subgoal_tac "max 0 (sizeST (map Val vs @ S) - sizeST S) = sizeST (map Val vs @ S) - sizeST S",simp)
apply (subst max_1,simp+)
apply (subst max_2,simp) 
apply (simp, simp, simp)
by (rule sizeST_Val_vs_length_vs)


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 maxFreshWords_App_primops:
  " [|v1 = atom2val E1 a1; v2 = atom2val E1 a2; v = execOp oper v1 v2; topDepth rho < length S;
     fv (AppE f [a1, a2] [] a)  ⊆ dom (fst (E1, E2));
     ∀ a ∈ set [a1, a2]. atom a;
    (E1, E2) \<Join> ( rho ,  S) ; td = topDepth rho; k0 ≤ k; S' = drop td S|]
       ==> 2 = maxFreshWords
               (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,elim conjE)
apply (frule_tac a="a1" and k="k" in identityEnvironment_item_val,assumption+)
apply (frule_tac a="a2" and k="k" in identityEnvironment_item_val,assumption+)
apply (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps)
apply clarsimp
apply (simp add: sizeST.simps)
apply (frule maxFreshWords_1)
by simp


lemma sizeST_append:
"sizeST (xs @ ys) = sizeST xs + sizeST ys"
apply (induct xs arbitrary: ys) apply (simp add: sizeST.simps)
apply (simp add: sizeST.simps) apply (case_tac a)
apply (simp add: sizeST.simps)+
done



lemma sizeST_list_Val:
 "∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). a = Val v
 ==> sizeST ((map (item2Stack k S) (map (atom2item rho) as))) = int (length as)"
apply (induct as)
 apply (simp add: map.simps)
 apply (simp add: sizeST.simps)
 apply (simp add: map.simps)
 apply (simp add: sizeST.simps)
done

lemma sizeST_list_Reg:
 "∀ r ∈ set (map (item2Stack k S) (map (region2item rho) rr)). r = Reg r'
 ==> sizeST ((map (item2Stack k S) (map (region2item rho) rr))) = int (length rr)"
apply (induct rr)
 apply (simp add: map.simps)
 apply (simp add: sizeST.simps)
 apply (simp add: map.simps)
 apply (simp add: sizeST.simps)
done



lemma app1:
  "[| length as = length xs; ∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). a = Val v; td < length S;
     length rr = length rs; ∀ r ∈ set (map (item2Stack k S) (map (region2item rho) rr)). r = Reg r'|] 
    ==> maxFreshWords
                   (rev ([((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)))] @
                         ((h, k), k0, (q, Suc (Suc j)),
                         append (map (item2Stack k S) (map (atom2item rho) as))
                           (append (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)])) = int (length xs) + int (length rs)"
apply (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps) 
apply (subst sizeST_append)+ apply simp
apply (subst sizeST_list_Val [where v="v"],simp)+ 
apply (subst sizeST_list_Reg [where r'="r'"],simp)+ apply simp
by (frule maxFreshWords_1,simp)


declare identityEnvironment.simps [simp del]

lemma app2:
  "[|(E1, E2) \<Join> (rho,S); td = topDepth rho;
    length as = length xs; ∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). a = Val v;
    length rr = length rs; ∀ r ∈ set (map (item2Stack k S) (map (region2item rho) rr)). r = Reg r'; topDepth rho < length S|] 
    ==> 
    sizeSVMStateST
       ((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  (topDepth rho) S))) - 
   sizeSVMStateST
                (hd (rev ([((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 (topDepth rho) S)))] @
                          ((h, k), k0, (q, Suc (Suc j)),
                           append (map (item2Stack k S) (map (atom2item rho) as)) 
                                 (append (map (item2Stack k S) (map (region2item rho) rr)) ( drop (topDepth rho) S))) #
                          [((h, k), k0, (q, Suc j),
                            append (map (item2Stack k S) (map (atom2item rho) as)) 
                                 (append (map (item2Stack k S) (map (region2item rho) rr)) ( S)))] @
                          [((h, k), k0, (q, j), S)])))
  = int (length xs) + int (length rs) - int (topDepth rho)"
apply (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps)
apply (subst sizeST_append)+ 
apply (subst sizeST_list_Val [where v="v"],simp)
apply (subst sizeST_list_Reg [where r'="r'"],simp,simp)
by (frule continuations_bueno,assumption+,simp)


lemma maxFreshWords_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); 
     length as = length xs; length rr = length rs;
     finite (dom h); (E1, E2) \<Join> (rho,S); td = topDepth rho;
     s0 = ((h, k), k0, (q, j), S); td = topDepth rho; 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); 
     (δ, m, s) = (δ', ma, w);
      w = maxFreshWords (rev (sa # ss)); w > 0|]
       ==> max (int n + int l) (s + int n + int l - int td) =
          maxFreshWords
           (rev (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)]))"
apply (subgoal_tac  "∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). a = Val v")
 prefer 2 apply (rule app1_1)
apply (subgoal_tac "∀ r ∈ set (map (item2Stack k S) (map (region2item rho) rr)). r = Reg r'")
 prefer 2 apply (rule app1_2)
apply (frule_tac s="sa" in head_execSVMBalanced)
apply (case_tac "ss=[]",simp)
apply (simp add: rev.simps add: maxFreshWords.simps add: maximum.simps add: map.simps) 
apply clarsimp
apply (frule head_cons_execSVMBalanced,assumption+)
apply (erule exE) 
apply (drule_tac t="last ss" in sym, simp)
apply (subst cons_append_assoc [where x="((h', Suc k) \<down> k0, k0, (q', i), Val v # drop  (topDepth rho) S)"])
apply (subst cons_cons_append)
apply (subst cons_append 
       [where xs="((h, k), k0, (q, Suc (Suc j)),
            map (item2Stack k S) (map (atom2item rho) as) @ map (item2Stack k S) (map (region2item rho) rr) @ drop  (topDepth rho) 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 (subst cons_append_assoc [where x="((h', Suc k) \<down> k0, k0, (q', i), Val v # drop  (topDepth rho) S)"])
apply (subst maxFreshWords_P_rev)
apply (subgoal_tac "∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). a = Val v")
 prefer 2 apply (rule app1_1)
apply (subgoal_tac "∀ r ∈ set (map (item2Stack k S) (map (region2item rho) rr)). r = Reg r'")
 prefer 2 apply (rule app1_2)
apply (subst app1 [where xs="xs" and rs="rs"], assumption+)
apply (subgoal_tac
  "sizeSVMStateST
       ((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  (topDepth rho) S))) - 
   sizeSVMStateST
                (hd (rev ([((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 (topDepth rho) S)))] @
                          ((h, k), k0, (q, Suc (Suc j)),
                           append (map (item2Stack k S) (map (atom2item rho) as)) 
                                 (append (map (item2Stack k S) (map (region2item rho) rr)) ( drop (topDepth rho) S))) #
                          [((h, k), k0, (q, Suc j),
                            append (map (item2Stack k S) (map (atom2item rho) as)) 
                                 (append (map (item2Stack k S) (map (region2item rho) rr)) ( S)))] @
                          [((h, k), k0, (q, j), S)])))
  = int (length xs) + int (length rs) - int (topDepth rho)",simp)
by (rule app2, assumption+, simp, assumption+)

end