Theory diff_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. diff property *}

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

lemma empty_diff: "[]k = diff k h h"
by (simp add: diff_def add: emptyDelta_def, rule ext, simp)


lemma card_union_monotone: 
  " finite (dom h) ==> 
    card ({w. w = q ∧  region (h(p := None)(q \<mapsto> c), k) q = i} ∪ 
          {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i}) =
    card ({w. w = q ∧  region (h(p := None)(q \<mapsto> c), k) q = i})  +
    card ({w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i})"
apply (subgoal_tac "{w. w = q ∧  region (h(p := None)(q \<mapsto> c), k) q = i} ∩  
                    {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i} = {}")
 apply (subgoal_tac "finite {w. w = q ∧  region (h(p := None)(q \<mapsto> c), k) q = i}")
  apply (subgoal_tac "finite {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i}")
   apply (simp add: card_Un_Int)
  apply simp
 apply (case_tac "region (h(p := None)(q \<mapsto> c), k) q = i",simp,simp)
by blast

lemma card_union_monotone_2:  
  " finite (dom h) 
==> card ({w ∈ dom h. w = p ∧ region (h, k) p = i} ∪ 
          {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i}) =
    card ({w ∈ dom h. w = p ∧ region (h, k) p = i}) +
    card ({w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i})"
apply (subgoal_tac "{w ∈ dom h. w = p ∧ region (h, k) p = i} ∩  
                    {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i} = {}")
 apply (subgoal_tac "finite {w ∈ dom h. w = p ∧ region (h, k) p = i}") 
  apply (subgoal_tac "finite {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i}")
   apply (simp add: card_Un_Int)
  apply simp
 apply simp
by blast


lemma diff_monotone_aux_2:  
  "{w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i} =  
             {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i}"
apply (subgoal_tac 
  " w ∈ dom h --> w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i 
    ==> w ∈ dom h --> w ≠ p ∧ region (h(p := None), k) w = i")
 apply (subgoal_tac "w ∈ dom h --> w ≠ p ∧ region (h(p := None), k) w = i 
                     ==> w ∈ dom h --> region (h, k) w = i")
by (auto, simp_all add: region_def)

lemma diff_monotone_aux: 
  "[|finite (dom h);
    h p = Some c; 
    SafeHeap.fresh q h |] 
   ==> diff k (h, k) ((h(p := None))(q \<mapsto> c), k) = diff k (h,k) (h,k)"
apply (simp add: diff_def)
apply (unfold numCellsRegion_def)
apply (rule ext)
apply (case_tac "i <= k")
apply simp_all
apply (subgoal_tac 
  " {w. (((w = q) ∨ ((w ∈ (dom h)) ∧ (w ≠ p))) ∧ ((region (((h(p := None))(q \<mapsto> c)), k) w) = i))} =
    {w. w=q ∧ region (h(p := None)(q \<mapsto> c), k) q = i} ∪ 
    {w∈ dom h. w ∈ dom h ∧ w≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i}") 
 prefer 2 apply auto
apply (subgoal_tac 
  "[|  h p = Some c; 
    SafeHeap.fresh q h |]
  ==> {w ∈ dom h. region (h, k) w = i} =
    {w ∈ dom h. w = p ∧ region (h, k) p = i} ∪ 
    {w ∈ dom h. w ∈ dom h ∧ w≠ q ∧ w≠ p ∧ region (h, k) w = i}",simp) 
 prefer 2 apply (simp add: SafeHeap.fresh_def, blast) 
apply (subgoal_tac 
   " finite (dom h) 
     ==> card ({w. w = q ∧  region (h(p := None)(q \<mapsto> c), k) q = i} ∪ 
               {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i}) =
        card ({w. w = q ∧  region (h(p := None)(q \<mapsto> c), k) q = i})  +
        card ({w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i})",simp) 
prefer 2 apply (rule card_union_monotone,assumption)
apply (subgoal_tac 
  " finite (dom h) 
    ==> card ({w ∈ dom h. w = p ∧ region (h, k) p = i} ∪ 
              {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i}) =
        card ({w ∈ dom h. w = p ∧ region (h, k) p = i}) +
        card ({w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i})",simp)
 prefer 2 apply (rule card_union_monotone_2,assumption+)
apply (subgoal_tac
  "[| h p = Some c |] 
    ==> card {w. w=q ∧ region (h(p := None)(q \<mapsto> c), k) q = i} = 
        card {w. w = p ∧ region (h, k) p = i}",simp) 
prefer 2 
apply (subgoal_tac "region (h(p := None)(q \<mapsto> c), k) q =  region (h, k) p",simp)
 apply (case_tac "region (h, k) p = i",simp,simp)
apply (simp add: region_def)
apply (subgoal_tac
  " {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h(p := None)(q \<mapsto> c), k) w = i} = 
    {w ∈ dom h. w ≠ q ∧ w ≠ p ∧ region (h, k) w = i}",simp) 
prefer 2  apply (rule diff_monotone_aux_2)
apply (subgoal_tac "p ∈ dom h") prefer 2 apply (erule domI)
apply (subgoal_tac
  "p ∈ dom h 
   ==>  {w. w = p ∧ region (h, k) p = i} = 
        {w ∈ dom h. w = p ∧ region (h, k) p = i}")
apply simp
by blast


lemma diff_monotone: "[| finite (dom h); h p = Some c; SafeHeap.fresh q h |] 
       ==>  []k = diff k (h, k) (h(p := None)(q \<mapsto> c), k)"
apply (frule_tac h="h" and k="k" in diff_monotone_aux,assumption+,simp)
by (rule empty_diff)


lemma diff_IntT:
  "[]k = diff k (h, k) (h, k)"
by (rule empty_diff)

lemma diff_BoolT:
  "[]k = diff k (h, k) (h, k)"
by (rule empty_diff)

lemma diff_VarE:
  "[]k = diff k (h, k) (h, k)"
by (rule empty_diff)

lemma diff_CopyE:
  "[|m = SafeRASemantics.size h pa; 
    j <= k;
    SafeHeap.copy (h, k) j pa = ((h', k), p') |] 
   ==> [j \<mapsto> m] = diff k (h, k) (h', k)"
by (frule A7, elim conjE, simp)

lemma diff_ReuseE:
  "[| finite (dom h); h pa = Some c; SafeHeap.fresh q h |]
   ==> []k = diff k (h, k) (h(pa := None)(q \<mapsto> c), k)"
by (rule diff_monotone,assumption+)


lemma diff_Let1:
  "[|(δ1, m1, s1) = (δ, m, w); (δ2, m2, s2) = (δ', ma, wa);
    δ = diff k (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k);
    δ' = diff k (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) (h'', k)|] 
   ==> δ1 ⊕ δ2 = diff k (h, k) (h'', k)"
apply (unfold diff_def)
apply (unfold addDelta_def)
apply (rule ext) apply simp_all
apply auto
done


lemma diff_let2_aux2_1:
  "{w. w = p  ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j} =
   {w. w = p  ∧ region ([p \<mapsto> (j, C, as)], ka) w = j}"
apply auto
by (simp_all add: region_def)


lemma diff_let2_aux2_2:
  "fresh p ha ==>
   {w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j} =
   {w. w ∈ dom ha ∧ region (ha, ka) w = j}"
apply auto
apply (simp_all add: region_def)
apply (simp add: fresh_def)
apply (simp add: dom_def)
done

lemma diff_let2_aux2_3:
  "[| finite (dom ha);  fresh p ha |]  ==>
   card ({w ∈ dom ha. region (ha, ka) w = j} ∪ 
         {w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = j}) =
   card ({w ∈ dom ha. region (ha, ka) w = j}) + 
   card ({w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = j})"
apply (unfold region_def)
apply (unfold fresh_def)
apply auto
done


lemma diff_let2_aux2:
  "[| finite (dom ha); fresh p ha|]  ==>
   numCellsRegion (ha(p \<mapsto> (j, C, as)), ka) j =
   numCellsRegion (ha, ka) j  + numCellsRegion (empty(p \<mapsto> (j, C, as)), ka) j"
apply (unfold numCellsRegion_def)
apply auto
apply (subgoal_tac 
  "{w. (w = p ∨ w ∈ dom ha) ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j} =
   {w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j} ∪ 
   {w. w = p  ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j}")
prefer 2 apply blast
apply (subgoal_tac
  "{w. w = p  ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j} =
   {w. w = p  ∧ region ([p \<mapsto> (j, C, as)], ka) w = j}") prefer 2 apply (rule diff_let2_aux2_1)
apply (subgoal_tac
  "{w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = j} =
   {w. w ∈ dom ha ∧ region (ha, ka) w = j}") prefer 2 apply (rule diff_let2_aux2_2,assumption+)
apply simp
apply (subgoal_tac
  "finite (dom ha) ==>
   card ({w ∈ dom ha. region (ha, ka) w = j} ∪ 
         {w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = j}) =
   card ({w ∈ dom ha. region (ha, ka) w = j}) + 
   card ({w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = j})") prefer 2 apply (rule diff_let2_aux2_3,assumption+)
apply simp
done

(*
lemma diff_let2_aux3:
 "numCellsRegion ([p \<mapsto> (j, C, as)], ka) j = 1"
apply (simp add: numCellsRegion_def)
apply (simp add: region_def)
done
*)


lemma diff_let2_aux1:
  "[| finite (dom ha); fresh p ha|]  ==>
   numCellsRegion (ha(p \<mapsto> (j,(C,as))),ka) j =
   numCellsRegion (ha, ka) j + 1"
apply (subgoal_tac 
  "numCellsRegion (ha(p \<mapsto> (j, C, as)), ka) j =
   numCellsRegion (ha, ka) j  + numCellsRegion (empty(p \<mapsto> (j, C, as)), ka) j",simp)
apply (simp add: numCellsRegion_def)
apply (simp add: region_def)
by (rule diff_let2_aux2)


lemma diff_let2_aux4_1:
  "[|  SafeHeap.fresh p ha; i ≠j |]  ==>
   {w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w ∈ dom ha ∧ region (ha, ka) w = i}"
apply auto
apply (unfold region_def) apply (unfold  SafeHeap.fresh_def)
apply auto
done


lemma diff_let2_aux4_2:
  "[|  SafeHeap.fresh p ha; i ≠j |]  ==>
    {w. w = p ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} ∪
    {w ∈ dom ha. region (ha, ka) w = i} =
    {w ∈ dom ha. region (ha, ka) w = i}"
apply auto
apply (unfold region_def) apply (unfold  SafeHeap.fresh_def)
apply auto
done


lemma diff_let2_aux4:
  "[| finite (dom ha);  SafeHeap.fresh p ha; j ≤ ka; i ≠ j|]  ==> 
   numCellsRegion (ha(p \<mapsto> (j, C, as)), ka) i = numCellsRegion (ha, ka) i"
apply (unfold numCellsRegion_def)
apply auto
apply (subgoal_tac
  "{w. (w = p ∨ w ∈ dom ha) ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w = p ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} ∪
   {w. w≠p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i}")
prefer 2 apply blast
apply simp
apply (subgoal_tac
  "{w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w ∈ dom ha ∧ region (ha, ka) w = i}")
apply simp
apply (subgoal_tac
  " {w. w = p ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} ∪
    {w ∈ dom ha. region (ha, ka) w = i} =
    {w ∈ dom ha. region (ha, ka) w = i}")
apply simp
apply (rule diff_let2_aux4_2,assumption+)
apply (rule diff_let2_aux4_1,assumption+)
done



lemma diff_let2_aux2_1_otro:
  "{w. w = p  ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w = p  ∧ region ([p \<mapsto> (j, C, as)], ka) w = i}"
apply auto
by (simp_all add: region_def)

lemma diff_let2_aux2_2_otro:
  "fresh p ha ==>
   {w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w ∈ dom ha ∧ region (ha, ka) w = i}"
apply auto
apply (simp_all add: region_def)
apply (simp add: fresh_def)
apply (simp add: dom_def)
apply (simp add: fresh_def)
apply auto
done


lemma diff_let2_aux2_3_otro:
  "[| finite (dom ha);  fresh p ha; i ≠ j |]  ==>
   card ({w ∈ dom ha. region (ha, ka) w = i} ∪ 
         {w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = i}) =
   card ({w ∈ dom ha. region (ha, ka) w = i}) + 
   card ({w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = i})"
apply (unfold region_def)
apply (unfold fresh_def)
apply auto
done


lemma diff_let2_aux2_otro:
  "[| finite (dom ha); fresh p ha; i≠ j|]  ==>
   numCellsRegion (ha(p \<mapsto> (j, C, as)), ka) i =
   numCellsRegion (ha, ka) i  + numCellsRegion (empty(p \<mapsto> (j, C, as)), ka) i"
apply (unfold numCellsRegion_def)
apply auto
apply (subgoal_tac 
  "{w. (w = p ∨ w ∈ dom ha) ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} ∪ 
   {w. w = p  ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i}")
prefer 2 apply blast
apply (subgoal_tac
  "{w. w = p  ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w = p  ∧ region ([p \<mapsto> (j, C, as)], ka) w = i}") prefer 2 apply (rule diff_let2_aux2_1_otro)
apply (subgoal_tac
  "{w. w ≠ p ∧ w ∈ dom ha ∧ region (ha(p \<mapsto> (j, C, as)), ka) w = i} =
   {w. w ∈ dom ha ∧ region (ha, ka) w = i}") prefer 2 apply (rule diff_let2_aux2_2_otro,assumption+)
apply simp
apply (subgoal_tac
  "finite (dom ha) ==>
   card ({w ∈ dom ha. region (ha, ka) w = i} ∪ 
         {w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = i}) =
   card ({w ∈ dom ha. region (ha, ka) w = i}) + 
   card ({w. w = p ∧ region ([p \<mapsto> (j, C, as)], ka) w = i})") prefer 2 apply (rule diff_let2_aux2_3_otro,assumption+)
apply simp
done


lemma diff_Let2:
  "[| finite (dom h);  
     fresh pa h; 
     j ≤ k;
     (δ, m, s) = (δ', ma, w);
      δ' = diff k (h(pa \<mapsto> (j, C, map (atom2val E1) as)), k) (h', k)|]  
  ==> δ ⊕ [j \<mapsto> 1] = diff k (h, k) (h', k)"
apply (unfold diff_def)
apply (rule ext) apply simp_all
apply (case_tac "i <= k")
apply (unfold addDelta_def) 
apply clarsimp
apply (case_tac "i=j")
apply (subgoal_tac 
  "numCellsRegion (h(pa \<mapsto> (j, C, map (atom2val E1) as)), k) j = 
   numCellsRegion (h, k) j + 1")
prefer 2 apply (rule diff_let2_aux1,assumption+)
 apply auto
apply (subgoal_tac
  "numCellsRegion (h(pa \<mapsto> (j, C, map (atom2val E1) as)), k) i =
   numCellsRegion (h, k) i  + numCellsRegion (empty(pa \<mapsto> (j, C, map (atom2val E1) as)), k) i")
prefer 2 apply (rule diff_let2_aux2_otro,assumption+) apply simp 
apply (simp add: numCellsRegion_def)
apply (simp add: region_def)
done


lemma cased_aux1:
  "[|finite (dom h); h pa = Some (j, C, vs); j ≤ k; i ≤ k; i ≠ j|] 
   ==> numCellsRegion (h(pa := None), k) i = numCellsRegion (h, k) i"
apply (unfold numCellsRegion_def, auto)
apply (subgoal_tac "{w ∈ dom h. w ≠ pa ∧ region (h(pa := None), k) w = i} =  
                    {w ∈ dom h. region (h, k) w = i}",simp)
by (simp add: region_def, auto)


lemma cased_aux2_1: "h pa = Some (j, C, vs) ==> {w ∈ dom h. w=pa ∧ region (h,k) w = j} = {pa}"
by (simp add: region_def,auto)

lemma cased_aux2_2:
  "[| finite (dom h);  h pa = Some (j, C, vs) |] 
  ==> int (card ({w ∈ dom h. region (h, k) w = j} - {pa})) = int (card {w ∈ dom h. region (h, k) w = j}) - 1"
apply (subgoal_tac "pa ∈ {w ∈ dom h. region (h, k) w = j}")
 apply (subst card_Diff_singleton,simp,simp)
 apply (subgoal_tac "card {w ∈ dom h. region (h, k) w = j} >= 1",simp)
 apply (subgoal_tac "∃S'. {w ∈ dom h. region (h, k) w = j} = S' ∪ {pa} ∧ pa ∉ S'")
  apply (erule exE, simp) apply (elim conjE) apply (subst card_insert_if) 
   defer apply simp
  apply (rule_tac x="{w ∈ dom h. w ≠ pa ∧ region (h, k) w = j}" in exI, simp)
  apply (simp add: region_def, auto)
 apply (simp add: region_def)
apply (subgoal_tac "S' = {w ∈ dom h. w ≠ pa ∧ region (h, k) w = j}",simp)
by (simp add: region_def,auto)

lemma cased_aux2:
  "[|finite (dom h); h pa = Some (j, C, vs); j ≤ k|] 
  ==> numCellsRegion (h(pa := None), k) j = numCellsRegion (h, k) j - 1"
apply (simp add: numCellsRegion_def)
apply (subgoal_tac "{w ∈ dom h. w ≠ pa ∧ region (h(pa := None), k) w = j} =  
                    {w ∈ dom h. region (h, k) w = j} - 
                    {w ∈ dom h. w=pa ∧ region (h,k) w = j}",simp)
apply (subst cased_aux2_1,assumption+)
apply (rule cased_aux2_2, assumption+)
by (simp add: region_def,auto)


lemma diff_CaseD:
  "[| finite (dom h);  
     h pa = Some (j, C, vs);
    (δ, m, s) = (δ', ma, w); j <= k;
    δ' = diff k (h(pa := None), k) (h', k)|]  
  ==> δ ⊕ [j \<mapsto> -1] = diff k (h, k) (h', k)"
apply (unfold diff_def)
apply (rule ext, simp_all)
apply (case_tac "i <= k")
 apply (unfold addDelta_def, clarsimp)
 apply (case_tac "i=j")
  apply (subgoal_tac  "numCellsRegion (h(pa:=None), k) j = numCellsRegion (h, k) j - 1", auto) 
 apply (rule cased_aux2, assumption+)
by (rule cased_aux1, assumption+)


lemma diff_App1:
  "diff k (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) =  diff k (h, k) (h', k)"
apply (unfold diff_def)
apply (rule ext, simp, rule impI)
apply (unfold numCellsRegion_def, simp add: restrict_map_def, unfold region_def) 
apply (case_tac "(λx. if x ∈ dom h' ∧ fst (the (h' x)) ≤ k then h' x else None, k)",auto)
apply (subgoal_tac "i ≤ k ==>
        {w. (w ∈ dom h' ∧ fst (the (h' w)) ≤ k -->
                  w ∈ dom (λx. if x ∈ dom h' ∧ fst (the (h' x)) ≤ k then h' x else None) ∧
                  option_case undefined (prod_case (λr. prod_case (λc xs. r))) (h' w) = i) ∧
                 ((w ∈ dom h' --> ¬ fst (the (h' w)) ≤ k) -->
                  w ∈ dom (λx. if x ∈ dom h' ∧ fst (the (h' x)) ≤ k then h' x else None) ∧ undefined = i)} =
        {w ∈ dom h'. option_case undefined (prod_case (λr. prod_case (λc xs. r))) (h' w) = i}", simp, auto)
  apply (split split_if_asm) 
   apply (erule_tac x="a" in allE, erule_tac x="aa" in allE, erule_tac x="b" in allE, simp)
  apply simp
 apply (split split_if_asm) 
   apply (erule_tac x="a" in allE, erule_tac x="aa" in allE, erule_tac x="b" in allE, simp)
by (simp, split split_if_asm,simp,simp)


lemma diff_App2:
  "diff k (h,k) (h',k) = (diff (k+1) (h,k+1) (h',k+1))(k + 1 := None)"
apply (unfold diff_def)
apply (rule ext)
apply simp
apply (rule impI) apply (rule impI)
apply (subgoal_tac "numCellsRegion (h, Suc k) i = numCellsRegion (h, k) i",simp)
 apply (subgoal_tac "numCellsRegion (h', k) i = numCellsRegion (h', Suc k) i",simp)
 apply (simp add: numCellsRegion_def add: region_def)
by (simp add: numCellsRegion_def add: region_def)



lemma diff_App:
  "[| (δ, m, s) = (δ', ma, w);
     δ' = diff (k + 1) (h, k + 1) (h', k + 1)|] 
  ==> δ(k + 1 := None) = diff k (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)"
apply simp
apply (subgoal_tac "diff k (h,k) (h',k) = (diff (k+1) (h,k+1) (h',k+1))(k + 1 := None)",simp)
 apply (subgoal_tac "diff k (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k) =  diff k (h, k) (h', k)",simp)
 apply (rule diff_App1)
by (rule diff_App2)


end