Theory CommCSL

section ‹CommCSL›

theory CommCSL
  imports Lang StateModel
begin

definition no_guard :: "('i, 'a) heap ⇒ bool" where
  "no_guard h ⟷ get_gs h = None ∧ (∀k. get_gu h k = None)"

typedef 'a precondition = "{ pre :: ('a ⇒ 'a ⇒ bool) |pre. ∀a b. pre a b ⟶ (pre b a ∧ pre a a) }"
  using Sup2_E by auto

lemma charact_rep_prec:
  assumes "Rep_precondition pre a b"
  shows "Rep_precondition pre b a ∧ Rep_precondition pre a a"
  using Rep_precondition assms by fastforce

typedef ('i, 'a) indexed_precondition = "{ pre :: ('i ⇒ 'a ⇒ 'a ⇒ bool) |pre. ∀a b k. pre k a b ⟶ (pre k b a ∧ pre k a a) }"
  using Sup2_E by auto

lemma charact_rep_indexed_prec:
  assumes "Rep_indexed_precondition pre k a b"
  shows "Rep_indexed_precondition pre k b a ∧ Rep_indexed_precondition pre k a a"
  by (metis (no_types, lifting) Abs_indexed_precondition_cases Rep_indexed_precondition_cases Rep_indexed_precondition_inverse assms mem_Collect_eq)

type_synonym 'a list_exp = "store ⇒ 'a list"

subsection ‹Assertion Language›

datatype ('i, 'a, 'v) assertion =
  Bool bexp
  | Emp
  | And "('i, 'a, 'v) assertion" "('i, 'a, 'v) assertion"
  | Star "('i, 'a, 'v) assertion" "('i, 'a, 'v) assertion"    ("_ * _" 70)
  | Low bexp
  | LowExp exp

  | PointsTo exp prat exp
  | Exists var "('i, 'a, 'v) assertion"

  | EmptyFullGuards

  | PreSharedGuards "'a precondition"
  | PreUniqueGuards "('i, 'a) indexed_precondition"


  | View "normal_heap ⇒ 'v" "('i, 'a, 'v) assertion" "store ⇒ 'v"
  | SharedGuard prat "store ⇒ 'a multiset"
  | UniqueGuard 'i "'a list_exp"

  | Imp bexp "('i, 'a, 'v) assertion"
  | NoGuard

inductive PRE_shared_simpler :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
  Empty: "PRE_shared_simpler spre {#} {#}"
| Step: "⟦ PRE_shared_simpler spre a b ; spre xa xb ⟧ ⟹ PRE_shared_simpler spre (a + {# xa #}) (b + {# xb #})"


definition PRE_unique :: "('b ⇒ 'b ⇒ bool) ⇒ 'b list ⇒ 'b list ⇒ bool" where
  "PRE_unique upre uargs uargs' ⟷ length uargs = length uargs' ∧ (∀i. i ≥ 0 ∧ i < length uargs' ⟶ upre (uargs ! i) (uargs' ! i))"

fun hyper_sat :: "(store × ('i, 'a) heap) ⇒ (store × ('i, 'a) heap) ⇒ ('i, 'a, nat) assertion ⇒ bool" ("_, _ ⊨ _" [51, 65, 66] 50) where
  "(s, _), (s', _)  ⊨ Bool b ⟷ bdenot b s ∧ bdenot b s'"
| "(_, h), (_, h') ⊨ Emp ⟷ dom (get_fh h) = {} ∧ dom (get_fh h') = {}"
| "σ, σ' ⊨ And A B ⟷ σ, σ' ⊨ A ∧ σ, σ' ⊨ B"

| "(s, h), (s', h')  ⊨ Star A B ⟷ (∃h1 h2 h1' h2'. Some h = Some h1 ⊕ Some h2 ∧ Some h' = Some h1' ⊕ Some h2'
  ∧ (s, h1), (s', h1') ⊨ A ∧ (s, h2), (s', h2') ⊨ B)"
| "(s, h), (s', h') ⊨ Low e ⟷ bdenot e s = bdenot e s'"

| "(s, h), (s', h') ⊨ PointsTo loc p x ⟷ get_fh h (edenot loc s) = Some (p, edenot x s) ∧ get_fh h' (edenot loc s') = Some (p, edenot x s')
∧ dom (get_fh h) = {edenot loc s} ∧ dom (get_fh h') = {edenot loc s'}"
| "(s, h), (s', h') ⊨ Exists x A ⟷ (∃v v'. (s(x := v), h), (s'(x := v'), h') ⊨ A)"

| "(s, h), (s', h') ⊨ EmptyFullGuards ⟷ (get_gs h = Some (pwrite, {#}) ∧ (∀k. get_gu h k = Some []) ∧ get_gs h' = Some (pwrite, {#}) ∧ (∀k. get_gu h' k = Some []))"

| "(s, h), (s', h') ⊨ PreSharedGuards spre ⟷
  (∃sargs sargs'. get_gs h = Some (pwrite, sargs) ∧ get_gs h' = Some (pwrite, sargs') ∧ PRE_shared_simpler (Rep_precondition spre) sargs sargs'
  ∧ get_fh h = Map.empty ∧ get_fh h' = Map.empty)"
| "(s, h), (s', h') ⊨ PreUniqueGuards upre ⟷
  (∃uargs uargs'. (∀k. get_gu h k = Some (uargs k)) ∧ (∀k. get_gu h' k = Some (uargs' k)) ∧ (∀k. PRE_unique (Rep_indexed_precondition upre k) (uargs k) (uargs' k)) ∧ get_fh h = Map.empty ∧ get_fh h' = Map.empty)"

| "(s, h), (s', h') ⊨ View f J e ⟷ ((s, h), (s', h') ⊨ J ∧ f (normalize (get_fh h)) = e s ∧ f (normalize (get_fh h')) = e s')"
| "(s, h), (s', h') ⊨ SharedGuard π ms ⟷ ((∀k. get_gu h k = None ∧ get_gu h' k = None) ∧ get_gs h = Some (π, ms s) ∧ get_gs h' = Some (π, ms s')
            ∧ get_fh h = Map.empty ∧ get_fh h' = Map.empty)"

| "(s, h), (s', h') ⊨ UniqueGuard k lexp ⟷ (get_gs h = None ∧ get_gu h k = Some (lexp s) ∧ get_gu h' k = Some (lexp s') ∧ get_gs h' = None
            ∧ get_fh h = Map.empty ∧ get_fh h' = Map.empty ∧ (∀k'. k' ≠ k ⟶ get_gu h k' = None ∧ get_gu h' k' = None))"

