Theory AutoCorres2.SepFrame
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 s⇩0 and s⇩1 where pre_P: "P (f x) s⇩0" and pre_R: "R (h x) s⇩1" and
disj: "s⇩0 ⊥ s⇩1" and m: "lift_hst x = s⇩1 ++ s⇩0"
by (clarsimp simp: sep_conj_def map_ac_simps)
with orig_spec hi_f have nofault: "¬ exec_fatal C Γ
(restrict_htd x (dom s⇩0))"
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 s⇩0)) ⦈)⟩ ⇒
Normal (s⦇ hst_htd := (restrict_s (hst_htd s) (dom s⇩0)) ⦈)" and
"point_eq_mod (lift_state (hst_mem s,hst_htd s))
(lift_state (hst_mem x,hst_htd x)) (dom s⇩0)"
by (auto simp: restrict_htd_def dest: mem_safe_NormalD)
moreover from this m disj have "s⇩1 = lift_hst s |` (UNIV - dom s⇩0)"
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 s⇩0" 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)
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 &(p→f))::'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 &(p→f))::'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