Quelle  Guards.thy

subsection ‹Consistency›

text ‹In this file, we define several notions and prove many lemmas about guard states, which are useful
  prove that the rules of the logic are sound.›

theory Guards
  imports StateModel CommCSL AbstractCommutativity
begin

text ‹A state is "consistent" iff:
 . All its permissions are full
 . Has unique guards iff has shared guard
 . The values in the fractional heaps are "reachable" wrt to the sequence and multiset of actions
 . Has exactly guards for the names in "scope"›

definition reachable :: "('i, 'a, 'v) single_context ==> 'v ==> ('i, 'a) heap ==> bool" where
  "reachable scont v0 h ⟷ (∀sargs uargs. get_gs h = Some (pwrite, sargs) ∧ (∀k. get_gu h k = Some (uargs k))
\<longrightarrow> reachable_value (saction scont) (uaction scont) v0 sargs uargs (view scont (normalize (get_fh h))))"

lemma reachableI:
  assumes "∧sargs uargs. get_gs h = Some (pwrite, sargs) ∧ (∀k. get_gu h k = Some (uargs k))
\<Longrightarrow> reachable_value (saction scont) (uaction scont) v0 sargs uargs (view scont (normalize (get_fh h)))"
  shows "reachable scont v0 h"
  by (metis assms reachable_def)

lemma reachableE:
  assumes "reachable scont v0 h"
  and "get_gs h = Some (pwrite, sargs)"
  and "∧k. get_gu h k = Some (uargs k)"
  shows "reachable_value (saction scont) (uaction scont) v0 sargs uargs (view scont (normalize (get_fh h)))"
by (meson assms reachable_def)

definition all_guards :: "('i, 'a) heap ==> bool" where
  "all_guards h ⟷ (∃v. get_gs h = Some (pwrite, v)) ∧ (∀k. get_gu h k ≠ None)"

lemma no_guardI:
  assumes "get_gs h = None"
      and "∧k. get_gu h k = None"
    shows "no_guard h"
  using assms(1) assms(2) no_guard_def by blast

definition semi_consistent :: "('i, 'a, 'v) single_context ==> 'v ==> ('i, 'a) heap ==> bool" where
  "semi_consistent Γ v0 h ⟷ all_guards h ∧ reachable Γ v0 h"

lemma semi_consistentE:
  assumes "semi_consistent Γ v0 h"
  shows "∃sargs uargs. get_gs h = Some (pwrite, sargs) ∧ (∀k. get_gu h k = Some (uargs k))
  ∧ reachable_value (saction Γ) (uaction Γ) v0 sargs uargs (view Γ (normalize (get_fh h)))"
proof -
  let ?uargs = "λk. (SOME x. get_gu h k = Some x)"
  have "∧k. get_gu h k = Some (?uargs k)"
  proof -
    fix k have "∃x. get_gu h k = Some x"
      by (meson all_guards_def assms option.exhaust_sel semi_consistent_def)
    then show "get_gu h k = Some (?uargs k)"
      by fastforce
  qed
  moreover obtain sargs where "get_gs h = Some (pwrite, sargs)"
    by (meson all_guards_def assms semi_consistent_def)
  ultimately have "reachable_value (saction Γ) (uaction Γ) v0 sargs ?uargs (view Γ (normalize (get_fh h)))"
    by (meson assms reachableE semi_consistent_def)
  then show ?thesis
    using ‹∧k. get_gu h k = Some (SOME x. get_gu h k = Some x)› ‹get_gs h = Some (pwrite, sargs)› by fastforce
qed

lemma semi_consistentI:
  assumes "all_guards h"
      and "reachable Γ v0 h"
    shows "semi_consistent Γ v0 h"
  by (simp add: assms(1) assms(2) semi_consistent_def)

lemma no_guard_then_smaller_same:
  assumes "Some h = Some a ⊕ Some b"
      and "no_guard h"
    shows "no_guard a"
proof (rule no_guardI)
  show "get_gs a = None"
    by (metis add_gs.elims assms(1) assms(2) no_guard_def option.simps(3) plus_extract(2))
  fix k
  have "get_gu h k = None"
    by (meson assms(2) no_guard_def)
  then show "get_gu a k = None"
    by (metis assms(1) full_uguard_sum_same option.exhaust)
qed

lemma all_guardsI:
  assumes "∧k. get_gu h k ≠ None"
       and "∃v. get_gs h = Some (pwrite, v)"
     shows "all_guards h"
  using all_guards_def assms(1) assms(2) by blast

