Theory AutoCorres2.SepFrame

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* License: BSD, terms see file ./LICENSE *)

theory SepFrame
imports SepTactic
begin

class heap_state_type'

instance heap_state_type'  type ..

consts
  hst_mem :: "'a::heap_state_type'  heap_mem"
  hst_mem_update :: "(heap_mem  heap_mem)  'a::heap_state_type'  'a"
  hst_htd :: "'a::heap_state_type'  heap_typ_desc"
  hst_htd_update :: "(heap_typ_desc  heap_typ_desc)  'a::heap_state_type'  'a"

class heap_state_type = heap_state_type' +
  assumes hst_htd_htd_update [simp]: "hst_htd (hst_htd_update d s) = d (hst_htd s)"
  assumes hst_mem_mem_update [simp]: "hst_mem (hst_mem_update h s) = h (hst_mem s)"
  assumes hst_htd_mem_update [simp]: "hst_htd (hst_mem_update h s) = hst_htd s"
  assumes hst_mem_htd_update [simp]: "hst_mem (hst_htd_update d s) = hst_mem s"

translations
  "s hst_mem := x" <= "CONST hst_mem_update (K_record x) s"
  "s hst_htd := x" <= "CONST hst_htd_update (K_record x) s"

definition lift_hst :: "'a::heap_state_type'  heap_state" where
  "lift_hst s  lift_state (hst_mem s,hst_htd s)"

definition point_eq_mod :: "('a  'b)  ('a  'b)  'a set  bool" where
  "point_eq_mod f g X  x. x  X  f x = g x"

definition exec_fatal :: "('s,'b,'c) com  ('s,'b,'c) body  's  bool" where
  "exec_fatal C Γ s  (f. Γ  C,Normal s  Fault f)  (Γ  C,Normal s  Stuck)"

definition restrict_htd :: "'s::heap_state_type'  s_addr set  's" where
  "restrict_htd s X  s hst_htd := restrict_s (hst_htd s) X "

definition restrict_safe_OK ::
  "'s  's  ('s  ('s,'c) xstate)  s_addr set  ('s::heap_state_type','b,'c) com 
     ('s,'b,'c) body  bool" where
  "restrict_safe_OK s t f X C Γ 
      Γ  C,(Normal (restrict_htd s X))  f (restrict_htd t X) 
      point_eq_mod (lift_state (hst_mem t,hst_htd t)) (lift_state (hst_mem s,hst_htd s)) X"

definition restrict_safe ::
  "'s  ('s,'c) xstate  ('s::heap_state_type','b,'c) com  ('s,'b,'c) body  bool" where
  "restrict_safe s t C Γ 
     X. (case t of
            Normal t'  restrict_safe_OK s t' Normal X C Γ
          | Abrupt t'  restrict_safe_OK s t' Abrupt X C Γ
          | _  False) 
         exec_fatal C Γ (restrict_htd s X)"

definition mem_safe :: "('s::{heap_state_type',type},'b,'c) com  ('s,'b,'c) body  bool" where
  "mem_safe C Γ  s t. Γ  C,Normal s  t  restrict_safe s t C Γ"

definition point_eq_mod_safe ::
  "'s::{heap_state_type',type} set  ('s  's)  ('s  s_addr  'c)  bool" where
  "point_eq_mod_safe P f g  s X. restrict_htd s X  P  point_eq_mod (g (f s)) (g s) X"

definition comm_restrict :: "('s::{heap_state_type',type}  's)  's  s_addr set  bool" where
  "comm_restrict f s X  f (restrict_htd s X) = restrict_htd (f s) X"

definition comm_restrict_safe :: "'s set  ('s::{heap_state_type',type}  's)  bool" where
  "comm_restrict_safe P f  s X. restrict_htd s X  P  comm_restrict f s X"

definition htd_ind :: "('a::{heap_state_type',type}  'b)  bool" where
  "htd_ind f  x s. f s = f (hst_htd_update x s)"

definition mono_guard :: "'s::{heap_state_type',type} set  bool" where
  "mono_guard P  s X. restrict_htd s X  P  s  P"

definition expr_htd_ind :: "'s::{heap_state_type',type} set  bool" where
  "expr_htd_ind P  d s. s hst_htd := d   P = (s  P)"

primrec intra_safe :: "('s::heap_state_type','b,'c) com   bool"
where
  "intra_safe Skip = True"
| "intra_safe (Basic f) = (comm_restrict_safe UNIV f 
      point_eq_mod_safe UNIV f (λs. lift_state (hst_mem s,hst_htd s)))"
| "intra_safe (Spec r) = (Γ. mem_safe (Spec r) (Γ :: ('s,'b,'c) body))"
| "intra_safe (Seq C D) = (intra_safe C  intra_safe D)"
| "intra_safe (Cond P C D) = (expr_htd_ind P  intra_safe C  intra_safe D)"
| "intra_safe (While P C) = (expr_htd_ind P  intra_safe C)"
| "intra_safe (Call p) = True"
| "intra_safe (DynCom f) = (htd_ind f  (s. intra_safe (f s)))"
| "intra_safe (Guard f P C) = (mono_guard P  (case C of
      Basic g  comm_restrict_safe P g 
                 point_eq_mod_safe P g (λs. lift_state (hst_mem s,hst_htd s))
      | _  intra_safe C))"
