# 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)

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|"
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)"

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
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›

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
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|"
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"
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"
then show ?thesis
using ‹Some x = ω ⊖ a ⊕ r› by blast
qed

subsection ‹Lifting the algebra to sets of states›

"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"
qed

lemma x_elem_set_product:
"x ∈ A ⊗ B ⟷ (∃a b. a ∈ A ∧ b ∈ B ∧ Some x = a ⊕ b)"

lemma x_elem_set_product_splus:
"x ∈ A ⊗ B ⟷ (∃a b. a ∈ A ∧ b ∈ B ∧ Some x = splus (Some a) (Some b))"

"(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"

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 "{φ'} ≫ {φ}"

"φ ∈ A ⊗ B ⟷ (∃a b. Some φ = a ⊕ b ∧ a ∈ A ∧ b ∈ B)"

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"
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"
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"

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"
moreover have "lb = drop ?n l"
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)

"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"
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"
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

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"
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}"
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"