| "(s, h), (s', h') ⊨ LowExp e ⟷ edenot e s = edenot e s'"

| "(s, h), (s', h') ⊨ Imp b A ⟷ bdenot b s = bdenot b s' ∧ (bdenot b s ⟶ (s, h), (s', h') ⊨ A)"

| "(s, h), (s', h') ⊨ NoGuard ⟷ (get_gs h = None ∧ (∀k. get_gu h k = None) ∧ get_gs h' = None ∧ (∀k. get_gu h' k = None))"

lemma sat_PreUniqueE:
  assumes "(s, h), (s', h') ⊨ PreUniqueGuards upre"
  shows "∃uargs uargs'. (∀k. get_gu h k = Some (uargs k)) ∧ (∀k. get_gu h' k = Some (uargs' k)) ∧ (∀k. PRE_unique (Rep_indexed_precondition upre k) (uargs k) (uargs' k))"
  using assms by auto


lemma decompose_heap_triple:
  "h = (get_fh h, get_gs h, get_gu h)"
  by simp


definition depends_only_on :: "(store ⇒ 'v) ⇒ var set ⇒ bool" where
  "depends_only_on e S ⟷ (∀s s'. agrees S s s' ⟶ e s = e s')"

lemma depends_only_onI:
  assumes "⋀s s' :: store. agrees S s s' ⟹ e s = e s'"
  shows "depends_only_on e S"
  using assms depends_only_on_def by blast

definition fvS :: "(store ⇒ 'v) ⇒ var set" where
  "fvS e = (SOME S. depends_only_on e S)"

lemma fvSE:
  assumes "agrees (fvS e) s s'"
  shows "e s = e s'"
