Theory SepAlgebra

section ‹Separation Algebra›

text ‹In this section, we formalize the concept of a separation algebra~\<^cite>‹"Calcagno2007" and "Dockins2009"›, on which our package logic is based.›

theory SepAlgebra
  imports Main
begin

type_synonym 'a property = "'a ⇒ bool"

locale sep_algebra =

  fixes plus :: "'a ⇒ 'a ⇒ 'a option" (infixl ‹⊕› 63)

  fixes core :: "'a ⇒ 'a" (‹ |_| ›)
  (* Largest duplicable part of a state *)

  assumes commutative: "a ⊕ b = b ⊕ a"
      and asso1: "a ⊕ b = Some ab ∧ b ⊕ c = Some bc ⟹ ab ⊕ c = a ⊕ bc"
      and asso2: "a ⊕ b = Some ab ∧ b ⊕ c = None ⟹ ab ⊕ c = None"

(* The core of x is the max of { p | pure p ∧ x ≥ p} *)
      and core_is_smaller: "Some x = x ⊕ |x|"
      and core_is_pure: "Some |x| = |x| ⊕ |x|"
      and core_max: "Some x = x ⊕ c ⟹ (∃r. Some |x| = c ⊕ r)"
      and core_sum: "Some c = a ⊕ b ⟹ Some |c| = |a| ⊕ |b|"

      and positivity: "a ⊕ b = Some c ⟹ Some c = c ⊕ c ⟹ Some a = a ⊕ a"
      and cancellative: "Some a = b ⊕ x ⟹ Some a = b ⊕ y ⟹ |x| = |y| ⟹ x = y"

begin

lemma asso3:
  assumes "a ⊕ b = None"
      and "b ⊕ c = Some bc"
    shows "a ⊕ bc = None"
  by (metis assms(1) assms(2) sep_algebra.asso2 sep_algebra.commutative sep_algebra_axioms)

subsection  ‹Definitions›

definition defined :: "'a ⇒ 'a ⇒ bool" (infixl ‹##› 62) where
  "a ## b ⟷ a ⊕ b ≠ None"

definition greater :: "'a ⇒ 'a ⇒ bool" (infixl ‹≽› 50) where
  "a ≽ b ⟷ (∃c. Some a = b ⊕ c)"

definition pure :: "'a ⇒ bool" where
  "pure a ⟷ Some a = a ⊕ a"

definition minus :: "'a ⇒ 'a ⇒ 'a" (infixl ‹⊖› 63)
  where "b ⊖ a = (THE_default b (λx. Some b = a ⊕ x ∧ x ≽ |b| ))"

definition add_set :: "'a set ⇒ 'a set ⇒ 'a set" (infixl ‹⊗› 60) where
  "A ⊗ B = { φ | φ a b. a ∈ A ∧ b ∈ B ∧ Some φ = a ⊕ b }"

definition greater_set :: "'a set ⇒ 'a set ⇒ bool" (infixl ‹≫› 50) where
  "A ≫ B ⟷ (∀a ∈ A. ∃b ∈ B. a ≽ b)"

definition up_closed :: "'a set ⇒ bool" where
  "up_closed A ⟷ (∀φ'. (∃φ ∈ A. φ' ≽ φ) ⟶ φ' ∈ A)"

definition equiv :: "'a set ⇒ 'a set ⇒ bool" (infixl ‹∼› 40) where
  "A ∼ B ⟷ A ≫ B ∧ B ≫ A"

definition setify :: "'a property ⇒ ('a set ⇒ bool)" where
  "setify P A ⟷ (∀x ∈ A. P x)"

definition mono_prop :: "'a property ⇒ bool" where
  "mono_prop P ⟷ (∀x y. y ≽ x ∧ P x ⟶ P y)"

definition under :: "'a set ⇒ 'a ⇒ 'a set" where
  "under A ω = { ω' | ω'. ω' ∈ A ∧ ω ≽ ω'}"

definition max_projection_prop :: "('a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool" where
  "max_projection_prop P f ⟷ (∀x. x ≽ f x ∧ P (f x) ∧
  (∀p. P p ∧ x ≽ p ⟶ f x ≽ p))"

inductive multi_plus :: "'a list ⇒ 'a ⇒ bool" where
  MPSingle: "multi_plus [a] a"
| MPConcat: "⟦ length la > 0 ; length lb > 0 ; multi_plus la a ; multi_plus lb b ; Some ω = a ⊕ b ⟧ ⟹ multi_plus (la @ lb)  ω"

fun splus :: "'a option ⇒ 'a option ⇒ 'a option" where
  "splus None _ = None"
| "splus _ None = None"
| "splus (Some a) (Some b) = a ⊕ b"



subsection ‹First lemmata›

lemma greater_equiv:
  "a ≽ b ⟷ (∃c. Some a = c ⊕ b)"
  using commutative greater_def by auto

lemma smaller_compatible:
  assumes "a' ## b"
      and "a' ≽ a"
    shows "a ## b"
  by (metis (full_types) assms(1) assms(2) asso3 commutative defined_def greater_def)

lemma bigger_sum_smaller:
  assumes "Some c = a ⊕ b"
      and "a ≽ a'"
    shows "∃b'. b' ≽ b ∧ Some c = a' ⊕ b'"