lemma all_guards_same:
  assumes "all_guards a"
      and "Some h = Some a ⊕ Some b"
    shows "all_guards h"
proof (rule all_guardsI)
  show "∃v. get_gs h = Some (pwrite, v)"
    using all_guards_def assms(1) assms(2) full_sguard_sum_same by blast
  fix k have "get_gu a k ≠ None"
    by (meson all_guards_def assms(1))
  then show "get_gu h k ≠ None"
    apply (cases "get_gu b k")
     apply (metis assms(2) full_uguard_sum_same not_Some_eq)
    by (metis assms(2) full_uguard_sum_same option.discI plus_comm)
qed

definition empty_unique where
  "empty_unique _ = None"

definition remove_guards :: "('i, 'a) heap ==> ('i, 'a) heap" where
  "remove_guards h = (get_fh h, None, empty_unique)"

lemma remove_guards_smaller:
  "h ⪰ remove_guards h"
proof -
  have "remove_guards h ## (Map.empty, get_gs h, get_gu h)"
  proof (rule compatibleI)
    show "compatible_fract_heaps (get_fh (remove_guards h)) (get_fh (Map.empty, get_gs h, get_gu h))"
      using compatible_fract_heapsI by force
    show "∧k. get_gu (remove_guards h) k = None ∨ get_gu (Map.empty, get_gs h, get_gu h) k = None"
      by (simp add: empty_unique_def remove_guards_def)
    show "∧p p'. get_gs (remove_guards h) = Some p ∧ get_gs (Map.empty, get_gs h, get_gu h) = Some p' ==> pgte pwrite (padd (fst p) (fst p'))"
      by (simp add: remove_guards_def)
  qed
  then obtain x where "Some x = Some (remove_guards h) ⊕ Some (Map.empty, get_gs h, get_gu h)"
    by auto
  moreover have "x = h"
  proof (rule heap_ext)
    show "get_fh x = get_fh h"
      by (metis add_fh_map_empty add_get_fh calculation fst_conv get_fh.elims remove_guards_def)
    show "get_gs x = get_gs h"
      by (metis calculation fst_eqD get_gs.elims plus_comm remove_guards_def snd_eqD sum_gs_one_none)
    show "get_gu x = get_gu h"
    proof (rule ext)
      fix k
      have "get_gu (remove_guards h) k = None"
        by (simp add: empty_unique_def remove_guards_def)       
      then show "get_gu x k = get_gu h k"
        by (metis (mono_tags, lifting) add_gu_def add_gu_single.simps(1) calculation get_gu.elims plus_extract(3) snd_eqD)
    qed
  qed
  ultimately show ?thesis
    using larger_def by blast
qed

lemma no_guard_remove:
  assumes "Some a = Some b ⊕ Some c"
      and "no_guard c"
    shows "get_gs a = get_gs b"
      and "get_gu a = get_gu b"
  using assms(1) assms(2) no_guard_def sum_gs_one_none apply blast
proof (rule ext)
  fix k
  have "get_gu c k = None"
    by (meson assms(2) no_guard_def)
  then show "get_gu a k = get_gu b k"
    by (metis (no_types, lifting) add_gu_def add_gu_single.simps(1) assms(1) plus_comm plus_extract(3))
qed

lemma full_guard_comp_then_no:
  assumes "a ## b"
      and "all_guards a"
    shows "no_guard b"
proof (rule no_guardI)
  show "∧k. get_gu b k = None"
    by (meson all_guards_def assms(1) assms(2) compatible_def)
  show "get_gs b = None"
  proof (rule ccontr)
    assume "get_gs b ≠ None"
    then obtain gb where "get_gs b = Some gb"
      by blast
    moreover obtain v where "get_gs a = Some (pwrite, v)"
      by (meson all_guards_def assms(2))
    moreover have "pgt (padd pwrite (fst gb)) pwrite"
      using sum_larger by auto
    ultimately show False
      by (metis assms(1) compatible_def fst_eqD not_pgte_charact)
  qed
qed

lemma sum_of_no_guards:
  assumes "no_guard a"
      and "no_guard b"
      and "Some x = Some a ⊕ Some b"
    shows "no_guard x"
  by (metis assms(1) assms(2) assms(3) no_guard_def no_guard_remove(1) no_guard_remove(2))

lemma no_guard_remove_guards:
  "no_guard (remove_guards h)"
  by (simp add: empty_unique_def no_guard_def remove_guards_def)

lemma get_fh_remove_guards:
  "get_fh (remove_guards h) = get_fh h"
  by (simp add: remove_guards_def)