proof -
  have "depends_only_on e UNIV"
  proof (rule depends_only_onI)
    fix s s' :: store assume "agrees UNIV s s'"
    have "s = s'"
    proof (rule ext)
      fix x :: var have "x ∈ UNIV"
        by auto
      then show "s x = s' x"
        by (meson ‹agrees UNIV s s'› agrees_def)
    qed
    then show "e s = e s'" by simp
  qed
  then show ?thesis
    by (metis assms depends_only_on_def fvS_def someI_ex)
qed


fun fvA :: "('i, 'a, 'v) assertion ⇒ var set" where
  "fvA (Bool b) = fvB b"
| "fvA (And A B) = fvA A ∪ fvA B"
| "fvA (Star A B) = fvA A ∪ fvA B"
| "fvA (Low e) = fvB e"
| "fvA Emp = {}"
| "fvA (PointsTo v va vb) = fvE v ∪ fvE vb"
| "fvA (Exists x A) = fvA A - {x}"
| "fvA (SharedGuard _ e) = fvS e"
| "fvA (UniqueGuard _ e) = fvS e"
| "fvA (View view A e) = fvA A ∪ fvS e"
| "fvA (PreSharedGuards _) = {}"
| "fvA (PreUniqueGuards _) = {}"
| "fvA EmptyFullGuards = {}"
| "fvA (LowExp x) = fvE x"
| "fvA (Imp b A) = fvB b ∪ fvA A"

definition subS :: "var ⇒ exp ⇒ (store ⇒ 'v) ⇒ (store ⇒ 'v)" where
  "subS x E e = (λs. e (s(x := edenot E s)))"

lemma subS_assign:
  "subS x E e s  ⟷ e (s(x := edenot E s))"
  by (simp add: subS_def)

fun collect_existentials :: "('i, 'a, nat) assertion ⇒ var set" where
  "collect_existentials (And A B) = collect_existentials A ∪ collect_existentials B"
| "collect_existentials (Star A B) = collect_existentials A ∪ collect_existentials B"
| "collect_existentials (Exists x A) = collect_existentials A ∪ {x}"
| "collect_existentials (View view A e) = collect_existentials A"
| "collect_existentials (Imp _ A) = collect_existentials A"
| "collect_existentials _ = {}"

fun subA :: "var ⇒ exp ⇒ ('i, 'a, nat) assertion ⇒ ('i, 'a, nat) assertion" where
  "subA x E (And A B) = And (subA x E A) (subA x E B)"
| "subA x E (Star A B) = Star (subA x E A) (subA x E B)"
| "subA x E (Bool B) = Bool (subB x E B)"
| "subA x E (Low e) = Low (subB x E e)"
| "subA x E (LowExp e) = LowExp (subE x E e)"
| "subA x E (UniqueGuard k e) = UniqueGuard k (subS x E e)"
| "subA x E (SharedGuard π e) = SharedGuard π (subS x E e)"
| "subA x E (View view A e) = View view (subA x E A) (subS x E e)"
| "subA x E (PointsTo loc π e) = PointsTo (subE x E loc) π (subE x E e)"
| "subA x E (Exists y A) = (if x = y then Exists y A else Exists y (subA x E A))"
| "subA x E (Imp b A) = Imp (subB x E b) (subA x E A)"
| "subA _ _ A = A"

lemma subA_assign:
  assumes "collect_existentials A ∩ fvE E = {}"
  shows "(s, h), (s', h') ⊨ subA x E A ⟷ (s(x := edenot E s), h), (s'(x := edenot E s'), h') ⊨ A"
  using assms
proof (induct A arbitrary: s h s' h')
  case (And A1 A2)
  then show ?case
    by (simp add: disjoint_iff_not_equal)
next
  case (Star A1 A2)
  then show ?case
    by (simp add: disjoint_iff_not_equal)
next
  case (Bool x)
  then show ?case
    by (metis hyper_sat.simps(1) subA.simps(3) subB_assign)
next
  case (Low x2)
  then show ?case
    by (metis (no_types, lifting) hyper_sat.simps(5) subA.simps(4) subB_assign)
next
  case (LowExp x2)
  then show ?case
    by (metis (no_types, lifting) hyper_sat.simps(14) subA.simps(5) subE_assign)
next
  case (PointsTo x1a x2 x3)
  then show ?case
    by (metis (no_types, lifting) hyper_sat.simps(6) subA.simps(9) subE_assign)
next
  case (Exists y A)
  then have asm0: "collect_existentials A ∩ fvE E = {}"
    by auto
  show ?case (is "?A ⟷ ?B")
  proof
    show "?A ⟹ ?B"
    proof -
      assume ?A
      show ?B
      proof (cases "x = y")
        case True
        then show ?thesis by (metis (no_types, opaque_lifting) ‹?A› fun_upd_upd hyper_sat.simps(7) subA.simps(10))
      next
        case False
        then obtain v v' where "(s(y := v), h), (s'(y := v'), h') ⊨ subA x E A"
          using ‹(s, h), (s', h') ⊨ subA x E (Exists y A)› by auto
        then have "((s(y := v))(x := edenot E (s(y := v))), h), ((s'(y := v'))(x := edenot E (s'(y := v'))), h') ⊨ A"
          using Exists asm0 by blast
        moreover have "y ∉ fvE E"
          using Exists.prems by force
        then have "edenot E (s(y := v)) = edenot E s ∧ edenot E (s'(y := v')) = edenot E s'"
          by (metis agrees_update exp_agrees)
        moreover have "(s(y := v))(x := edenot E s) = (s(x := edenot E s))(y := v)
        ∧ (s'(y := v'))(x := edenot E s') = (s'(x := edenot E s'))(y := v')"
          by (simp add: False fun_upd_twist)
        ultimately show ?thesis using False hyper_sat.simps(7)
          by metis
      qed
    qed
    assume ?B
    show ?A
    proof (cases "x = y")
      case True
      then show ?thesis
        using ‹(s(x := edenot E s), h), (s'(x := edenot E s'), h') ⊨ Exists y A› by fastforce
    next
      case False
      then obtain v v' where "((s(x := edenot E s))(y := v), h), ((s'(x := edenot E s'))(y := v'), h') ⊨ A"
        using ‹(s(x := edenot E s), h), (s'(x := edenot E s'), h') ⊨ Exists y A› hyper_sat.simps(7) by blast
      moreover have "(s(y := v))(x := edenot E s) = (s(x := edenot E s))(y := v)
      ∧ (s'(y := v'))(x := edenot E s') = (s'(x := edenot E s'))(y := v')"
        by (simp add: False fun_upd_twist)
      then have "((s(y := v))(x := edenot E (s(y := v))), h), ((s'(y := v'))(x := edenot E (s'(y := v'))), h') ⊨ A"
        using Exists.prems calculation by auto
      then show ?thesis
        by (metis Exists.hyps False asm0 hyper_sat.simps(7) subA.simps(10))
    qed
  qed
next
  case (View x1a A x3)
  then show ?case
    by (metis (mono_tags, lifting) collect_existentials.simps(4) hyper_sat.simps(11) subA.simps(8) subS_def)
next
  case (SharedGuard x1a x2)
  then show ?case
    by (metis (mono_tags, lifting) hyper_sat.simps(12) subA.simps(7) subS_def)
next
  case (UniqueGuard x)
  then show ?case
    by (metis (mono_tags, lifting) hyper_sat.simps(13) subA.simps(6) subS_def)
next
  case (Imp b A)
  then show ?case
    by (metis collect_existentials.simps(5) hyper_sat.simps(15) subA.simps(11) subB_assign)
qed (auto)

lemma PRE_uniqueI:
  assumes "length uargs = length uargs'"
      and "⋀i. i ≥ 0 ∧ i < length uargs' ⟹ upre (uargs ! i) (uargs' ! i)"
    shows "PRE_unique upre uargs uargs'"
  using assms PRE_unique_def by blast

lemma PRE_unique_implies_tl:
  assumes "PRE_unique upre (ta # qa) (tb # qb)"
  shows "PRE_unique upre qa qb"
proof (rule PRE_uniqueI)
  show "length qa = length qb"
    by (metis PRE_unique_def assms diff_Suc_1 length_Cons)
  fix i assume "0 ≤ i ∧ i < length qb"
  then have "upre ((ta # qa) ! (i + 1)) ((tb # qb) ! (i + 1))"
    using assms PRE_unique_def [of upre ‹ta # qa› ‹tb # qb›]
    by (auto simp add: less_Suc_eq_le dest: spec [of _ ‹Suc i›])
  then show "upre (qa ! i) (qb ! i)"
    by simp
qed


lemma charact_PRE_unique:
  assumes "PRE_unique (Rep_indexed_precondition pre k) a b"
  shows "PRE_unique (Rep_indexed_precondition pre k) b a ∧ PRE_unique (Rep_indexed_precondition pre k) a a"
  using assms
proof (induct "length a" arbitrary: a b)
  case 0
  then show ?case
    by (simp add: PRE_unique_def)
next
  case (Suc n)
  then obtain ha ta hb tb where "a = ha # ta" "b = hb # tb"
    by (metis One_nat_def PRE_unique_def Suc_le_length_iff le_add1 plus_1_eq_Suc)
  then have "n = length ta"
    using Suc.hyps(2) by auto
  then have "PRE_unique (Rep_indexed_precondition pre k) tb ta ∧ PRE_unique (Rep_indexed_precondition pre k) ta ta"
    by (metis PRE_unique_implies_tl Suc.hyps(1) Suc.prems ‹a = ha # ta› ‹b = hb # tb›)
  then show ?case
    by (metis PRE_unique_def Suc.prems charact_rep_indexed_prec)
qed

lemma charact_PRE_shared_simpler:
  assumes "PRE_shared_simpler rpre a b"
      and "Rep_precondition pre = rpre"
  shows "PRE_shared_simpler (Rep_precondition pre) b a ∧ PRE_shared_simpler (Rep_precondition pre) a a"
  using assms
proof (induct arbitrary: pre rule: PRE_shared_simpler.induct)
  case (Empty spre)
  then show ?case
    by (simp add: PRE_shared_simpler.Empty)
next
  case (Step spre a b xa xb)
  then have "spre xb xa ∧ spre xa xa" using charact_rep_prec by metis
  then show ?case
    by (metis PRE_shared_simpler.Step Step.hyps(2) Step.prems)
qed


lemma always_sat_refl_aux:
  assumes "(s, h), (s', h') ⊨ A"
  shows "(s, h), (s, h) ⊨ A"
  using assms
proof (induct A arbitrary: s h s' h')
  case (Star A B)
  then obtain ha hb ha' hb' where "Some h = Some ha ⊕ Some hb" "Some h' = Some ha' ⊕ Some hb'"
    "(s, ha), (s', ha') ⊨ A" "(s, hb), (s', hb') ⊨ B"
    by auto
  then have "(s, ha), (s, ha) ⊨ A ∧ (s, hb), (s, hb) ⊨ B"
    using Star.hyps(1) Star.hyps(2) by blast
  then show ?case
    using ‹Some h = Some ha ⊕ Some hb› hyper_sat.simps(4) by blast
next
  case (Exists x A)
  then show ?case
    by (meson hyper_sat.simps(7))
next
  case (PreSharedGuards x)
  then show ?case
    using charact_PRE_shared_simpler by force
next
  case (PreUniqueGuards upre)
  then obtain uargs uargs' where "(∀k. get_gu h k = Some (uargs k)) ∧
        (∀k. get_gu h' k = Some (uargs' k)) ∧ (∀k. PRE_unique (Rep_indexed_precondition upre k) (uargs k) (uargs' k)) ∧ get_fh h = Map.empty ∧ get_fh h' = Map.empty"
    using hyper_sat.simps(10)[of s h s' h' upre] by blast
  then show "(s, h), (s, h) ⊨ PreUniqueGuards upre"
    using charact_PRE_unique hyper_sat.simps(10)[of s h s h upre]
    by metis
qed (auto)

lemma always_sat_refl:
  assumes "σ, σ' ⊨ A"
  shows "σ, σ ⊨ A"
  by (metis always_sat_refl_aux assms prod.exhaust_sel)

lemma agrees_same_aux:
  assumes "agrees (fvA A) s s''"
    and "(s, h), (s', h') ⊨ A"
  shows "(s'', h), (s', h') ⊨ A"
  using assms
proof (induct A arbitrary: s s' s'' h h')
  case (Bool b)
  then show ?case by (simp add: bexp_agrees)
next
  case (And A1 A2)
  then show ?case using fvA.simps(2) hyper_sat.simps(3)
    by (metis (mono_tags, lifting) UnCI agrees_def)
next
  case (Star A B)
  then obtain ha hb ha' hb' where "Some h = Some ha ⊕ Some hb" "Some h' = Some ha' ⊕ Some hb'"
    "(s, ha), (s', ha') ⊨ A" "(s, hb), (s', hb') ⊨ B"
    by auto
  then have "(s'', ha), (s', ha') ⊨ A ∧ (s'', hb), (s', hb') ⊨ B"
    using Star.hyps[of s s'' _ s' _] Star.prems(1)
    by (simp add: agrees_def)
  then show ?case
    using ‹Some h = Some ha ⊕ Some hb› ‹Some h' = Some ha' ⊕ Some hb'› hyper_sat.simps(4) by blast
next
  case (Low e)
  then have "bdenot e s = bdenot e s''"
    by (metis bexp_agrees fvA.simps(4))
  then show ?case using Low by simp
next
  case (LowExp e)
  then have "edenot e s = edenot e s''"
    by (metis exp_agrees fvA.simps(14))
  then show ?case using LowExp by simp
next
  case (PointsTo l π v)
  then have "edenot l s = edenot l s'' ∧ edenot v s = edenot v s''"
    by (simp add: agrees_def exp_agrees)
  then show ?case using PointsTo by auto
next
  case (Exists x A)
  then obtain v v' where "(s(x := v), h), (s'(x := v'), h') ⊨ A"
    by auto
  moreover have "agrees (fvA A) (s(x := v)) (s''(x := v))"
  proof (rule agreesI)
    fix y show "y ∈ fvA A ⟹ (s(x := v)) y = (s''(x := v)) y"
      apply (cases "y = x")
       apply simp
      using Diff_iff[of y "fvA A" "{x}"] Exists.prems(1) agrees_def empty_iff fun_upd_apply[of s x v] fun_upd_apply[of s'' x v] fvA.simps(7) insert_iff
      by metis
  qed
  ultimately have "(s''(x := v), h), (s'(x := v'), h') ⊨ A"
    using Exists.hyps by blast
  then show ?case by auto
next
  case (View x1a A e)
  then have "(s'', h), (s', h') ⊨ A ∧ e s = e s''"
    using fvA.simps(10) fvSE hyper_sat.simps(11) agrees_union
    by metis
  then show ?case
    using View.prems(2) by auto
next
  case (SharedGuard x1a x2)
  then show ?case using fvSE by auto
next
  case (UniqueGuard x)
  then show ?case using fvSE by auto
next
  case (Imp b A)
  then show ?case
    by (metis agrees_union bexp_agrees fvA.simps(15) hyper_sat.simps(15))
qed (auto)

lemma agrees_same:
  assumes "agrees (fvA A) s s''"
  shows "(s, h), (s', h') ⊨ A ⟷ (s'', h), (s', h') ⊨ A"
  by (metis (mono_tags, lifting) agrees_def agrees_same_aux assms)

lemma sat_comm_aux:
  "(s, h), (s', h') ⊨ A ⟹ (s', h'), (s, h) ⊨ A"
proof (induct A arbitrary: s h s' h')
  case (Star A B)
  then obtain ha hb ha' hb' where "Some h = Some ha ⊕ Some hb" "Some h' = Some ha' ⊕ Some hb'"
    "(s, ha), (s', ha') ⊨ A" "(s, hb), (s', hb') ⊨ B"
    by auto
  then have "(s', ha'), (s, ha) ⊨ A ∧ (s', hb'), (s, hb) ⊨ B"
    using Star.hyps(1) Star.hyps(2) by presburger
  then show ?case
    using ‹Some h = Some ha ⊕ Some hb› ‹Some h' = Some ha' ⊕ Some hb'› hyper_sat.simps(4) by blast
next
  case (Exists x A)
  then obtain v v' where "(s(x := v), h), (s'(x := v'), h') ⊨ A"
    by auto
  then have "(s'(x := v'), h'), (s(x := v), h) ⊨ A"
    using Exists.hyps by blast
  then show ?case by auto
next
  case (PreSharedGuards x)
  then show ?case
    by (meson charact_PRE_shared_simpler hyper_sat.simps(9))
next
  case (PreUniqueGuards upre)
  then obtain uargs uargs' where "(∀k. get_gu h k = Some (uargs k)) ∧
        (∀k. get_gu h' k = Some (uargs' k)) ∧ (∀k. PRE_unique (Rep_indexed_precondition upre k) (uargs k) (uargs' k)) ∧ get_fh h = Map.empty ∧ get_fh h' = Map.empty"
    using hyper_sat.simps(10)[of s h s' h' upre] by blast
  then show "(s', h'), (s, h) ⊨ PreUniqueGuards upre"
    using charact_PRE_unique hyper_sat.simps(10)[of s' h' s h upre]
    by metis
qed (auto)

lemma sat_comm:
  "σ, σ' ⊨ A ⟷ σ', σ ⊨ A"
  using sat_comm_aux surj_pair by metis

definition precise where
  "precise J ⟷ (∀s1 H1 h1 h1' s2 H2 h2 h2'. H1 ≽ h1 ∧ H1 ≽ h1' ∧ H2 ≽ h2 ∧ H2 ≽ h2'
  ∧ (s1, h1), (s2, h2) ⊨ J ∧ (s1, h1'), (s2, h2') ⊨ J ⟶ h1' = h1 ∧ h2' = h2)"

lemma preciseI:
  assumes "⋀s1 H1 h1 h1' s2 H2 h2 h2'. H1 ≽ h1 ∧ H1 ≽ h1' ∧ H2 ≽ h2 ∧ H2 ≽ h2' ⟹
        (s1, h1), (s2, h2) ⊨ J ⟹ (s1, h1'), (s2, h2') ⊨ J ⟹ h1' = h1 ∧ h2' = h2"
  shows "precise J"
  using assms precise_def by blast

lemma preciseE:
  assumes "precise J"
      and "H1 ≽ h1 ∧ H1 ≽ h1' ∧ H2 ≽ h2 ∧ H2 ≽ h2'"
      and "(s1, h1), (s2, h2) ⊨ J ∧ (s1, h1'), (s2, h2') ⊨ J"
    shows "h1' = h1 ∧ h2' = h2"
  using assms(1) assms(2) assms(3) precise_def by blast



definition unary where
  "unary J ⟷ (∀s h s' h'. (s, h), (s, h) ⊨ J ∧ (s', h'), (s', h') ⊨ J ⟶ (s, h), (s', h') ⊨ J)"

lemma unaryI:
  assumes "⋀s1 h1 s2 h2. (s1, h1), (s1, h1) ⊨ J ∧ (s2, h2), (s2, h2) ⊨ J ⟹ (s1, h1), (s2, h2) ⊨ J"
    shows "unary J"
  using assms unary_def by blast

lemma unary_smallerI:
  assumes "⋀σ1 σ2. σ1, σ1 ⊨ J ∧ σ2, σ2 ⊨ J ⟹ σ1, σ2 ⊨ J"
    shows "unary J"
  using assms unary_def by blast

lemma unaryE:
  assumes "unary J"
      and "(s, h), (s, h) ⊨ J ∧ (s', h'), (s', h') ⊨ J"
    shows "(s, h), (s', h') ⊨ J"
  using assms(1) assms(2) unary_def by blast


definition entails :: "('i, 'a, nat) assertion ⇒ ('i, 'a, nat) assertion ⇒ bool" where
  "entails A B ⟷ (∀σ σ'. σ, σ' ⊨ A ⟶ σ, σ' ⊨ B)"

lemma entailsI:
  assumes "⋀x y. x, y ⊨ A ⟹ x, y ⊨ B"
  shows "entails A B"
  using assms entails_def by blast

lemma sat_points_to:
  assumes "(s, h :: ('i, 'a) heap), (s, h) ⊨ PointsTo a π e"
  shows "get_fh h = [edenot a s ↦ (π, edenot e s)]"
proof -
  have "get_fh h (edenot a s) = Some (π, edenot e s) ∧ dom (get_fh h) = {edenot a s}"
    using assms by auto
  then show ?thesis
    by fastforce
qed



lemma unary_inv_then_view:
  assumes "unary J"
  shows "unary (View f J e)"
proof (rule unaryI)
  fix s h s' h'
  assume asm0: "(s, h), (s, h) ⊨ View f J e ∧ (s', h'), (s', h') ⊨ View f J e"
  then show "(s, h), (s', h') ⊨ View f J e"
    by (meson assms hyper_sat.simps(11) unaryE)
qed

lemma precise_inv_then_view:
  assumes "precise J"
  shows "precise (View f J e)"
proof (rule preciseI)
  fix s1 H1 h1 h1' s2 H2 h2 h2'
  assume asm0: "H1 ≽ h1 ∧ H1 ≽ h1' ∧ H2 ≽ h2 ∧ H2 ≽ h2'" "(s1, h1), (s2, h2) ⊨ View f J e"
    "(s1, h1'), (s2, h2') ⊨ View f J e"
  then show "h1' = h1 ∧ h2' = h2"
    by (meson assms hyper_sat.simps(11) preciseE)
qed

fun syntactic_unary :: "('i, 'a, nat) assertion ⇒ bool" where
  "syntactic_unary (Bool b) ⟷ True"
| "syntactic_unary (And A B) ⟷ syntactic_unary A ∧ syntactic_unary B"
| "syntactic_unary (Star A B) ⟷ syntactic_unary A ∧ syntactic_unary B"
| "syntactic_unary (Low e) ⟷ False"
| "syntactic_unary Emp ⟷ True"
| "syntactic_unary (PointsTo v va vb) ⟷ True"
| "syntactic_unary (Exists x A) ⟷ syntactic_unary A"
| "syntactic_unary (SharedGuard _ e) ⟷ True"
| "syntactic_unary (UniqueGuard _ e) ⟷ True"
| "syntactic_unary (View view A e) ⟷ syntactic_unary A"
| "syntactic_unary (PreSharedGuards _) ⟷ False"
| "syntactic_unary (PreUniqueGuards _) ⟷ False"
| "syntactic_unary EmptyFullGuards ⟷ True"
| "syntactic_unary (LowExp x) ⟷ False"
| "syntactic_unary (Imp b A) ⟷ False"

lemma syntactic_unary_implies_unary:
  assumes "syntactic_unary A"
  shows "unary A"
  using assms
proof (induct A)
  case (And A1 A2)
  show ?case
  proof (rule unary_smallerI)
    fix σ1 σ2
    assume "σ1, σ1 ⊨ And A1 A2 ∧ σ2, σ2 ⊨ And A1 A2"
    then have "σ1, σ2 ⊨ A1 ∧ σ1, σ2 ⊨ A2"
      using And unary_def
      by (metis hyper_sat.simps(3) prod.exhaust_sel syntactic_unary.simps(2))
    then show "σ1, σ2 ⊨ And A1 A2"
      using hyper_sat.simps(3) by blast
  qed
next
  case (Star A B)
  then have "unary A ∧ unary B" by simp
  show ?case
  proof (rule unaryI)
    fix s1 h1 s2 h2
    assume asm0: "(s1, h1), (s1, h1) ⊨ Star A B ∧ (s2, h2), (s2, h2) ⊨ Star A B"
    then obtain a1 b1 a2 b2 where "Some h1 = Some a1 ⊕ Some b1" "(s1, a1), (s1, a1) ⊨ A" "(s1, b1), (s1, b1) ⊨ B"
     "Some h2 = Some a2 ⊕ Some b2" "(s2, a2), (s2, a2) ⊨ A" "(s2, b2), (s2, b2) ⊨ B"
      by (meson always_sat_refl hyper_sat.simps(4))
    then have "(s1, a1), (s2, a2) ⊨ A ∧ (s1, b1), (s2, b2) ⊨ B"
      using ‹unary A ∧ unary B› unaryE by blast
    then show "(s1, h1), (s2, h2) ⊨ Star A B"
      using ‹Some h1 = Some a1 ⊕ Some b1› ‹Some h2 = Some a2 ⊕ Some b2› hyper_sat.simps(4) by blast
  qed
next
  case (Exists x A)
  then have "unary A" by simp
  show ?case
  proof (rule unaryI)
    fix s1 h1 s2 h2
    assume "(s1, h1), (s1, h1) ⊨ Exists x A ∧ (s2, h2), (s2, h2) ⊨ Exists x A"
    then obtain v1 v2 where "(s1(x := v1), h1), (s1(x := v1), h1) ⊨ A ∧ (s2(x := v2), h2), (s2(x := v2), h2) ⊨ A"
      by (meson always_sat_refl hyper_sat.simps(7))
    then have "(s1(x := v1), h1), (s2(x := v2), h2) ⊨ A"
      using ‹unary A› unary_def by blast
    then show "(s1, h1), (s2, h2) ⊨ Exists x A" by auto
  qed
next
  case (View view A x)
  then have "unary A" by simp
  show ?case
  proof (rule unaryI)
    fix s1 h1 s2 h2
    assume asm0: "(s1, h1), (s1, h1) ⊨ View view A x ∧ (s2, h2), (s2, h2) ⊨ View view A x"
    then have "(s1, h1), (s2, h2) ⊨ A"
      by (meson ‹unary A› hyper_sat.simps(11) unaryE)
    then show "(s1, h1), (s2, h2) ⊨ View view A x"
      using asm0 by fastforce
  qed
qed (auto simp add: unary_def)

record ('i, 'a, 'v) single_context =
  view :: "(loc ⇀ val) ⇒ 'v"
  abstract_view :: "'v ⇒ 'v"
  saction :: "'v ⇒ 'a ⇒ 'v"
  uaction :: "'i ⇒ 'v ⇒ 'a ⇒ 'v"
  invariant :: "('i, 'a, 'v) assertion"

type_synonym ('i, 'a, 'v) cont = "('i, 'a, 'v) single_context option"

definition no_guard_assertion where
  "no_guard_assertion A ⟷ (∀s1 h1 s2 h2. (s1, h1), (s2, h2) ⊨ A ⟶ no_guard h1 ∧ no_guard h2)"

text ‹Axiom that says that view only depends on the part of the heap described by inv›
definition view_function_of_inv :: "('i, 'a, nat) single_context ⇒ bool" where
  "view_function_of_inv Γ ⟷ (∀(h :: ('i, 'a) heap) (h' :: ('i, 'a) heap) s. (s, h), (s, h) ⊨ invariant Γ ∧ (h' ≽ h)
  ⟶ view Γ (normalize (get_fh h)) = view Γ (normalize (get_fh h')))"

definition wf_indexed_precondition :: "('i ⇒ 'a ⇒ 'a ⇒ bool) ⇒ bool" where
  "wf_indexed_precondition pre ⟷ (∀a b k. pre k a b ⟶ (pre k b a ∧ pre k a a))"

definition wf_precondition :: "('a ⇒ 'a ⇒ bool) ⇒ bool" where
  "wf_precondition pre ⟷ (∀a b. pre a b ⟶ (pre b a ∧ pre a a))"


lemma wf_precondition_rep_prec:
  assumes "wf_precondition pre"
  shows "Rep_precondition (Abs_precondition pre) = pre"
  using Abs_precondition_inverse[of pre] assms mem_Collect_eq wf_precondition_def[of pre]
  by blast


lemma wf_indexed_precondition_rep_prec:
  assumes "wf_indexed_precondition pre"
  shows "Rep_indexed_precondition (Abs_indexed_precondition pre) = pre"
  using Abs_indexed_precondition_inverse[of pre] assms mem_Collect_eq wf_indexed_precondition_def[of pre]
  by blast


definition LowView where
  "LowView f A x = (Exists x (And (View f A (λs. s x)) (LowExp (Evar x))))"

lemma LowViewE:
  assumes "(s, h), (s', h') ⊨ LowView f A x"
      and "x ∉ fvA A"
    shows "(s, h), (s', h') ⊨ A ∧ f (normalize (get_fh h)) = f (normalize (get_fh h'))"
proof -
  obtain v v' where "(s(x := v), h), (s'(x := v'), h') ⊨ And (View f A (λs. s x)) (LowExp (Evar x))"
    by (metis LowView_def assms(1) hyper_sat.simps(7))
  then obtain "(s(x := v), h), (s'(x := v'), h') ⊨ View f A (λs. s x)"
        "(s(x := v), h), (s'(x := v'), h') ⊨ LowExp (Evar x)"
    using hyper_sat.simps(3) by blast
  then obtain "(s(x := v), h), (s'(x := v'), h') ⊨ A" "v = v'"
      "f (normalize (get_fh h)) = f (normalize (get_fh h'))"
    by simp
  moreover have "(s, h), (s', h') ⊨ A"
    by (meson agrees_same agrees_update assms(2) calculation(1) sat_comm_aux)
  ultimately show ?thesis by blast
qed

lemma LowViewI:
  assumes "(s, h), (s', h') ⊨ A"
      and "f (normalize (get_fh h)) = f (normalize (get_fh h'))"
      and "x ∉ fvA A"
    shows "(s, h), (s', h') ⊨ LowView f A x"
proof -
  let ?s = "s(x := f (normalize (get_fh h)))"
  let ?s' = "s'(x := f (normalize (get_fh h')))"
  have "(?s, h), (?s', h') ⊨ A"
    by (meson agrees_same_aux agrees_update assms(1) assms(3) sat_comm_aux)
  then have "(?s, h), (?s', h') ⊨ And (View f A (λs. s x)) (LowExp (Evar x))"
    using assms(2) by auto
  then show ?thesis using LowView_def
    by (metis hyper_sat.simps(7))
qed

definition disjoint :: "('a set) ⇒ ('a set) ⇒ bool" 
  where "disjoint h1 h2 = (h1 ∩ h2 = {})"

definition unambiguous where
  "unambiguous A x ⟷ (∀s1 h1 s2 h2 v1 v2 v1' v2'. (s1(x := v1), h1), (s2(x := v2), h2) ⊨ A
  ∧ (s1(x := v1'), h1), (s2(x := v2'), h2) ⊨ A ⟶ v1 = v1' ∧ v2 = v2')"

definition all_axioms :: "('v ⇒ 'w) ⇒ ('v ⇒ 'a ⇒ 'v) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('i ⇒ 'v ⇒ 'b ⇒ 'v) ⇒ ('i ⇒ 'b ⇒ 'b ⇒ bool) ⇒ bool" where
  "all_axioms α sact spre uact upre ⟷

―‹Every action's relational precondition is sufficient to preserve the low-ness of the abstract view of the resource value:›
  (∀v v' sarg sarg'. α v = α v' ∧ spre sarg sarg' ⟶ α (sact v sarg) = α (sact v' sarg')) ∧
  (∀v v' uarg uarg' i. α v = α v' ∧ upre i uarg uarg' ⟶ α (uact i v uarg) = α (uact i v' uarg')) ∧

  (∀sarg sarg'. spre sarg sarg' ⟶ spre sarg' sarg') ∧
  (∀uarg uarg' i. upre i uarg uarg' ⟶ upre i uarg' uarg') ∧

―‹All relevant pairs of actions commute w.r.t. the abstract view:›
  (∀v v' sarg sarg'. α v = α v' ∧ spre sarg sarg ∧ spre sarg' sarg' ⟶ α (sact (sact v sarg) sarg') = α (sact (sact v' sarg') sarg)) ∧
  (∀v v' sarg uarg i. α v = α v' ∧ spre sarg sarg ∧ upre i uarg uarg ⟶ α (sact (uact i v uarg) sarg) = α (uact i (sact v' sarg) uarg)) ∧
  (∀v v' uarg uarg' i i'. i ≠ i' ∧ α v = α v' ∧ upre i uarg uarg ∧ upre i' uarg' uarg'
  ⟶ α (uact i' (uact i v uarg) uarg') = α (uact i (uact i' v' uarg') uarg))"

subsection ‹Rules of the Logic›

inductive CommCSL :: "('i, 'a, nat) cont ⇒ ('i, 'a, nat) assertion ⇒ cmd ⇒ ('i, 'a, nat) assertion ⇒ bool"
   ("_ ⊢ {_} _ {_}" [51,0,0] 81) where
  RuleSkip: "Δ ⊢ {P} Cskip {P}"
| RuleAssign: "⟦ ⋀Γ. Δ = Some Γ ⟹ x ∉ fvA (invariant Γ) ; collect_existentials P ∩ fvE E = {} ⟧ ⟹ Δ ⊢ {subA x E P} Cassign x E {P} "
| RuleNew: "⟦ x ∉ fvE E; ⋀Γ. Δ = Some Γ ⟹ x ∉ fvA (invariant Γ) ∧ view_function_of_inv Γ ⟧ ⟹ Δ ⊢ {Emp} Calloc x E {PointsTo (Evar x) pwrite E}"
| RuleWrite: "⟦ ⋀Γ. Δ = Some Γ ⟹ view_function_of_inv Γ ; v ∉ fvE loc ⟧
  ⟹ Δ ⊢ {Exists v (PointsTo loc pwrite (Evar v))} Cwrite loc E {PointsTo loc pwrite E}"
| "⟦ ⋀Γ. Δ = Some Γ ⟹ x ∉ fvA (invariant Γ) ∧ view_function_of_inv Γ ; x ∉ fvE E ∪ fvE e ⟧ ⟹
  Δ ⊢ {PointsTo E π e} Cread x E {And (PointsTo E π e) (Bool (Beq (Evar x) e))}"
| RuleShare: "⟦ Γ = ⦇ view = f, abstract_view = α, saction = sact, uaction = uact, invariant = J ⦈ ; all_axioms α sact spre uact upre ;
  Some Γ ⊢ {Star P EmptyFullGuards} C {Star Q (And (PreSharedGuards (Abs_precondition spre)) (PreUniqueGuards (Abs_indexed_precondition upre)))};
  view_function_of_inv Γ ; unary J ; precise J ; wf_indexed_precondition upre ; wf_precondition spre ; x ∉ fvA J ;
  no_guard_assertion (Star P (LowView (α ∘ f) J x)) ⟧ ⟹ None ⊢ {Star P (LowView (α ∘ f) J x)} C {Star Q (LowView (α ∘ f) J x)}"
| RuleAtomicUnique: "⟦ Γ = ⦇ view = f, abstract_view = α, saction = sact, uaction = uact, invariant = J ⦈ ;
  no_guard_assertion P ; no_guard_assertion Q ;
    None ⊢ {Star P (View f J (λs. s x))} C {Star Q (View f J (λs. uact index (s x) (map_to_arg (s uarg))))} ;
    precise J ; unary J ; view_function_of_inv Γ ; x ∉ fvC C ∪ fvA P ∪ fvA Q ∪ fvA J ; uarg ∉ fvC C ; 
    l ∉ fvC C ; x ∉ fvS (λs. map_to_list (s l)) ; x ∉ fvS (λs. map_to_arg (s uarg) # map_to_list (s l)) ⟧
  ⟹ Some Γ ⊢ {Star P (UniqueGuard index (λs. map_to_list (s l)))} Catomic C {Star Q (UniqueGuard index (λs. map_to_arg (s uarg) # map_to_list (s l)))}"
| RuleAtomicShared: "⟦ Γ = ⦇ view = f, abstract_view = α, saction = sact, uaction = uact, invariant = J ⦈ ; no_guard_assertion P ; no_guard_assertion Q ;
  None ⊢ {Star P (View f J (λs. s x))} C {Star Q (View f J (λs. sact (s x) (map_to_arg (s sarg))))} ;
  precise J ; unary J ; view_function_of_inv Γ ; x ∉ fvC C ∪ fvA P ∪ fvA Q ∪ fvA J ; sarg ∉ fvC C ;
  ms ∉ fvC C ; x ∉ fvS (λs. map_to_multiset (s ms)) ; x ∉ fvS (λs. {# map_to_arg (s sarg) #} + map_to_multiset (s ms)) ⟧
  ⟹ Some Γ ⊢ {Star P (SharedGuard π (λs. map_to_multiset (s ms)))} Catomic C {Star Q (SharedGuard π (λs. {# map_to_arg (s sarg) #} + map_to_multiset (s ms)))}"
| RulePar: "⟦ Δ ⊢ {P1} C1 {Q1} ; Δ ⊢ {P2} C2 {Q2} ; disjoint (fvA P1 ∪ fvC C1 ∪ fvA Q1) (wrC C2) ;
  disjoint (fvA P2 ∪ fvC C2 ∪ fvA Q2) (wrC C1) ; ⋀Γ. Δ = Some Γ ⟹ disjoint (fvA (invariant Γ)) (wrC C2) ;
  ⋀Γ. Δ = Some Γ ⟹ disjoint (fvA (invariant Γ)) (wrC C1) ; precise P1 ∨ precise P2 ⟧
  ⟹ Δ ⊢ {Star P1 P2} Cpar C1 C2 {Star Q1 Q2}"
| RuleIf1: "⟦ Δ ⊢ {And P (Bool b)} C1 {Q} ; Δ ⊢ {And P (Bool (Bnot b))} C2 {Q} ⟧
  ⟹ Δ ⊢ {And P (Low b)} Cif b C1 C2 {Q}"
| RuleIf2: "⟦ Δ ⊢ {And P (Bool b)} C1 {Q} ; Δ ⊢ {And P (Bool (Bnot b))} C2 {Q} ; unary Q ⟧
  ⟹ Δ ⊢ {P} Cif b C1 C2 {Q}"
| RuleSeq: "⟦ Δ ⊢ {P} C1 {R} ; Δ ⊢ {R} C2 {Q} ⟧ ⟹ Δ ⊢ {P} Cseq C1 C2 {Q}"
| RuleFrame: "⟦ Δ ⊢ {P} C {Q} ; disjoint (fvA R) (wrC C) ; precise P ∨ precise R ⟧
  ⟹ Δ ⊢ {Star P R} C {Star Q R}"
| RuleCons: "⟦ Δ ⊢ {P'} C {Q'} ; entails P P' ; entails Q' Q ⟧ ⟹ Δ ⊢ {P} C {Q}"
| RuleExists: "⟦ Δ ⊢ {P} C {Q} ; x ∉ fvC C ; ⋀Γ. Δ = Some Γ ⟹ x ∉ fvA (invariant Γ) ; unambiguous P x ⟧
  ⟹ Δ ⊢ {Exists x P} C {Exists x Q}"
| RuleWhile1: "Δ ⊢ {And I (Bool b)} C {And I (Low b)} ⟹ Δ ⊢ {And I (Low b)} Cwhile b C {And I (Bool (Bnot b))}"
| RuleWhile2: "⟦ unary I ; Δ ⊢ {And I (Bool b)} C {I} ⟧ ⟹ Δ ⊢ {I} Cwhile b C {And I (Bool (Bnot b))}"

end