Quelle  Safety.thy

subsection ‹Safety and Hoare Triples›

text ‹In this file, the meaning of Hoare triples (Definition 4.1), through a notion of safety
 see Section 4 and Appendix C). We also prove useful lemmas for the soundness proof.›

theory Safety
  imports Guards
begin

subsubsection ‹Preliminaries›

(* Enforces no-guard *)
definition sat_inv :: "store ==> ('i, 'a) heap ==> ('i, 'a, nat) single_context ==> bool" where
  "sat_inv s hj Γ ⟷ (s, hj), (s, hj) ⊨ invariant Γ ∧ no_guard hj"

lemma sat_invI:
  assumes "(s, hj), (s, hj) ⊨ invariant Γ"
      and "no_guard hj"
    shows "sat_inv s hj Γ"
  by (simp add: assms(1) assms(2) sat_inv_def)


text ‹s and s' can differ on variables outside of vars, does not change anything.
 -fvs S vars means that vars is an upper-bound of "fv S"›

definition upper_fvs :: "(store × ('i, 'a) heap) set ==> var set ==> bool" where
  "upper_fvs S vars ⟷ (∀s s' h. (s, h) ∈ S ∧ agrees vars s s' ⟶ (s', h) ∈ S)"

text ‹Only need to agree on vars›
definition upperize where
  "upperize S vars = { σ' |σ σ'. σ ∈ S ∧ snd σ = snd σ' ∧ agrees vars (fst σ) (fst σ')}"

definition close_var where
  "close_var S x = { ((fst σ)(x := v), snd σ) |σ v. σ ∈ S }"

lemma upper_fvsI:
  assumes "∧s s' h. (s, h) ∈ S ∧ agrees vars s s' ==> (s', h) ∈ S"
  shows "upper_fvs S vars"
  using assms upper_fvs_def by blast

lemma pair_sat_comm:
  assumes "pair_sat S S' A"
  shows "pair_sat S' S A"
proof (rule pair_satI)
  fix s h s' h' assume "(s, h) ∈ S' ∧ (s', h') ∈ S"
  then show "(s, h), (s', h') ⊨ A"
    using assms pair_sat_def sat_comm by blast
qed

lemma in_upperize:
  "(s', h) ∈ upperize S vars ⟷ (∃s. (s, h) ∈ S ∧ agrees vars s s')" (is "?A ⟷ ?B")
proof
  show "?A ==> ?B"
    by (simp add: upperize_def)
  show "?B ==> ?A"
    using upperize_def by fastforce
qed

lemma upper_fvs_upperize:
  "upper_fvs (upperize S vars) vars"