definition pair_sat :: "(store × ('i, 'a) heap) set ==> (store × ('i, 'a) heap) set ==> ('i, 'a, nat) assertion ==> bool" where
  "pair_sat S S' Q ⟷ (∀σ σ'. σ ∈ S ∧ σ' ∈ S' ⟶ σ, σ' ⊨ Q)"

lemma pair_satI:
  assumes "∧s h s' h'. (s, h) ∈ S ∧ (s', h') ∈ S' ==> (s, h), (s', h') ⊨ Q"
  shows "pair_sat S S' Q"
  by (simp add: assms pair_sat_def)

lemma pair_sat_smallerI:
  assumes "∧σ σ'. σ ∈ S ∧ σ' ∈ S' ==> σ, σ' ⊨ Q"
  shows "pair_sat S S' Q"
  by (simp add: assms pair_sat_def)

lemma pair_satE:
  assumes "pair_sat S S' Q"
      and "(s, h) ∈ S ∧ (s', h') ∈ S'"
    shows "(s, h), (s', h') ⊨ Q"
  using assms(1) assms(2) pair_sat_def by blast

definition add_states :: "(store × ('i, 'a) heap) set ==> (store × ('i, 'a) heap) set ==> (store × ('i, 'a) heap) set" where
  "add_states S1 S2 = {(s, H) |s H h1 h2. Some H = Some h1 ⊕ Some h2 ∧ (s, h1) ∈ S1 ∧ (s, h2) ∈ S2}"

lemma add_states_sat_star:
  assumes "pair_sat SA SA' A"
      and "pair_sat SB SB' B"
    shows "pair_sat (add_states SA SB) (add_states SA' SB') (Star A B)"
proof (rule pair_satI)
  fix s h s' h'
  assume asm0: "(s, h) ∈ add_states SA SB ∧ (s', h') ∈ add_states SA' SB'"
  then obtain ha hb ha' hb' where "(s, ha) ∈ SA" "(s, hb) ∈ SB" "(s', ha') ∈ SA'" "(s', hb') ∈ SB'"
  "Some h = Some ha ⊕ Some hb" "Some h' = Some ha' ⊕ Some hb'"
    using add_states_def[of SA SB] add_states_def[of SA' SB'] fst_eqD mem_Collect_eq snd_conv
    by auto
  then show "(s, h), (s', h') ⊨ Star A B"
    by (meson assms(1) assms(2) hyper_sat.simps(4) pair_sat_def)
qed

lemma add_states_subset:
  assumes "S1 ⊆ S1'"
  shows "add_states S1 S2 ⊆ add_states S1' S2"
proof
  fix x assume "x ∈ add_states S1 S2"
  then show "x ∈ add_states S1' S2"
    using add_states_def[of S1 S2] add_states_def[of S1' S2] assms mem_Collect_eq[of x] subsetD[of S1 S1']
    by blast
qed

lemma add_states_comm:
  "add_states S1 S2 = add_states S2 S1"
proof -
  have "∧S1 S2. add_states S1 S2 ⊆ add_states S2 S1"
  proof -
    fix S1 S2
    show "add_states S1 S2 ⊆ add_states S2 S1"
    proof
      fix x assume "x ∈ add_states S1 S2"
      then obtain h1 h2 where "Some (snd x) = Some h1 ⊕ Some h2" "(fst x, h1) ∈ S1" "(fst x, h2) ∈ S2"
        using add_states_def[of S1 S2] fst_conv mem_Collect_eq[of x] snd_eqD
        by auto
      moreover have "Some (snd x) = Some h2 ⊕ Some h1"
        by (simp add: calculation(1) plus_comm)
      ultimately show "x ∈ add_states S2 S1"
        using add_states_def[of S2 S1] mem_Collect_eq[of x] surjective_pairing[of x] by blast
    qed
  qed
  then show ?thesis by blast
qed

text ‹The following lemma is the reason why we require many assertions to be precise in the logic.›
lemma magic_lemma:
  assumes "Some x1 = Some a1 ⊕ Some j1"
      and "Some x2 = Some a2 ⊕ Some j2"
      and "(s1, x1), (s2, x2) ⊨ Star A J"
      and "(s1, j1), (s2, j2) ⊨ J"
      and "precise J"
    shows "(s1, a1), (s2, a2) ⊨ A"