proof -
  obtain r where "Some a = a' ⊕ r" 
    using assms(2) greater_def by auto
  then obtain br where "Some br = r ⊕ b"
    by (metis assms(1) asso2 domD domIff option.discI)
  then have "Some c = a' ⊕ br" 
    by (metis ‹Some a = a' ⊕ r› assms(1) asso1)
  then show ?thesis 
    using ‹Some br = r ⊕ b› commutative greater_def by force
qed

subsubsection ‹splus›

lemma splus_develop:
  assumes "Some a = b ⊕ c"
  shows "a ⊕ d = splus (splus (Some b) (Some c)) (Some d)"
  by (metis assms splus.simps(3))

lemma splus_comm:
  "splus a b = splus b a"
  apply (cases a)
   apply (cases b)
    apply simp_all
  apply (cases b)
  by (simp_all add: commutative)

lemma splus_asso:
  "splus (splus a b) c = splus a (splus b c)"
proof (cases a)
  case None
  then show ?thesis 
    by simp
next
  case (Some a')
  then have "a = Some a'" by simp
  then show ?thesis
  proof (cases b)
    case None
    then show ?thesis by (simp add: Some)
  next
    case (Some b')
    then have "b = Some b'" by simp
    then show ?thesis
    proof (cases c)
      case None
      then show ?thesis by (simp add: splus_comm)
    next
      case (Some c')
      then have "c = Some c'" by simp
      then show ?thesis
      proof (cases "a' ⊕ b'")
        case None
        then have "a' ⊕ b' = None" by simp
        then show ?thesis
        proof (cases "b' ⊕ c'")
          case None
          then show ?thesis 
            by (simp add: Some ‹a = Some a'› ‹a' ⊕ b' = None› ‹b = Some b'›)
        next
          case (Some bc)
          then show ?thesis
            by (metis (full_types) None ‹a = Some a'› ‹b = Some b'› ‹c = Some c'› sep_algebra.asso2 sep_algebra_axioms splus.simps(2) splus.simps(3) splus_comm)
        qed
      next
        case (Some ab)
        then have "Some ab = a' ⊕ b'" by simp
        then show ?thesis
        proof (cases "b' ⊕ c'")
          case None
          then show ?thesis 
            by (metis Some ‹a = Some a'› ‹b = Some b'› ‹c = Some c'› asso2 splus.simps(2) splus.simps(3))
        next
          case (Some bc)
          then show ?thesis
            by (metis ‹Some ab = a' ⊕ b'› ‹a = Some a'› ‹b = Some b'› ‹c = Some c'› sep_algebra.asso1 sep_algebra_axioms splus.simps(3))
        qed
      qed
    qed
  qed
qed







subsubsection ‹Pure›

(* Maybe need more *)
lemma pure_stable:
  assumes "pure a"
      and "pure b"
      and "Some c = a ⊕ b"
    shows "pure c"
  by (metis assms asso1 commutative pure_def)

(* Specific to pure *)
lemma pure_smaller:
  assumes "pure a"
      and "a ≽ b"
    shows "pure b"
  by (metis assms greater_def positivity pure_def)


subsection ‹Succ is an order›

lemma succ_antisym:
  assumes "a ≽ b"
      and "b ≽ a"
    shows "a = b"
proof -
  obtain ra where "Some a = b ⊕ ra" 
    using assms(1) greater_def by auto
  obtain rb where "Some b = a ⊕ rb" 
    using assms(2) greater_def by auto
  then have "Some a = splus (Some a) (splus (Some ra) (Some rb))"
  proof -
    have "Some b = splus (Some a) (Some rb)"
      by (simp add: ‹Some b = a ⊕ rb›)
    then show ?thesis
      by (metis (full_types) ‹Some a = b ⊕ ra› sep_algebra.splus.simps(3) sep_algebra_axioms splus_asso splus_comm)
  qed
  moreover have "Some b = splus (Some b) (splus (Some ra) (Some rb))"
    by (metis ‹Some a = b ⊕ ra› ‹Some b = a ⊕ rb› sep_algebra.splus.simps(3) sep_algebra_axioms splus_asso)
  moreover have "pure ra ∧ pure rb"
  proof -
    obtain rab where "Some rab = ra ⊕ rb" 
      by (metis calculation(2) splus.elims splus.simps(3))
    then have "|a| ≽ rab" 
      by (metis calculation(1) core_max greater_def splus.simps(3))
    then have "pure rab" 
      using core_is_pure pure_def pure_smaller by blast
    moreover have "rab ≽ ra ∧ rab ≽ rb" 
      using ‹Some rab = ra ⊕ rb› greater_def greater_equiv by blast
    ultimately have "pure ra" using pure_smaller 
      by blast
    moreover have "pure rb" 
      using ‹pure rab› ‹rab ≽ ra ∧ rab ≽ rb› pure_smaller by blast
    ultimately show ?thesis 
      by blast
  qed
  ultimately show ?thesis 
    by (metis ‹Some b = a ⊕ rb› option.inject pure_def sep_algebra.splus.simps(3) sep_algebra_axioms splus_asso)
qed

lemma succ_trans:
  assumes "a ≽ b"
      and "b ≽ c"
    shows "a ≽ c"
  using assms(1) assms(2) bigger_sum_smaller greater_def by blast

lemma succ_refl:
  "a ≽ a" 
  using core_is_smaller greater_def by blast








subsection ‹Core (pure) and stabilize (stable)›

lemma max_projection_propI:
  assumes "⋀x. x ≽ f x"
      and "⋀x. P (f x)"
      and "⋀x p. P p ∧ x ≽ p ⟹ f x ≽ p"
    shows "max_projection_prop P f"
  by (simp add: assms(1) assms(2) assms(3) max_projection_prop_def)

lemma max_projection_propE:
  assumes "max_projection_prop P f"
    shows "⋀x. x ≽ f x"
      and "⋀x. P (f x)"
      and "⋀x p. P p ∧ x ≽ p ⟹ f x ≽ p"
  using assms max_projection_prop_def by auto

lemma max_projection_prop_pure_core:
  "max_projection_prop pure core"
proof (rule max_projection_propI)
  fix x
  show "x ≽ |x|" 
    using core_is_smaller greater_equiv by blast
  show "pure |x|" 
    by (simp add: core_is_pure pure_def)
  show "⋀p. pure p ∧ x ≽ p ⟹ |x| ≽ p"
  proof -
    fix p assume "pure p ∧ x ≽ p"
    then obtain r where "Some x = p ⊕ r" 
      using greater_def by blast
    then show "|x| ≽ p"
      by (metis ‹pure p ∧ x ≽ p› asso1 commutative core_max greater_equiv pure_def)
  qed
qed

lemma mpp_smaller:
  assumes "max_projection_prop P f"
  shows "x ≽ f x"
  using assms max_projection_propE(1) by auto

lemma mpp_compatible:
  assumes "max_projection_prop P f"
      and "a ## b"
    shows "f a ## f b"
  by (metis (mono_tags, opaque_lifting) assms(1) assms(2) commutative defined_def max_projection_prop_def smaller_compatible)



lemma mpp_prop:
  assumes "max_projection_prop P f"
  shows "P (f x)"
  by (simp add: assms max_projection_propE(2))


lemma mppI:
  assumes "max_projection_prop P f"
      and "a ≽ x"
      and "P x"
      and "x ≽ f a"
    shows "x = f a"
proof -
  have "f a ≽ x" 
    using assms max_projection_propE(3) by auto
  then show ?thesis 
    by (simp add: assms(4) succ_antisym)
qed

lemma mpp_invo:
  assumes "max_projection_prop P f"
  shows "f (f x) = f x"
  using assms max_projection_prop_def succ_antisym by auto

lemma mpp_mono:
  assumes "max_projection_prop P f"
      and "a ≽ b"
    shows "f a ≽ f b"
  by (metis assms max_projection_prop_def succ_trans)


subsection ‹Subtraction›

lemma addition_bigger:
  assumes "a' ≽ a"
      and "Some x' = a' ⊕ b"
      and "Some x = a ⊕ b"
    shows "x' ≽ x"
  by (metis assms asso1 bigger_sum_smaller greater_def)


lemma smaller_than_core:
  assumes "y ≽ x"
      and "Some z = x ⊕ |y|"
    shows "|z| = |y|"
proof -
  have "Some |z| = |x| ⊕ |y|"
    using assms(2) core_sum max_projection_prop_pure_core mpp_invo by fastforce
  then have "Some |z| = |x| ⊕ |y|"
    by simp
  moreover have "|z| ≽ |y|" 
    using calculation greater_equiv by blast
  ultimately show ?thesis 
    by (meson addition_bigger assms(1) assms(2) core_is_smaller core_sum greater_def succ_antisym)
qed

lemma extract_core:
  assumes "Some b = a ⊕ x ∧ x ≽ |b|"
  shows "|x| = |b|"
proof -
  obtain r where "Some x = r ⊕ |b|"
    using assms greater_equiv by auto
  show ?thesis
  proof (rule smaller_than_core)
    show "Some x = r ⊕ |b|"
      using ‹Some x = r ⊕ |b|› by auto
    show "b ≽ r"
      by (metis ‹Some x = r ⊕ |b|› assms commutative greater_def succ_trans)
  qed
qed


lemma minus_unique:
  assumes "Some b = a ⊕ x ∧ x ≽ |b|"
      and "Some b = a ⊕ y ∧ y ≽ |b|"
    shows "x = y"
proof -
  have "|x| = |b|"
    using assms(1) extract_core by blast
  moreover have "|y| = |b|"
    using assms(2) extract_core by blast
  ultimately show ?thesis
    using assms(1) assms(2) cancellative by auto
qed

lemma minus_exists:
  assumes "b ≽ a"
  shows "∃x. Some b = a ⊕ x ∧ x ≽ |b|"
  using assms bigger_sum_smaller core_is_smaller by blast

lemma minus_equiv_def:
  assumes "b ≽ a"
    shows "Some b = a ⊕ (b ⊖ a) ∧ (b ⊖ a) ≽ |b|"
proof -
  let ?x = "THE_default b (λx. Some b = a ⊕ x ∧ x ≽ |b| )"
  have "(λx. Some b = a ⊕ x ∧ x ≽ |b| ) ?x"
  proof (rule THE_defaultI')
    show "∃!x. Some b = a ⊕ x ∧ x ≽ |b|"
      using assms local.minus_unique minus_exists by blast
  qed
  then show ?thesis by (metis minus_def)
qed

lemma minus_default:
  assumes "¬ b ≽ a"
  shows "b ⊖ a = b"
  using THE_default_none assms greater_def minus_def by fastforce

lemma minusI:
  assumes "Some b = a ⊕ x"
      and "x ≽ |b|"
    shows "x = b ⊖ a"  
  using assms(1) assms(2) greater_def local.minus_unique minus_equiv_def by blast

lemma minus_core:
  "|a ⊖ b| = |a|"
proof (cases "a ≽ b")
  case True
  then have "Some a = b ⊕ (a ⊖ b) ∧ a ⊖ b ≽ |a|"
    using minus_equiv_def by auto
  then show ?thesis
    using extract_core by blast
next
  case False
  then show ?thesis by (simp add: minus_default)
qed


lemma minus_core_weaker:
  "|a ⊖ b| = |a| ⊖ |b|"
proof (cases "a ≽ b")
  case True
  then show ?thesis 
    by (metis greater_equiv max_projection_prop_pure_core minus_core minus_default minus_equiv_def mpp_invo succ_antisym)
next
  case False
  then show ?thesis
    by (metis greater_equiv max_projection_prop_pure_core minus_default minus_equiv_def mpp_invo succ_antisym)
qed

lemma minus_equiv_def_any_elem:
  assumes "Some x = a ⊕ b"
  shows "Some (x ⊖ a) = b ⊕ |x|"
proof -
  obtain r where "Some r = b ⊕ |x|" 
    by (metis assms core_is_smaller domD domIff option.simps(3) sep_algebra.asso2 sep_algebra_axioms)
  have "r = x ⊖ a"
  proof (rule minusI)
    show "Some x = a ⊕ r" 
      by (metis ‹Some r = b ⊕ |x|› assms asso1 core_is_smaller)
    moreover show "r ≽ |x|"
      using ‹Some r = b ⊕ |x|› greater_equiv by blast
  qed
  then show ?thesis 
    using ‹Some r = b ⊕ |x|› by blast
qed

lemma minus_bigger:
  assumes "Some x = a ⊕ b"
  shows "x ⊖ a ≽ b"
  using assms greater_def minus_equiv_def_any_elem by blast

lemma minus_smaller:
  assumes "x ≽ a"
  shows "x ≽ x ⊖ a"
  using assms greater_equiv minus_equiv_def by blast

lemma minus_sum:
  assumes "Some a = b ⊕ c"
      and "x ≽ a"
    shows "x ⊖ a = (x ⊖ b) ⊖ c"
proof (rule minusI)
  obtain r where "Some r = c ⊕ (x ⊖ a)"
    by (metis assms(1) assms(2) asso2 minus_equiv_def option.exhaust_sel)
  have "r = (x ⊖ b)"
  proof (rule minusI)
    show "Some x = b ⊕ r" 
      by (metis ‹Some r = c ⊕ (x ⊖ a)› assms(1) assms(2) asso1 minus_equiv_def)
    moreover show "r ≽ |x|" 
      by (meson ‹Some r = c ⊕ (x ⊖ a)› assms(2) greater_equiv sep_algebra.minus_equiv_def sep_algebra_axioms succ_trans)
  qed
  then show "Some (x ⊖ b) = c ⊕ (x ⊖ a)" 
    using ‹Some r = c ⊕ (x ⊖ a)› by blast
  moreover show "x ⊖ a ≽ |x ⊖ b|"
    by (simp add: assms(2) minus_core minus_equiv_def)
qed

lemma smaller_compatible_core:
  assumes "y ≽ x"
  shows "x ## |y|"
  by (metis assms asso2 core_is_smaller defined_def greater_equiv option.discI)

lemma smaller_pure_sum_smaller:
  assumes "y ≽ a"
      and "y ≽ b"
      and "Some x = a ⊕ b"
      and "pure b"
    shows "y ≽ x"
proof -
  obtain r where "Some y = r ⊕ b" "r ≽ a"
    by (metis assms(1) assms(2) assms(4) asso1 greater_equiv pure_def)
  then show ?thesis
    using addition_bigger assms(3) by blast
qed

lemma greater_minus_trans:
  assumes "y ≽ x"
      and "x ≽ a"
    shows "y ⊖ a ≽ x ⊖ a"
proof -
  obtain r where "Some y = x ⊕ r" 
    using assms(1) greater_def by blast
  then obtain ra where "Some x = a ⊕ ra" 
    using assms(2) greater_def by blast
  then have "Some (x ⊖ a) = ra ⊕ |x|"
    by (simp add: minus_equiv_def_any_elem)
  then obtain yy where "Some yy = (x ⊖ a) ⊕ r" 
    by (metis (full_types) ‹Some y = x ⊕ r› assms(2) asso3 commutative minus_equiv_def not_Some_eq)
  then obtain "Some x = a ⊕ (x ⊖ a)" "x ⊖ a ≽  |x|"
    by (simp_all add: assms(2) sep_algebra.minus_equiv_def sep_algebra_axioms)
  then obtain y' where "Some y' = a ⊕ yy"
    using ‹Some y = x ⊕ r› ‹Some yy = x ⊖ a ⊕ r› asso1
    by metis
  moreover have "y ≽ y'"
    by (metis ‹Some x = a ⊕ (x ⊖ a)› ‹Some y = x ⊕ r› ‹Some yy = x ⊖ a ⊕ r› asso1 calculation option.inject succ_refl)
  moreover obtain x' where "Some x' = (x ⊖ a) ⊕ a" 
    using assms(2) commutative minus_equiv_def by fastforce
  then have "y ≽ x'" 
    by (metis assms(1) assms(2) commutative minus_equiv_def option.sel)
  moreover have "x' ≽ x ⊖ a" 
    using ‹Some x' = x ⊖ a ⊕ a› greater_def by auto
  ultimately show ?thesis 
    using ‹Some x' = x ⊖ a ⊕ a› ‹Some y = x ⊕ r› assms(2) asso1 commutative greater_equiv minus_bigger minus_equiv_def option.sel sep_algebra.succ_trans sep_algebra_axioms
  proof -
    have f1: "Some y' = a ⊕ yy"
      by (simp add: ‹Some y' = a ⊕ yy› commutative)
    then have "y = y'"
      by (metis ‹Some y = x ⊕ r› ‹Some yy = x ⊖ a ⊕ r› ‹x ≽ a› asso1 minus_equiv_def option.sel)
    then show ?thesis
      using f1 by (metis (no_types) ‹Some yy = x ⊖ a ⊕ r› commutative greater_equiv minus_bigger sep_algebra.succ_trans sep_algebra_axioms)
  qed
qed




lemma minus_and_plus:
  assumes "Some ω' = ω ⊕ r"
      and "ω ≽ a"
    shows "Some (ω' ⊖ a) = (ω ⊖ a) ⊕ r"
proof -
  have "ω ≽ ω ⊖ a" 
    by (simp add: assms(2) minus_smaller)
  then have "(ω ⊖ a) ## r" 
    by (metis (full_types) assms(1) defined_def option.discI sep_algebra.smaller_compatible sep_algebra_axioms)
  then obtain x where "Some x = (ω ⊖ a) ⊕ r"
    using defined_def by auto
  then have "Some ω' = a ⊕ x ∧ x ≽ |ω'|"
    by (metis (no_types, lifting) assms asso1 core_sum max_projection_prop_pure_core minus_core minus_equiv_def mpp_smaller option.inject)
  then have "x = ω' ⊖ a" 
    by (simp add: minusI)
  then show ?thesis 
    using ‹Some x = ω ⊖ a ⊕ r› by blast
qed









subsection ‹Lifting the algebra to sets of states›

lemma add_set_commm:
  "A ⊗ B = B ⊗ A"
proof
  show "A ⊗ B ⊆ B ⊗ A"
    using add_set_def sep_algebra.commutative sep_algebra_axioms by fastforce
  show "B ⊗ A ⊆ A ⊗ B"
    using add_set_def commutative by fastforce
qed

lemma x_elem_set_product:
  "x ∈ A ⊗ B ⟷ (∃a b. a ∈ A ∧ b ∈ B ∧ Some x = a ⊕ b)"
  using sep_algebra.add_set_def sep_algebra_axioms by fastforce

lemma x_elem_set_product_splus:
  "x ∈ A ⊗ B ⟷ (∃a b. a ∈ A ∧ b ∈ B ∧ Some x = splus (Some a) (Some b))"
  using sep_algebra.add_set_def sep_algebra_axioms by fastforce

lemma add_set_asso:
  "(A ⊗ B) ⊗ C = A ⊗ (B ⊗ C)" (is "?A = ?B")
proof -
  have "?A ⊆ ?B"
  proof (rule subsetI)
    fix x assume "x ∈ ?A"
    then obtain ab c where "Some x = ab ⊕ c" "ab ∈ A ⊗ B" "c ∈ C"
      using x_elem_set_product by auto
    then obtain a b where "Some ab = a ⊕ b" "a ∈ A" "b ∈ B"
      using x_elem_set_product by auto
    then obtain bc where "Some bc = b ⊕ c" 
      by (metis ‹Some x = ab ⊕ c› asso2 option.exhaust)
    then show "x ∈ ?B" 
      by (metis ‹Some ab = a ⊕ b› ‹Some x = ab ⊕ c› ‹a ∈ A› ‹b ∈ B› ‹c ∈ C› asso1 x_elem_set_product)
  qed
  moreover have "?B ⊆ ?A"
  proof (rule subsetI)
    fix x assume "x ∈ ?B"
    then obtain a bc where "Some x = a ⊕ bc" "a ∈ A" "bc ∈ B ⊗ C"
      using x_elem_set_product by auto
    then obtain b c where "Some bc = b ⊕ c" "c ∈ C" "b ∈ B"
      using x_elem_set_product by auto
    then obtain ab where "Some ab = a ⊕ b"
      by (metis ‹Some x = a ⊕ bc› asso3 option.collapse)
    then show "x ∈ ?A"
      by (metis ‹Some bc = b ⊕ c› ‹Some x = a ⊕ bc› ‹a ∈ A› ‹b ∈ B› ‹c ∈ C› asso1 x_elem_set_product)
  qed
  ultimately show ?thesis by blast
qed

lemma up_closedI:
  assumes "⋀φ' φ. (φ' :: 'a) ≽ φ ∧ φ ∈ A ⟹ φ' ∈ A"
  shows "up_closed A"
  using assms up_closed_def by blast

lemma up_closed_plus_UNIV:
  "up_closed (A ⊗ UNIV)"
proof (rule up_closedI)
  fix φ φ'
  assume asm: "φ' ≽ φ ∧ φ ∈ A ⊗ UNIV"
  then obtain r a b where "Some φ' = φ ⊕ r" "Some φ = a ⊕ b" "a ∈ A"
    using greater_def x_elem_set_product by auto
  then obtain br where "Some br = b ⊕ r" 
    by (metis asso2 option.exhaust_sel)
  then have "Some φ' = a ⊕ br" 
    by (metis ‹Some φ = a ⊕ b› ‹Some φ' = φ ⊕ r› splus.simps(3) splus_asso)
  then show "φ' ∈ A ⊗ UNIV" 
    using ‹a ∈ A› x_elem_set_product by auto
qed


lemma succ_set_trans:
  assumes "A ≫ B"
      and "B ≫ C"
    shows "A ≫ C"
  by (meson assms(1) assms(2) greater_set_def succ_trans)

lemma greater_setI:
  assumes "⋀a. a ∈ A ⟹ (∃b ∈ B. a ≽ b)"
    shows "A ≫ B"
  by (simp add: assms greater_set_def)  

lemma bigger_set:
  assumes "A' ≫ A"
  shows "A' ⊗ B ≫ A ⊗ B"
proof (rule greater_setI)
  fix x assume "x ∈ A' ⊗ B"
  then obtain a' b where "Some x = a' ⊕ b" "a' ∈ A'" "b ∈ B"
    using x_elem_set_product by auto
  then obtain a where "a' ≽ a" "a ∈ A"
    using assms greater_set_def by blast
  then obtain ab where "Some ab = a ⊕ b"
    by (metis ‹Some x = a' ⊕ b› asso2 domD domIff greater_equiv)
  then show "∃ab∈A ⊗ B. x ≽ ab"
    using ‹Some x = a' ⊕ b› ‹a ∈ A› ‹a' ≽ a› ‹b ∈ B› addition_bigger x_elem_set_product by blast
qed

lemma bigger_singleton:
  assumes "φ' ≽ φ"
  shows "{φ'} ≫ {φ}"
  by (simp add: assms greater_set_def)

lemma add_set_elem:
  "φ ∈ A ⊗ B ⟷ (∃a b. Some φ = a ⊕ b ∧ a ∈ A ∧ b ∈ B)"
  using add_set_def by auto

lemma up_closed_sum:
  assumes "up_closed A"
    shows "up_closed (A ⊗ B)"
proof (rule up_closedI)
  fix φ' φ assume asm: "φ' ≽ φ ∧ φ ∈ A ⊗ B"
  then obtain a b where "a ∈ A" "b ∈ B" "Some φ = a ⊕ b" 
    using add_set_elem by auto
  moreover obtain r where "Some φ' = φ ⊕ r" 
    using asm greater_def by blast
  then obtain ar where "Some ar = a ⊕ r" 
    by (metis asso2 calculation(3) commutative option.exhaust_sel option.simps(3))
  then have "ar ∈ A" 
    by (meson assms calculation(1) greater_def sep_algebra.up_closed_def sep_algebra_axioms)
  then show "φ' ∈ A ⊗ B" 
    by (metis ‹Some φ' = φ ⊕ r› ‹Some ar = a ⊕ r› add_set_elem asso1 calculation(2) calculation(3) commutative)
qed

lemma up_closed_bigger_subset:
  assumes "up_closed B"
      and "A ≫ B"
    shows "A ⊆ B"
  by (meson assms(1) assms(2) greater_set_def sep_algebra.up_closed_def sep_algebra_axioms subsetI)

lemma up_close_equiv:
  assumes "up_closed A"
      and "up_closed B"
    shows "A ∼ B ⟷ A = B"
proof -
  have "A ∼ B ⟷ A ≫ B ∧ B ≫ A" 
    using local.equiv_def by auto
  also have "... ⟷ A ⊆ B ∧ B ⊆ A" 
    by (metis assms(1) assms(2) greater_set_def set_eq_subset succ_refl up_closed_bigger_subset)
  ultimately show ?thesis 
    by blast
qed

lemma equiv_stable_sum:
  assumes "A ∼ B"
  shows "A ⊗ C ∼ B ⊗ C"
  using assms bigger_set local.equiv_def by auto

lemma equiv_up_closed_subset:
  assumes "up_closed A"
      and "equiv B C"
    shows "B ⊆ A ⟷ C ⊆ A" (is "?B ⟷ ?C")
proof -
  have "?B ⟹ ?C"
    by (meson greater_set_def up_closed_def equiv_def assms(1) assms(2) subsetD subsetI)
  moreover have "?C ⟹ ?B"
    by (meson greater_set_def up_closed_def equiv_def assms(1) assms(2) subsetD subsetI)
  ultimately show ?thesis by blast
qed

lemma mono_propI:
  assumes "⋀x y. y ≽ x ∧ P x ⟹ P y"
  shows "mono_prop P"
  using assms mono_prop_def by blast

lemma mono_prop_set:
  assumes "A ≫ B"
      and "setify P B"
      and "mono_prop P"
    shows "setify P A"
  using assms(1) assms(2) assms(3) greater_set_def local.setify_def mono_prop_def by auto

lemma mono_prop_set_equiv:
  assumes "mono_prop P"
      and "equiv A B"
    shows "setify P A ⟷ setify P B"
  by (meson assms(1) assms(2) local.equiv_def sep_algebra.mono_prop_set sep_algebra_axioms)

lemma setify_sum:
  "setify P (A ⊗ B) ⟷ (∀x ∈ A. setify P ({x} ⊗ B))" (is "?A ⟷ ?B")
proof -
  have "?A ⟹ ?B" 
    using local.setify_def sep_algebra.add_set_elem sep_algebra_axioms singletonD by fastforce
  moreover have "?B ⟹ ?A" 
    using add_set_elem local.setify_def by fastforce
  ultimately show ?thesis by blast
qed

lemma setify_sum_image:
  "setify P ((Set.image f A) ⊗ B) ⟷ (∀x ∈ A. setify P ({f x} ⊗ B))"
proof
  show "setify P (f ` A ⊗ B) ⟹ ∀x∈A. setify P ({f x} ⊗ B)"
    by (meson rev_image_eqI sep_algebra.setify_sum sep_algebra_axioms)
  show "∀x∈A. setify P ({f x} ⊗ B) ⟹ setify P (f ` A ⊗ B)"
    by (metis (mono_tags, lifting) image_iff sep_algebra.setify_sum sep_algebra_axioms)
qed

lemma equivI:
  assumes "A ≫ B"
    and "B ≫ A"
    shows "equiv A B"
  by (simp add: assms(1) assms(2) local.equiv_def)

lemma sub_bigger:
  assumes "A ⊆ B"
  shows "A ≫ B" 
  by (meson assms greater_set_def in_mono succ_refl)

lemma larger_set_refl:
  "A ≫ A"
  by (simp add: sub_bigger)


definition upper_closure where
  "upper_closure A = { φ' |φ' φ. φ' ≽ φ ∧ φ ∈ A }"



lemma upper_closure_up_closed:
  "up_closed (upper_closure A)"
proof (rule up_closedI)
  fix φ' φ
  assume asm0: "φ' ≽ φ ∧ φ ∈ upper_closure A"
  then obtain a where "a ∈ A ∧ φ ≽ a"
    using sep_algebra.upper_closure_def sep_algebra_axioms by fastforce
  then have "φ' ≽ a"
    using asm0 succ_trans by blast
  then show "φ' ∈ upper_closure A"
    using ‹a ∈ A ∧ φ ≽ a› upper_closure_def by auto
qed


subsection ‹Addition of more than two states›

lemma multi_decompose:
  assumes "multi_plus l ω"
    shows "length l ≥ 2 ⟹ (∃a b la lb. l = la @ lb ∧ length la > 0 ∧ length lb > 0 ∧ multi_plus la a ∧ multi_plus lb b ∧ Some ω = a ⊕ b)"
  using assms
  apply (rule multi_plus.cases)
  by auto[2]



lemma multi_take_drop:
  assumes "multi_plus l ω"
      and "length l ≥ 2"
    shows "∃n a b. n > 0 ∧ n < length l ∧ multi_plus (take n l) a ∧ multi_plus (drop n l) b ∧ Some ω = a ⊕ b"
proof -
  obtain a b la lb where asm0: "l = la @ lb ∧ length la > 0 ∧ length lb > 0 ∧ multi_plus la a ∧ multi_plus lb b ∧ Some ω = a ⊕ b"
    using assms(1) assms(2) multi_decompose by blast
  let ?n = "length la"
  have "la = take ?n l"
    by (simp add: asm0)
  moreover have "lb = drop ?n l" 
    by (simp add: asm0)
  ultimately show ?thesis 
    by (metis asm0 length_drop zero_less_diff)
qed

lemma multi_plus_single:
  assumes "multi_plus [v] a"
  shows "a = v"
  using assms
  apply (cases)
  apply simp
  by (metis (no_types, lifting) Nil_is_append_conv butlast.simps(2) butlast_append length_greater_0_conv)

lemma multi_plus_two:
  assumes "length l ≥ 2"
  shows "multi_plus l ω ⟷ (∃a b la lb. l = (la @ lb) ∧ length la > 0 ∧ length lb > 0 ∧ multi_plus la a ∧ multi_plus lb b ∧ Some ω = a ⊕ b)" (is "?A ⟷ ?B")
  by (meson MPConcat assms multi_decompose)

lemma multi_plus_head_tail:
  "length l ≤ n ∧ length l ≥ 2 ⟶ (multi_plus l ω ⟷ (∃r. Some ω = (List.hd l) ⊕ r ∧ multi_plus (List.tl l) r))"
proof (induction n arbitrary: l ω)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then have IH: "⋀(l :: 'a list) ω. length l ≤ n ∧ length l ≥ 2 ⟶ multi_plus l ω = (∃r. Some ω = hd l ⊕ r ∧ multi_plus (tl l) r)"
    by blast
  then show ?case
  proof (cases "n = 0")
    case True
    then have "n = 0" by simp
    then show ?thesis by linarith
  next
    case False
    then have "length (l :: 'a list) ≥ 2 ∧ length l ≤ n + 1 ⟹ multi_plus l ω ⟷ (∃r. Some ω = hd l ⊕ r ∧ multi_plus (tl l) r)"
      (is "length l ≥ 2  ∧ length l ≤ n + 1 ⟹ ?A ⟷ ?B")
    proof -
      assume asm: "length (l :: 'a list) ≥ 2 ∧ length l ≤ n + 1"
      have "?B ⟹ ?A"
      proof -
        assume "?B"
        then obtain r where "Some ω = hd l ⊕ r ∧ multi_plus (tl l) r" by blast
        then have "multi_plus [hd l] (hd l)" 
          using MPSingle by blast
        moreover have "[hd l] @ (tl l) = l" 
          by (metis Suc_le_length_iff asm append_Cons list.collapse list.simps(3) numeral_2_eq_2 self_append_conv2)
        ultimately show ?A 
          by (metis (no_types, lifting) MPConcat Suc_1 Suc_le_mono asm ‹Some ω = hd l ⊕ r ∧ multi_plus (tl l) r› append_Nil2 length_Cons length_greater_0_conv list.size(3) not_one_le_zero zero_less_Suc)
      qed
      moreover have "?A ⟹ ?B"
      proof -
        assume ?A
        then obtain la lb a b where "l = la @ lb" "length la > 0" "length lb > 0" "multi_plus la a" "multi_plus lb b" "Some ω = a ⊕ b"
          using asm multi_decompose by blast
        then have r0: "length la ≤ n ∧ length la ≥ 2 ⟶ multi_plus la a = (∃r. Some a = hd la ⊕ r ∧ multi_plus (tl la) r)"
          using IH by blast
        then show ?B
        proof (cases "length la ≥ 2")
          case True
          then obtain ra where "Some a = (hd la) ⊕ ra" "multi_plus (tl la) ra"
            by (metis Suc_eq_plus1 ‹0 < length lb› ‹l = la @ lb› r0 ‹multi_plus la a› append_eq_conv_conj asm drop_eq_Nil le_add1 le_less_trans length_append length_greater_0_conv less_Suc_eq_le order.not_eq_order_implies_strict)
          moreover obtain rab where "Some rab = ra ⊕ b"
            by (metis ‹Some ω = a ⊕ b› calculation(1) asso2 option.exhaust_sel)
          then have "multi_plus ((tl la) @ lb) rab" 
            by (metis (no_types, lifting) Nil_is_append_conv ‹multi_plus lb b› calculation(2) length_greater_0_conv list.simps(3) multi_plus.cases sep_algebra.MPConcat sep_algebra_axioms)
          moreover have "Some ω = hd la ⊕ rab" 
            by (metis ‹Some ω = a ⊕ b› ‹Some rab = ra ⊕ b› asso1 calculation(1))
          ultimately show ?B 
            using ‹0 < length la› ‹l = la @ lb› by auto
        next
          case False
          then have "length la = 1" 
            using ‹0 < length la› by linarith
          then have "la = [a]"
            by (metis Nitpick.size_list_simp(2) One_nat_def Suc_le_length_iff ‹multi_plus la a› diff_Suc_1 le_numeral_extra(4) length_0_conv list.sel(3) sep_algebra.multi_plus_single sep_algebra_axioms)
          then show ?thesis 
            using ‹Some ω = a ⊕ b› ‹l = la @ lb› ‹multi_plus lb b› by auto
        qed
      qed
      then show ?thesis using calculation by blast
    qed
    then show ?thesis by (metis (no_types, lifting) Suc_eq_plus1)
  qed
qed

lemma not_multi_plus_empty:
  "¬ multi_plus [] ω"
  by (metis Nil_is_append_conv length_greater_0_conv list.simps(3) sep_algebra.multi_plus.simps sep_algebra_axioms)

lemma multi_plus_deter:
  "length l ≤ n ⟹ multi_plus l ω ⟹ multi_plus l ω' ⟹ ω = ω'"
proof (induction n arbitrary: l ω ω')
  case 0
  then show ?case 
    using multi_plus.cases by auto
next
  case (Suc n)
  then show ?case
  proof (cases "length l ≥ 2")
    case True
    then obtain r where "Some ω = (List.hd l) ⊕ r ∧ multi_plus (List.tl l) r"
      using Suc.prems(2) multi_plus_head_tail by blast
    moreover obtain r' where "Some ω' = (List.hd l) ⊕ r' ∧ multi_plus (List.tl l) r'"
      using Suc.prems(3) True multi_plus_head_tail by blast
    ultimately have "r = r'" 
      by (metis Suc.IH Suc.prems(1) drop_Suc drop_eq_Nil)
    then show ?thesis 
      by (metis ‹Some ω = hd l ⊕ r ∧ multi_plus (tl l) r› ‹Some ω' = hd l ⊕ r' ∧ multi_plus (tl l) r'› option.inject)
  next
    case False
    then have "length l ≤ 1" 
      by simp
    then show ?thesis
    proof (cases "length l = 0")
      case True
      then show ?thesis
        using Suc.prems(2) sep_algebra.not_multi_plus_empty sep_algebra_axioms by fastforce
    next
      case False
      then show ?thesis 
        by (metis One_nat_def Suc.prems(2) Suc.prems(3) Suc_length_conv ‹length l ≤ 1› le_SucE le_zero_eq length_greater_0_conv less_numeral_extra(3) sep_algebra.multi_plus_single sep_algebra_axioms)
    qed      
  qed
qed

lemma multi_plus_implies_multi_plus_of_drop:
  assumes "multi_plus l ω"
      and "n < length l"
    shows "∃a. multi_plus (drop n l) a ∧ ω ≽ a"
  using assms
proof (induction n arbitrary: l ω)
  case 0
  then show ?case using succ_refl by fastforce
next
  case (Suc n)
  then have "length l ≥ 2" 
    by linarith
  then obtain r where "Some ω = (List.hd l) ⊕ r ∧ multi_plus (List.tl l) r" 
    using Suc.prems(1) multi_plus_head_tail by blast
  then obtain a where "multi_plus (drop n (List.tl l)) a ∧ r ≽ a" 
    using Suc.IH Suc.prems(2) by fastforce
  then show ?case 
    by (metis ‹Some ω = hd l ⊕ r ∧ multi_plus (tl l) r› bigger_sum_smaller commutative drop_Suc greater_def)
qed

lemma multi_plus_bigger_than_head:
  assumes "length l > 0"
      and "multi_plus l ω"
    shows "ω ≽ List.hd l"
proof (cases "length l ≥ 2")
  case True
  then obtain r where "Some ω = (List.hd l) ⊕ r ∧ multi_plus (List.tl l) r" 
    using assms(1) assms(2) multi_plus_head_tail by blast
  then show ?thesis 
    using greater_def by blast
next
  case False
  then show ?thesis
    by (metis Cons_nth_drop_Suc MPSingle assms(1) assms(2) drop_0 drop_eq_Nil hd_conv_nth length_greater_0_conv not_less_eq_eq numeral_2_eq_2 sep_algebra.multi_plus_deter sep_algebra_axioms succ_refl)
qed

lemma multi_plus_bigger:
  assumes "i < length l"
      and "multi_plus l ω"
    shows "ω ≽ (l ! i)"
proof -
  obtain a where "multi_plus (drop i l) a ∧ ω ≽ a"
    using assms(1) assms(2) multi_plus_implies_multi_plus_of_drop order.strict_trans by blast
  moreover have "List.hd (drop i l) = l ! i" 
    by (simp add: assms(1) hd_drop_conv_nth)
  then show ?thesis
    by (metis (no_types, lifting) succ_trans assms(1) assms(2) drop_eq_Nil leD length_greater_0_conv multi_plus_bigger_than_head multi_plus_implies_multi_plus_of_drop)
qed


lemma sum_then_singleton:
  "Some a = b ⊕ c ⟷ {a} = {b} ⊗ {c}" (is "?A ⟷ ?B")
proof -
  have "?A ⟹ ?B"
  proof -
    assume ?A
    then have "{a} ⊆ {b} ⊗ {c}"
      using add_set_elem by auto
    moreover have "{b} ⊗ {c} ⊆ {a}"
    proof (rule subsetI)
      fix x assume "x ∈ {b} ⊗ {c}"
      then show "x ∈ {a}"
        by (metis ‹Some a = b ⊕ c› option.sel sep_algebra.add_set_elem sep_algebra_axioms singleton_iff)
    qed
    ultimately show ?thesis by blast
  qed
  moreover have "?B ⟹ ?A" 
    using add_set_elem by auto
  ultimately show ?thesis by blast
qed

lemma empty_set_sum:
  "{} ⊗ A = {}" 
  by (simp add: add_set_def)


end

end