proof (rule upper_fvsI)
  fix s s' h
  assume "(s, h) ∈ upperize S vars ∧ agrees vars s s'"
  then obtain s'' where "(s'', h) ∈ S ∧ agrees vars s'' s"
    by (meson in_upperize)
  then have "agrees vars s'' s'"
    using ‹(s, h) ∈ upperize S vars ∧ agrees vars s s'› agrees_def[of vars s s']
    agrees_def[of vars s'' s] agrees_def[of vars s'' s']
    by simp
  then show "(s', h) ∈ upperize S vars"
    using ‹(s'', h) ∈ S ∧ agrees vars s'' s› upperize_def by fastforce
qed

lemma upperize_larger:
  "S ⊆ upperize S vars"
proof
  fix x assume "x ∈ S"
  moreover have "agrees vars (fst x) (fst x)"
    using agrees_def by blast
  ultimately show "x ∈ upperize S vars"
    by (metis (mono_tags, lifting) CollectI upperize_def)
qed

lemma pair_sat_upperize:
  assumes "pair_sat S S' A"
  shows "pair_sat (upperize S (fvA A)) S' A"
proof (rule pair_satI)
  fix s h s' h'
  assume asm0: "(s, h) ∈ upperize S (fvA A) ∧ (s', h') ∈ S'"
  then obtain s'' where "agrees (fvA A) s s''" "(s'', h) ∈ S"
    using agrees_def[of "fvA A" s s'] in_upperize[of s h S "fvA A"]
    by (metis agrees_def)
  then show "(s, h), (s', h') ⊨ A"
    using agrees_same asm0 assms pair_sat_def by blast
qed

lemma in_close_var:
  "(s', h) ∈ close_var S x ⟷ (∃s v. (s, h) ∈ S ∧ s' = s(x := v))" (is "?A ⟷ ?B")
proof
  show "?A ==> ?B"
    using close_var_def[of S x] mem_Collect_eq prod.inject surjective_pairing
    by auto
  show "?B ==> ?A"
    using close_var_def by fastforce
qed

lemma pair_sat_close_var:
  assumes "x ∉ fvA A"
      and "pair_sat S S' A"
  shows "pair_sat (close_var S x) S' A"
proof (rule pair_satI)
  fix s h s' h'
  assume "(s, h) ∈ close_var S x ∧ (s', h') ∈ S'"
  then show "(s, h), (s', h') ⊨ A"
    by (metis (no_types, lifting) agrees_same agrees_update assms in_close_var pair_sat_def)
qed

lemma pair_sat_close_var_double:
  assumes "pair_sat S S' A"
      and "x ∉ fvA A"
  shows "pair_sat (close_var S x) (close_var S' x) A"
  using assms pair_sat_close_var pair_sat_comm by blast

lemma close_var_subset:
  "S ⊆ close_var S x"
proof
  fix y assume "y ∈ S"
  then have "fst y = (fst y)(x := (fst y x))"
    by simp
  then show "y ∈ close_var S x"
    by (metis ‹y ∈ S› in_close_var prod.exhaust_sel)
qed

lemma upper_fvs_close_vars:
  "upper_fvs (close_var S x) (- {x})"
proof (rule upper_fvsI)
  fix s s' h
  assume "(s, h) ∈ close_var S x ∧ agrees (- {x}) s s'"
  have "s(x := s' x) = s'"
  proof (rule ext)
    fix y show "(s(x := s' x)) y = s' y"
      by (metis (mono_tags, lifting) ComplI ‹(s, h) ∈ close_var S x ∧ agrees (- {x}) s s'› agrees_def fun_upd_apply singleton_iff)
  qed
  then show "(s', h) ∈ close_var S x"
    by (metis ‹(s, h) ∈ close_var S x ∧ agrees (- {x}) s s'› fun_upd_upd in_close_var)
qed

lemma sat_inv_agrees:
  assumes "sat_inv s hj Γ"
      and "agrees (fvA (invariant Γ)) s s'"
    shows "sat_inv s' hj Γ"
  by (meson agrees_same assms sat_comm sat_inv_def)

lemma abort_iff_fvC:
  assumes "agrees (fvC C) s s'"
  shows "aborts C (s, h) ⟷ aborts C (s', h)"
  using aborts_agrees assms fst_conv snd_eqD
  by (metis (mono_tags, lifting) agrees_def)

lemma view_function_of_invE:
  assumes "view_function_of_inv Γ"
      and "sat_inv s h Γ"
      and "(h' :: ('i, 'a) heap) ⪰ h"
    shows "view Γ (normalize (get_fh h)) = view Γ (normalize (get_fh h'))"
  using assms(1) assms(2) assms(3) sat_inv_def view_function_of_inv_def by blast



subsubsection Safety

fun no_abort :: "('i, 'a, nat) cont ==> cmd ==> store ==> ('i, 'a) heap ==> bool" where
  "no_abort None C s h ⟷ (∀hf H. Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H
  ⟶ ¬ aborts C (s, normalize (get_fh H)))"
| "no_abort (Some Γ) C s h ⟷ (∀hf H hj v0. Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧
  semi_consistent Γ v0 H ∧ sat_inv s hj Γ
  ⟶ ¬ aborts C (s, normalize (get_fh H)))"

lemma no_abortI:
  assumes "∧(hf :: ('i, 'a) heap) (H :: ('i, 'a) heap). Some H = Some h ⊕ Some hf ∧ Δ = None ∧ full_ownership (get_fh H) ∧ no_guard H ==> ¬ aborts C (s, normalize (get_fh H))"
      and "∧H hf hj v0 Γ. Δ = Some Γ ∧ Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ
  ==> ¬ aborts C (s, normalize (get_fh H))"
    shows "no_abort Δ C s (h :: ('i, 'a) heap)"
  apply (cases Δ)
  using assms(1) no_abort.simps(1) apply blast
  using assms(2) no_abort.simps(2) by blast

lemma no_abortSomeI:
  assumes "∧H hf hj v0. Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ
  ==> ¬ aborts C (s, normalize (get_fh H))"
  shows "no_abort (Some Γ) C s (h :: ('i, 'a) heap)"
  using assms no_abort.simps(2) by blast

lemma no_abortNoneI:
  assumes "∧(hf :: ('i, 'a) heap) (H :: ('i, 'a) heap). Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ==> ¬ aborts C (s, normalize (get_fh H))"
  shows "no_abort (None :: ('i, 'a, nat) cont) C s (h :: ('i, 'a) heap)"
  using assms no_abort.simps(1) by blast

lemma no_abortE:
  assumes "no_abort Δ C s h"
  shows "Some H = Some h ⊕ Some hf ==> Δ = None ==> full_ownership (get_fh H) ==> no_guard H ==> ¬ aborts C (s, normalize (get_fh H))"
    and "Δ = Some Γ ==> Some H = Some h ⊕ Some hj ⊕ Some hf ==> sat_inv s hj Γ ==> full_ownership (get_fh H) ==> semi_consistent Γ v0 H
  ==> ¬ aborts C (s, normalize (get_fh H))"
  using assms no_abort.simps(1) apply blast
  by (metis assms no_abort.simps(2))

text ‹We define the notion of safety, central to the meaning of Hoare triples, as follows (Definition C.1 in the appendix).›
fun safe :: "nat ==> ('i, 'a, nat) cont ==> cmd ==> (store × ('i, 'a) heap) ==> (store × ('i, 'a) heap) set ==> bool" where
  "safe 0 _ _ _ _ ⟷ True"

| "safe (Suc n) None C (s, h) S ⟷ (C = Cskip ⟶ (s, h) ∈ S) ∧ no_abort (None :: ('i, 'a, nat) cont) C s h ∧ accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h) ∧
(∀H hf C' s' h'. Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H
 ∧ red C (s, normalize (get_fh H)) C' (s', h')
\<longrightarrow> (∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s', h'') S))"

| "safe (Suc n) (Some Γ) C (s, h) S ⟷ (C = Cskip ⟶ (s, h) ∈ S) ∧ no_abort (Some Γ) C s h ∧ accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h) ∧
(∀H hf C' s' h' hj v0. Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ
 ∧ red C (s, normalize (get_fh H)) C' (s', h')
\<longrightarrow> (∃h'' H' hj'. full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ
 ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S))"

lemma safeNoneI:
  assumes "C = Cskip ==> (s, h) ∈ S"
      and "no_abort None C s h"
      and "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
      and "∧H hf C' s' h'. Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s, normalize (get_fh H)) C' (s', h')
  ==> (∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s', h'') S)"
shows "safe (Suc n) (None :: ('i, 'a, nat) cont) C (s, h :: ('i, 'a) heap) S"
  using assms by auto

lemma safeSomeI:
  assumes "C = Cskip ==> (s, h) ∈ S"
      and "no_abort (Some Γ) C s h"
      and "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
      and "∧H hf C' s' h' hj v0. Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H)
        ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, normalize (get_fh H)) C' (s', h')
\<Longrightarrow> (∃h'' H' hj'. full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ
 ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S)"
shows "safe (Suc n) (Some Γ) C (s, h :: ('i, 'a) heap) S"
  using assms by auto

lemma safeI:
  fixes Δ :: "('i, 'a, nat) cont"
  assumes "C = Cskip ==> (s, h) ∈ S"
      and "no_abort Δ C s h"
      and "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
      and "∧H hf C' s' h'. Δ = None ==> Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s, normalize (get_fh H)) C' (s', h')
  ==> (∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s', h'') S)"
      and "∧H hf C' s' h' hj v0 Γ. Δ = Some Γ ==> Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H)
        ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, normalize (get_fh H)) C' (s', h')
\<Longrightarrow> (∃h'' H' hj'. full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ
 ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S)"
    shows "safe (Suc n) Δ C (s, h :: ('i, 'a) heap) S"
proof (cases Δ)
  case None
  then show ?thesis
    using assms by auto
next
  case (Some Γ)
  then show ?thesis using safeSomeI assms
    by simp
qed


lemma safeSomeAltI:
  assumes "C = Cskip ==> (s, h) ∈ S"
      and "∧H hf hj v0. Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ
  ==> ¬ aborts C (s, normalize (get_fh H))"
      and "∧H hf C' s' h' hj v0. Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H)
        ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ==> red C (s, normalize (get_fh H)) C' (s', h')
\<Longrightarrow> (∃h'' H' hj'. full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ
 ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S)"
      and "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
    shows "safe (Suc n) (Some Γ) C (s, h :: ('i, 'a) heap) S"
  using assms(1)
proof (rule safeSomeI)
  show "no_abort (Some Γ) C s h" using assms(2) no_abortSomeI by blast
  show "∧H hf C' s' h' hj v0.
       Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h') ==>
       (∃h'' H' hj'.
           full_ownership (get_fh H') ∧
           semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S)"
    using assms(3) by blast
qed (auto simp add: assms)

lemma safeAccessesE:
  assumes "safe (Suc n) Δ C σ S"
  shows "accesses C (fst σ) ⊆ dom (fst (snd σ)) ∧ writes C (fst σ) ⊆ fpdom (fst (snd σ))"
  apply (cases Δ)
  using assms safe.simps(2)[of n C "fst σ" "snd σ" S] safe.simps(3)[of n _ C "fst σ" "snd σ" S] by simp_all

lemma safeSomeE:
  assumes "safe (Suc n) (Some Γ) C (s, h :: ('i, 'a) heap) S"
  shows "C = Cskip ==> (s, h) ∈ S"
      and "no_abort (Some Γ) C s h"
      and "Some H = Some h ⊕ Some hj ⊕ Some hf ==> full_ownership (get_fh H)
        ==> semi_consistent Γ v0 H ==> sat_inv s hj Γ ==> red C (s, normalize (get_fh H)) C' (s', h')
\<Longrightarrow> (∃h'' H' hj'. full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ
 ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S)"
  using assms safe.simps(3)[of n Γ C s h S] by blast+

lemma safeNoneE:
  assumes "safe (Suc n) (None :: ('i, 'a, nat) cont) C (s, h :: ('i, 'a) heap) S"
    shows "C = Cskip ==> (s, h) ∈ S"
      and "no_abort (None :: ('i, 'a, nat) cont) C s h"
      and "Some H = Some h ⊕ Some hf ==> full_ownership (get_fh H) ==> no_guard H ==> red C (s, normalize (get_fh H)) C' (s', h')
  ==> (∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s', h'') S)"
  using assms safe.simps(2)[of n C s h S] by blast+

lemma safeNoneE_bis:
  fixes no_cont :: "('i, 'a, nat) cont"
  assumes "safe (Suc n) no_cont C (s, h :: ('i, 'a) heap) S"
      and "no_cont = None"
    shows "C = Cskip ==> (s, h) ∈ S"
      and "no_abort no_cont C s h"
      and "Some H = Some h ⊕ Some hf ==> full_ownership (get_fh H) ==> no_guard H ==> red C (s, normalize (get_fh H)) C' (s', h')
  ==> (∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n no_cont C' (s', h'') S)"
  using assms safe.simps(2)[of n C s h S] by blast+


subsubsection ‹Useful results about safety›


lemma no_abort_larger:
  assumes "h' ⪰ h"
    and "no_abort Γ C s h"
  shows "no_abort Γ C s h'"
proof (rule no_abortI)
  show "∧hf H. Some H = Some h' ⊕ Some hf ∧ Γ = None ∧ full_ownership (get_fh H) ∧ no_guard H ==> ¬ aborts C (s, FractionalHeap.normalize (get_fh H))"
    using assms(1) assms(2) larger_def larger_trans no_abort.simps(1) by blast
  show "∧H hf hj v0 Γ'.
       Γ = Some Γ' ∧ Some H = Some h' ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ' v0 H ∧ sat_inv s hj Γ' ==>
       ¬ aborts C (s, FractionalHeap.normalize (get_fh H))"
  proof -
    fix H hf hj v0 Γ'
    assume asm0: "Γ = Some Γ' ∧ Some H = Some h' ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ' v0 H ∧ sat_inv s hj Γ'"
    moreover obtain r where "Some h' = Some h ⊕ Some r"
      using assms(1) larger_def by blast
    then obtain hf' where "Some hf' = Some hf ⊕ Some r"
      by (metis (no_types, opaque_lifting) calculation not_None_eq plus.simps(1) plus_asso plus_comm)
    then have "Some H = Some h ⊕ Some hj ⊕ Some hf'"
      by (metis (no_types, opaque_lifting) ‹Some h' = Some h ⊕ Some r› calculation plus_asso plus_comm)
    then show "¬ aborts C (s, FractionalHeap.normalize (get_fh H))"
      using assms(2) calculation no_abortE(2) by blast
  qed
qed

lemma safe_larger_set_aux:
  fixes Δ :: "('i, 'a, nat) cont"
  assumes "safe n Δ C (s, h) S"
      and "S ⊆ S'"
    shows "safe n Δ C (s, h) S'"
  using assms
proof (induct n arbitrary: s h C)
  case (Suc n)
  show ?case
  proof (rule safeI)
    show "C = Cskip ==> (s, h) ∈ S'"
      by (metis (no_types, opaque_lifting) Suc.prems(1) assms(2) not_Some_eq safeNoneE_bis(1) safeSomeE(1) subset_iff)
    show "no_abort Δ C s h"
      apply (cases Δ)
      using Suc.prems(1) safeNoneE_bis(2) apply blast
      using Suc.prems(1) safeSomeE(2) by blast

    show "∧H hf C' s' h'.
       Δ = None ==>
       Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h') ==>
       ∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s', h'') S'"
      using Suc.hyps Suc.prems(1) assms(2) safeNoneE(3)[of n C s h] by blast

    show "∧H hf C' s' h' hj v0 Γ.
       Δ = Some Γ ==>
       Some H = Some h ⊕ Some hj ⊕ Some hf ∧
       full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h') ==>
       ∃h'' H' hj'.
          full_ownership (get_fh H') ∧
          semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S'"
    proof -
      fix H hf C' s' h' hj v0 Γ
      assume asm0: "Δ = Some Γ" "Some H = Some h ⊕ Some hj ⊕ Some hf ∧
       full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h')"
      then show "∃h'' H' hj'. full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ
      ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S'"
        using safeSomeE(3)[of n Γ C s h S] Suc.hyps Suc.prems(1) assms(2) by blast
    qed
    show "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
      by (metis Suc.prems(1) fst_conv safeAccessesE snd_conv)
  qed
qed (simp)

lemma safe_larger_set:
  assumes "safe n Δ C σ S"
      and "S ⊆ S'"
    shows "safe n Δ C σ S'"
  using assms safe_larger_set_aux[of n Δ C "fst σ" "snd σ" S S']
  by auto

lemma safe_smaller_aux:
  fixes Δ :: "('i, 'a, nat) cont"
  assumes "m ≤ n"
      and "safe n Δ C (s, h) S"
    shows "safe m Δ C (s, h) S"
  using assms
proof (induct n arbitrary: s h C m)
  case (Suc n)
  show ?case
  proof (cases m)
    case (Suc k)
    then have "k ≤ n"
      using Suc.prems(1) by fastforce
    moreover have "safe (Suc k) Δ C (s, h) S"
    proof (rule safeI)
      show "C = Cskip ==> (s, h) ∈ S"
        using Suc.prems(2) safe.elims(2) by blast
      show "no_abort Δ C s h"
        apply (cases Δ)
        using Suc.prems(2) safeNoneE(2) apply blast
        using Suc.prems(2) safeSomeE(2) by blast
      show "∧H hf C' s' h'.
       Δ = None ==>
       Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h') ==>
       ∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe k (None :: ('i, 'a, nat) cont) C' (s', h'') S"
      proof -
        fix H hf C' s' h'
        assume asm0: "Δ = None" "Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h')"
        then obtain h'' H' where "full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s', h'') S"
          using Suc.prems(2) safeNoneE(3) by blast
        then show "∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe k (None :: ('i, 'a, nat) cont) C' (s', h'') S"
          using Suc.hyps asm0(1) calculation by blast
      qed
      show "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
        by (metis Suc.prems(2) fst_eqD safeAccessesE snd_eqD)
      fix H hf C' s' h' hj v0 Γ
      assume asm0: "Δ = Some Γ" "Some H = Some h ⊕ Some hj ⊕ Some hf ∧
       full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h')"
      then show "∃h'' H' hj'.
          full_ownership (get_fh H') ∧
          semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe k (Some Γ) C' (s', h'') S"
        using Suc.prems(2) safeSomeE(3)[of n Γ C s h S H hj hf v0 C' s' h'] Suc.hyps
        using calculation by blast
    qed
    ultimately show ?thesis
      using Suc by auto
  qed (simp)
qed (simp)

lemma safe_smaller:
  assumes "m ≤ n"
      and "safe n Δ C σ S"
    shows "safe m Δ C σ S"
  by (metis assms(1) assms(2) safe_smaller_aux surj_pair)


text ‹If it is safe to execute n steps of C in the state (s0, h), then it is also safe to execute it
  the state (s1, h), provided that s0 and s1 agree on the values of variables that are free in C, the
 , and the postcondition.›

lemma safe_free_vars_aux:
  fixes Δ :: "('i, 'a, nat) cont"
  assumes "safe n Δ C (s0, h) S"
      and "agrees (fvC C ∪ vars) s0 s1"
      and "upper_fvs S vars"
      and "∧Γ. Δ = Some Γ ==> agrees (fvA (invariant Γ)) s0 s1"
    shows "safe n Δ C (s1, h) S"
  using assms
proof (induct n arbitrary: s0 h s1 C)
  case (Suc n)
  show ?case
  proof (rule safeI)
    show "C = Cskip ==> (s1, h) ∈ S"
      by (metis Suc.prems(1) Suc.prems(2) agrees_union assms(3) not_Some_eq safeNoneE_bis(1) safeSomeE(1) upper_fvs_def)
    show "no_abort Δ C s1 h"
    proof (rule no_abortI)
      show "∧hf H. Some H = Some h ⊕ Some hf ∧ Δ = None ∧ full_ownership (get_fh H) ∧ no_guard H ==> ¬ aborts C (s1, FractionalHeap.normalize (get_fh H))"
        using Suc.prems(1) Suc.prems(2) abort_iff_fvC agrees_union no_abortE(1) safeNoneE(2) by blast
      show "∧H hf hj v0 Γ. Δ = Some Γ ∧ Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s1 hj Γ ==>
       ¬ aborts C (s1, FractionalHeap.normalize (get_fh H))"
      proof -
        fix H hf hj v0 Γ
        assume asm0: "Δ = Some Γ ∧ Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s1 hj Γ"
        then have "sat_inv s0 hj Γ"
          using Suc.prems(4) agrees_def sat_inv_agrees
          by (metis (mono_tags, opaque_lifting))
        then have "¬ aborts C (s0, FractionalHeap.normalize (get_fh H))"
          using Suc.prems(1) asm0 no_abort.simps(2) safeSomeE(2) by blast
        then show "¬ aborts C (s1, FractionalHeap.normalize (get_fh H))"
          using Suc.prems(2) abort_iff_fvC agrees_union by blast
      qed
    qed
    show "∧H hf C' s1' h'.
       Δ = None ==>
       Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s1, FractionalHeap.normalize (get_fh H)) C' (s1', h') ==>
       ∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s1', h'') S"
    proof -
      fix H hf C' s1' h'
      assume asm0: "Δ = None"
        "Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s1, FractionalHeap.normalize (get_fh H)) C' (s1', h')"
      then obtain s0' where "red C (s0, FractionalHeap.normalize (get_fh H)) C' (s0', h')" "agrees (fvC C ∪ vars) s1' s0'"
        using red_agrees[of C "(s1, FractionalHeap.normalize (get_fh H))" C' "(s1', h')" "fvC C ∪ vars"]
        using Suc.prems(2) agrees_def fst_conv snd_conv sup_ge1
        by (metis (mono_tags, lifting))
      then obtain h'' H' where
        r: "full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s0', h'') S"
        using Suc.prems(1) asm0(1) asm0(2) safeNoneE(3) by blast
      then have "safe n (None :: ('i, 'a, nat) cont) C' (s1', h'') S"
        using Suc.hyps[of C'  s0' h'' s1']
        using ‹agrees (fvC C ∪ vars) s1' s0'› agrees_union asm0(1) asm0(2) assms(3) option.distinct(1) red_properties(1)
        by (metis (mono_tags, lifting) agrees_def subset_iff)
      then show "∃h'' H'. full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n (None :: ('i, 'a, nat) cont) C' (s1', h'') S"
        using r by blast
    qed
    show "accesses C s1 ⊆ dom (fst h) ∧ writes C s1 ⊆ fpdom (fst h)"
      by (metis Suc.prems(1) Suc.prems(2) accesses_agrees writes_agrees agrees_union fst_conv safeAccessesE snd_conv)
    fix H hf C' s1' h' hj v0 Γ
    assume asm0: "Δ = Some Γ"
      "Some H = Some h ⊕ Some hj ⊕ Some hf ∧ full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s1 hj Γ ∧ red C (s1, normalize (get_fh H)) C' (s1', h')"
    then obtain s0' where "red C (s0, FractionalHeap.normalize (get_fh H)) C' (s0', h')" "agrees (fvC C ∪ vars ∪ fvA (invariant Γ)) s1' s0'"
      using red_agrees[of C "(s1, FractionalHeap.normalize (get_fh H))" C' "(s1', h')" "fvC C ∪ vars ∪ fvA (invariant Γ)"]
      using Suc.prems(2) Suc.prems(4) agrees_comm agrees_union fst_conv snd_conv sup_assoc sup_ge1
      by (metis (no_types, lifting))
    moreover have "sat_inv s0 hj Γ"
      using Suc.prems(4) agrees_comm asm0(1) asm0(2) sat_inv_agrees by blast
    ultimately obtain h'' H' hj' where r: "full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s0' hj' Γ
  ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s0', h'') S"
      using Suc.prems(1) asm0(1) asm0(2) safeSomeE(3)[of n Γ C s0 h S H hj hf]
      by blast
    then have "sat_inv s1' hj' Γ"
      using ‹agrees (fvC C ∪ vars ∪ fvA (invariant Γ)) s1' s0'› agrees_comm agrees_union sat_inv_agrees by blast
    moreover have "safe n (Some Γ) C' (s1', h'') S"
      using Suc.hyps[of C' s0' h'' s1'] ‹agrees (fvC C ∪ vars ∪ fvA (invariant Γ)) s1' s0'› ‹red C (s0, FractionalHeap.normalize (get_fh H)) C' (s0', h')›
        agrees_def agrees_union asm0(1) assms(3) option.inject r red_properties
      by (metis (mono_tags, lifting) subset_Un_eq)
    ultimately show "∃h'' H' hj'.
          full_ownership (get_fh H') ∧
          semi_consistent Γ v0 H' ∧
          sat_inv s1' hj' Γ ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s1', h'') S"
      using r by blast
  qed
qed (simp)


lemma safe_free_vars_None:
  assumes "safe n (None :: ('i, 'a, nat) cont) C (s, h) S"
      and "agrees (fvC C ∪ vars) s s'"
      and "upper_fvs S vars"
    shows "safe n (None :: ('i, 'a, nat) cont) C (s', h) S"
  by (meson assms(1) assms(2) assms(3) not_Some_eq safe_free_vars_aux)

lemma safe_free_vars_Some:
  assumes "safe n (Some Γ) C (s, h) S"
      and "agrees (fvC C ∪ vars ∪ fvA (invariant Γ)) s s'"
      and "upper_fvs S vars"
    shows "safe n (Some Γ) C (s', h) S"
  by (metis agrees_union assms(1) assms(2) assms(3) option.inject safe_free_vars_aux)

lemma safe_free_vars:
  fixes Δ :: "('i, 'a, nat) cont"
  assumes "safe n Δ C (s, h) S"
      and "agrees (fvC C ∪ vars) s s'"
      and "upper_fvs S vars"
      and "∧Γ. Δ = Some Γ ==> agrees (fvA (invariant Γ)) s s'"
    shows "safe n Δ C (s', h) S"
proof (cases Δ)
  case None
  then show ?thesis
    using assms(1) assms(2) assms(3) safe_free_vars_None by blast
next
  case (Some Γ)
  then show ?thesis
    using agrees_union assms(1) assms(2) assms(3) assms(4) safe_free_vars_Some by blast
qed


lemma restrict_safe_to_bounded:
  assumes "safe n Δ C (s, h) S"
      and "bounded h"
  shows "safe n Δ C (s, h) (Set.filter (bounded ∘ snd) S)"
  using assms
proof (induct n arbitrary: s h C)
  case (Suc n)
  show ?case
  proof (rule safeI)
    have "C = Cskip ==> (s, h) ∈ S"
      using Suc.prems(1) safe.elims(2) by blast
    then show "C = Cskip ==> (s, h) ∈ Set.filter (bounded ∘ snd) S"
      by (simp add: Suc.prems(2))
    show "no_abort Δ C s h" using Suc.prems(1) safe.elims(2) by blast
    show "accesses C s ⊆ dom (fst h) ∧ writes C s ⊆ fpdom (fst h)"
      by (metis Suc.prems(1) fst_conv safeAccessesE snd_conv)
    fix H hf C' s' h'
    assume asm0: "Δ = None" "Some H = Some h ⊕ Some hf ∧ full_ownership (get_fh H) ∧ no_guard H ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h')"
    then obtain h'' H' where "full_ownership (get_fh H') ∧
          no_guard H' ∧
          h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n None C' (s', h'') S"
      using Suc.prems(1) safeNoneE(3) by blast
    then have "safe n None C' (s', h'') (Set.filter (bounded ∘ snd) S)"
      using Suc(1)[of C' s' h''] apply simp
      using ‹[safe n Δ C' (s', h'') S; bounded h''] ==> safe n Δ C' (s', h'') (Set.filter (bounded ∘ snd) S)› ‹full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n None C' (s', h'') S› asm0(1) bounded_smaller_sum full_ownership_then_bounded by blast
    then show "∃h'' H'.
          full_ownership (get_fh H') ∧
          no_guard H' ∧
          h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n None C' (s', h'') (Set.filter (bounded ∘ snd) S)"
      using ‹full_ownership (get_fh H') ∧ no_guard H' ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hf ∧ safe n None C' (s', h'') S› by blast
  next
    fix H hf C' s' h' hj v0 Γ
    assume asm0: "Δ = Some Γ" "Some H = Some h ⊕ Some hj ⊕ Some hf ∧
       full_ownership (get_fh H) ∧ semi_consistent Γ v0 H ∧ sat_inv s hj Γ ∧ red C (s, FractionalHeap.normalize (get_fh H)) C' (s', h')"
    then obtain h'' H' hj' where " full_ownership (get_fh H') ∧
          semi_consistent Γ v0 H' ∧
          sat_inv s' hj' Γ ∧
          h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S"
      using Suc.prems(1) safeSomeE(3) by blast
    then have "safe n (Some Γ) C' (s', h'') (Set.filter (bounded ∘ snd) S)"
      using Suc(1) [of C' s' h''] asm0(1) by (auto split: if_splits)
        (metis (lifting)
          ‹full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S›
          bounded_smaller_sum full_ownership_then_bounded get_fh.simps plus.simps(3))
    then show "∃h'' H' hj'.
          full_ownership (get_fh H') ∧
          semi_consistent Γ v0 H' ∧
          sat_inv s' hj' Γ ∧
          h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') (Set.filter (bounded ∘ snd) S)"
      using ‹full_ownership (get_fh H') ∧ semi_consistent Γ v0 H' ∧ sat_inv s' hj' Γ ∧ h' = FractionalHeap.normalize (get_fh H') ∧ Some H' = Some h'' ⊕ Some hj' ⊕ Some hf ∧ safe n (Some Γ) C' (s', h'') S› by blast

  qed
qed (simp)



subsubsection ‹Hoare triples›

text ‹The following defines when Hoare triples are valid, based on Definition 4.1.›

definition hoare_triple_valid :: "('i, 'a, nat) cont ==> ('i, 'a, nat) assertion ==> cmd ==> ('i, 'a, nat) assertion ==> bool"
  (‹_ ⊨ {_} _ {_}› [51,0,0] 81) where
  "hoare_triple_valid Γ P C Q ⟷ (∃Σ. (∀σ n. σ, σ ⊨ P ∧ bounded (snd σ) ⟶ safe n Γ C σ (Σ σ)) ∧
  (∀σ σ'. σ, σ' ⊨ P ⟶ pair_sat (Σ σ) (Σ σ') Q))"

lemma hoare_triple_validI:
  assumes "∧s h n. (s, h), (s, h) ⊨ P ==> safe n Γ C (s, h) (Σ (s, h))"
      and "∧s h s' h'. (s, h), (s', h') ⊨ P ==> pair_sat (Σ (s, h)) (Σ (s', h')) Q"
    shows "hoare_triple_valid Γ P C Q"
  by (metis assms(1) assms(2) hoare_triple_valid_def prod.collapse)

lemma hoare_triple_validI_bounded:
  assumes "∧s h n. (s, h), (s, h) ⊨ P ==> bounded h ==> safe n Γ C (s, h) (Σ (s, h))"
      and "∧s h s' h'. (s, h), (s', h') ⊨ P ==> pair_sat (Σ (s, h)) (Σ (s', h')) Q"
    shows "hoare_triple_valid Γ P C Q"
  by (metis assms(1) assms(2) hoare_triple_valid_def prod.collapse)

lemma hoare_triple_valid_smallerI:
  assumes "∧σ n. σ, σ ⊨ P ==> safe n Γ C σ (Σ σ)"
      and "∧σ σ'. σ, σ' ⊨ P ==> pair_sat (Σ σ) (Σ σ') Q"
    shows "hoare_triple_valid Γ P C Q"
  using assms hoare_triple_valid_def by metis

lemma hoare_triple_valid_smallerI_bounded:
  assumes "∧σ n. σ, σ ⊨ P ==> bounded (snd σ) ==> safe n Γ C σ (Σ σ)"
      and "∧σ σ'. σ, σ' ⊨ P ==> pair_sat (Σ σ) (Σ σ') Q"
    shows "hoare_triple_valid Γ P C Q"
  using assms hoare_triple_valid_def by metis

lemma hoare_triple_validE:
  assumes "hoare_triple_valid Γ P C Q"
  shows "∃Σ. (∀σ n. σ, σ ⊨ P ∧ bounded (snd σ) ⟶ safe n Γ C σ (Σ σ)) ∧
  (∀σ σ'. σ, σ' ⊨ P ⟶ pair_sat (Σ σ) (Σ σ') Q)"
  using assms hoare_triple_valid_def by blast

lemma hoare_triple_valid_simplerE:
  assumes "hoare_triple_valid Γ P C Q"
      and "σ, σ' ⊨ P"
      and "bounded (snd σ)"
      and "bounded (snd σ')"
    shows "∃S S'. safe n Γ C σ S ∧ safe n Γ C σ' S' ∧ pair_sat S S' Q"
  by (meson always_sat_refl assms hoare_triple_validE sat_comm)


end