proof -
  obtain a1' a2' j1' j2' where "Some x1 = Some a1' ⊕ Some j1'"
   "Some x2 = Some a2' ⊕ Some j2'" "(s1, j1'), (s2, j2') ⊨ J"  "(s1, a1'), (s2, a2') ⊨ A"
    using assms(3) hyper_sat.simps(4) by blast
  have "j1 = j1' ∧ j2 = j2'"
    using assms(5)
  proof (rule preciseE)
    show "x1 ⪰ j1' ∧ x1 ⪰ j1 ∧ x2 ⪰ j2' ∧ x2 ⪰ j2"
      by (metis ‹Some x1 = Some a1' ⊕ Some j1'› ‹Some x2 = Some a2' ⊕ Some j2'› assms(1) assms(2) larger_def plus_comm)
    show "(s1, j1'), (s2, j2') ⊨ J ∧ (s1, j1), (s2, j2) ⊨ J"
      by (simp add: ‹(s1, j1'), (s2, j2') ⊨ J› assms(4))
  qed
  then have "a1 = a1' ∧ a2 = a2'"
    using ‹Some x1 = Some a1' ⊕ Some j1'› ‹Some x2 = Some a2' ⊕ Some j2'› addition_cancellative assms(1) assms(2) by blast
  then show ?thesis
    using ‹(s1, a1'), (s2, a2') ⊨ A› by blast
qed


lemma full_no_guard_same_normalize:
  assumes "full_ownership (get_fh h) ∧ no_guard h"
      and "full_ownership (get_fh h') ∧ no_guard h'"
      and "normalize (get_fh h) = normalize (get_fh h')"
    shows "h = h'"
proof (rule heap_ext)
  show "get_gu h = get_gu h'"
    apply (rule ext)
    by (metis assms(1) assms(2) no_guard_def)
  show "get_gs h = get_gs h'"
    by (metis assms(1) assms(2) no_guard_def)
  show "get_fh h = get_fh h'"
  proof (rule ext)
    fix l show "get_fh h l = get_fh h' l"
      apply (cases "get_fh h l")
      apply (metis FractionalHeap.normalize_eq(1) assms(3))
      apply (cases "get_fh h' l")
      apply (metis FractionalHeap.normalize_eq(1) assms(3))
      by (metis FractionalHeap.normalize_def apply_opt.simps(2) assms(1) assms(2) assms(3) full_ownership_def prod.collapse)
  qed
qed

lemma get_fh_same_then_remove_guards_same:
  assumes "get_fh a = get_fh b"
  shows "remove_guards a = remove_guards b"
  by (metis assms remove_guards_def)


lemma remove_guards_sum:
  assumes "Some x = Some a ⊕ Some b"
  shows "Some (remove_guards x) = Some (remove_guards a) ⊕ Some (remove_guards b)"