| "intra_safe Throw = True"
| "intra_safe (Catch C D) = (intra_safe C  intra_safe D)"

instance state_ext :: (heap_state_type',type) heap_state_type' ..

overloading
  hs_mem_state  hst_mem
  hs_mem_update_state  hst_mem_update
  hs_htd_state  hst_htd
  hs_htd_update_state  hst_htd_update
begin
  definition hs_mem_state [simp]: "hs_mem_state  hst_mem  globals"
  definition hs_mem_update_state [simp]: "hs_mem_update_state  globals_update  hst_mem_update"
  definition hs_htd_state[simp]: "hs_htd_state  hst_htd  globals"
  definition hs_htd_update_state [simp]: "hs_htd_update_state  globals_update  hst_htd_update"
end

instance state_ext :: (heap_state_type,type) heap_state_type
  by intro_classes auto

primrec
  intra_deps :: "('s','b,'c) com  'b set"
where
  "intra_deps Skip = {}"
| "intra_deps (Basic f) = {}"
| "intra_deps (Spec r) = {}"
| "intra_deps (Seq C D) = (intra_deps C  intra_deps D)"
| "intra_deps (Cond P C D) = (intra_deps C  intra_deps D)"
| "intra_deps (While P C) = intra_deps C"
| "intra_deps (Call p) = {p}"
| "intra_deps (DynCom f) = {intra_deps (f s) | s. True}"
| "intra_deps (Guard f P C) = intra_deps C"
| "intra_deps Throw = {}"
| "intra_deps (Catch C D) = (intra_deps C  intra_deps D)"


inductive_set
  proc_deps :: "('s','b,'c) com  ('s,'b,'c) body  'b set"
  for "C" :: "('s','b,'c) com"
  and "Γ" :: "('s,'b,'c) body"
where
  "x  intra_deps C  x  proc_deps C Γ"
| " x  proc_deps C Γ; Γ x = Some D; y  intra_deps D   y  proc_deps C Γ"

text ‹----›

lemma point_eq_mod_refl [simp]:
  "point_eq_mod f f X"
  by (simp add: point_eq_mod_def)

lemma point_eq_mod_subs:
  " point_eq_mod f g Y; Y  X   point_eq_mod f g X"
  by (force simp: point_eq_mod_def)

lemma point_eq_mod_trans:
  " point_eq_mod x y X; point_eq_mod y z X   point_eq_mod x z X"
  by (force simp: point_eq_mod_def)

lemma mem_safe_NormalD:
  " Γ  C,Normal s  Normal t; mem_safe C Γ;
      ¬ exec_fatal C Γ (restrict_htd s X)  
      (Γ  C,(Normal (restrict_htd s X))  Normal (restrict_htd t X) 
       point_eq_mod (lift_state (hst_mem t,hst_htd t))
          (lift_state (hst_mem s,hst_htd s)) X)"
  by (force simp: mem_safe_def restrict_safe_def restrict_safe_OK_def)

lemma mem_safe_AbruptD:
  " Γ  C,Normal s  Abrupt t; mem_safe C Γ;
      ¬ exec_fatal C Γ (restrict_htd s X)  
      (Γ  C,(Normal (restrict_htd s X))  Abrupt (restrict_htd t X) 
       point_eq_mod (lift_state (hst_mem t,hst_htd t))
          (lift_state (hst_mem s,hst_htd s)) X)"
  by (force simp: mem_safe_def restrict_safe_def restrict_safe_OK_def)

lemma mem_safe_FaultD:
  " Γ  C,Normal s  Fault f; mem_safe C Γ  
      exec_fatal C Γ (restrict_htd s X)"
  by (force simp: mem_safe_def restrict_safe_def)

lemma mem_safe_StuckD:
  " Γ  C,Normal s  Stuck; mem_safe C Γ  
      exec_fatal C Γ (restrict_htd s X)"
  by (force simp: mem_safe_def restrict_safe_def)

lemma lift_state_d_restrict [simp]:
  "lift_state (h,(restrict_s d X)) = lift_state (h,d) |` X"
  by (auto simp: lift_state_def restrict_map_def restrict_s_def split: s_heap_index.splits)

lemma dom_merge_restrict [simp]:
  "(x ++ y) |` dom y = y"
  by (rule map_add_restrict_dom_right)

lemma dom_compl_restrict [simp]:
  "x |` (UNIV - dom x) = Map.empty"
  by (force simp: restrict_map_def)

lemma lift_state_point_eq_mod:
  " point_eq_mod (lift_state (h,d)) (lift_state (h',d')) X  
      lift_state (h,d) |` (UNIV - X) =
          lift_state (h',d') |` (UNIV - X)"
  by (auto simp: point_eq_mod_def restrict_map_def)

lemma htd_'_update_ind [simp]:
  "htd_ind f  f (hst_htd_update x s) = f s"
  by (simp add: htd_ind_def)

lemma sep_frame':
  assumes orig_spec:  "s. Γ  s. P (f ´(λx. x)) (lift_hst ´(λx. x))
                               C
                               Q (g s ´(λx. x)) (lift_hst ´(λx. x))"
      and hi_f: "htd_ind f" and hi_g: "htd_ind g"
      and hi_g': "s. htd_ind (g s)"
      and safe: "mem_safe (C::('s::heap_state_type,'b,'c) com) Γ"
  shows "s. Γ  s. (P (f ´(λx. x)) * R (h ´(λx. x))) (lift_hst ´(λx. x))
                 C
                 (Q (g s ´(λx. x)) * R (h s)) (lift_hst ´(λx. x))"
  apply (standard, rule hoare_complete, simp only: valid_def, clarify)
proof -
  fix ta x
  assume ev: "Γ C,Normal x  ta" and
      pre: "(P (f x) * R (h x)) (lift_hst x)"
  then obtain s0 and s1 where pre_P: "P (f x) s0" and pre_R: "R (h x) s1" and
      disj: "s0  s1" and m: "lift_hst x = s1 ++ s0"
    by (clarsimp simp: sep_conj_def map_ac_simps)
  with orig_spec hi_f have nofault: "¬ exec_fatal C Γ
      (restrict_htd x (dom s0))"
    by (force simp: exec_fatal_def image_def lift_hst_def cvalid_def valid_def
                    restrict_htd_def
              dest: hoare_sound)
  show "ta  Normal ` {t. (Q (g x t) * R (h x)) (lift_hst t)}"
  proof (cases ta)
    case (Normal s)
    moreover from this ev safe nofault have ev': "Γ 
        C,Normal (x hst_htd := (restrict_s (hst_htd x) (dom s0)) ) 
           Normal (s hst_htd := (restrict_s (hst_htd s) (dom s0)) )" and
        "point_eq_mod (lift_state (hst_mem s,hst_htd s))
            (lift_state (hst_mem x,hst_htd x)) (dom s0)"
      by (auto simp: restrict_htd_def dest: mem_safe_NormalD)
    moreover from this m disj have "s1 = lift_hst s |` (UNIV - dom s0)"
      apply(clarsimp simp: lift_hst_def)
      apply(subst lift_state_point_eq_mod)
       apply(fastforce dest: sym)
      apply(simp add: lift_hst_def lift_state_point_eq_mod map_add_restrict)
      apply(subst restrict_map_subdom, auto dest: map_disjD)
      done
    ultimately show ?thesis using orig_spec hi_f hi_g hi_g' pre_P pre_R m
      by (force simp: cvalid_def valid_def image_def lift_hst_def
                      map_disj_def
                intro: sep_conjI dest: hoare_sound)
  next
    case (Abrupt s) with ev safe nofault orig_spec pre_P hi_f m show ?thesis
      apply simp
      apply (drule spec)
      apply (drule hoare_sound)
      apply (drule_tac X="dom s0" in mem_safe_AbruptD)
      by (assumption+, force simp: valid_def cvalid_def lift_hst_def restrict_htd_def)
  next
    case (Fault f) with ev safe nofault show ?thesis
      by (force dest: mem_safe_FaultD)
  next
    case Stuck with ev safe nofault show ?thesis
      by (force dest: mem_safe_StuckD)
  qed
qed

lemma sep_frame:
  " k = (λs. (hst_mem s,hst_htd s));
      s. Γ  s. P (f ´(λx. x)) (lift_state (k ´(λx. x)))
              C
              Q (g s ´(λx. x)) (lift_state (k ´(λx. x)));
      htd_ind f; htd_ind g; s. htd_ind (g s);
      mem_safe (C::('s::heap_state_type,'b,'c) com) Γ  
      s. Γ  s. (P (f ´(λx. x)) * R (h ´(λx. x))) (lift_state (k ´(λx. x)))
               C
               (Q (g s ´(λx. x)) * R (h s)) (lift_state (k ´(λx. x)))"
  apply(simp only:)
  apply(fold lift_hst_def)
  apply(erule (4) sep_frame')
  done


lemma point_eq_mod_safe [simp]:
  " point_eq_mod_safe P f g; restrict_htd s X  P; x  X  
      g (f s) x = (g s) x"
  apply(simp add: point_eq_mod_safe_def point_eq_mod_def)
  apply(cases x, force)
  done

lemma comm_restrict_safe [simp]:
  " comm_restrict_safe P f; restrict_htd s X  P  
        restrict_htd (f s ) X = f (restrict_htd s X)"
  by (simp add: comm_restrict_safe_def comm_restrict_def)

lemma mono_guardD:
  " mono_guard P; restrict_htd s X  P   s  P"
  by (unfold mono_guard_def, fast)

lemma expr_htd_ind:
  "expr_htd_ind P  restrict_htd s X  P = (s  P)"
  by (simp add: expr_htd_ind_def restrict_htd_def)

(* exec.intros without those already declared as [intro] *)
lemmas exec_other_intros = exec.intros(1-3) exec.intros(5-14) exec.intros(16-17) exec.intros(19-)

lemma exec_fatal_Seq:
  "exec_fatal C Γ s  exec_fatal (C;;D) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros)

lemma exec_fatal_Seq2:
  " Γ  C,Normal s  Normal t; exec_fatal D Γ t   exec_fatal (C;;D) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros)

lemma exec_fatal_Cond:
  "exec_fatal (Cond P C D) Γ s = (if s  P then exec_fatal C Γ s else
      exec_fatal D Γ s)"
  by (force simp: exec_fatal_def intro: exec_other_intros
            elim: exec_Normal_elim_cases)

lemma exec_fatal_While:
  " exec_fatal C Γ s; s  P   exec_fatal (While P C) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros
            elim: exec_Normal_elim_cases)

lemma exec_fatal_While2:
  " exec_fatal (While P C) Γ t; Γ  C,Normal s  Normal t; s  P  
      exec_fatal (While P C) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros
            elim: exec_Normal_elim_cases)

lemma exec_fatal_Call:
  " Γ p = Some C; exec_fatal C Γ s   exec_fatal (Call p) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros)

lemma exec_fatal_DynCom:
  "exec_fatal (f s) Γ s  exec_fatal (DynCom f) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros)

lemma exec_fatal_Guard:
  "exec_fatal (Guard f P C) Γ s = (s  P  exec_fatal C Γ s)"
proof (cases "s  P")
  case True thus ?thesis
    by (force simp: exec_fatal_def intro: exec_other_intros
              elim: exec_Normal_elim_cases)
next
  case False thus ?thesis
    by (force simp: exec_fatal_def intro: exec_other_intros)
qed

lemma restrict_safe_Guard:
  assumes restrict: "restrict_safe s t C Γ"
  shows "restrict_safe s t (Guard f P C) Γ"
proof (cases t)
  case (Normal s) with restrict show ?thesis
    by (force simp: restrict_safe_def restrict_safe_OK_def exec_fatal_Guard
              intro: exec_other_intros)
next
  case (Abrupt s) with restrict show ?thesis
    by (force simp: restrict_safe_def restrict_safe_OK_def exec_fatal_Guard
              intro: exec_other_intros)
next
  case (Fault f) with restrict show ?thesis
    by (force simp: restrict_safe_def exec_fatal_Guard)
next
  case Stuck with restrict show ?thesis
    by (force simp: restrict_safe_def exec_fatal_Guard)
qed

lemma restrict_safe_Guard2:
  " s  P; mono_guard P   restrict_safe s (Fault f) (Guard f P C) Γ"
  by (force simp: restrict_safe_def exec_fatal_def intro: exec_other_intros
            dest: mono_guardD)

lemma exec_fatal_Catch:
  "exec_fatal C Γ s  exec_fatal (TRY C CATCH D END) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros)

lemma exec_fatal_Catch2:
  " Γ  C,Normal s  Abrupt t; exec_fatal D Γ t  
      exec_fatal (TRY C CATCH D END) Γ s"
  by (force simp: exec_fatal_def intro: exec_other_intros)

lemma intra_safe_restrict [rule_format]:
  assumes safe_env: "n C. Γ n = Some C  intra_safe C" and
      exec: "Γ  C,s  t"
  shows "s'. s = Normal s'  intra_safe C  restrict_safe s' t C Γ"
using exec
proof induct
  case (Skip s) thus ?case
    by (force simp: restrict_safe_def restrict_safe_OK_def intro: exec_other_intros)
next
  case (Guard s' P C t f) show ?case
  proof (cases "g. C = Basic g")
    case False with Guard show ?thesis
      by - (clarsimp, split com.splits, auto dest: restrict_safe_Guard)
  next
    case True with Guard show ?thesis
      by (cases t) (force simp: restrict_safe_def restrict_safe_OK_def
                                point_eq_mod_safe_def exec_fatal_Guard
                          intro: exec_other_intros
                          elim: exec_Normal_elim_cases,
                    (fast elim: exec_Normal_elim_cases)+)
  qed
next
  case (GuardFault C f P s) thus ?case
    by (force dest: restrict_safe_Guard2)
next
  case (FaultProp C f) thus ?case by simp
next
  case (Basic f s) thus ?case
    by (force simp: restrict_safe_def restrict_safe_OK_def point_eq_mod_safe_def
              intro: exec_other_intros)
next
  case (Spec r s t) thus ?case
    by (fastforce simp: mem_safe_def intro: exec.Spec)
next
  case (SpecStuck r s) thus ?case
    by (simp add: exec.SpecStuck mem_safe_StuckD restrict_safe_def)
next
  case (Seq C s sa D ta) show ?case
  proof (cases sa)
    case (Normal s') with Seq show ?thesis
      by (cases ta)
         (clarsimp simp: restrict_safe_def restrict_safe_OK_def,
          (drule_tac x=X in spec)+, auto intro: exec_other_intros point_eq_mod_trans
                                               exec_fatal_Seq exec_fatal_Seq2)+
  next
    case (Abrupt s') with Seq show ?thesis
      by (force simp: restrict_safe_def restrict_safe_OK_def
                intro: exec_other_intros dest: exec_fatal_Seq
                elim: exec_Normal_elim_cases)
  next
    case (Fault f) with Seq show ?thesis
      by (force simp: restrict_safe_def dest: exec_fatal_Seq
                elim: exec_Normal_elim_cases)
  next
    case Stuck with Seq show ?thesis
      by (force simp: restrict_safe_def dest: exec_fatal_Seq
                elim: exec_Normal_elim_cases)
  qed
next
  case (CondTrue s P C t D) thus ?case
    by (cases t)
       (auto simp: restrict_safe_def restrict_safe_OK_def exec_fatal_Cond
             intro: exec_other_intros dest: expr_htd_ind split: if_split_asm)
next
  case (CondFalse s P C t D) thus ?case
    by (cases t)
       (auto simp: restrict_safe_def restrict_safe_OK_def exec_fatal_Cond
             intro: exec_other_intros dest: expr_htd_ind split: if_split_asm)
next
  case (WhileTrue P C s s' t) show ?case
  proof (cases s')
    case (Normal sa) with WhileTrue show ?thesis
      by (cases t)
         (clarsimp simp: restrict_safe_def restrict_safe_OK_def,
          (drule_tac x=X in spec)+, auto simp: expr_htd_ind intro: exec_other_intros
               point_eq_mod_trans exec_fatal_While exec_fatal_While2)+
  next
    case (Abrupt sa) with WhileTrue show ?thesis
      by (force simp: restrict_safe_def restrict_safe_OK_def expr_htd_ind
                intro: exec_other_intros exec_fatal_While
                elim: exec_Normal_elim_cases)
  next
    case (Fault f) with WhileTrue show ?thesis
      by (force simp: restrict_safe_def expr_htd_ind intro: exec_fatal_While)
  next
    case Stuck with WhileTrue show ?thesis
      by (force simp: restrict_safe_def expr_htd_ind intro: exec_fatal_While)
  qed
next
  case (WhileFalse P C s) thus ?case
    by (force simp: restrict_safe_def restrict_safe_OK_def expr_htd_ind
              intro: exec_other_intros)
next
  case (Call C p s t) with safe_env show ?case
    by (cases t)
       (auto simp: restrict_safe_def restrict_safe_OK_def
             intro: exec_fatal_Call exec_other_intros)
next
  case (CallUndefined p s) thus ?case
    by (force simp: restrict_safe_def exec_fatal_def intro: exec_other_intros)

next
  case (StuckProp C) thus ?case by simp
next
  case (DynCom f s t) thus ?case
    by (cases t)
       (auto simp: restrict_safe_def restrict_safe_OK_def
                   restrict_htd_def
             intro!: exec_other_intros exec_fatal_DynCom)
next
  case (Throw s) thus ?case
    by (force simp: restrict_safe_def restrict_safe_OK_def intro: exec_other_intros)
next
  case (AbruptProp C s) thus ?case by simp
next
  case (CatchMatch C D s s' t) thus ?case
    by (cases t)
       (clarsimp simp: restrict_safe_def, drule_tac x=X in spec,
        auto simp: restrict_safe_OK_def intro: exec_other_intros point_eq_mod_trans
             dest: exec_fatal_Catch exec_fatal_Catch2)+
next
  case (CatchMiss C s t D) thus ?case
    by (cases t)
       (clarsimp simp: restrict_safe_def, drule_tac x=X in spec,
        auto simp: restrict_safe_OK_def intro: exec_other_intros
             dest: exec_fatal_Catch)+
qed

lemma intra_mem_safe:
  " n C. Γ n = Some C  intra_safe C; intra_safe C   mem_safe C Γ"
  by (force  simp: mem_safe_def intro: intra_safe_restrict)

lemma point_eq_mod_safe_triv:
  "(s. g (f s) = g s)  point_eq_mod_safe P f g"
  by (simp add: point_eq_mod_safe_def point_eq_mod_def)

lemma comm_restrict_safe_triv:
  "(s X. f (s hst_htd := restrict_s (hst_htd s) X ) =
      (f s) hst_htd := restrict_s (hst_htd (f s)) X )  comm_restrict_safe P f"
  by (force simp: comm_restrict_safe_def comm_restrict_def restrict_htd_def)

lemma mono_guard_UNIV [simp]:
  "mono_guard UNIV"
  by (force simp: mono_guard_def)

lemma mono_guard_triv:
  "(s X. s hst_htd := X   g  s  g)  mono_guard g"
  by (unfold mono_guard_def, unfold restrict_htd_def, fast)

lemma mono_guard_triv2:
  "(s X. s hst_htd := X   g = ((s::'a::heap_state_type')  g)) 
      mono_guard g"
  by (unfold mono_guard_def, unfold restrict_htd_def, fast)

lemma dom_restrict_s:
  "x  dom_s (restrict_s d X)  x  dom_s d  x  X"
  by (auto simp: restrict_s_def dom_s_def split: if_split_asm)

lemma mono_guard_ptr_safe:
  " s. d s = hst_htd (s::'a::heap_state_type); htd_ind p  
      mono_guard {s. ptr_safe (p s) (d s)}"
  by (auto simp: mono_guard_def ptr_safe_def restrict_htd_def dest: subsetD dom_restrict_s)

lemma point_eq_mod_safe_ptr_safe_update:
  " d = (hst_htd::'a::heap_state_type  heap_typ_desc);
      m = (λs. hst_mem_update (heap_update (p s) ((v s)::'b::mem_type)) s);
      h = hst_mem; k = (λs. lift_state (h s,d s)); htd_ind p  
      point_eq_mod_safe {s. ptr_safe (p s) (d s)} m k"
  apply (clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def heap_update_def
                        restrict_htd_def lift_state_def
                  intro!: heap_update_nmem_same
                  split: s_heap_index.splits)
  apply(subgoal_tac "(a,SIndexVal)  s_footprint (p s)")
   apply(drule (1) subsetD)
   apply(drule dom_restrict_s, clarsimp)
  apply(drule intvlD, clarsimp)
  apply(erule s_footprintI2)
  done

lemma field_ti_s_sub_typ:
  "field_lookup (export_uinfo (typ_info_t TYPE('b::mem_type))) f 0 = Some (typ_uinfo_t TYPE('a),b) 
      s_footprint ((Ptr &(pf))::'a::mem_type ptr)  s_footprint (p::'b ptr)"
  by (drule field_ti_s_sub) (simp add: s_footprint_def)

lemma ptr_safe_mono:
  " ptr_safe (p::'a::mem_type ptr) d; field_lookup (typ_info_t TYPE('a)) f 0
      = Some (t,n); export_uinfo t = typ_uinfo_t TYPE('b)  
      ptr_safe ((Ptr &(pf))::'b::mem_type ptr) d"
  unfolding ptr_safe_def
  by (drule field_lookup_export_uinfo_Some) (auto dest: field_ti_s_sub_typ)

lemma point_eq_mod_safe_ptr_safe_update_fl:
  " d = (hst_htd::'a::heap_state_type  heap_typ_desc);
      m = (λs. hst_mem_update (heap_update (Ptr &((p s)f)) ((v s)::'b::mem_type)) s);
      h = hst_mem; k = (λs. lift_state (h s,d s)); htd_ind p;
      field_lookup (typ_info_t TYPE('c)) f 0 = Some (t,n);
      export_uinfo t = typ_uinfo_t TYPE('b)  
      point_eq_mod_safe {s. ptr_safe ((p::'a  'c::mem_type ptr) s) (d s)} m k"
  apply(drule (3) point_eq_mod_safe_ptr_safe_update)
   apply(fastforce simp: htd_ind_def)
  apply(fastforce simp: point_eq_mod_safe_def intro!: ptr_safe_mono)
  done

context
begin

private method m =
  (clarsimp simp: ptr_retyp_d_eq_snd ptr_retyp_footprint list_map_eq,
   erule notE,
   drule intvlD, clarsimp,
   (rule s_footprintI; assumption?),
   subst (asm) unat_of_nat,
   (subst (asm) mod_less; assumption?),
   subst len_of_addr_card,
   erule less_trans,
   simp)

lemma point_eq_mod_safe_ptr_safe_tag:
  " d = (hst_htd::'a::heap_state_type  heap_typ_desc); h = hst_mem;
     m = (λs. hst_htd_update (ptr_retyp (p s)) s);
     k = (λs. lift_state (h s,d s));
     htd_ind p  
   point_eq_mod_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m k"
  supply if_split_asm[split]
  supply unsigned_of_nat [simp del]
  apply(clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def)
  apply(subgoal_tac "(a,b)  s_footprint (p (restrict_htd s X))")
   prefer 2
   apply(fastforce simp: restrict_htd_def dest: dom_restrict_s)
  apply(clarsimp simp: restrict_htd_def  lift_state_def split: s_heap_index.split option.splits)
  apply (safe; m?)
    apply(fastforce simp: ptr_retyp_d_eq_fst dest!: intvlD dest: s_footprintI2)
   apply(fastforce simp: ptr_retyp_d_eq_fst)
  apply(subst (asm) ptr_retyp_d_eq_snd, clarsimp)
  done

end

lemma comm_restrict_safe_ptr_safe_tag:
  fixes d::"'a::heap_state_type  heap_typ_desc"
  assumes
    fun_d: "d = hst_htd" and
    fun_upd: "m = (λs. hst_htd_update (ptr_retyp (p s)) s)" and
    ind: "htd_ind p" and
    upd: "d d' (s::'a).
               hst_htd_update (d s) (hst_htd_update (d' s) s) = hst_htd_update ((d s)  (d' s)) s"
  shows "comm_restrict_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m"
proof -
  {
    fix s X
    assume "ptr_safe (p (restrict_htd s X)) (d (restrict_htd s X))"
    moreover from ind
    have p: "p (restrict_htd s X) = p s"
      by (simp add:  restrict_htd_def)
    ultimately
    have "ptr_retyp (p s) (restrict_s (hst_htd s) X) = restrict_s (ptr_retyp (p s) (hst_htd s))  X"
      using fun_d
      supply unsigned_of_nat [simp del]
      apply -
      apply(rule ext)
      apply(clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def restrict_htd_def)
      subgoal for x
        apply(cases "x  {ptr_val (p s)..+size_of TYPE('b)}")
         apply(clarsimp simp: ptr_retyp_d restrict_map_def restrict_s_def)
         apply(subst ptr_retyp_d; simp)
        apply(clarsimp simp: ptr_retyp_footprint restrict_map_def restrict_s_def)
        apply(subst ptr_retyp_footprint, simp)
        apply(rule conjI)
         apply(subgoal_tac "(x,SIndexVal)  s_footprint (p s)")
          apply(fastforce simp: dom_s_def)
         apply(fastforce dest: intvlD elim: s_footprintI2)
        apply(rule ext)
        apply(clarsimp simp: map_add_def list_map_eq)
        apply(subgoal_tac "(x,SIndexTyp y)  s_footprint (p s)")
         apply(fastforce simp: dom_s_def split: if_split_asm)
        apply(drule intvlD, clarsimp)
        apply(rule s_footprintI; assumption?)
        apply(metis len_of_addr_card less_trans max_size mod_less word_unat.eq_norm)
        done
      done
    hence "((ptr_retyp (p s)  (λx _. x) (restrict_s (hst_htd s) X)::heap_typ_desc  heap_typ_desc) =
              (λx _. x) (restrict_s (ptr_retyp (p s) (hst_htd s)) X))"
      by - (rule ext, simp)
    moreover from upd have "hst_htd_update (ptr_retyp (p s))
        (hst_htd_update ((λx _. x) (restrict_s (hst_htd s) X)) s) =
         hst_htd_update (((ptr_retyp (p s))  ((λx _. x) (restrict_s (hst_htd s) X)))) s" .
    moreover from upd
    have
      "hst_htd_update ((λx _. x) (restrict_s (ptr_retyp (p s) (hst_htd s)) X))
                    (hst_htd_update (ptr_retyp (p s)) s) =
     hst_htd_update (((λx _. x) (restrict_s ((ptr_retyp (p s) (hst_htd s))) X))  (ptr_retyp (p s))) s" .
    ultimately have "m (restrict_htd s X) = restrict_htd (m s) X" using fun_d fun_upd upd p
      by (simp add: restrict_htd_def o_def)
  }
  thus ?thesis 
    by (simp only: comm_restrict_safe_def comm_restrict_def, auto)
qed

lemmas intra_sc = hrs_comm comp_def hrs_htd_update_htd_update
  point_eq_mod_safe_triv comm_restrict_safe_triv mono_guard_triv2
  mono_guard_ptr_safe point_eq_mod_safe_ptr_safe_update
  point_eq_mod_safe_ptr_safe_tag comm_restrict_safe_ptr_safe_tag
  point_eq_mod_safe_ptr_safe_update_fl

declare expr_htd_ind_def [iff]
declare htd_ind_def [iff]

lemma proc_deps_Skip [simp]:
  "proc_deps Skip Γ = {}"
  by (force elim: proc_deps.induct)

lemma proc_deps_Basic [simp]:
  "proc_deps (Basic f) Γ = {}"
  by (force elim: proc_deps.induct)

lemma proc_deps_Spec [simp]:
  "proc_deps (Spec r) Γ = {}"
  by (force elim: proc_deps.induct)

lemma proc_deps_Seq [simp]:
  "proc_deps (Seq C D) Γ = proc_deps C Γ  proc_deps D Γ"
proof
  show "proc_deps (C;; D) Γ  proc_deps C Γ  proc_deps D Γ"
    by - (standard, erule proc_deps.induct, auto intro: proc_deps.intros)
next
  show "proc_deps C Γ  proc_deps D Γ  proc_deps (C;; D) Γ"
    by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+
qed

lemma proc_deps_Cond [simp]:
  "proc_deps (Cond P C D) Γ = proc_deps C Γ  proc_deps D Γ"
proof
  show "proc_deps (Cond P C D) Γ  proc_deps C Γ  proc_deps D Γ"
    by (standard, erule proc_deps.induct, auto intro: proc_deps.intros)
next
  show "proc_deps C Γ  proc_deps D Γ  proc_deps (Cond P C D) Γ"
    by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+
qed

lemma proc_deps_While [simp]:
  "proc_deps (While P C) Γ = proc_deps C Γ"
  by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+

lemma proc_deps_Guard [simp]:
  "proc_deps (Guard f P C) Γ = proc_deps C Γ"
  by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+

lemma proc_deps_Throw [simp]:
  "proc_deps Throw Γ = {}"
  by (force elim: proc_deps.induct)

lemma proc_deps_Catch [simp]:
  "proc_deps (Catch  C D) Γ = proc_deps C Γ  proc_deps D Γ"
proof
  show "proc_deps (Catch C D) Γ  proc_deps C Γ  proc_deps D Γ"
    by (standard, erule proc_deps.induct, auto intro: proc_deps.intros)
next
  show "proc_deps C Γ  proc_deps D Γ  proc_deps (Catch C D) Γ"
    by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+
qed

lemma proc_deps_Call [simp]:
  "proc_deps (Call p) Γ = {p}  (case Γ p of Some C 
      proc_deps C (Γ(p := None)) | _  {})" (is "?X = ?Y  ?Z")
proof
  note proc_deps.intros[intro]
  show "?X  ?Y  ?Z"
    apply (rule subsetI, erule proc_deps.induct, fastforce)
    subgoal for x' x D y
      apply (cases "x=p") 
       apply (auto split: option.splits)
      done
    done
next
  show "?Y  ?Z  ?X"
    apply (clarsimp, standard)
  proof -
    show "p  ?X" by (force intro: proc_deps.intros)
  next
    show "?Z  ?X"
      by (split option.splits, standard, force intro: proc_deps.intros)
         (clarify, erule proc_deps.induct;
          force intro: proc_deps.intros split: if_split_asm)
  qed
qed

lemma proc_deps_DynCom [simp]:
  "proc_deps (DynCom f) Γ = {proc_deps (f s) Γ | s. True}"
  by (rule equalityI; clarsimp; erule proc_deps.induct; force intro: proc_deps.intros)

lemma proc_deps_restrict:
  "proc_deps C Γ  proc_deps C (Γ(p := None))  proc_deps (Call p) Γ"
proof
  fix xa
  assume mem: "xa  proc_deps C Γ"
  hence "p. xa  proc_deps C (Γ(p := None))  proc_deps (Call p) Γ" (is "?X")
  using mem
  proof induct
    fix x
    assume "x  intra_deps C"
    thus "p. x  proc_deps C (Γ(p := None))  proc_deps (Call p) Γ"
      by (force intro: proc_deps.intros)
  next
    fix D x y
    assume x:
      "x  proc_deps C Γ"
      "x  proc_deps C Γ  p. x  proc_deps C (Γ(p := None))  proc_deps (Call p) Γ"
      "Γ x = Some D"
      "y  intra_deps D"
      "y  proc_deps C Γ"
    show "p. y  proc_deps C (Γ(p := None))  proc_deps (Call p) Γ"
    proof clarify
      fix p
      assume y: "y  proc_deps (Call p) Γ"
      show "y  proc_deps C (Γ(p := None))"
      proof (cases "x=p")
        case True with x y show ?thesis
          by (force intro: proc_deps.intros)
      next
        case False with x y show ?thesis
          by (clarsimp, drule_tac x=p in spec)
             (auto intro: proc_deps.intros split: option.splits)
      qed
    qed
  qed
  thus "xa  proc_deps C (Γ(p := None))  proc_deps (Call p) Γ" by simp
qed

lemma exec_restrict:
  assumes exec: "Γ'  C,s  t"
  shows "Γ X.  Γ' = Γ |` X; proc_deps C Γ  X   Γ  C,s  t"
using exec
proof induct
  case (Call p C s t)
  thus ?case
    using proc_deps_restrict [of C Γ p] by (force intro: exec_other_intros)
qed (force intro: exec_other_intros)+

lemma exec_restrict2:
  assumes exec: "Γ  C,s  t"
  shows "X. proc_deps C Γ  X  Γ |` X  C,s  t"
using exec
proof induct
  case (Call p C s t) thus ?case
  using proc_deps_restrict [of C Γ p]
    by (auto intro!: exec_other_intros split: option.splits)
next
  case (DynCom f s t) thus ?case
    by - (rule exec.intros, simp, blast)
qed (auto intro: exec_other_intros)

lemma exec_restrict_eq:
  "Γ |` proc_deps C Γ  C,s  t = Γ  C,s  t"
  by (fast intro: exec_restrict exec_restrict2)

lemma mem_safe_restrict:
  "mem_safe C Γ = mem_safe C (Γ |` proc_deps C Γ)"
  by (auto simp: mem_safe_def restrict_safe_def restrict_safe_OK_def
                 exec_restrict_eq exec_fatal_def
           split: xstate.splits)

end