proof -
  have "remove_guards a ## remove_guards b"
    by (metis (no_types, lifting) assms compatible_def compatible_eq get_fh_remove_guards no_guard_def no_guard_remove_guards option.distinct(1))
  then obtain y where "Some y = Some (remove_guards a) ⊕ Some (remove_guards b)"
    by auto
  moreover have "remove_guards x = y"
    by (metis (no_types, lifting) ‹remove_guards a ## remove_guards b› add_get_fh assms calculation get_fh_remove_guards get_gu.simps no_guard_def no_guard_remove(1) no_guard_remove(2) no_guard_remove_guards option.inject plus.simps(3) plus_extract(2) remove_guards_def snd_eqD)
  ultimately show ?thesis by blast
qed

lemma no_guard_smaller:
  assumes "a ⪰ b"
  shows "remove_guards a ⪰ remove_guards b"
using assms larger_def remove_guards_sum by blast

definition add_empty_guards :: "('i, 'a) heap ==> ('i, 'a) heap" where
  "add_empty_guards h = (get_fh h, Some (pwrite, {#}), (λ_. Some []))"

lemma no_guard_map_empty_compatible:
  assumes "no_guard a"
      and "get_fh b = Map.empty"
    shows "a ## b"
  by (metis (no_types, lifting) assms(1) assms(2) compatible_def compatible_fract_heapsI no_guard_def option.simps(3))

lemma no_guard_add_empty_is_add:
  assumes "no_guard h"
  shows "Some (add_empty_guards h) = Some h ⊕ Some (Map.empty, Some (pwrite, {#}), (λ_. Some []))"
proof -
  obtain x where "Some x = Some h ⊕ Some (Map.empty, Some (pwrite, {#}), (λ_. Some []))"
    by (simp add: assms no_guard_map_empty_compatible)
  moreover have "add_empty_guards h = x"
  proof (rule heap_ext)
    show "get_fh (add_empty_guards h) = get_fh x"
      by (metis add_empty_guards_def add_fh_map_empty add_get_fh calculation fst_conv get_fh.elims)
    show "get_gs (add_empty_guards h) = get_gs x"
      by (metis add_empty_guards_def assms calculation get_gs.elims no_guard_remove(1) plus_comm snd_eqD)
    show "get_gu (add_empty_guards h) = get_gu x"
      by (metis add_empty_guards_def assms calculation get_gu.elims no_guard_remove(2) plus_comm snd_eqD)
  qed
  ultimately show ?thesis by blast
qed

lemma no_guard_and_sat_p_empty_guards:
  assumes "(s, h), (s', h') ⊨ A"
      and "no_guard h ∧ no_guard h'"
    shows "(s, add_empty_guards h), (s', add_empty_guards h') ⊨ Star A EmptyFullGuards"
proof -
  have "(s, (Map.empty, Some (pwrite, {#}), (λ_. Some []))), (s', (Map.empty, Some (pwrite, {#}), (λ_. Some []))) ⊨ EmptyFullGuards"
    by simp
  then show ?thesis
    using assms(1) assms(2) hyper_sat.simps(4) no_guard_add_empty_is_add by blast
qed

lemma no_guard_add_empty_guards_sum:
  assumes "no_guard x"
      and "Some x = Some a ⊕ Some b"
    shows "Some (add_empty_guards x) = Some (add_empty_guards a) ⊕ Some b"
  using assms(1) assms(2) no_guard_add_empty_is_add[of a] no_guard_add_empty_is_add[of x]
    no_guard_then_smaller_same[of x a b] plus_asso plus_comm
  by (metis (no_types, lifting))

lemma semi_consistent_empty_no_guard_initial_value:
  assumes "no_guard h"
  shows "semi_consistent Γ (view Γ (FractionalHeap.normalize (get_fh h))) (add_empty_guards h)"
proof (rule semi_consistentI)
  show "all_guards (add_empty_guards h)"
    by (simp add: add_empty_guards_def all_guards_def)
  show "reachable Γ (view Γ (FractionalHeap.normalize (get_fh h))) (add_empty_guards h)"
  proof (rule reachableI)
    fix sargs uargs
    assume asm0: "get_gs (add_empty_guards h) = Some (pwrite, sargs) ∧ (∀k. get_gu (add_empty_guards h) k = Some (uargs k))"
    then have "sargs = {#} ∧ uargs = (λk. [])"
      by (metis add_empty_guards_def fst_conv get_gs.simps get_gu.simps option.sel snd_conv)
    then show "reachable_value (saction Γ) (uaction Γ) (view Γ (FractionalHeap.normalize (get_fh h))) sargs uargs
        (view Γ (FractionalHeap.normalize (get_fh (add_empty_guards h))))"
      by (simp add: Self add_empty_guards_def)
  qed
qed

lemma no_guards_remove_same:
  assumes "no_guard h"
  shows "h = remove_guards (add_empty_guards h)"
  by (metis add_empty_guards_def addition_cancellative assms fst_conv get_fh.elims get_fh_remove_guards no_guard_add_empty_is_add no_guard_remove_guards)

lemma no_guards_remove:
  "no_guard h ⟷ h = remove_guards h"
  by (metis get_fh_remove_guards no_guard_remove_guards no_guards_remove_same remove_guards_def)

definition add_sguard_to_no_guard :: "('i, 'a) heap ==> prat ==> 'a multiset ==> ('i, 'a) heap" where
  "add_sguard_to_no_guard h π ms = (get_fh h, Some (π, ms), (λ_. None))"


lemma get_fh_add_sguard:
  "get_fh (add_sguard_to_no_guard h π ms) = get_fh h"
  by (simp add: add_sguard_to_no_guard_def)

lemma add_sguard_as_sum:
  assumes "no_guard h"
  shows "Some (add_sguard_to_no_guard h π ms) = Some h ⊕ Some (Map.empty, Some (π, ms), (λ_. None))"
proof -
  obtain x where "Some x = Some h ⊕ Some (Map.empty, Some (π, ms), (λ_. None))"
    by (simp add: assms no_guard_map_empty_compatible)
  moreover have "x = add_sguard_to_no_guard h π ms"
  proof (rule heap_ext)
    show "get_fh x = get_fh (add_sguard_to_no_guard h π ms)"
      by (metis add_fh_map_empty add_get_fh calculation fst_conv get_fh.elims get_fh_add_sguard)
    show "get_gs x = get_gs (add_sguard_to_no_guard h π ms)"
      by (metis add_sguard_to_no_guard_def assms calculation get_gs.elims no_guard_def plus_comm snd_eqD sum_gs_one_none)
    show "get_gu x = get_gu (add_sguard_to_no_guard h π ms)"
      by (metis add_sguard_to_no_guard_def assms calculation get_gu.simps no_guard_remove(2) plus_comm snd_conv)
  qed
  ultimately show ?thesis by blast
qed

definition add_uguard_to_no_guard :: "'i ==> ('i, 'a) heap ==> 'a list ==> ('i, 'a) heap" where
  "add_uguard_to_no_guard k h l = (get_fh h, None, (λ_. None)(k := Some l))"


lemma get_fh_add_uguard:
  "get_fh (add_uguard_to_no_guard k h l) = get_fh h"
  by (simp add: add_uguard_to_no_guard_def)

lemma prove_sum:
  assumes "a ## b"
      and "∧x. Some x = Some a ⊕ Some b ==> x = y"
    shows "Some y = Some a ⊕ Some b"
  using assms(1) assms(2) by fastforce

lemma add_uguard_as_sum:
  assumes "no_guard h"
  shows "Some (add_uguard_to_no_guard k h l) = Some h ⊕ Some (Map.empty, None, (λ_. None)(k := Some l))"
proof (rule prove_sum)
  show "h ## (Map.empty, None, [k ↦ l])"
    by (simp add: assms no_guard_map_empty_compatible)
  fix x assume asm0: "Some x = Some h ⊕ Some (Map.empty, None, [k ↦ l])"
  show "x = add_uguard_to_no_guard k h l"
  proof (rule heap_ext)
    show "get_fh x = get_fh (add_uguard_to_no_guard k h l)"
      by (metis add_fh_map_empty add_get_fh asm0 fst_conv get_fh.elims get_fh_add_uguard)
    show "get_gs x = get_gs (add_uguard_to_no_guard k h l)"
      by (metis add_uguard_to_no_guard_def asm0 assms get_gs.elims no_guard_def plus_comm snd_eqD sum_gs_one_none)
    show "get_gu x = get_gu (add_uguard_to_no_guard k h l)"
      by (metis add_uguard_to_no_guard_def asm0 assms get_gu.elims no_guard_remove(2) plus_comm snd_eqD)
  qed
qed


lemma no_guard_and_no_heap:
  assumes "Some h = Some p ⊕ Some g"
      and "no_guard p"
      and "get_fh g = Map.empty"
    shows "remove_guards h = p"
proof (rule heap_ext)
  show "get_fh (remove_guards h) = get_fh p"
  proof -
    have "get_fh (remove_guards h) = get_fh h"
      using get_fh_remove_guards by blast
    moreover have "get_fh h = add_fh (get_fh p) (get_fh g)"
      using add_get_fh assms(1) by blast
    ultimately show ?thesis
      by (metis assms(1) assms(3) ext get_fh.simps sum_second_none_get_fh)
  qed
  show "get_gs (remove_guards h) = get_gs p"
    by (metis assms(2) no_guard_def no_guard_remove_guards)
  show "get_gu (remove_guards h) = get_gu p"
    by (metis ‹get_fh (remove_guards h) = get_fh p› assms(2) get_fh_remove_guards no_guards_remove remove_guards_def)
qed


lemma decompose_guard_remove_easy:
  "Some h = Some (remove_guards h) ⊕ Some (Map.empty, get_gs h, get_gu h)"
proof (rule prove_sum)
  show "remove_guards h ## (Map.empty, get_gs h, get_gu h)"
    by (simp add: no_guard_map_empty_compatible no_guard_remove_guards)
  fix x assume asm0: "Some x = Some (remove_guards h) ⊕ Some (Map.empty, get_gs h, get_gu h)"
  show "x = h"
  proof (rule heap_ext)
    show "get_fh x = get_fh h"
      by (metis add_fh_map_empty add_get_fh asm0 fst_conv get_fh.elims get_fh_remove_guards)
    show "get_gs x = get_gs h"
      by (metis asm0 fst_conv get_gs.simps no_guard_remove(1) no_guard_remove_guards plus_comm snd_conv)
    show "get_gu x = get_gu h"
      by (metis asm0 get_gu.elims no_guard_remove(2) no_guard_remove_guards plus_comm snd_eqD)
  qed
qed


lemma all_guards_no_guard_propagates:
  assumes "all_guards x"
      and "Some x = Some a ⊕ Some b"
      and "no_guard a"
    shows "all_guards b"
  by (metis all_guards_def assms(1) assms(2) assms(3) no_guard_def no_guard_remove(2) plus_comm sum_gs_one_none)

lemma all_guards_exists_uargs:
  assumes "all_guards x"
  shows "∃uargs. ∀k. get_gu x k = Some (uargs k)"
proof -
  let ?uargs = "λk. the (get_gu x k)"
  have "∧k. get_gu x k = Some (?uargs k)"
    by (metis all_guards_def assms option.collapse)
  then show ?thesis
    by fastforce
qed

lemma all_guards_sum_known_one:
  assumes "Some x = Some a ⊕ Some b"
      and "all_guards x"
      and "∧k. get_gu a k = None"
      and "get_gs a = Some (π, ms)"
    shows "∃π' msf uargs. (∀k. get_gu b k = Some (uargs k)) ∧
  ((π = pwrite ∧ get_gs b = None ∧ msf = {#}) ∨ (pwrite = padd π π' ∧ get_gs b = Some (π', msf)))"
proof (cases "π = pwrite")
  case True
  then have "get_gs b = None"
    using add_gs.simps(2)[of "(π, ms)"] add_gs_cancellative add_gs_comm assms(1) assms(4) full_sguard_sum_same
      plus_extract(2)[of x a b]
    by metis
  moreover obtain uargs where "∧k. get_gu x k = Some (uargs k)"
    using all_guards_exists_uargs assms(2) by blast
  moreover have "∧k. get_gu b k = Some (uargs k)"
  proof -
    fix k
    have "get_gu a k = None"
      using assms(3) by auto
    then show "get_gu b k = Some (uargs k)"
      by (metis (no_types, opaque_lifting) add_gu_def add_gu_single.simps(1) assms(1) calculation(2) plus_extract(3))
  qed
  ultimately show ?thesis
    using True by blast
next
  case False
  then obtain π' msf where "get_gs b = Some (π', msf)"
    by (metis all_guards_def assms(1) assms(2) assms(4) fst_conv option.exhaust_sel option.sel prod.exhaust_sel sum_gs_one_none)
  moreover obtain v where "get_gs x = Some (pwrite, v)"
    by (meson all_guards_def assms(2))
  ultimately have "pwrite = padd π π'"
    by (metis Pair_inject assms(1) assms(4) option.inject sum_gs_one_some)
  then show ?thesis
    by (metis (mono_tags, opaque_lifting) ‹get_gs b = Some (π', msf)› add_gu_def add_gu_single.simps(1) all_guards_exists_uargs assms(1) assms(2) assms(3) plus_extract(3))
qed

fun add_pwrite_option where
  "add_pwrite_option None = None"
| "add_pwrite_option (Some x) = Some (pwrite, x)"

definition denormalize :: "normal_heap ==> ('i, 'a) heap" where
  "denormalize H = ((λl. add_pwrite_option (H l)), None, (λ_. None))"

lemma denormalize_properties:
  shows "no_guard (denormalize H)"
    and "full_ownership (get_fh (denormalize H))"
    and "normalize (get_fh (denormalize H)) = H"
    and "full_ownership (get_fh h) ∧ no_guard h ==> denormalize (normalize (get_fh h)) = h"
    and "full_ownership (get_fh h) ==> denormalize (normalize (get_fh h)) = remove_guards h"
      apply (simp add: denormalize_def no_guardI)
  using full_ownershipI[of "get_fh (denormalize H)"] add_pwrite_option.elims denormalize_def fst_conv get_fh.elims option.distinct(1) option.sel apply metis
proof -
  show "normalize (get_fh (denormalize H)) = H"
  proof (rule ext)
    fix l show "normalize (get_fh (denormalize H)) l = H l"
      by (metis FractionalHeap.normalize_eq(1) FractionalHeap.normalize_eq(2) add_pwrite_option.elims denormalize_def fst_conv get_fh.elims)
  qed
  show "full_ownership (get_fh h) ∧ no_guard h ==> denormalize (FractionalHeap.normalize (get_fh h)) = h"
  proof -
    assume asm0: "full_ownership (get_fh h) ∧ no_guard h"
    show "denormalize (FractionalHeap.normalize (get_fh h)) = h"
    proof (rule heap_ext)
      show "get_fh (denormalize (FractionalHeap.normalize (get_fh h))) = get_fh h"
      proof (rule ext)
        fix x show "get_fh (denormalize (FractionalHeap.normalize (get_fh h))) x = get_fh h x"
        proof (cases "get_fh h x")
          case None
          then show ?thesis
            by (metis FractionalHeap.normalize_eq(1) add_pwrite_option.simps(1) denormalize_def fst_conv get_fh.elims)
        next
          case (Some p)
          then have "fst p = pwrite"
            by (meson asm0 full_ownership_def)
          then show ?thesis
            by (metis FractionalHeap.normalize_eq(2) Some add_pwrite_option.simps(2) denormalize_def fst_conv get_fh.elims prod.collapse)
        qed
      qed
      show "get_gs (denormalize (FractionalHeap.normalize (get_fh h))) = get_gs h"
        by (metis asm0 denormalize_def fst_conv get_gs.elims no_guard_def snd_eqD)
      show "get_gu (denormalize (FractionalHeap.normalize (get_fh h))) = get_gu h"
        by (metis ‹get_fh (denormalize (FractionalHeap.normalize (get_fh h))) = get_fh h› ‹get_gs (denormalize (FractionalHeap.normalize (get_fh h))) = get_gs h› asm0 denormalize_def full_no_guard_same_normalize get_gu.simps no_guard_def snd_conv)
    qed
  qed
  assume asm0: "full_ownership (get_fh h)"
  show "denormalize (FractionalHeap.normalize (get_fh h)) = remove_guards h"
  proof (rule heap_ext)
    show "get_fh (denormalize (FractionalHeap.normalize (get_fh h))) = get_fh (remove_guards h)"
    proof (rule ext)
      fix x show "get_fh (denormalize (FractionalHeap.normalize (get_fh h))) x = get_fh (remove_guards h) x"
      proof (cases "get_fh h x")
        case None
        then show ?thesis
          by (metis FractionalHeap.normalize_eq(1) add_pwrite_option.simps(1) denormalize_def fst_eqD get_fh.elims get_fh_remove_guards)
      next
        case (Some p)
        then have "fst p = pwrite"
          by (meson asm0 full_ownership_def)
        then show ?thesis
          by (metis FractionalHeap.normalize_eq(2) Some add_pwrite_option.simps(2) denormalize_def fst_conv get_fh.elims get_fh_remove_guards prod.collapse)
      qed
    qed
    show "get_gs (denormalize (FractionalHeap.normalize (get_fh h))) = get_gs (remove_guards h)"
      by (simp add: denormalize_def remove_guards_def)
    show "get_gu (denormalize (FractionalHeap.normalize (get_fh h))) = get_gu (remove_guards h)"
      by (metis ‹get_fh (denormalize (FractionalHeap.normalize (get_fh h))) = get_fh (remove_guards h)› ‹get_gs (denormalize (FractionalHeap.normalize (get_fh h))) = get_gs (remove_guards h)› asm0 denormalize_def full_no_guard_same_normalize get_fh_remove_guards get_gu.simps no_guard_def no_guard_remove_guards snd_conv)
  qed
qed

lemma no_guard_then_sat_star_uguard:
  assumes "no_guard h ∧ no_guard h'"
      and "(s, h), (s', h') ⊨ Q"
    shows "(s, add_uguard_to_no_guard k h (e s)), (s', add_uguard_to_no_guard k h' (e s')) ⊨ Star Q (UniqueGuard k e)"
proof -
  obtain "Some (add_uguard_to_no_guard k h (e s)) = Some h ⊕ Some (Map.empty, None, [k ↦ e s])"
    "Some (add_uguard_to_no_guard k h' (e s')) = Some h' ⊕ Some (Map.empty, None, [k ↦ e s'])"
    by (simp add: add_uguard_as_sum assms(1))
  moreover have "(s, (Map.empty, None, [k ↦ e s])), (s', (Map.empty, None, [k ↦ e s'])) ⊨ UniqueGuard k e"
    by simp
  ultimately show ?thesis using assms(2) by fastforce
qed


lemma no_guard_then_sat_star:
  assumes "no_guard h ∧ no_guard h'"
      and "(s, h), (s', h') ⊨ Q"
    shows "(s, add_sguard_to_no_guard h π (ms s)), (s', add_sguard_to_no_guard h' π (ms s')) ⊨ Star Q (SharedGuard π ms)"
proof -
  obtain "Some (add_sguard_to_no_guard h π (ms s)) = Some h ⊕ Some (Map.empty, Some (π, ms s), (λ_. None))"
    "Some (add_sguard_to_no_guard h' π (ms s')) = Some h' ⊕ Some (Map.empty, Some (π, ms s'), (λ_. None))"
    using add_sguard_as_sum assms(1) by blast
  moreover have "(s, (Map.empty, Some (π, ms s), (λ_. None))), (s', (Map.empty, Some (π, ms s'), (λ_. None))) ⊨ SharedGuard π ms"
    by simp
  ultimately show ?thesis using assms(2) by fastforce
qed


end