Theory Phi_BI.Algebras

theory Algebras
  imports
    "HOL-Library.Product_Plus"
    "HOL-Library.Finite_Map" HOL.Rat "Phi_Document.Base"
begin

setup ‹
   Attrib.setup \<^binding>‹locale_intro› (Scan.succeed Locale.intro_add) ""
#> Attrib.setup \<^binding>‹locale_witness› (Scan.succeed Locale.witness_add) ""
› (*TODO: move this*)

(*TODO: do not add ‹locale_intro› everywhere, the performance of locale_intro_tactic is bad.
  They do not use an indexing structure. The Locale package of Isabelle is not that good. *)

section ‹Algebra Structures›

subsection ‹Preliminary Structures›

subsubsection ‹Homomorphism-like›

locale homo_one =
  fixes ψ :: " 'a::one ⇒ 'b::one "
  assumes homo_one[iff]: "ψ 1 = 1"
begin

declare homo_one_axioms[simp]

end

locale simple_homo_mul =
  fixes ψ :: ‹ 'a::one ⇒ 'b::one ›
    and D :: ‹ 'a set › ― ‹The domain is still required. For example, consider the homomorphism
                            from mult-element algebra to single element algebra,
                            the homomorphism cannot be simple unless the domain of the homomorphism
                            is limited to {1}.›
  assumes kernel_is_1[iff]: ‹x ∈ D ⟹ ψ x = 1 ⟷ x = 1›
      and simple_homo_mul_dom[simp]: ‹1 ∈ D›
begin

sublocale homo_one by (standard, insert simple_homo_mul_dom, blast)

end

lemma simple_homo_mul_sub_dom:
  ‹ D' ⊆ D ∧ 1 ∈ D'
⟹ simple_homo_mul ψ D
⟹ simple_homo_mul ψ D' ›
  unfolding simple_homo_mul_def
  by clarsimp blast

locale homo_zero =
  fixes φ :: ‹ 'a::zero ⇒ 'b::zero ›
  assumes homo_zero[iff]: ‹φ 0 = 0›

locale homo_mult =
  fixes φ :: " 'a::times ⇒ 'b::times "
  assumes homo_mult: "φ (x * y) = φ x * φ y"

(*lemma homo_mult:
  ‹homo_mult φ ⟷ (φ 1 = 1) ∧ (∀ x y. φ (x * y) = φ x * φ y)›
  unfolding homo_mult_def homo_mult_axioms_def homo_one_def .. *)

(*
locale mult_strip_011 = ― ‹it is an orthogonal property›
  fixes ψ :: " 'a::times ⇒ 'b::times "
  assumes mult_strip_011: ‹a * ψ b = ψ c ⟷ (∃a'. a = ψ a' ∧ a' * b = c)›
*)

locale homo_add =
  fixes φ :: ‹ 'a::plus ⇒ 'b::plus ›
  assumes homo_add: ‹φ (x + y) = φ x + φ y›


subsubsection ‹Group-like›

class mult_1 = times + one +
  assumes mult_1_left [simp]: "1 * x = x"
      and mult_1_right[simp]: "x * 1 = x"

subclass (in monoid_mult) mult_1
  by (standard; insert local.mult_1_left local.mult_1_right; blast)

(* TODO
class add_left_neutral = plus +
  fixes left_neutral_0 :: ‹'a ⇒ 'a› ("𝟬⇩L")
  assumes ‹𝟬⇩L x + x = x›*)

class add_0 = plus + zero +
  assumes add_0_add_0_left [simp]: ‹0 + x = x›
      and add_0_add_0_right[simp]: ‹x + 0 = x›

class ab_group_mult = inverse + comm_monoid_mult +
  assumes ab_left_inverse: "inverse a * a = 1"
  assumes ab_diff_conv_add_uminus: "a / b = a * (inverse b)"

class semigroup_mult_left_cancel = semigroup_mult +
  assumes semigroup_mult_left_cancel: ‹a * c = b * c ⟷ a = b›

class no_inverse = times + one +
  assumes no_inverse[simp]: ‹a * b = 1 ⟷ a = 1 ∧ b = 1›

class no_negative = plus + zero +
  assumes no_negative[simp]: ‹a + b = 0 ⟷ a = 0 ∧ b = 0›

instantiation nat :: no_negative begin
instance by standard simp
end

instantiation nat :: no_inverse begin
instance by standard simp
end

class add_order_0 = ord + zero + plus +
  assumes add_nonneg_nonneg: ‹0 ≤ a ⟹ 0 ≤ b ⟹ 0 ≤ a + b›
      and add_pos_pos: ‹0 < a ⟹ 0 < b ⟹ 0 < a + b›

subclass (in ordered_comm_monoid_add) add_order_0
  by (standard; simp add: add_nonneg_nonneg add_pos_pos)

subsection ‹Separation Algebras›

subsubsection ‹Separation Disjunction›

class sep_disj =
  fixes sep_disj :: "'a => 'a => bool" (infix "##" 60)

class total_sep_disj = sep_disj +
  assumes total_sep_disj[simp]: ‹x ## y›

class comm_sep_disj = sep_disj +
  assumes sep_disj_commuteI: "x ## y ⟹ y ## x"
begin
lemma sep_disj_commute: "x ## y ⟷ y ## x"
  by (blast intro: sep_disj_commuteI)
end

subsubsection ‹Separation Magma›

class sep_magma = sep_disj + times
begin
definition join_sub (infix "≼⇩S⇩L" 50)
  where ‹join_sub y z ⟷ (∃x. z = y * x ∧ y ## x)›
end

class sep_cancel = sep_magma +
  assumes sep_cancel: ‹c ## a ⟹ c ## b ⟹ c * a = c * b ⟹ a = b›

class positive_sep_magma = sep_magma +
  assumes join_positivity: ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›

class strict_positive_sep_magma = sep_magma +
  assumes join_strict_positivity: ‹a ## b ⟹ a = a * b ⟹ False›

text ‹Usually, we extend the carrier set of the partial algebra to the total universe by
  importing the outside elements with no defined multiplication on them (except that to
  identity element and zero). It works in most cases
  but an exception is in semimodule structures where a notion of carrier set is required, so we
  give this below.›

class mul_carrier =
  fixes mul_carrier :: ‹'a ⇒ bool›

(*
class extended_partial_mul_algebra = mul_carrier + sep_disj +
  ― ‹characterizes the partial algebras extended to the universe carrier set›
  assumes sep_disj_gives_carrier: ‹a ## b ⟹ mul_carrier a ∧ mul_carrier b›
*)

class sep_carrier = mul_carrier + sep_magma +
  assumes mul_carrier_closed: ‹ ⟦ mul_carrier a; mul_carrier b; a ## b ⟧ ⟹ mul_carrier (a * b) ›

class sep_refl = sep_magma +
  assumes sep_refl_mult_I: ‹a ## b ⟹ a ## a ⟹ b ## b ⟹ a * b ## a * b›
  ― ‹Sometimes, ‹x ## x› can be used to represent if ‹x› is in the carrier set,
      recall the sep algebras as partial algebras are implicitly extended to the whole universe
      and leaving the elements out the carrier having no defined group operation. ›

subsubsection ‹Separation Semigroup›

class sep_semigroup = positive_sep_magma +
  assumes sep_mult_assoc:
    "⟦ x ## y; x * y ## z ⟧ ⟹ (x * y) * z = x * (y * z)"
  assumes sep_disj_multD1: "⟦ x ## y * z; y ## z ⟧ ⟹ x ## y"
  assumes sep_disj_multI1: "⟦ x ## y * z; y ## z ⟧ ⟹ x * y ## z"
  assumes sep_disj_multD2: "⟦ x * y ## z; x ## y ⟧ ⟹ y ## z"
  assumes sep_disj_multI2: "⟦ x * y ## z; x ## y ⟧ ⟹ x ## y * z"
begin
lemma sep_mult_assoc':
    "⟦ y ## z; x ## y * z ⟧ ⟹ x * (y * z) = (x * y) * z"
  by (metis local.sep_disj_multD1 local.sep_disj_multI1 local.sep_mult_assoc)

end

lemma join_sub_antisym: ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ False›
  for x :: ‹'a :: {sep_semigroup, strict_positive_sep_magma}›
  unfolding join_sub_def apply clarsimp
  using join_positivity join_strict_positivity join_sub_def by blast

class sep_ab_semigroup = sep_semigroup + comm_sep_disj +
  assumes sep_mult_commute: "x ## y ⟹ x * y = y * x"
begin

lemma self_sep_disj:
  ‹x ## y ⟹ x * y ## x * y ⟹ x ## x›
  ‹x ## y ⟹ x * y ## x * y ⟹ y ## y›
  using local.sep_disj_commute local.sep_disj_multD1 sep_disj_multD2 by blast+

end

class sep_disj_distrib = sep_magma +
  assumes sep_disj_distrib_right[simp]: ‹b ## c ⟹ a ## b * c ⟷ a ## b ∧ a ## c›
  assumes sep_disj_distrib_left [simp]: ‹a ## b ⟹ a * b ## c ⟷ a ## c ∧ b ## c›

subsubsection ‹Unital Separation›

class sep_magma_1 = sep_magma + mult_1 +
  assumes sep_magma_1_left  [simp]: "x ## 1"
  assumes sep_magma_1_right [simp]: "1 ## x"

class sep_magma_0 = sep_magma_1 + mult_zero + zero_neq_one +
  assumes sep_magma_0_left  [simp]: "x ## 0 ⟷ x = 1"
  assumes sep_magma_0_right [simp]: "0 ## x ⟷ x = 1"

class sep_carrier_1 = sep_carrier + sep_magma_1 +
  assumes sep_carrier_1[simp]: ‹mul_carrier 1›

class sep_carrier_0 = sep_carrier + sep_magma_0 +
  assumes sep_carrier_0[simp]: ‹mul_carrier 0›

class sep_no_inverse = sep_magma_1 +
  assumes sep_no_inverse[simp]: ‹x ## y ⟹ x * y = 1 ⟷ x = 1 ∧ y = 1›

class positive_sep_magma_1 = sep_magma_1 + positive_sep_magma
begin
subclass sep_no_inverse
  by (standard, metis local.join_positivity local.join_sub_def local.mult_1_left local.sep_magma_1_right)
end

subsubsection ‹Separation Monoid›

class sep_monoid = sep_magma_1 + sep_semigroup
begin
subclass positive_sep_magma_1 ..
end

definition (in times) subsume (infix "≼⇩×" 50)
  where ‹subsume y z ⟷ (∃x. z = y * x)›

class positive_mult = times +
  assumes positive_mult: ‹x ≼⇩× y ⟹ y ≼⇩× x ⟹ x = y›

class positive_mult_one = positive_mult + mult_1
begin
subclass no_inverse by (standard, metis local.mult_1_left local.positive_mult times.subsume_def)
end

class total_sep_monoid = monoid_mult + positive_mult + total_sep_disj
begin
subclass sep_magma .
subclass sep_monoid proof
  fix x y z :: 'a
  show ‹x ## 1› by simp
  show ‹1 ## x› by simp
  show ‹x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)›
    using mult_assoc by blast
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    by (clarsimp simp add: join_sub_def, metis local.positive_mult times.subsume_def)
  show ‹x ## y * z ⟹ y ## z ⟹ x ## y› by simp
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z› by simp
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z› by simp
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z › by simp
qed
subclass positive_mult_one ..
end

subsubsection ‹Separation Algebra›

class sep_algebra = sep_magma_1 + sep_ab_semigroup
begin

subclass sep_monoid ..

lemma sep_mult_left_commute[simp]:
  "b ## (a * c) ⟹ a ## c ⟹ b * (a * c) = a * (b * c)"
  by (metis local.sep_disj_commute local.sep_disj_multD2 local.sep_mult_assoc local.sep_mult_commute)

lemma join_sub_frame_left:
  ‹r ## y ⟹ x ≼⇩S⇩L y ⟹ r * x ≼⇩S⇩L r * y›
  unfolding join_sub_def
  by(clarsimp, metis local.sep_disj_multD1 local.sep_disj_multI1 local.sep_mult_assoc)

lemma join_sub_frame_right:
  ‹r ## y ⟹ x ≼⇩S⇩L y ⟹ r * x ≼⇩S⇩L r * y›
  unfolding join_sub_def
  by(clarsimp, metis local.sep_disj_multD1 local.sep_disj_multI1 local.sep_mult_assoc)

(*lemma
  ‹r ## y ⟹ r ## x ⟹ r * x ≼⇩S⇩L r * y ⟹ x ≼⇩S⇩L y›
  unfolding join_sub_def apply clarsimp *)

lemma join_sub_ext_left:
  ‹z ## y ⟹ x ≼⇩S⇩L y ⟹ x ≼⇩S⇩L z * y›
  unfolding join_sub_def
  by (clarsimp, metis local.sep_disj_commuteI local.sep_disj_multI1 local.sep_mult_commute)

lemma join_sub_ext_right:
  ‹y ## z ⟹ x ≼⇩S⇩L y ⟹ x ≼⇩S⇩L y * z›
  unfolding join_sub_def
  by (clarsimp, metis local.sep_disj_commute local.sep_disj_multD1 local.sep_disj_multI1 local.sep_mult_assoc local.sep_mult_commute)

end

subsubsection ‹Special Separation Algebras›

class total_sep_algebra = comm_monoid_mult + positive_mult + total_sep_disj
begin
subclass sep_magma .
subclass sep_algebra proof
  fix x y z :: 'a
  show ‹x ## 1› by simp
  show ‹1 ## x› by simp
  show ‹x ## y ⟹ x * y = y * x› by (simp add: mult_commute)
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z› by simp
  show ‹x ## y * z ⟹ y ## z ⟹ x ## y› by simp
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    by (metis local.join_sub_def local.positive_mult times.subsume_def)
  show ‹x ## y ⟹ y ## x› by simp
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z› by simp
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z› by simp
  show ‹x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)›
    by (simp add: mult_assoc)
qed
subclass total_sep_monoid ..
end

class discrete_semigroup = sep_disj + times +
  assumes discrete_disj[simp]: "¬ x ## y"
begin
subclass sep_magma .
subclass sep_ab_semigroup by (standard; simp add: local.join_sub_def)
subclass sep_cancel by (standard; simp)
subclass strict_positive_sep_magma by (standard; simp)
end

class discrete_monoid = sep_disj + mult_1 +
  assumes discrete_disj_1[simp]: ‹x ## y ⟷ x = 1 ∨ y = 1›
begin
subclass sep_magma .
subclass sep_algebra proof
  fix x y z :: 'a
  show ‹x ## y ⟹ x * y = y * x› by fastforce
  show ‹x ## y * z ⟹ y ## z ⟹ x ## y›
    by (metis local.mult_1_right local.discrete_disj_1)
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z›
    by (metis local.mult_1_left local.discrete_disj_1)
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    unfolding join_sub_def by (clarsimp, metis local.mult_1_right)
  show ‹x ## 1› by simp
  show ‹1 ## x› by simp
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z›
    by (metis local.mult_1_left local.discrete_disj_1)
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z›
    by (metis local.mult_1_right local.discrete_disj_1)
  show ‹x ## y ⟹ y ## x›
    using local.discrete_disj_1 by blast
  show ‹x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)› by force
qed
end



subsubsection ‹Strict Subsumption›

definition join_sub_strict :: ‹'a::sep_magma ⇒ 'a::sep_magma ⇒ bool› (infix "≺⇩S⇩L" 50)
  where ‹join_sub_strict y z ⟷ join_sub y z ∧ y ≠ z›


interpretation join_sub: order ‹join_sub::'a::sep_monoid ⇒ 'a ⇒ bool› join_sub_strict
proof
  fix x y z :: 'a
  show ‹(x ≺⇩S⇩L y) = (x ≼⇩S⇩L y ∧ ¬ y ≼⇩S⇩L x)›
    using join_positivity join_sub_strict_def by blast
  show ‹x ≼⇩S⇩L x›
    unfolding join_sub_strict_def join_sub_def
    by (rule exI[where x=1], simp)
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L z ⟹ x ≼⇩S⇩L z›
    unfolding join_sub_strict_def join_sub_def
    using sep_disj_multI2 sep_mult_assoc by blast
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    unfolding join_sub_strict_def join_sub_def
    using join_positivity join_sub_def by blast
qed

interpretation join_sub: order_bot 1 ‹join_sub::'a::sep_monoid ⇒ 'a ⇒ bool› join_sub_strict
proof
  fix a :: 'a
  show ‹1 ≼⇩S⇩L a›
    unfolding join_sub_strict_def join_sub_def
    by force
qed




subsection ‹Hierarchical Algebra›

text ‹Hierarchical Algebra models tree-like data structures.

It is a module-like structure with a path as its scalar, e.g. a list.
The monoid operation of the scalar is path concatenation, and the monoid operation of the elements
is composition of two separated parts of the data structure.
It is different with semimodule in that the scalar is not a semiring but only a monoid.
The scalar does not have addition operation.›

(*It is nothing but just a semimodule, or even not, just containing scalar associativity
  and separation homo*)

(*locale hierarchical_alg =
  fixes locate :: ‹'path::monoid_mult ⇒ 'a::sep_algebra ⇒ 'a› (infixr ":‣" 75)
  assumes locate_distrib_right: ‹path :‣ (x * y) = path :‣ x * path :‣ y›
    and   locate_assoc: ‹pa :‣ pb :‣ x = (pa * pb) :‣ x›
    and   locate_left_1:  ‹1 :‣ x = x›
    and   locate_right_1: ‹path :‣ 1 = 1›*)

text ‹As an example, a structure ‹struct { struct {A a; B b} c; D d; }› may be represented by
‹c :‣ (a :‣ va * b :‣ vb) * d :‣ vd›. ›


subsection ‹Permission Algebra›

text ‹An algebra for objects that can be partially owned, and shared.

The range of the ownership is [0,∞). Albeit the total permission is 1, the permission can be
greater than 1.
This relaxation eases various things.
We do not need to check the permission does not exceed 1 when merge two permissions.
The share (division by 2) and the merge are then free of side conditions.
In the hierarchical algebra, the permission of a leaf can be greater than 1 when the permission
of the node is less than 1, e.g. ‹0.5 ⨸ node_a :‣ (leaf_a :‣ 2 ⨸ a * leaf_b 1 ⨸ a ) › which actually means
‹node_a :‣ (leaf_a :‣ 1 ⨸ a * leaf_b :‣ 0.5 ⨸ a )›.
This helps the localized reasoning that focuses on the ‹node_a› by allowing disregarding to the
environmental permission totally.

TODO: limited by automation, the ownership of an object is represented by \<^typ>‹rat›
which includes negative rationals.
It is rather cumbersome cuz assertions have to again and again assert the permission is greater than
(or equal to) 0.
A better choice is using non-negative rationals only, like the type ‹posrat›, see comments in
Phi-Preliminary.›

class raw_share =
  fixes share :: ‹rat ⇒ 'a ⇒ 'a› (infixr "⦼" 75)
    ― ‹‹n ⦼ a› divides ‹a› into ‹n› proportion of the original share, for ‹0 < n < 1››

class share = raw_share + ― ‹share algebra for semigroup, where unit ‹1› is not defined›
  assumes share_share_assoc0: ‹0 < n ⟹ 0 < m ⟹ share n (share m x) = share (n * m) x›
    and   share_left_one[simp]:  ‹share 1 x = x›

class share_one = share + one +
  assumes share_right_one[simp]: ‹share n 1 = 1›
    and   share_left_0[simp]:    ‹share 0 x = 1›
begin
lemma share_share: ‹0 ≤ n ⟹ 0 ≤ m ⟹ share n (share m x) = share (n * m) x›
  using less_eq_rat_def local.share_share_assoc0 by fastforce
end

class share_one_eq_one_iff = share_one +
  assumes share_one_eq_one_iff[simp]: ‹0 < n ⟹ share n x = 1 ⟷ x = 1›

class share_carrier = sep_carrier + share +
  assumes share_carrier_closed: ‹0 < n ⟹ mul_carrier x ⟹ mul_carrier (share n x)›

class share_carrier_1 = sep_carrier_1 + share_one +
  assumes share_carrier_closed_1: ‹0 ≤ n ⟹ mul_carrier x ⟹ mul_carrier (share n x)›
begin
subclass share_carrier by (standard; simp add: share_carrier_closed_1)
end

class share_inj = raw_share +
  assumes share_inj[simp]: ‹0 < n ⟹ share n x = share n y ⟷ x = y›
begin

lemma share_inj': ‹0 < n ⟹ inj (share n)›
  unfolding inj_def
  by clarsimp

end

class share_sep_disj = share + comm_sep_disj + sep_carrier +
  assumes share_sep_disj_left[simp]: ‹0 < n ⟹ share n x ## y ⟷ x ## y›
          ― ‹the share operation is independent with sep_disj. The multiplication defined between
              two elements are also defined on their shared portions. ›
      and share_disj_sdistr: ‹ mul_carrier x ⟹ x ## x›
          ― ‹The original form of the condition is,
                  ‹⟦ n < 0 ; m < 0 ; mul_carrier x ⟧ ⟹ share n x ## share m x›
              any element in the algebra can be divided into any portions.
              By simplifying using share_sep_disj_left, we get the form above.›
begin

lemma share_sep_disj_right[simp]:
        ‹0 < n ⟹ y ## share n x ⟷ y ## x›
  using local.share_sep_disj_left sep_disj_commute by force

end

class share_nun_semimodule = share_sep_disj + sep_ab_semigroup + share_carrier +
      ―‹nun stands for non-unital›
  assumes share_sep_left_distrib_0:  ‹ ⟦ 0 < n ; 0 < m ; mul_carrier x ⟧ ⟹ share n x * share m x = share (n+m) x›
    and   share_sep_right_distrib_0: ‹0 < n ⟹ x ## y ⟹ share n x * share n y = share n (x * y)›
    and   share_sub_0: ‹0 < n ∧ n < 1 ⟹ mul_carrier x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x›

class share_semimodule = share_sep_disj + share_one + sep_algebra + share_carrier_1 +
  assumes share_sep_left_distrib:  ‹0 ≤ n ⟹ 0 ≤ m ⟹ mul_carrier x ⟹ share n x * share m x = share (n+m) x›
    and   share_sep_right_distrib: ‹0 ≤ n ⟹ x ## y ⟹ share n x * share n y = share n (x * y)›
    and   share_sub: ‹0 ≤ n ∧ n ≤ 1 ⟹ mul_carrier x ⟹ share n x ≼⇩S⇩L x›
begin

subclass share_nun_semimodule proof
  fix x y :: 'a
  fix n m :: rat
  show ‹0 < n ⟹ 0 < m ⟹ mul_carrier x ⟹ share n x * share m x = share (n + m) x›
    by (meson local.share_sep_left_distrib order_less_le)
  show ‹0 < n ⟹ x ## y ⟹ share n x * share n y = share n (x * y)›
    using local.share_sep_right_distrib order_less_imp_le by blast
  show ‹0 < n ∧ n < 1 ⟹ mul_carrier x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x›
    by (simp add: local.share_sub)
qed

end

subsubsection ‹Derivatives›

class share_resistence_nun = raw_share +
  assumes share_resistence_nun[simp]: ‹share n x = x›
begin
subclass share by (standard; simp)
end

class share_resistence = raw_share + one +
  assumes share_resistence[simp]: ‹share n x = (if n = 0 then 1 else x)›
begin
subclass share by (standard; simp)
end


subsection ‹Homomorphisms›

locale homo_mul_carrier =
  fixes ψ :: ‹'a::mul_carrier ⇒ 'b::mul_carrier›
  assumes homo_mul_carrier: ‹mul_carrier x ⟹ mul_carrier (ψ x)›

locale homo_sep_disj =
  fixes ψ :: ‹'a::sep_disj ⇒ 'b::sep_disj›
  assumes sep_disj_homo_semi[simp]: ‹a ## b ⟶ ψ a ## ψ b›

locale closed_homo_sep_disj =
  fixes ψ :: ‹'a::sep_disj ⇒ 'b::sep_disj›
  assumes sep_disj_homo[iff]: ‹ψ a ## ψ b ⟷ a ## b›
begin
sublocale homo_sep_disj by standard simp
end

locale homo_sep_mult =
  fixes ψ :: " 'a::sep_magma ⇒ 'b::sep_magma "
  assumes homo_mult: "x ## y ⟹ ψ (x * y) = ψ x * ψ y"

locale homo_join_sub =
  fixes ψ :: ‹'a::sep_magma ⇒ 'b::sep_magma›
    and D :: ‹'a set›
  assumes homo_join_sub: ‹x ∈ D ∧ y ∈ D ⟹ ψ x ≼⇩S⇩L ψ y ⟷ x ≼⇩S⇩L y›

locale homo_sep = homo_sep_mult ψ + homo_sep_disj ψ
  for ψ :: ‹'a::sep_magma ⇒ 'b::sep_magma›
  ― ‹Non-closed (weak) homomorphism. This is the standard homomorphism in partial algebras. []›

text ‹
  Note a non-closed homomorphism only requires the right-half entailment of the separation disjunction
  (‹x ## y ⟶ ψ x ## ψ y›, it is an implication instead of an equation).

  It provides more flexibility where the target algebra ‹𝔅›
  can define more behaviors between the projected elements of the source algebra ‹𝒜›.
  As an instance showing the value of the flexibility, we consider
  the embedding into a permission algebra from a discrete unital algebra (where the separation
  between any two elements are undefined unless one of the element is the identity)
  ‹ψ 1 = 1    ψ x = Perm(1,x)    where fraction p in Perm(p,x) is the permission, and 1 is the total permission›
  it requires this flexibility if we allow super-permission in our formalization.
  Note the permission algebra supports scalar operation, ‹c ⋅ Perm(p,x) = Perm(c⋅p, x)›, a permission
  can be temporarily larger than 1 inside the inner operation of a scalar expression, only if after
  the scalar operation, the permission is less or equal than 1.
  It means ‹Perm(1,x) * Perm(1,x) = Prem(2,x)› is defined, and if the insertion requires bi-direction
  homomorphism of the separation disjunction, from it we have ‹x * x› is defined, which is contrast
  with the discrete source algebra.
  The bi-direction homomorphism is allowed only if we prohibit super-permission, but it destroys the
  semimodule property of the permission algebra.
  The super-permission frees us from checking the overflow of the permission addition and makes
  the expressiveness more flexible.

  (Unclosed separation homomorphism does not represent any problem in this case,
   because the domain domain of the embedding is usually structures of memory objects,
   of which the domainoid is usually determined, and therefore of which the separation disjunction can be
   decided.)

  By contrast, if the homomorphism is not assumed to be closed, i.e., from ‹ψ x ## ψ y› we cannot have ‹x ## y›,
  we can only have one side transformation ‹ψ (x * y) ⟶ ψ x * ψ y› but not the other side
  ‹ψ x * ψ y ⟶ ψ (x * y)› because we don't know if ‹x ## y›.
  This side of transformation is still important and necessary.

  There is no alternative way to the flexibility including super-permission, but the separatablity
  can be checked automatically and in most cases, the separatablity between
  two φ-types ‹x : T› and ‹y : U› can be inferred from the types ‹T› and ‹U›. A type usually
  records which part of the resource does this φ-type assertion specifies (otherwise, it is impossible
  to reason the transformation that extracts a certain part of the resource which is used locally by
  a subroutine, note the reasoning is type-guided).
  From this domain of specification, we can check the separatablity by checking the domains are disjoint.

  The reasoning procedure is given by ‹φSep_Disj› later.
›

locale closed_homo_sep = homo_sep + closed_homo_sep_disj

locale homo_share =
  fixes ψ :: " 'a::raw_share ⇒ 'b::raw_share "
  assumes share_homo: ‹ψ (n ⦼ x) = n ⦼ (ψ x)›


subsubsection ‹Orthogonal Homomorphism›

text ‹
The property specifies the homomorphism is right-orthogonal to every group action.
See https://math.stackexchange.com/questions/4748364

This property essentially says we put something into another big container where the 'factors' of
the original things are independent with other stuffs, e.g. this sort of resource has no
interference with other sorts, so they are orthogonal.
›

locale sep_orthogonal = homo_sep ψ
  for ψ :: ‹'a::sep_magma ⇒ 'b::sep_magma›
  and D :: ‹'a set› ― ‹carrier set of the source algebra,
            Previously we implicitly extend the carrier set to be the universe of the type.
            It can be done because for any element ‹d› not belonging to the carrier set,
            only if ‹d› has no defined operation with any element including itself,
            the introduction of ‹d› doesn't affect anything.
            However here, if ‹a = ψ d› accidentally belongs to the target algebra, ‹d› matters,
            so we must give the carrier set explicitly to exclude such ‹d›.›
        ― ‹It is a bad idea to reuse ‹mul_carrier› to replace ‹D› here. ‹sep_orthogonal› is mainly
            used in fictional SL where the actual domain can be various and even for example dependent
            on the key of the map (e.g., later in the memory model of C, the domain of each block
            depends on the type of the block which is acquired from the key of the map modelling
            the memory). ‹mul_carrier› is fixed to its logic type can never be so flexible.
            ‹mul_carrier› is designed for simplifying the specification of separation semimodules.
            Properties of separation semimodules are bound to the type, by means of type classes,
            so it is okay to again use a type class to bind the carrier set to the types.›
+ assumes sep_orthogonal: ‹b ∈ D ∧ c ∈ D ⟹ ψ b ## a ⟹ ψ b * a = ψ c ⟷ (∃a'. a = ψ a' ∧ b * a' = c ∧ b ## a' ∧ a' ∈ D)›
begin


lemma sep_orthogonal'[no_atp]:
  ‹b ∈ D ∧ c ∈ D ⟹ ψ b ## a ⟹ ψ c = ψ b * a ⟷ (∃a'. a = ψ a' ∧ b * a' = c ∧ b ## a' ∧ a' ∈ D)›
  by (metis sep_orthogonal)

sublocale homo_join_sub ψ
  apply standard
  unfolding join_sub_def
  by (metis homo_mult sep_disj_homo_semi sep_orthogonal)

text ‹The weak homomorphism of ‹≼⇩S⇩L›, ‹x ≼⇩S⇩L z ⟶ ψ x ≼⇩S⇩L ψ z› is trivially true but the reversed
so-called closed homo ‹ψ x ≼⇩S⇩L ψ z ⟶ x ≼⇩S⇩L z› is not seen even in closed separation homo.

‹ψ x ≼⇩S⇩L ψ z ⟶ x ≼⇩S⇩L z  ⟺  ∀y'. ψ z = y' * ψ x ⟶ ∃y. z = y * x›
can be unfolded to a form really similar (but weaker) to the orthogonal homo
(the only difference is it doesn't require ‹y' = ψ y›). So orthogonal homo entails the closed homo
of join_sub, but not reversely.›

end

locale sep_orthogonal_1 = sep_orthogonal ψ D
  for ψ :: ‹'a::sep_magma_1 ⇒ 'b::sep_magma_1› and D
+ assumes one_in_D: ‹1 ∈ D›
begin

sublocale homo_one ψ
  by (standard, metis mult_1_class.mult_1_left mult_1_class.mult_1_right one_in_D sep_magma_1_left sep_orthogonal)

end



locale sep_orthogonal_monoid = sep_orthogonal_1 ψ D
  for ψ :: ‹'a::sep_monoid ⇒ 'b::sep_monoid› and D
begin

lemma simple_homo_mul[simp]:
  ‹simple_homo_mul ψ D›
  unfolding simple_homo_mul_def
  by (metis homo_join_sub homo_one join_sub.bot.extremum join_sub.bot.extremum_uniqueI one_in_D)

end

locale cancl_sep_orthogonal_monoid = sep_orthogonal_monoid ψ D
  for ψ :: ‹'a::{sep_cancel, sep_monoid} ⇒ 'b::sep_monoid› and D

locale share_orthogonal_homo = sep_orthogonal_monoid ψ D
  for ψ :: ‹'a::sep_algebra ⇒ 'b::share_semimodule› and D
+ assumes share_orthogonal: ‹b ∈ D ∧ c ∈ D ⟹ ψ b ## a ⟹ 0 < n ∧ n ≤ 1 ⟹
                           share n (ψ b) * a = ψ c ⟷ (∃a'. a = share (1-n) (ψ b) * ψ a' ∧ b * a' = c ∧ b ## a' ∧ a' ∈ D)›
    and   share_bounded: ‹⟦ b ∈ D ∧ c ∈ D ; ψ b ## a ; n > 1 ; ψ b ≠ 1 ⟧ ⟹ share n (ψ b) * a ≠ ψ c›
    and   ψ_mul_carrier: ‹x ∈ D ⟹ mul_carrier (ψ x) ›
begin

lemma share_orthogonal'[no_atp]:
  ‹b ∈ D ∧ c ∈ D ⟹ ψ b ## a ⟹ 0 < n ∧ n ≤ 1 ⟹
      ψ c = share n (ψ b) * a ⟷ (∃a'. a = share (1-n) (ψ b) * ψ a' ∧ b * a' = c ∧ b ## a' ∧ a' ∈ D)›
  by (metis share_orthogonal)

lemma
  join_sub_share_join_sub_whole: ‹0 < n ∧ n ≤ 1 ⟹ x ∈ D ∧ y ∈ D ⟹ share n (ψ x) ≼⇩S⇩L ψ y ⟷ x ≼⇩S⇩L y›
  unfolding join_sub_def
  by ((rule; clarsimp simp add: homo_mult),
      metis share_orthogonal,
      meson ψ_mul_carrier join_sub_def join_sub_ext_right less_eq_rat_def sep_disj_homo_semi share_sep_disj_left share_sub)
  

(* lemma ‹0 < n ∧ n ≤ 1 ⟹ share n (ψ x) ≼⇩S⇩L ψ x›
  by (simp add: ψ_mul_carrier share_sub) *)

end

(*
locale share_orthogonal_homo_L =
  fixes ψ :: ‹'a::sep_algebra ⇒ 'b::share_semimodule›
  assumes share_orthogonal_homo': ‹id share_orthogonal_homo ψ›
begin
sublocale share_orthogonal_homo using share_orthogonal_homo'[simplified] .
end *)


locale cancl_share_orthogonal_homo = share_orthogonal_homo ψ D
  for ψ :: ‹'a::{sep_cancel, sep_algebra} ⇒ 'b::share_semimodule› and D
begin

sublocale cancl_sep_orthogonal_monoid ..

end


subsubsection ‹With Discrete Algebra›

lemma homo_sep_disj_discrete[simp]:
  ‹homo_sep_disj ψ›
  for ψ :: ‹'a::discrete_semigroup ⇒ 'b::sep_disj›
  unfolding homo_sep_disj_def
  by simp

lemma homo_sep_disj_discrete_1[simp]:
  ‹ homo_one ψ
⟹ homo_sep_disj ψ›
  for ψ :: ‹'a::discrete_monoid ⇒ 'b::sep_magma_1›
  unfolding homo_sep_disj_def homo_one_def
  by simp

lemma closed_homo_sep_disj_discrete[simp]:
  ‹closed_homo_sep_disj ψ›
  for ψ :: ‹'a::discrete_semigroup ⇒ 'b::discrete_semigroup›
  unfolding closed_homo_sep_disj_def
  by simp

lemma closed_homo_sep_disj_discrete_1[simp]:
  ‹ simple_homo_mul ψ UNIV
⟹ closed_homo_sep_disj ψ›
  for ψ :: ‹'a::discrete_monoid ⇒ 'b::discrete_monoid›
  unfolding closed_homo_sep_disj_def simple_homo_mul_def
  by simp

lemma homo_sep_mult_discrete[simp]:
  ‹homo_sep_mult ψ›
  for ψ :: ‹'a::discrete_semigroup ⇒ 'b::sep_magma›
  unfolding homo_sep_mult_def
  by simp

lemma homo_sep_discrete[simp]:
  ‹homo_sep ψ›
  for ψ :: ‹'a::discrete_semigroup ⇒ 'b::sep_magma›
  unfolding homo_sep_def
  by simp

lemma closed_homo_sep_discrete[simp]:
  ‹closed_homo_sep ψ›
  for ψ :: ‹'a::discrete_semigroup ⇒ 'b::discrete_semigroup›
  unfolding closed_homo_sep_def
  by simp


subsection ‹Partial Additive Structures›

subsubsection ‹Domain of the Addition›

paragraph ‹Addition›

class dom_of_add =
  fixes dom_of_add :: ‹'a ⇒ 'a ⇒ bool› (infix "##⇩+" 60)

class total_dom_of_add = dom_of_add +
  assumes total_dom_of_add[simp]: ‹x ##⇩+ y›

class comm_dom_of_add = dom_of_add +
  assumes dom_of_add_commuteI: "x ##⇩+ y ⟹ y ##⇩+ x"
begin
lemma dom_of_add_commute: "x ##⇩+ y ⟷ y ##⇩+ x"
  by (blast intro: dom_of_add_commuteI)
end

paragraph ‹Subtraction›

class dom_of_minus =
  fixes dom_of_minus :: ‹'a ⇒ 'a ⇒ bool› (infix "##⇩-" 60)

class total_dom_of_minus = dom_of_minus +
  assumes total_dom_of_minus[simp]: ‹x ##⇩- y›


subsubsection ‹Partial Additive Magma›

class partial_add_magma = dom_of_add + plus
begin

definition additive_join_sub (infix "≼⇩+" 50)
  where ‹additive_join_sub y z ⟷ (∃x. z = x + y ∧ x ##⇩+ y)›

end

class partial_add_cancel = partial_add_magma +
  assumes partial_add_cancel: ‹a ##⇩+ c ⟹ b ##⇩+ c ⟹ a + c = b + c ⟹ a = b›

class positive_partial_add_magma = partial_add_magma +
  assumes additive_join_positivity: ‹x ≼⇩+ y ⟹ y ≼⇩+ x ⟹ x = y›

class strict_positive_partial_add_magma = partial_add_magma +
  assumes additive_join_strict_positivity: ‹b ##⇩+ a ⟹ a = b + a ⟹ False›


subsubsection ‹Partial Additive Semigroup›

class partial_semigroup_add = partial_add_magma +
  assumes partial_add_assoc:
    "⟦ x ##⇩+ y; x + y ##⇩+ z ⟧ ⟹ (x + y) + z = x + (y + z)"
  assumes partial_add_dom_multD1: "⟦ x ##⇩+ y + z; y ##⇩+ z ⟧ ⟹ x ##⇩+ y"
  assumes partial_add_dom_multI1: "⟦ x ##⇩+ y + z; y ##⇩+ z ⟧ ⟹ x + y ##⇩+ z"
  assumes partial_add_dom_multD2: "⟦ x + y ##⇩+ z; x ##⇩+ y ⟧ ⟹ y ##⇩+ z"
  assumes partial_add_dom_multI2: "⟦ x + y ##⇩+ z; x ##⇩+ y ⟧ ⟹ x ##⇩+ y + z"
begin

lemma partial_add_assoc':
    "⟦ y ##⇩+ z; x ##⇩+ y + z ⟧ ⟹ x + (y + z) = (x + y) + z"
  by (metis local.partial_add_assoc local.partial_add_dom_multD1 local.partial_add_dom_multI1)

end

lemma positive_join_sub_antisym: ‹x ≼⇩+ y ⟹ y ≼⇩+ x ⟹ False›
  for x :: ‹'a :: {partial_semigroup_add, strict_positive_partial_add_magma}›
  unfolding additive_join_sub_def
  by (clarsimp, metis additive_join_strict_positivity partial_add_assoc' partial_add_dom_multI1)

class partial_ab_semigroup_add = partial_semigroup_add + comm_dom_of_add +
  assumes partial_add_commute: "x ##⇩+ y ⟹ x + y = y + x"
begin

lemma self_dom_of_add_destruct:
  ‹x ##⇩+ y ⟹ x + y ##⇩+ x + y ⟹ x ##⇩+ x›
  ‹x ##⇩+ y ⟹ x + y ##⇩+ x + y ⟹ y ##⇩+ y›
  using local.dom_of_add_commute local.partial_add_dom_multD1 apply blast
  using local.dom_of_add_commute local.partial_add_dom_multD2 by blast

end

class dom_of_add_intuitive = partial_add_magma +
  assumes dom_of_add_intuitive_right[simp]: ‹b ##⇩+ c ⟹ a ##⇩+ b + c ⟷ a ##⇩+ b ∧ a ##⇩+ c›
  assumes dom_of_add_intuitive_left [simp]: ‹a ##⇩+ b ⟹ a + b ##⇩+ c ⟷ a ##⇩+ c ∧ b ##⇩+ c›

paragraph ‹Cancellative›

class partial_cancel_semigroup_add = partial_semigroup_add +
  assumes partial_add_left_imp_eq : "⟦ a ##⇩+ b; a ##⇩+ c ⟧ ⟹ a + b = a + c ⟹ b = c"
  assumes partial_add_right_imp_eq: "⟦ b ##⇩+ a; c ##⇩+ a ⟧ ⟹ b + a = c + a ⟹ b = c"
begin

lemma partial_add_left_cancel [simp]: "⟦ a ##⇩+ b ; a ##⇩+ c ⟧ ⟹ a + b = a + c ⟷ b = c"
  using local.partial_add_left_imp_eq by blast
  
lemma partial_add_right_cancel [simp]: "⟦ b ##⇩+ a ; c ##⇩+ a ⟧ ⟹ b + a = c + a ⟷ b = c"
  using local.partial_add_right_imp_eq by blast

end

class partial_cancel_ab_semigroup_add = partial_ab_semigroup_add + dom_of_minus + minus +
  assumes partial_add_diff_cancel_left'[simp]: ‹a ##⇩+ b ⟹ (a + b) - a = b›
      and partial_add_diff_cancel_left'_dom: ‹a ##⇩+ b ⟹ (a + b) ##⇩- a›
  assumes partial_diff_diff_add: ‹b ##⇩+ c ⟹ a ##⇩- (b + c) ⟹ a - b - c = a - (b + c)›
      and partial_diff_diff_add_dom: ‹a ##⇩- b ∧ (a - b) ##⇩- c ⟷ b ##⇩+ c ∧ a ##⇩- (b + c)›
begin

lemma partial_add_diff_cancel_right'_dom [simp]:
  ‹a ##⇩+ b ⟹ a + b ##⇩- b›
  by (metis local.dom_of_add_commute local.partial_add_commute local.partial_add_diff_cancel_left'_dom)

lemma partial_add_diff_cancel_right' [simp]:
  "a ##⇩+ b ⟹ (a + b) - b = a"
  by (metis local.dom_of_add_commute local.partial_add_commute local.partial_add_diff_cancel_left')

subclass partial_cancel_semigroup_add
  by (standard,
      metis local.partial_add_diff_cancel_left',
      metis partial_add_diff_cancel_right')

lemma partial_add_diff_cancel_left_dom[simp]:
  ‹⟦ c ##⇩+ a ; c ##⇩+ b ⟧ ⟹ c + a ##⇩- c + b ⟷ a ##⇩- b›
  by (metis local.partial_add_diff_cancel_left' local.partial_add_diff_cancel_left'_dom local.partial_diff_diff_add_dom)

lemma partial_add_diff_cancel_left [simp]:
  "⟦ c ##⇩+ a ; c ##⇩+ b ; a ##⇩- b ⟧ ⟹ (c + a) - (c + b) = a - b"
  by (metis local.partial_add_diff_cancel_left' local.partial_diff_diff_add partial_add_diff_cancel_left_dom)

lemma partial_add_diff_cancel_right_dom [simp]:
  "⟦ a ##⇩+ c ; b ##⇩+ c ⟧ ⟹ a + c ##⇩- b + c = a ##⇩- b"
  by (metis local.dom_of_add_commute local.partial_add_commute partial_add_diff_cancel_left_dom)

lemma add_diff_cancel_right [simp]:
  "⟦ a ##⇩+ c ; b ##⇩+ c; a ##⇩- b ⟧ ⟹ (a + c) - (b + c) = a - b"
  by (metis local.dom_of_add_commute local.partial_add_commute partial_add_diff_cancel_left)


lemma partial_diff_right_commute: "b ##⇩+ c ⟹ a ##⇩- (b + c) ⟹ a - c - b = a - b - c"
  by (simp add: dom_of_add_commute local.partial_add_commute local.partial_diff_diff_add)

lemma partial_add_implies_diff_dom:
  ‹c ##⇩+ b ⟹ c + b = a ⟹ a ##⇩- b›
  by fastforce

lemma partial_add_implies_diff:
  ‹c ##⇩+ b ⟹ c + b = a ⟹ c = a - b›
  by fastforce

end

paragraph ‹Ordered›

class partial_canonically_ordered_ab_semigroup_add = partial_cancel_semigroup_add + order +
  assumes partial_le_iff_add: "a ≤ b ⟷ (∃c. b = a + c ∧ a ##⇩+ c)"


subsubsection ‹Unital Partial Additive Structures›

class partial_add_magma_0 = partial_add_magma + add_0 +
  assumes partial_add_0_left  [simp]: "x ##⇩+ 0"
  assumes partial_add_0_right [simp]: "0 ##⇩+ x"

class partial_add_no_negative = partial_add_magma_0 +
  assumes partial_add_no_negative[simp]: ‹x ##⇩+ y ⟹ x + y = 0 ⟷ x = 0 ∧ y = 0›

class positive_partial_add_magma_0 = partial_add_magma_0 + positive_partial_add_magma
begin
subclass partial_add_no_negative
  by standard (metis add_0_add_0_right local.additive_join_positivity local.additive_join_sub_def local.partial_add_0_left)
end

subsubsection ‹Partial Additive Monoid›

class partial_add_monoid = partial_add_magma_0 + partial_semigroup_add

(* definition (in plus) additive_subsume (infix "≼⇩+''" 50)
  where ‹additive_subsume y z ⟷ (∃x. z = x + y)›

class positive_add = plus +
  assumes positive_add: ‹x ≼⇩+' y ⟹ y ≼⇩+' x ⟹ x = y›

class positive_add_0 = positive_add + add_0
begin

subclass no_negative
  by standard  (metis add_0_add_0_right local.positive_add plus.additive_subsume_def)
  
end *)

class total_partial_add_monoid = monoid_add + total_dom_of_add
begin
subclass partial_add_magma .
subclass partial_add_monoid proof
  fix x y z :: 'a
  show ‹x ##⇩+ 0› by simp
  show ‹0 ##⇩+ x› by simp
  show ‹x ##⇩+ y ⟹ x + y ##⇩+ z ⟹ x + y + z = x + (y + z)›
    by (simp add: add_assoc)
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x ##⇩+ y› by simp
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x + y ##⇩+ z› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ y ##⇩+ z› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ x ##⇩+ y + z › by simp
  show ‹0 + x = x› by simp
  show ‹x + 0 = x› by simp
qed
end

subsubsection ‹Partial Commutative Addition Monoid›

class partial_add_ab_monoid = partial_add_magma_0 + partial_ab_semigroup_add
begin

subclass partial_add_monoid ..

lemma partial_add_left_commute[simp]:
  "b ##⇩+ (a + c) ⟹ a ##⇩+ c ⟹ b + (a + c) = a + (b + c)"
  by (metis local.dom_of_add_commuteI local.partial_add_assoc local.partial_add_commute local.partial_add_dom_multD1)

lemma additive_join_sub_frame:
  ‹r ##⇩+ y ⟹ x ≼⇩+ y ⟹ r + x ≼⇩+ r + y›
  unfolding additive_join_sub_def
  by (clarsimp, metis local.dom_of_add_commute local.partial_add_commute local.partial_add_dom_multI1)

lemma additive_join_sub_ext_left:
  ‹z ##⇩+ y ⟹ x ≼⇩+ y ⟹ x ≼⇩+ z + y›
  unfolding additive_join_sub_def
  using local.partial_add_assoc' local.partial_add_dom_multI1 by auto

lemma additive_join_sub_ext_right:
  ‹y ##⇩+ z ⟹ x ≼⇩+ y ⟹ x ≼⇩+ y + z›
  unfolding additive_join_sub_def
  by (metis local.dom_of_add_commute local.partial_add_assoc' local.partial_add_commute local.partial_add_dom_multI1)

end


class total_partial_add_ab_monoid = comm_monoid_add + total_dom_of_add
begin
subclass partial_add_magma .
subclass partial_add_ab_monoid proof
  fix x y z :: 'a
  show ‹x ##⇩+ 0› by simp
  show ‹0 ##⇩+ x› by simp
  show ‹x ##⇩+ y ⟹ x + y = y + x› by (simp add: add_commute) 
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x + y ##⇩+ z› by simp
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x ##⇩+ y› by simp
(*  show ‹x ≼⇩+ y ⟹ y ≼⇩+ x ⟹ x = y›
    by (metis local.additive_join_sub_def local.positive_add plus.additive_subsume_def) *)
  show ‹x ##⇩+ y ⟹ y ##⇩+ x› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ y ##⇩+ z› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ x ##⇩+ y + z› by simp
  show ‹x ##⇩+ y ⟹ x + y ##⇩+ z ⟹ x + y + z = x + (y + z)› using add_assoc by blast
  show ‹x + 0 = x› by simp
  show ‹0 + x = x› by simp
qed
subclass total_partial_add_monoid ..
end

class discrete_partial_semigroup_add = dom_of_add + plus +
  assumes discrete_dom_of_add[simp]: "x ##⇩+ y ⟷ x = y"
    and discrete_add[simp]: "x + y = (if x = y then x else undefined)"
begin
subclass partial_add_magma .
subclass partial_ab_semigroup_add proof
  fix x y z :: 'a
  show ‹x ##⇩+ y ⟹ x + y = y + x› by simp
(*  show ‹x ≼⇩+ y ⟹ y ≼⇩+ x ⟹ x = y› unfolding additive_join_sub_def by force *)
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x ##⇩+ y› by simp
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x + y ##⇩+ z› by simp
  show ‹x ##⇩+ y ⟹ y ##⇩+ x› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ y ##⇩+ z› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ x ##⇩+ y + z› by simp
  show ‹x ##⇩+ y ⟹ x + y ##⇩+ z ⟹ x + y + z = x + (y + z)› by simp
  (*show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    using local.join_sub_def by force*)
qed
end

class empty_partial_semigroup_add = dom_of_add + plus +
  assumes empty_dom_of_add[simp]: "¬ x ##⇩+ y"
begin
subclass partial_add_magma .
subclass partial_ab_semigroup_add by (standard; simp add: additive_join_sub_def)
subclass partial_add_cancel by (standard; simp)
subclass strict_positive_partial_add_magma by (standard; simp)
end

class empty_partial_add_monoid = dom_of_add + add_0 +
  assumes empty_dom_of_add_1[simp]: ‹x ##⇩+ y ⟷ x = 0 ∨ y = 0›
begin
subclass partial_add_magma .
subclass partial_add_ab_monoid proof
  fix x y z :: 'a
  show ‹x ##⇩+ y ⟹ x + y = y + x› by fastforce
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x ##⇩+ y›
    using local.empty_dom_of_add_1 by fastforce
  show ‹x ##⇩+ y + z ⟹ y ##⇩+ z ⟹ x + y ##⇩+ z›
    using local.empty_dom_of_add_1 by fastforce
(*  show ‹x ≼⇩+ y ⟹ y ≼⇩+ x ⟹ x = y›
    unfolding additive_join_sub_def by (clarsimp, metis add_0_add_0_left) *)
  show ‹x ##⇩+ 0› by simp
  show ‹0 ##⇩+ x› by simp
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ y ##⇩+ z›
    by (metis add_0_add_0_left local.empty_dom_of_add_1)
  show ‹x + y ##⇩+ z ⟹ x ##⇩+ y ⟹ x ##⇩+ y + z›
    using local.empty_dom_of_add_1 by fastforce
  show ‹x ##⇩+ y ⟹ y ##⇩+ x›
    using local.empty_dom_of_add_1 by blast
  show ‹x ##⇩+ y ⟹ x + y ##⇩+ z ⟹ x + y + z = x + (y + z)› by force
qed
end

subsection ‹Module Structures for Separation›

text ‹The right distributivity of a module forms a homomorphism over the group operation,
  so we don't cover it here.›

locale module_for_sep =
  fixes smult :: ‹'s ⇒ 'a ⇒ 'a›
    and Ds :: ‹'s ⇒ bool› ― ‹gives the carrier set of the scalars›

text ‹It seems there is not a standard definition for modules on partial rings.
  In our formalization, we assume the scalar distributivity is available on any elements of the ring.
›

locale module_S_distr = module_for_sep +
  assumes module_scalar_distr: ‹ ⟦ Ds (s::'s::partial_add_magma); Ds t; s ##⇩+ t ; mul_carrier (a :: 'a :: sep_carrier) ⟧
                             ⟹ smult (s + t) a = smult s a * smult t a ∧ smult s a ## smult t a ›

locale module_scalar_assoc = module_for_sep +
  assumes module_scalar_assoc: ‹⟦ Ds s; Ds t ⟧ ⟹ smult s (smult t a) = smult (s * t) a›
  ― ‹Recall we always follow the order of the associativity.

      Here we do not require ‹mul_carrier a› in order to get a type equation ‹F s (F t T) = F (t * s) T›
      that is condition-less about abstract objects.

      For elements outside the carrier set, simply extend the scalar multiplication on them to identity
      function.
›

locale module_scalar_identity = module_for_sep +
  assumes module_scalar_identity: ‹smult 1 a = a›

locale module_scalar_zero = module_for_sep +
  assumes module_scalar_zero: ‹smult 0 a = 1›

lemma module_scalar_identity_share[simp]:
  ‹module_scalar_identity (share :: rat ⇒ 'a::share ⇒ 'a)›
  unfolding module_scalar_identity_def
  by simp

lemma module_scalar_zero_share[simp]:
  ‹module_scalar_zero (share :: rat ⇒ 'a::share_one ⇒ 'a)›
  unfolding module_scalar_zero_def
  by simp

lemma module_scalar_assoc_share0[simp]:
  ‹module_scalar_assoc (share :: rat ⇒ 'a::share ⇒ 'a) (λn. 0 < n)›
  unfolding module_scalar_assoc_def
  by (simp add: share_share_assoc0)

lemma module_scalar_assoc_share[simp]:
  ‹module_scalar_assoc (share :: rat ⇒ 'a::share_one ⇒ 'a) (λn. 0 ≤ n)›
  unfolding module_scalar_assoc_def
  by (simp add: share_share)

instantiation rat :: total_partial_add_ab_monoid
begin
definition dom_of_add_rat :: ‹rat ⇒ rat ⇒ bool› where [iff]: ‹dom_of_add_rat _ _ ⟷ True›
instance by standard simp
end

lemma module_S_distr_share:
  ‹module_S_distr (share :: rat ⇒ 'a::share_semimodule ⇒ 'a) (λn. 0 ≤ n)›
  unfolding module_S_distr_def
  using share_disj_sdistr
  by (auto simp add: less_eq_rat_def share_sep_left_distrib )

lemma module_S_distr_share_0:
  ‹module_S_distr (share :: rat ⇒ 'a::share_nun_semimodule ⇒ 'a) (λn. 0 < n)›
  unfolding module_S_distr_def
  using share_disj_sdistr
  by (auto simp add: share_sep_left_distrib_0)



section ‹Instances of Algebras›

(*TODO: some structures like partial map contain many helper lemmas that
are not settled down properly.*)

subsection ‹Lambda Identity›

lemma simple_homo_mul_id[simp]:
  ‹1 ∈ D ⟹ simple_homo_mul (λx. x) D›
  unfolding simple_homo_mul_def
  by simp

lemma homo_one_id[simp, locale_intro]:
  ‹ homo_one (λx. x) ›
  unfolding homo_one_def
  by simp

lemma homo_mul_carrier_id[simp, locale_intro]:
  ‹homo_mul_carrier (λx. x)›
  unfolding homo_mul_carrier_def
  by blast

lemma homo_sep_disj_id[simp, locale_intro]:
  ‹homo_sep_disj (λx. x)›
  unfolding homo_sep_disj_def
  by simp

lemma closed_homo_sep_disj_id[simp, locale_intro]:
  ‹ closed_homo_sep_disj (λx. x) ›
  unfolding closed_homo_sep_disj_def
  by simp

lemma homo_sep_mult_id[simp, locale_intro]:
  ‹ homo_sep_mult (λx. x) ›
  unfolding homo_sep_mult_def
  by simp

lemma homo_sep_id[simp, locale_intro]:
  ‹homo_sep (λx. x)›
  unfolding homo_sep_def
  by simp

lemma closed_homo_sep_id[simp, locale_intro]:
  ‹ closed_homo_sep (λx. x) ›
  unfolding closed_homo_sep_def
  by simp

lemma homo_share_id[simp, locale_intro]:
  ‹ homo_share (λx. x) ›
  unfolding homo_share_def
  by blast

(*
lemma
  ‹ sep_orthogonal (λx. x) D ›
  unfolding sep_orthogonal_def sep_orthogonal_axioms_def
  by simp *)


subsection ‹Functional Composition›

text ‹Most of homomorphic properties have both identity rule and composition rule, forming them a sub-category.›

lemma simple_homo_mul_comp[simp]:
  ‹ g ` Dg ⊆ Df
⟹ simple_homo_mul f Df
⟹ simple_homo_mul g Dg
⟹ simple_homo_mul (f o g) Dg›
  unfolding simple_homo_mul_def
  by (simp add: image_subset_iff)

lemma homo_one_comp[simp, locale_intro]:
  ‹ homo_one f
⟹ homo_one g
⟹ homo_one (f o g) ›
  unfolding homo_one_def
  by simp

lemma homo_mul_carrier_comp[simp, locale_intro]:
  ‹ homo_mul_carrier g
⟹ homo_mul_carrier f
⟹ homo_mul_carrier (f o g)›
  unfolding homo_mul_carrier_def
  by clarsimp

lemma homo_sep_disj_comp[simp, locale_intro]:
  ‹ homo_sep_disj f
⟹ homo_sep_disj g
⟹ homo_sep_disj (f o g) ›
  unfolding homo_sep_disj_def
  by simp

lemma closed_homo_sep_disj_comp[simp, locale_intro]:
  ‹ closed_homo_sep_disj f
⟹ closed_homo_sep_disj g
⟹ closed_homo_sep_disj (f o g)›
  unfolding closed_homo_sep_disj_def
  by simp

lemma homo_sep_mult_comp[simp, locale_intro]:
  ‹ homo_sep_disj f
⟹ homo_sep_mult f
⟹ homo_sep_mult g
⟹ homo_sep_mult (g o f)›
  unfolding homo_sep_mult_def homo_sep_disj_def
  by clarsimp

lemma homo_sep_comp[simp, locale_intro]:
  ‹homo_sep f ⟹ homo_sep g ⟹ homo_sep (f o g)›
  unfolding homo_sep_mult_def homo_sep_disj_def homo_sep_def
  by simp

lemma closed_homo_sep_comp[simp, locale_intro]:
  ‹ closed_homo_sep f
⟹ closed_homo_sep g
⟹ closed_homo_sep (f o g)›
  unfolding closed_homo_sep_def
  by simp

lemma homo_share_comp[simp]:
  ‹ homo_share f
⟹ homo_share g
⟹ homo_share (f o g) ›
  unfolding homo_share_def
  by clarsimp

lemma sep_orthogonal_comp:
  ‹ g ` Dg ⊆ Df
⟹ sep_orthogonal f Df ⟹ sep_orthogonal g Dg ⟹ sep_orthogonal (f o g) Dg›
  unfolding sep_orthogonal_def sep_orthogonal_axioms_def
  by (clarsimp simp add: homo_sep_comp subset_iff image_iff Bex_def,
      smt (verit, ccfv_threshold) homo_sep.axioms(2) homo_sep_disj.sep_disj_homo_semi)

lemma sep_orthogonal_1_comp:
  ‹ g ` Dg ⊆ Df
⟹ sep_orthogonal_1 f Df ⟹ sep_orthogonal_1 g Dg ⟹ sep_orthogonal_1 (f o g) Dg›
  unfolding sep_orthogonal_1_def
  by (clarsimp simp add: homo_sep_comp subset_iff image_iff Bex_def,
      metis image_subsetI sep_orthogonal_comp)

lemma sep_orthogonal_monoid_comp[locale_intro]:
  ‹ g ` Dg ⊆ Df ⟹ sep_orthogonal_monoid f Df ⟹ sep_orthogonal_monoid g Dg ⟹ sep_orthogonal_monoid (f o g) Dg›
  unfolding sep_orthogonal_monoid_def using sep_orthogonal_1_comp .

lemma share_orthogonal_homo_composition[locale_intro]:
  assumes dom_trans: ‹g ` Dg ⊆ Df›
      and f: ‹share_orthogonal_homo f Df›
      and g: ‹sep_orthogonal_monoid g Dg›
    shows ‹share_orthogonal_homo (f o g) Dg›
proof -
  interpret f: share_orthogonal_homo f Df using f .
  interpret g: sep_orthogonal_monoid g Dg using g .
  have f': ‹sep_orthogonal_monoid f Df› by (simp add: f.sep_orthogonal_monoid_axioms)
  have g': ‹sep_orthogonal_monoid g Dg› by (simp add: g.sep_orthogonal_monoid_axioms)
  have t[simp]: ‹x ∈ Dg ⟹ g x ∈ Df› for x using dom_trans by blast 

  show ?thesis
    unfolding share_orthogonal_homo_def share_orthogonal_homo_axioms_def
    apply (auto simp add: f.share_orthogonal)
    apply (meson dom_trans f' g' sep_orthogonal_monoid_comp)
    using g.sep_orthogonal apply auto[1]
    using g.homo_mult apply auto[1]
    using f.share_bounded t apply blast
    using f.ψ_mul_carrier t by blast 

qed


subsection ‹Option›

instantiation option :: (times) times begin
definition "times_option x' y' =
  (case x' of Some x ⇒ (case y' of Some y ⇒ Some (x * y) | _ ⇒ x')
      | None ⇒ y')"

lemma times_option[simp]:
  "Some x * Some y = Some (x * y)"
  "x' * None = x'"
  "None * x' = x'"
  by (cases x', simp_all add: times_option_def)+

lemma times_option_not_none[simp]:
  ‹x * Some y ≠ None›
  ‹Some y * x ≠ None›
  by (cases x; simp)+

instance ..
end

instantiation option :: (plus) plus begin
definition ‹plus_option x' y' = (case x' of Some x ⇒ (case y' of Some y ⇒ Some (x + y) | _ ⇒ x') | _ ⇒ y')›

lemma plus_option[simp]:
  ‹Some x + Some y = Some (x + y)›
  ‹x' + None = x'›
  ‹None + x' = x'›
  by (cases x'; simp add: plus_option_def)+

lemma plus_option_not_none[simp]:
  ‹x + Some y ≠ None›
  ‹Some y + x ≠ None›
  by (cases x; simp)+

instance ..
end

instantiation option :: (type) one begin
definition [simp]: "one_option = None"
instance ..
end

instantiation option :: (type) zero begin
definition [simp]: "zero_option = None"
instance ..
end

instantiation option :: (times) mult_1 begin
instance proof
  fix x :: ‹'a option›
  show ‹1 * x = x› by (cases x; simp)
  show ‹x * 1 = x› by (cases x; simp)
qed
end

instantiation option :: (plus) add_0 begin
instance proof
  fix x :: ‹'a option›
  show ‹0 + x = x› by (cases x; simp)
  show ‹x + 0 = x› by (cases x; simp)
qed
end

instantiation option :: (sep_disj) sep_disj begin

definition "sep_disj_option x' y' =
  (case x' of Some x ⇒ (case y' of Some y ⇒ x ## y | None ⇒ True) | _ ⇒ True)"

lemma sep_disj_option[simp]:
    "Some x ## Some y ⟷ x ## y"
    "None ## z"
    "z ## None"
  unfolding sep_disj_option_def
  apply simp by (cases z; simp)+

instance ..
end

lemma sep_disj_option_discrete[simp]:
  ‹x ## Some y ⟷ x = None›
  ‹Some y ## x ⟷ x = None›
  for y :: ‹'a :: discrete_semigroup›
  by (cases x; simp)+

instantiation option :: (comm_sep_disj) comm_sep_disj begin
instance apply (standard; case_tac x; case_tac y; simp)
  using sep_disj_commute by blast
end

instance option :: ("{sep_disj,times}") sep_magma ..

instance option :: ("{sep_disj,times}") sep_magma_1 proof
  fix x y :: ‹'a option›
  show ‹x ## 1› by simp
  show ‹1 ## x› by simp
qed

instantiation option :: (mul_carrier) mul_carrier begin

definition mul_carrier_option :: ‹'a option ⇒ bool›
  where ‹mul_carrier_option = pred_option mul_carrier ›

lemma mul_carrier_option[simp]:
  ‹mul_carrier None›
  ‹mul_carrier (Some x) ⟷ mul_carrier x›
  unfolding mul_carrier_option_def
  by simp_all

instance ..

end

instance option :: (sep_carrier) sep_carrier
  by (standard; case_tac a; case_tac b; simp add: mul_carrier_closed)

instance option :: (positive_sep_magma) positive_sep_magma_1 proof
  fix x y :: ‹'a option›
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    unfolding join_sub_def
    apply (cases x; clarsimp simp add: sep_disj_commute sep_mult_commute;
           cases y; clarsimp simp add: sep_disj_commute sep_mult_commute)
    apply (metis times_option_not_none(2))
     apply (metis times_option_not_none(2))
    apply (auto simp add: sep_disj_option_def split: option.split)
    subgoal for _ u v _ apply (cases u; cases v; simp)
      by (metis join_positivity join_sub_def) .
qed

instance option :: (sep_carrier) sep_carrier_1 by (standard; simp)

instance option :: (sep_semigroup) sep_monoid proof
  fix x y z :: ‹'a option›
  show ‹x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)›
    by (cases x; cases y; cases z; simp add: sep_disj_commute sep_mult_commute sep_mult_assoc)
  show ‹x ## y * z ⟹ y ## z ⟹ x ## y›
    apply (cases x; simp; cases y; simp; cases z; simp)
    using sep_disj_multD1 by blast
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z›
    apply (cases x; simp; cases y; simp; cases z; simp)
    using sep_disj_multI1 by blast
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z›
    apply (cases x; simp; cases y; simp; cases z; simp)
    using sep_disj_multD2 by blast
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z›
    apply (cases x; simp; cases y; simp; cases z; simp)
    using sep_disj_multI2 by blast
qed

instance option :: ("{strict_positive_sep_magma,sep_cancel}") sep_cancel
  apply (standard)
  apply (case_tac a; case_tac b; case_tac c; simp)
  using join_strict_positivity apply blast
  using join_strict_positivity apply fastforce
  using sep_cancel by blast

instance option :: (sep_ab_semigroup) sep_algebra proof
  fix x y z :: ‹'a option›
  show ‹x ## y ⟹ x * y = y * x› by (cases x; cases y; simp add: sep_disj_commute sep_mult_commute)
qed

instance option :: (discrete_semigroup) discrete_monoid
  by (standard; case_tac x; case_tac y; simp)

instantiation option :: (raw_share) raw_share begin
definition ‹share_option n = (if 0 < n then map_option (share n) else (λ_. None))›
instance ..
end

lemma share_option_simps[simp]:
  ‹share n None = None› ‹share 0 x = None› ‹0 < n ⟹ share n (Some x') = Some (share n x')›
  unfolding share_option_def by simp_all

instance option :: (share) share 
  by (standard; simp add: share_option_def; case_tac x; simp add: share_share_assoc0)

instance option :: (share_inj) share_inj
  by (standard; case_tac x; case_tac y; simp)

instance option :: (sep_disj_distrib) sep_disj_distrib proof
  fix a b c :: ‹'a option›
  show ‹b ## c ⟹ a ## b * c = (a ## b ∧ a ## c)› by (cases a; cases b; cases c; simp)
  show ‹a ## b ⟹ a * b ## c = (a ## c ∧ b ## c)› by (cases a; cases b; cases c; simp)
qed

instantiation option :: (share) share_one_eq_one_iff begin
instance by (standard; simp add: share_option_def; case_tac x; simp)
end

instance option :: (share_sep_disj) share_sep_disj
  by (standard; case_tac x; simp add: share_disj_sdistr;
                case_tac y; simp)

instantiation option :: (share_nun_semimodule) share_semimodule begin
instance proof
  fix n m :: rat
  fix x y :: ‹'a option›
  show ‹0 ≤ n ⟹ 0 ≤ m ⟹ mul_carrier x ⟹ share n x * share m x = share (n + m) x›
    by (case_tac x; clarsimp simp add: share_option_def share_sep_left_distrib_0 order_less_le)
  show ‹0 ≤ n ⟹ x ## y ⟹ share n x * share n y = share n (x * y)›
    by (case_tac x; case_tac y; clarsimp simp add: share_option_def share_sep_right_distrib_0)
  show ‹0 ≤ n ⟹ mul_carrier x ⟹ mul_carrier (n ⦼ x)›
    by (cases ‹n=0›; cases x; simp add: share_carrier_closed)
  show ‹0 ≤ n ∧ n ≤ 1 ⟹ mul_carrier x ⟹ share n x ≼⇩S⇩L x›
    unfolding join_sub_def apply (cases x; clarsimp simp add: share_option_def)
    apply (cases ‹n = 1›)
    apply (metis mult_1_class.mult_1_right sep_magma_1_left share_left_one)
    apply (cases ‹n = 0›, simp)
    subgoal premises prems for x'
    proof -
      have t1: ‹share n x' ≼⇩S⇩L x' ∨ share n x' = x'›
        by (meson antisym_conv2 prems(1) prems(3) prems(4) prems(5) share_sub_0)
      show ?thesis apply (insert t1)
        unfolding join_sub_def apply (elim disjE; clarsimp)
        apply (metis sep_disj_option(1) times_option(1))
        by (metis sep_disj_option(3) times_option(2))
    qed .
qed
end

instance option :: ("{sep_disj,times}") sep_no_inverse 
  by (standard; case_tac x; case_tac y; simp)

lemma times_option_none[simp]:
  ‹x * y = None ⟷ x = None ∧ y = None›
  by (simp add: option.case_eq_if times_option_def)

lemma Some_discrete_semigroup_sub_join[simp]:
  ‹Some x ≼⇩S⇩L X ⟷ X = Some x›
  for x :: ‹'a::discrete_semigroup›
  by (simp add: join_sub_def)


instantiation option :: (ab_semigroup_mult) comm_monoid_mult begin
instance apply (standard)
    apply (case_tac a; case_tac b; case_tac c; simp add: mult.assoc)
   apply (case_tac a; case_tac b; simp add: mult.commute)
  apply (case_tac a; simp) .
end

subsubsection ‹Homomorphism›

lemma homo_one_map_option[simp]:
  ‹homo_one (map_option f)›
  unfolding homo_one_def by simp

lemma simple_homo_mul_map_option[simp]:
  ‹simple_homo_mul (map_option f) UNIV›
  unfolding simple_homo_mul_def
  by simp

lemma homo_mul_carrier_map_option[simp]:
  ‹ homo_mul_carrier f
⟹ homo_mul_carrier (map_option f)›
  unfolding homo_mul_carrier_def
  by (clarsimp simp add: split_option_all)

lemma homo_sep_disj_map_option[simp]:
  ‹ homo_sep_disj f
⟹ homo_sep_disj (map_option f) ›
  unfolding homo_sep_disj_def
  by (clarsimp simp add: split_option_all)

lemma closed_homo_sep_disj_map_option[simp]:
  ‹ closed_homo_sep_disj f
⟹ closed_homo_sep_disj (map_option f) ›
  unfolding closed_homo_sep_disj_def
  by (clarsimp simp add: split_option_all)

lemma homo_sep_mult_map_option[simp]:
  ‹ homo_sep_mult f
⟹ homo_sep_mult (map_option f)  ›
  unfolding homo_sep_mult_def
  by (clarsimp simp add: split_option_all)

lemma homo_sep_map_option[simp]:
  ‹ homo_sep f
⟹ homo_sep (map_option f)  ›
  unfolding homo_sep_def
  by (clarsimp simp add: split_option_all)

lemma closed_homo_sep_map_option[simp, locale_intro]:
  ‹ closed_homo_sep f
⟹ closed_homo_sep (map_option f) ›
  unfolding closed_homo_sep_def
  by (clarsimp simp add: split_option_all)

lemma homo_share_map_option[simp]:
  ‹ homo_share ψ
⟹ homo_share (map_option ψ) ›
  unfolding homo_share_def
  by (clarsimp simp add: split_option_all share_option_def)

lemma homo_mult_map_option:
  ‹ homo_mult f
⟹ homo_mult (map_option f) ›
  unfolding homo_mult_def
  by (clarify; case_tac x; case_tac y; auto)

subsection ‹Product›

subsubsection ‹Auxiliary›

instantiation prod :: (one, one) one begin
definition "one_prod = (1,1)"
instance ..
end

instance prod :: (numeral, numeral) numeral ..

instantiation prod :: (divide, divide) divide begin
definition divide_prod :: ‹'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b› where
  ‹divide_prod x y = (fst x div fst y, snd x div snd y)›
instance ..
end


subsubsection ‹Total Algebras›

instantiation prod :: (times, times) times begin
definition "times_prod = (λ(x1,x2) (y1,y2). (x1 * y1, x2 * y2))"
lemma times_prod[simp]: "(x1,x2) * (y1,y2) = (x1 * y1, x2 * y2)"
  unfolding times_prod_def by simp
instance ..
end

lemma fst_one [simp]: "fst 1 = 1"
  unfolding one_prod_def by simp

lemma snd_one [simp]: "snd 1 = 1"
  unfolding one_prod_def by simp

instantiation prod :: (mult_zero, mult_zero) mult_zero begin
instance by (standard, simp_all add: zero_prod_def split_paired_all)
end

instantiation prod :: (semigroup_mult, semigroup_mult) semigroup_mult begin
instance by standard (simp_all add: split_paired_all algebra_simps)
end

instance prod :: (mult_1, mult_1) mult_1
  by (standard; simp add: one_prod_def split_paired_all)


instance prod :: (monoid_mult, monoid_mult) monoid_mult
  by standard (simp_all add: one_prod_def split_paired_all algebra_simps)

instance prod :: (no_inverse, no_inverse) no_inverse
  by (standard, simp add: one_prod_def times_prod_def split: prod.split) blast

instance prod :: (no_negative, no_negative) no_negative
  by (standard, simp add: zero_prod_def plus_prod_def split_paired_all split: prod.split, blast)

instance prod :: (ab_semigroup_mult, ab_semigroup_mult) ab_semigroup_mult
  by (standard, metis mult.commute prod.collapse times_prod)

instance prod :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult by standard simp

instance prod :: (semiring, semiring) semiring
 by (standard, simp_all add: split_paired_all distrib_right distrib_left)

instance prod :: (semiring_0, semiring_0) semiring_0 ..

instance prod :: (comm_semiring, comm_semiring) comm_semiring
 by (standard, simp add: split_paired_all comm_semiring_class.distrib)

instance prod :: (semiring_0_cancel, semiring_0_cancel) semiring_0_cancel ..

instance prod :: (ring, ring) ring ..

instance prod :: (comm_ring, comm_ring) comm_ring ..


subsubsection ‹Partial Algebras›

instantiation prod :: (sep_disj,sep_disj) sep_disj begin
definition ‹sep_disj_prod x y = (case x of (x1,x2) ⇒ case y of (y1,y2) ⇒ x1 ## y1 ∧ x2 ## y2)›
lemma sep_disj_prod[simp]:
  ‹(x1,y1) ## (x2,y2) ⟷ x1 ## x2 ∧ y1 ## y2›
  unfolding sep_disj_prod_def by simp
instance ..
end

instance prod :: (sep_magma,sep_magma) sep_magma ..


instantiation prod :: (mul_carrier, mul_carrier) mul_carrier  begin

definition mul_carrier_prod :: ‹'a × 'b ⇒ bool›
  where ‹mul_carrier_prod = pred_prod mul_carrier mul_carrier›

lemma mul_carrier_prod[simp]:
  ‹ mul_carrier (x,y) ⟷ mul_carrier x ∧ mul_carrier y ›
  unfolding mul_carrier_prod_def by simp

instance ..

end

instance prod :: (sep_carrier, sep_carrier) sep_carrier
  by (standard; clarsimp simp add: mul_carrier_closed)

instance prod :: (sep_magma_1, sep_magma_1) sep_magma_1
  by (standard; simp add: one_prod_def split_paired_all)

instance prod :: (sep_carrier_1, sep_carrier_1) sep_carrier_1
  by (standard; simp add: one_prod_def)

instance prod :: (sep_no_inverse, sep_no_inverse) sep_no_inverse
  by (standard, simp add: one_prod_def times_prod_def split: prod.split) force

instance prod :: (sep_cancel,sep_cancel) sep_cancel
  by (standard; case_tac a; case_tac b; case_tac c; simp; meson sep_cancel)

instance prod :: (sep_disj_distrib,sep_disj_distrib) sep_disj_distrib
  by (standard; case_tac a; case_tac b; case_tac c; simp; blast)


instance prod :: (zero_neq_one, zero_neq_one) zero_neq_one
  by (standard, simp add: zero_prod_def one_prod_def)

instance prod :: (semiring_1, semiring_1) semiring_1 ..

instance prod :: (ring_1, ring_1) ring_1 ..

instantiation prod :: (comm_ring_1, comm_ring_1) comm_ring_1 begin
instance ..
end



instantiation prod :: (inverse, inverse) inverse begin
definition inverse_prod :: ‹'a × 'b ⇒ 'a × 'b› where
  ‹inverse_prod x = (case x of (a,b) ⇒ (inverse a, inverse b))›
instance ..
end

subsubsection ‹Order›

instantiation prod :: (ord, ord) ord begin
definition less_eq_prod :: ‹'a × 'b ⇒ 'a × 'b ⇒ bool›
  where ‹less_eq_prod x y ⟷ fst x ≤ fst y ∧ snd x ≤ snd y›
definition less_prod :: ‹'a × 'b ⇒ 'a × 'b ⇒ bool›
  where ‹less_prod x y ⟷ fst x < fst y ∧ snd x < snd y›

lemma [simp]: ‹(x1,x2) < (y1,y2) ⟷ x1 < y1 ∧ x2 < y2› unfolding less_prod_def by simp
lemma [simp]: ‹(x1,x2) ≤ (y1,y2) ⟷ x1 ≤ y1 ∧ x2 ≤ y2› unfolding less_eq_prod_def by simp

instance ..
end

lemma less_eq_prod:
  ‹a ≤ b ⟷ fst a ≤ fst b ∧ snd a ≤ snd b›
  by (cases a; cases b; simp)

lemma less_prod:
  ‹a < b ⟷ fst a < fst b ∧ snd a < snd b›
  by (cases a; cases b; simp)

instance prod :: (add_order_0, add_order_0) add_order_0
  by (standard; case_tac a; case_tac b; simp add: zero_prod_def add_nonneg_nonneg add_pos_pos)


subsection ‹Coproduct›

instantiation sum :: (times, times) times begin
definition times_sum :: ‹'a + 'b ⇒ 'a + 'b ⇒ 'a + 'b›
  where "times_sum = (λx y. case x of Inl x1 ⇒ (case y of Inl y1 ⇒ Inl (x1 * y1))
                                    | Inr x2 ⇒ (case y of Inr y2 ⇒ Inr (x2 * y2)))"
lemma times_sum:
  ‹Inl x1 * Inl y1 = Inl (x1 * y1)›
  ‹Inr x2 * Inr y2 = Inr (x2 * y2)›
  unfolding times_sum_def by simp_all
instance ..
end

instantiation sum :: (plus, plus) plus begin
definition plus_sum :: ‹'a + 'b ⇒ 'a + 'b ⇒ 'a + 'b›
  where "plus_sum = (λx y. case x of Inl x1 ⇒ (case y of Inl y1 ⇒ Inl (x1 + y1))
                                   | Inr x2 ⇒ (case y of Inr y2 ⇒ Inr (x2 + y2)))"
lemma plus_sum[simp]:
  ‹Inl x1 + Inl y1 = Inl (x1 + y1)›
  ‹Inr x2 + Inr y2 = Inr (x2 + y2)›
  unfolding plus_sum_def by simp_all
instance ..
end




subsection ‹List›

text ‹We always follow the order of associativity. The list appending is right associative,
  meaning the new elements are at left, and multiplication is left associative where
  new elements are at the right, so here there is a reverse between the multiplication of list
  and concatenation.›

instantiation list :: (type) times begin
definition "times_list a b = a @ b"
instance ..
end

instantiation list :: (type) plus begin
definition [simp]: "plus_list a b = a @ b"
instance ..
end

instantiation list :: (type) zero begin
definition [simp]: "zero_list = []"
instance ..
end

instantiation list :: (type) one begin
definition [simp]: "one_list = []"
instance ..
end

instance list :: (type) no_inverse by (standard, simp add: times_list_def)

instance list :: (type) no_negative by (standard, simp add: plus_list_def)

instance list :: (type) semigroup_mult by standard (simp_all add: times_list_def)

instance list :: (type) semigroup_add by standard (simp_all add: plus_list_def)

instance list :: (type) monoid_mult by standard (simp_all add: times_list_def)

instance list :: (type) monoid_add by standard (simp_all add: plus_list_def)

instantiation list :: (type) sep_magma begin
definition sep_disj_list :: ‹'a list ⇒ 'a list ⇒ bool›
  where [simp]: ‹sep_disj_list _ _ = True›
instance by (standard; simp)
end

instantiation list :: (mul_carrier) mul_carrier begin

definition mul_carrier_list :: ‹'a list ⇒ bool›
  where [simp]: ‹mul_carrier_list = list_all mul_carrier›

instance ..
end

instance list :: (sep_carrier) sep_carrier
  by (standard; simp add: times_list_def)

instance list :: (type) sep_monoid
  by (standard; clarsimp simp add: times_list_def join_sub_def)

instance list :: (sep_carrier_1) sep_carrier_1
  by (standard; simp add: times_list_def)

instance list :: (type) sep_disj_distrib by (standard; simp)

instance list :: (type) sep_cancel
  by (standard; simp add: times_list_def)


subsection ‹Function›

subsubsection ‹Instantiations of Algebra›

paragraph ‹Basics›

instantiation "fun" :: (type,plus) plus begin
definition "plus_fun f g = (λx. f x + g x)"
instance ..
end

instantiation "fun" :: (type,times) times begin
definition "times_fun f g = (λx. f x * g x)"
instance ..
end

lemma times_fun: "(f * g) x = f x * g x"
  unfolding times_fun_def by simp

lemma plus_fun: "(f + g) x = f x + g x"
  unfolding plus_fun_def by simp

instantiation "fun" :: (type,zero) zero begin
definition "zero_fun = (λ(x::'a). (0::'b))"
instance ..
end

instantiation "fun" :: (type,one) one begin
definition "one_fun = (λ(x::'a). (1::'b))"
instance ..
end

lemma one_fun[simp]: "1 x = 1" unfolding one_fun_def by simp
lemma zero_fun[simp]: "0 x = 0" unfolding zero_fun_def by simp
lemmas zero_fun_eta = zero_fun_def[symmetric]

lemma fun_updt_1_1[simp]:
  ‹1(x := 1) = 1›
  unfolding fun_eq_iff by simp

lemma fun_updt_0_0[simp]:
  ‹0(x := 0) = 0›
  unfolding fun_eq_iff by simp


paragraph ‹Partial Multiplicative Algebras›

instance "fun" :: (type, no_inverse) no_inverse
  by (standard, simp add: one_fun_def times_fun fun_eq_iff, blast)

instance "fun" :: (type, no_negative) no_negative
  by (standard, simp del: zero_fun_eta add: zero_fun_def plus_fun fun_eq_iff, blast)

instance "fun" :: (type, semigroup_mult) semigroup_mult
  by (standard; simp add: mult.assoc times_fun_def)

instantiation "fun" :: (type,sep_disj) sep_disj begin
definition "sep_disj_fun m1 m2 = (∀x. m1 x ## m2 x)"
instance ..
end

instance "fun" :: (type,comm_sep_disj) comm_sep_disj
  by (standard, simp_all add: sep_disj_fun_def times_fun fun_eq_iff
                         add: sep_disj_commute sep_mult_commute )

lemma sep_disj_fun[simp]: ‹(f ## g) ⟹ f x ## g x›
  unfolding sep_disj_fun_def by blast

lemma sep_disj_fun_discrete:
  ‹f x = Some v ⟹ f ## g ⟹ g x = None›
  ‹f x = Some v ⟹ g ## f ⟹ g x = None›
  for v :: ‹'a :: discrete_semigroup›
  by (metis sep_disj_fun sep_disj_option_discrete)+


instance "fun" :: (type,mult_1) mult_1
  by (standard; simp add: one_fun_def times_fun_def)

instance "fun" :: (type,sep_magma) sep_magma ..

instance "fun" :: (type,sep_magma_1) sep_magma_1
 by (standard; simp add: sep_disj_fun_def)

instantiation "fun" :: (type, mul_carrier) mul_carrier begin

definition mul_carrier_fun :: ‹('a ⇒ 'b) ⇒ bool›
  where ‹mul_carrier_fun = (λf. ∀k. mul_carrier (f k))›

lemma mul_carrier_fun[simp]: ‹mul_carrier f = (∀k. mul_carrier (f k))›
  unfolding mul_carrier_fun_def ..

instance ..
end

instance "fun" :: (type, sep_carrier) sep_carrier
  by (standard; simp add: times_fun mul_carrier_closed)

instance "fun" :: (type, sep_carrier_1) sep_carrier_1
  by (standard; simp)

instance "fun" :: (type, sep_cancel) sep_cancel
  apply (standard; simp add: fun_eq_iff times_fun sep_disj_fun_def)
  using sep_cancel by blast

instance "fun" :: (type, sep_no_inverse) sep_no_inverse
  by (standard; simp add: one_fun_def fun_eq_iff times_fun; blast)

instance "fun" :: (type, sep_semigroup) sep_semigroup proof
  fix x y z :: "'a ⇒ 'b"
  show ‹x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)›
    apply (simp add: sep_disj_fun_def times_fun_def fun_eq_iff)
    using sep_mult_assoc by blast
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    unfolding join_sub_def apply (clarsimp simp add: times_fun fun_eq_iff)
    by (metis join_positivity join_sub_def sep_disj_fun)
  show ‹x ## y * z ⟹ y ## z ⟹ x ## y›
    apply (simp add: sep_disj_fun_def times_fun_def fun_eq_iff)
    using sep_disj_multD1 by blast
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z›
    apply (simp add: sep_disj_fun_def times_fun_def fun_eq_iff)
    using sep_disj_multI1 by blast
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z›
    apply (simp add: sep_disj_fun_def times_fun_def fun_eq_iff)
    using sep_disj_multD2 by blast
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z›
    apply (simp add: sep_disj_fun_def times_fun_def fun_eq_iff)
    using sep_disj_multI2 by blast
qed

instance "fun" :: (type,sep_ab_semigroup) sep_ab_semigroup proof
  fix x y z :: "'a ⇒ 'b"
  show ‹x ## y ⟹ x * y = y * x›
    by (simp add: sep_disj_fun_def times_fun_def fun_eq_iff sep_disj_commute sep_mult_commute)
qed

instance "fun" :: (type, sep_monoid) sep_monoid
  by (standard; simp add: sep_disj_fun_def fun_eq_iff times_fun_def; blast)

instance "fun" :: (type, sep_algebra) sep_algebra
  by (standard; simp add: sep_disj_fun_def fun_eq_iff times_fun_def; blast)

instance "fun" :: (type, sep_disj_distrib) sep_disj_distrib
  by (standard; simp add: sep_disj_fun_def times_fun; blast)

instance "fun" :: (type,monoid_mult) monoid_mult
  by standard (simp_all add: mult.commute times_fun_def fun_eq_iff)

instance "fun" :: (type,comm_monoid_mult) comm_monoid_mult
  by standard (simp_all add: mult.commute times_fun_def fun_eq_iff)

instance "fun" :: (type,monoid_add) monoid_add proof
  fix a b c :: ‹'a ⇒ 'b›
  show ‹a + b + c = a + (b + c)› unfolding plus_fun_def fun_eq_iff by (simp add: add.assoc)
  show ‹0 + a = a› unfolding plus_fun_def fun_eq_iff by (simp add: add.assoc)
  show ‹a + 0 = a› unfolding plus_fun_def fun_eq_iff by (simp add: add.assoc)
qed

instance "fun" :: (type,comm_monoid_add) comm_monoid_add proof
  fix a b :: ‹'a ⇒ 'b›
  show ‹a + b = b + a› unfolding plus_fun_def fun_eq_iff using add.commute by blast
  show ‹0 + a = a› unfolding plus_fun_def fun_eq_iff by simp
qed


subsubsection ‹Properties›

definition ‹pointwise_set D = {f. ∀ k. f k ∈ D}›


subsubsection ‹Multiplication with Function Update›

lemma times_fupdt_1_apply[simp]:
  "(1(k := x) * f) k = x * f k" for f :: "'a ⇒ 'b::monoid_mult"
  by (simp add: times_fun_def)

lemma times_fupdt_1_apply_sep[simp]:
  "(1(k := x) * f) k = x * f k" for f :: "'a ⇒ 'b::sep_monoid"
  by (simp add: times_fun_def)

lemma times_fupdt_1_apply'[simp]:
  "k' ≠ k ⟹ (1(k':=x) * f) k = f k" for f :: "'a ⇒ 'b::monoid_mult"
  by (simp add: times_fun_def)

lemma times_fupdt_1_apply'_sep[simp]:
  "k' ≠ k ⟹ (1(k':=x) * f) k = f k" for f :: "'a ⇒ 'b::sep_monoid"
  by (simp add: times_fun_def)

lemma times_fupdt_1_fupdt_1[simp]:
  "(1(k := x) * f)(k:=1) = f(k:=1)" for f :: "'a ⇒ 'b::monoid_mult"
  unfolding fun_upd_def fun_eq_iff times_fun_def by simp

lemma times_fupdt_1_fupdt_1_sep[simp]:
  "(1(k := x) * f)(k:=1) = f(k:=1)" for f :: "'a ⇒ 'b::sep_monoid"
  unfolding fun_upd_def fun_eq_iff times_fun_def by simp

lemma [simp]:
  "k' ≠ k ⟹ (1(k' := x) * f)(k:=1) = 1(k' := x) * f(k:=1)" for f :: "'a ⇒ 'b::monoid_mult"
  unfolding fun_upd_def fun_eq_iff times_fun_def by simp

lemma [simp]:
  "k' ≠ k ⟹ (1(k' := x) * f)(k:=1) = 1(k' := x) * f(k:=1)" for f :: "'a ⇒ 'b::sep_monoid"
  unfolding fun_upd_def fun_eq_iff times_fun_def by simp

instantiation "fun" :: (type,total_sep_monoid) total_sep_monoid begin
instance proof
  fix x y :: ‹'a ⇒ 'b›
  show ‹x ≼⇩× y ⟹ y ≼⇩× x ⟹ x = y›
    unfolding subsume_def apply (clarsimp simp add: times_fun_def fun_eq_iff)
    using positive_mult_class.positive_mult subsume_def by blast
  show ‹x ## y› by (simp add: sep_disj_fun_def)
qed
end

instantiation "fun" :: (type,total_sep_algebra) total_sep_algebra begin
instance ..
end


lemma fun_split_1: "f = 1(k:= f k) * f(k:=1)" for f :: "'a ⇒ 'b :: mult_1"
  unfolding fun_upd_def fun_eq_iff times_fun_def by simp

lemma fun_1upd1[simp]:
  "1(k := 1) = 1"
  unfolding one_fun_def fun_upd_def by simp

lemma fun_1upd_homo:
    "1(k := x) * 1(k := y) = 1(k := x * y)" for x :: "'a::sep_magma_1"
  unfolding one_fun_def fun_upd_def times_fun_def
  by fastforce

lemma fun_1upd_homo_right1:
    "f(k := x) * 1(k := y) = f(k := x * y)" for x :: "'a::sep_magma_1"
  unfolding one_fun_def fun_upd_def times_fun_def fun_eq_iff
  by clarsimp

lemma fun_1upd_homo_left1:
    "1(k := x) * f(k := y) = f(k := x * y)" for x :: "'a::sep_magma_1"
  unfolding one_fun_def fun_upd_def times_fun_def fun_eq_iff
  by clarsimp

lemma [simp]: "NO_MATCH (a::'a) (1::'a::one) ⟹ i ≠ k ⟹ f(i := a, k := 1) = f(k := 1, i := a)"
  using fun_upd_twist .


subsubsection ‹Share›

instantiation "fun" :: (type, raw_share) raw_share begin

definition share_fun :: ‹rat ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b›
  where ‹share_fun n f = share n o f›

instance ..
end

instance "fun" :: (type, share) share
  by (standard; simp add: share_fun_def fun_eq_iff share_share_assoc0)

instance "fun" :: (type, share_inj) share_inj
  by (standard; simp add: share_fun_def fun_eq_iff)

instance "fun" :: (type,share_one) share_one
  by (standard; simp add: share_fun_def fun_eq_iff)

instance "fun" :: (type,share_one_eq_one_iff) share_one_eq_one_iff
  by (standard; simp add: share_fun_def fun_eq_iff)

instance "fun" :: (type, share_sep_disj) share_sep_disj
  by (standard; simp add: share_fun_def fun_eq_iff sep_disj_fun_def share_disj_sdistr)

instance "fun" :: (type, share_semimodule) share_semimodule
proof
  fix n m :: rat
  and x y :: ‹'a ⇒ 'b›
  show ‹0 ≤ n ⟹ mul_carrier x ⟹ mul_carrier (n ⦼ x)›
    by (clarsimp simp add: share_fun_def share_carrier_closed_1)
  show ‹0 ≤ n ⟹ 0 ≤ m ⟹ mul_carrier x ⟹ n ⦼ x * m ⦼ x = (n + m) ⦼ x›
    by (clarsimp simp add: share_fun_def fun_eq_iff times_fun_def share_sep_left_distrib)
  show ‹0 ≤ n ⟹ x ## y ⟹ n ⦼ x * n ⦼ y = n ⦼ (x * y)›
    by (clarsimp simp add: share_fun_def fun_eq_iff times_fun_def share_sep_right_distrib)
  have t1: ‹0 ≤ n ∧ n ≤ 1 ⟹ ∀k. mul_carrier (x k) ⟹ ∀a. share n (x a) ≼⇩S⇩L (x a)›
    using share_sub by blast
  then show ‹0 ≤ n ∧ n ≤ 1 ⟹ mul_carrier x ⟹ n ⦼ x ≼⇩S⇩L x›
    by (clarsimp simp add: join_sub_def share_fun_def fun_eq_iff times_fun_def sep_disj_fun_def; metis)
qed

lemma share_fun_updt[simp]:
  ‹share n (f(k := v)) = (share n f)(k := share n v)›
  unfolding share_fun_def fun_eq_iff by simp


subsubsection ‹Homomorphisms›

lemma homo_add_funcomp[locale_intro]:
  assumes hom_f: ‹homo_add f›
  shows ‹homo_add ((o) f)›
proof -
  interpret f: homo_add f using hom_f .
  show ?thesis by (standard; simp add: fun_eq_iff plus_fun f.homo_add)
qed

lemma homo_zero_funcomp[locale_intro]:
  assumes hom_f: ‹homo_zero f›
  shows ‹homo_zero ((o) f)›
proof -
  interpret f: homo_zero f using hom_f .
  show ?thesis by (standard; simp add: fun_eq_iff)
qed

lemma homo_mult_funcomp[locale_intro]:
  assumes hom_f: ‹homo_mult f›
  shows ‹homo_mult ((o) f)›
proof -
  interpret f: homo_mult f using hom_f .
  show ?thesis by (standard; simp add: fun_eq_iff times_fun f.homo_mult)
qed

lemma homo_one_funcomp[simp, locale_intro]:
  assumes hom_f: ‹homo_one f›
  shows ‹homo_one ((o) f)›
proof -
  interpret f: homo_one f using hom_f .
  show ?thesis by (standard; simp add: fun_eq_iff)
qed

lemma simple_homo_mul_funcomp[simp]:
  ‹ simple_homo_mul f D
⟹ simple_homo_mul ((o) f) (pointwise_set D)›
  unfolding simple_homo_mul_def pointwise_set_def
  by (clarsimp simp add: Ball_def fun_eq_iff)

lemma homo_mul_funcomp[simp, locale_intro]:
  ‹ homo_mul_carrier f
⟹ homo_mul_carrier ((o) f) ›
  unfolding homo_mul_carrier_def
  by clarsimp

lemma homo_sep_disj_funcomp[simp, locale_intro]:
  ‹ homo_sep_disj f
⟹ homo_sep_disj ((o) f) ›
  unfolding homo_sep_disj_def
  by (clarsimp simp add: sep_disj_fun_def)

lemma closed_homo_sep_disj_funcomp[simp, locale_intro]:
  ‹ closed_homo_sep_disj f
⟹ closed_homo_sep_disj ((o) f) ›
  unfolding closed_homo_sep_disj_def
  by (clarsimp simp add: sep_disj_fun_def)

lemma homo_sep_mult_funcomp[simp, locale_intro]:
  ‹ homo_sep_mult f
⟹ homo_sep_mult ((o) f) ›
  unfolding homo_sep_mult_def
  by (clarsimp simp add: fun_eq_iff times_fun_def)

lemma homo_sep_funcomp[simp, locale_intro]:
  ‹ homo_sep f
⟹ homo_sep ((o) f) ›
  unfolding homo_sep_def
  by (clarsimp simp add: fun_eq_iff times_fun_def)

lemma closed_homo_sep_funcomp[simp, locale_intro]:
  ‹ closed_homo_sep f
⟹ closed_homo_sep ((o) f) ›
  unfolding closed_homo_sep_def
  by (clarsimp simp add: fun_eq_iff times_fun_def)

lemma (in homo_zero) fun_updt_single_point[simp]:
  ‹φ o 0(i := x) = 0(i := φ x)›
  unfolding fun_eq_iff by simp

lemma fun_updt_single_point[simp]:
  ‹homo_one φ ⟹ φ o 1(i := x) = 1(i := φ x)›
  unfolding fun_eq_iff homo_one_def by simp

lemma homo_share_funcomp[simp]:
  ‹ homo_share ψ
⟹ homo_share ((o) ψ)›
  unfolding homo_share_def
  by (clarsimp simp add: fun_eq_iff share_fun_def)


subsection ‹Finite Map›

instantiation fmap :: (type,times) times begin
context includes fmap.lifting begin
lift_definition times_fmap :: ‹('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap› is "(λf g x. (f x::'b option) * g x)"
  by (simp add: dom_def)
instance ..
end
end

context includes fmap.lifting begin
lemma times_fmlookup[simp]:
  ‹fmlookup (f * g) x = fmlookup f x * fmlookup g x› by (transfer; simp)
end

instantiation "fmap" :: (type,type) one begin
definition one_fmap :: ‹('a, 'b) fmap›
  where [iff]: ‹one_fmap = fmempty›
instance ..
end

lemma one_fmap[simp]: "fmlookup 1 x = 1" including fmap.lifting by (transfer; simp)

instantiation fmap :: (type,sep_disj) sep_disj begin
context includes fmap.lifting begin
lift_definition sep_disj_fmap :: ‹('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ bool›
  is "λm1 m2. (∀x. m1 x ## m2 x)" .
instance ..
end
end

context includes fmap.lifting begin

lemma fmap_times_fempty[simp]:
  ‹f * fmempty = f›
  ‹fmempty * f = f›
  by (transfer, auto, transfer, auto)

lemma fmap_sepdisj_fmempty[simp]:
  ‹f ## fmempty›
  ‹fmempty ## f›
  by (transfer, auto, transfer, auto)

end

instance "fmap" :: (type,times) mult_1
  including fmap.lifting
  by (standard; transfer; simp)


instance "fmap" :: (type,sep_magma) sep_magma ..

instantiation "fmap" :: (type, sep_carrier) sep_carrier begin

context includes fmap.lifting begin
lift_definition mul_carrier_fmap :: ‹('a, 'b) fmap ⇒ bool›
  is ‹λf. (∀k. mul_carrier (f k))› .

instance by (standard; transfer; simp add: mul_carrier_closed)

end

end

instance "fmap" :: (type,sep_magma) sep_magma_1
  including fmap.lifting
  by (standard; transfer; simp)
  
context includes fmap.lifting fset.lifting begin

lemma fmap_times_single[simp]:
  ‹s |∉| fmdom y ⟹ y * fmupd s x fmempty = fmupd s x y›
proof (transfer, auto)
  fix sa :: 'a and ya :: "'a ⇒ 'b option" and xa :: 'b
  assume a1: "(λx. ya x * map_upd sa xa (λx. None) x) ≠ map_upd sa xa ya"
  obtain zz :: "'a ⇒ 'b option" where
    f2: "∀X23. zz X23 = None"
    by moura
  obtain aa :: 'a and zza :: "'a ⇒ 'b option" where
    "ya aa * map_upd sa xa zza aa ≠ map_upd sa xa ya aa"
    using a1 by blast
  then show "∃b. ya sa = Some b"
  proof -
    obtain aaa :: 'a where
      f1: "ya aaa * map_upd sa xa (λa. None) aaa ≠ map_upd sa xa ya aaa"
      using a1 by blast
    obtain zzb :: "'a ⇒ 'b option" where
      f2: "∀X1. zzb X1 = None"
      by moura
    then have "ya aaa * map_upd sa xa zzb aaa ≠ map_upd sa xa ya aaa"
      using f1 by presburger
    then show ?thesis
      using f2 by (metis fun_upd_other fun_upd_same map_upd_def option.exhaust_sel times_option(2) times_option(3))
  qed
qed


lemma fmdom_times[simp]:
  ‹fmdom (fm1 * fm2) = fmdom fm1 |∪| fmdom fm2›
  by (transfer, auto simp add: domD domIff)

lemma fmupd_times_right:
  ‹ k |∉| fmdom y
⟹ fmupd k v (x * y) = fmupd k v x * y›
  by (transfer, auto simp: map_upd_def fun_eq_iff, insert domIff, fastforce)

lemma fmupd_times_left:
  ‹ k |∉| fmdom x
⟹ fmupd k v (x * y) = x * fmupd k v y›
  by (transfer, auto simp: map_upd_def fun_eq_iff, insert domIff, fastforce)

lemma sep_disj_fmupd_right[simp]:
  ‹ k |∉| fmdom f
⟹ k |∉| fmdom g
⟹ f ## g
⟹ f ## fmupd k v g ›
  by (transfer, auto simp add: map_upd_def)

lemma sep_disj_fmupd_left[simp]:
  ‹ k |∉| fmdom f
⟹ k |∉| fmdom g
⟹ g ## f
⟹ fmupd k v g ## f ›
  by (transfer, auto simp add: map_upd_def)

end


subsection ‹Unit›

instantiation unit :: plus begin
definition [simp]: "plus_unit (f::unit) (g::unit) = ()"
instance ..
end

instantiation unit :: times begin
definition [simp]: "times_unit (f::unit) (g::unit) = ()"
instance ..
end

instantiation unit :: zero begin
definition [simp]: "zero_unit = ()"
instance ..
end

instantiation unit :: one begin
definition [simp]: "one_unit = ()"
instance ..
end

instantiation unit :: monoid_mult begin
instance by standard simp_all
end

instance unit :: no_inverse by standard simp_all

instantiation unit :: no_negative begin
instance by standard simp_all
end

instantiation unit :: sep_disj_distrib begin
definition sep_disj_unit :: ‹unit ⇒ unit ⇒ bool› where [simp]: ‹sep_disj_unit _ _ = True›
instance by (standard; simp)
end

instance unit :: sep_no_inverse by standard simp_all

instance unit :: sep_cancel by standard simp

instantiation unit :: sep_carrier_1 begin

definition mul_carrier_unit :: ‹unit ⇒ bool› where [simp]: ‹mul_carrier_unit x = True ›

instance by (standard; simp)

end

subsection ‹Set›


instantiation set :: (type) zero begin
definition zero_set where "zero_set = {}"
instance ..
end

lemma zero_set_iff[simp]: ‹x ∉ 0› unfolding zero_set_def by simp

instantiation set :: (one) one begin
definition "one_set = {1::'a}"
instance ..
end

lemma set_in_1[simp]: "x ∈ 1 ⟷ x = 1"
  unfolding one_set_def by simp

instantiation set :: ("{sep_disj,times}") times begin
definition "times_set P Q = { x * y | x y. x ∈ P ∧ y ∈ Q ∧ x ## y }"
instance ..
end

lemma times_set_I[simp]: (*TODO: dangerous? ? I just added this to simp*)
  ‹x ∈ P ⟹ y ∈ Q ⟹ x ## y ⟹ x * y ∈ P * Q›
  unfolding times_set_def by simp blast

lemma set_mult_zero[iff]: "{} * S = {}" "S * {} = {}"
  unfolding times_set_def by simp_all

lemma set_mult_single: ‹A ## B ⟹ {A} * {B} = {A * B}›
  unfolding times_set_def set_eq_iff by simp

lemma set_mult_expn:
  ‹uv ∈ (S * T) ⟷ (∃u v. uv = u * v ∧ u ∈ S ∧ v ∈ T ∧ u ## v)›
  unfolding times_set_def by simp

lemma times_set_subset[intro, simp]:
  ‹B ⊆ B' ⟹ A * B ⊆ A * B'›
  ‹B ⊆ B' ⟹ B * A ⊆ B' * A›
  unfolding subset_iff times_set_def by simp_all blast+

instance set :: ("{sep_disj,times}") mult_zero 
  by (standard; simp add: zero_set_def times_set_def)

instance set :: ("{sep_magma_1,no_inverse}") no_inverse
  apply (standard, simp add: one_set_def times_set_def set_eq_iff)
  by (metis (no_types, opaque_lifting) no_inverse sep_magma_1_left sep_magma_1_right)

instantiation set :: (type) total_sep_disj begin
definition sep_disj_set :: ‹'a set ⇒ 'a set ⇒ bool› where [simp]: ‹sep_disj_set _ _ = True›
instance by (standard; simp)
end

instance set :: (sep_magma) sep_magma ..

instance set :: (sep_magma_1) sep_magma_1 proof
  fix x :: ‹'a set›
  show ‹1 * x = x› unfolding one_set_def times_set_def by simp
  show ‹x * 1 = x› unfolding one_set_def times_set_def by simp
  show ‹x ## 1› unfolding one_set_def sep_disj_set_def by simp
  show ‹1 ## x› unfolding one_set_def sep_disj_set_def by simp
qed

instance set :: (sep_no_inverse) sep_no_inverse
  apply (standard, simp add: one_set_def times_set_def set_eq_iff)
  by (metis (no_types, opaque_lifting) sep_magma_1_left sep_magma_1_right sep_no_inverse)

instantiation set :: (sep_disj_distrib) sep_disj_distrib begin
instance by (standard; simp)
end

instance set :: (sep_semigroup) semigroup_mult
  apply (standard; clarsimp simp add: times_set_def algebra_simps set_eq_iff; rule; clarsimp)
  using sep_disj_multD2 sep_disj_multI2 sep_mult_assoc apply blast
  by (metis sep_disj_multD1 sep_disj_multI1 sep_mult_assoc)

instance set :: (sep_monoid) monoid_mult
  by standard (simp_all add: one_set_def times_set_def)

instance set :: (sep_ab_semigroup) ab_semigroup_mult
  apply (standard; simp add: times_set_def set_eq_iff)
  using sep_disj_commute sep_mult_commute by blast

instance set :: (sep_algebra) comm_monoid_mult
  by (standard; simp_all add: one_set_def times_set_def)

instantiation set :: (type) comm_monoid_add begin
definition ‹plus_set = union›
instance by standard (auto simp add: plus_set_def zero_set_def)
end

instance set :: (type) ordered_comm_monoid_add
  by standard (auto simp add: plus_set_def zero_set_def)

lemma plus_set_in_iff[iff]:
  ‹x ∈ A + B ⟷ x ∈ A ∨ x ∈ B› unfolding plus_set_def by simp

lemma plus_set_S_S [simp]: ‹S + S = S› for S :: ‹'a set› unfolding plus_set_def by simp

instance set :: (sep_semigroup) ordered_semiring_0
  by standard (auto simp add: zero_set_def plus_set_def times_set_def)

instance set :: (sep_monoid) semiring_1
  by standard (auto simp add: zero_set_def plus_set_def times_set_def)

instance set :: (sep_ab_semigroup) ordered_comm_semiring
  by (standard, simp add: zero_set_def plus_set_def times_set_def,
      (insert mult.commute, blast)[1],
      simp)

instance set :: (sep_algebra) comm_semiring_1
  by standard (auto simp add: zero_set_def plus_set_def times_set_def)



paragraph ‹Partial Additive Commutative Monoid›

instantiation set :: (type) comm_dom_of_add begin
definition dom_of_add_set :: ‹'a set ⇒ 'a set ⇒ bool›
  where [iff]: ‹dom_of_add_set A B ⟷ (A ∩ B = {})›

instance by (standard, simp add: dom_of_add_set_def, blast)
end

instantiation set :: (type) dom_of_minus begin
definition dom_of_minus_set :: ‹'a set ⇒ 'a set ⇒ bool›
  where [simp]: ‹dom_of_minus_set A B ⟷ B ⊆ A›
instance ..
end

instance set :: (type) partial_cancel_ab_semigroup_add
  by (standard; simp add: dom_of_add_set_def plus_set_def; blast)

instance set :: (type) partial_canonically_ordered_ab_semigroup_add
  by (standard; simp add: dom_of_add_set_def; blast)

instance set :: (type) positive_partial_add_magma_0
  by (standard; simp add: dom_of_add_set_def zero_set_def additive_join_sub_def; blast)

instance set :: (type) partial_add_ab_monoid ..

paragraph ‹Rules for Specific Cases›

lemma dom_of_add_lcro_intvl[simp]:
  ‹ {a..<b} ##⇩+ {c..<d} ⟷ b ≤ a ∨ b ≤ c ∨ d ≤ c ∨ d ≤ a›
  for a :: ‹'a::linorder›
  unfolding dom_of_add_set_def
  by (auto simp add: set_eq_iff; meson leI nle_le)
  

subsection ‹Partial Map›

lemma one_partial_map: ‹1 = Map.empty›
  unfolding one_fun_def one_option_def ..

lemma times_fun_map_add_right:
  ‹dom f ∩ dom h = {} ⟹ (f * g) ++ h = f * (g ++ h)›
  unfolding times_fun_def fun_eq_iff map_add_def
  by (simp add: disjoint_iff domIff option.case_eq_if times_option_def)

subsubsection ‹Separation Disjunction›

lemma sep_disj_partial_map_del:
  ‹f ## g ⟹ f ## g(k := None)›
  unfolding sep_disj_fun_def sep_disj_option_def
  apply clarify subgoal premises prems for x
    apply (insert prems[THEN spec[where x=x]])
    by (cases ‹f x›; simp; cases ‹g x›; simp) .

lemma sep_disj_partial_map_disjoint:
  "f ## g ⟷ dom f ∩ dom g = {}"
  for f :: "'a ⇀ ('b :: discrete_semigroup)"
  unfolding sep_disj_fun_def sep_disj_option_def disjoint_iff
  by (smt (verit, ccfv_SIG) domD domIff discrete_disj option.simps(4) option.simps(5))


lemma sep_disj_partial_map_some_none:
  ‹f ## g ⟹ g k = Some v ⟹ f k = None›
  for f :: "'a ⇀ ('b :: discrete_semigroup)"
  using sep_disj_fun by fastforce

lemma sep_disj_partial_map_not_1_1:
  ‹f ## g ⟹ g k ≠ 1 ⟹ f k = 1›
  for f :: "'a ⇒ ('b :: discrete_monoid)"
  unfolding sep_disj_fun_def apply simp
  by blast


lemma sep_disj_partial_map_upd:
  ‹f ## g ⟹ k ∈ dom f ⟹ (f * g)(k := v) = (f(k:=v) * g)›
  for f :: "'a ⇀ ('b :: discrete_semigroup)"
  unfolding sep_disj_partial_map_disjoint fun_upd_def times_fun fun_eq_iff
  by (simp add: disjoint_iff domIff)

lemma discrete_semigroup_sepdisj_fun:
  ‹1(k ↦ x) ## a ⟹ 1(k := any) ## a›
  for x :: ‹'b::discrete_semigroup›
  unfolding sep_disj_fun_def
  by (metis discrete_disj_1 fun_upd_apply sep_disj_option_discrete(1))


lemma fun_sep_disj_fupdt[simp]:
  ‹f1 ## f2 ⟹ x1 ## x2 ⟹ f1(k := x1) ## f2(k := x2)›
  unfolding sep_disj_fun_def by simp

lemma fun_sep_disj_1_fupdt[simp]:
  ‹f(k := x1) ## 1(k := x2) ⟷ x1 ## x2›
  ‹1(k := x1) ## f(k := x2) ⟷ x1 ## x2›
  for x1 :: ‹'b :: sep_magma_1›
  unfolding sep_disj_fun_def by (simp; rule; clarsimp)+

lemma fun_sep_disj_imply_v:
  ‹f(k := x1) ## g(k := x2) ⟹ x1 ## x2›
  unfolding sep_disj_fun_def
  apply (clarsimp simp add: sep_disj_fun_def)
  by presburger

lemma share_1_fupdt[simp]:
  ‹share n (1(k := v)) = 1(k := share n v)›
  for v :: ‹'b::share_one›
  by simp

subsubsection ‹dom1: Domain except one›

definition "dom1 f = {x. f x ≠ 1}"

lemma dom1_1[simp]: "dom1 1 = {}"
  unfolding dom1_def by simp

lemma dom_1[simp]: "dom 1 = {}"
  by (simp add: one_fun_def)

lemma dom1_upd[simp]: "dom1 (f(x:=y)) = (if y = 1 then dom1 f - {x} else insert x (dom1 f))"
  unfolding dom1_def by auto

lemma dom1_dom: "dom1 = dom"
  by (metis fun_eq_iff dom1_def dom_def one_option_def)

lemma one_updt_one[simp]: "1(a:=1) = 1" unfolding one_fun_def fun_upd_def by simp

lemma v_neq_1_fupdt_neq_1[simp]: "x ≠ 1 ⟹ f(k:=x) ≠ 1"
  unfolding one_fun_def fun_upd_def fun_eq_iff by simp blast

lemma one_ringop_f_is_1[simp]: "1 o f = 1"
  unfolding one_fun_def fun_eq_iff by simp

lemma finite_dom1_mult1[simp]:
  "finite (dom1 (1(k:=v) * f)) ⟷ finite (dom1 f)"
  for f :: "'a ⇒ 'b :: sep_monoid"
proof -
  have "dom1 (1(k:=v) * f) = dom1 f ∨ dom1 (1(k:=v) * f) = insert k (dom1 f)
    ∨ dom1 (1(k:=v) * f) = dom1 f - {k}"
  for f :: "'a ⇒ 'b :: sep_monoid"
  unfolding dom1_def times_fun_def fun_upd_def set_eq_iff by simp
  then show ?thesis
    by (metis finite_Diff finite_insert infinite_remove)
qed

lemma dom1_disjoint_sep_disj:
  ‹dom1 g ∩ dom1 f = {} ⟹ g ## f›
  for f :: ‹'a ⇒ 'b::sep_magma_1›
  unfolding sep_disj_fun_def dom1_def set_eq_iff
  by (simp; metis sep_magma_1_left sep_magma_1_right)

lemma sep_disj_dom1_disj_disjoint:
  ‹g ## f ⟷ dom1 g ∩ dom1 f = {}›
  for f :: ‹'a ⇒ 'b::discrete_monoid›
  unfolding sep_disj_fun_def dom1_def set_eq_iff
  by clarsimp

lemma dom1_mult: ‹f ## g ⟹ dom1 (f * g) = dom1 f ∪ dom1 g›
  for f :: ‹'a ⇒ 'b :: {sep_no_inverse,sep_disj}›
  unfolding sep_disj_fun_def dom1_def set_eq_iff times_fun by simp

lemma dom_mult: ‹f ## g ⟹ dom (f * g) = dom f ∪ dom g›
  using dom1_mult dom1_dom by metis

(* lemma dom1_mult_disjoint: ‹dom1 (f * g) = dom1 f ∪ dom1 g›
  for f :: ‹'a ⇒ 'b :: no_inverse›
  unfolding sep_disj_fun_def dom1_def set_eq_iff times_fun by simp *)

lemma dom1_sep_mult_disjoint:
  ‹f ## g ⟹  dom1 (f * g) = dom1 f ∪ dom1 g›
  for f :: ‹'a ⇒ 'b :: positive_sep_magma_1›
  unfolding sep_disj_fun_def dom1_def set_eq_iff times_fun by simp

lemma disjoint_dom1_eq_1:
  ‹dom1 f ∩ dom1 g = {} ⟹ k ∈ dom1 f ⟹ g k = 1›
  ‹dom1 f ∩ dom1 g = {} ⟹ k ∈ dom1 g ⟹ f k = 1›
  unfolding dom1_def set_eq_iff by simp_all blast+

lemma fun_split_1_not_dom1:
  "k ∉ dom1 f ⟹ f(k := v) = 1(k:= v) * f" for f :: "'a ⇒ 'b::mult_1"
  unfolding fun_upd_def fun_eq_iff times_fun_def dom1_def by simp

lemma fun_split_1_not_dom:
  "k ∉ dom f ⟹ f(k := v) = 1(k:= v) * f"
  unfolding fun_upd_def fun_eq_iff times_fun_def dom_def by simp


subsubsection ‹Multiplication with Prod›

lemma fun_prod_homo:
  ‹prod (f * g) S = prod f S * prod g S›
  by (simp add: prod.distrib times_fun)

lemma prod_superset_dom1:
  ‹ finite S
⟹ dom1 f ⊆ S
⟹ prod f S = prod f (dom1 f)›
  subgoal premises prems proof -
    define R where ‹R ≡ S - dom1 f›
    have t1: ‹dom1 f ∩ R = {}›    using R_def by blast
    have t2: ‹S = dom1 f ∪ R›     using R_def prems(2) by blast
    have t3: ‹finite R›           using prems(1) t2 by blast
    have t4: ‹finite (dom1 f)›    using prems(1) t2 by blast
    have t5: ‹prod f S = prod f (dom1 f) * prod f R›
      using prod.union_disjoint t1 t2 t3 t4 by blast
    show ?thesis
      by (simp add: R_def dom1_def t5)
  qed .


subsubsection ‹Total Permission Transformation›

lemma pointwise_set_UNIV:
  ‹pointwise_set UNIV = UNIV›
  unfolding pointwise_set_def by simp

lemma sep_orthogonal_monoid_pointwise[locale_intro]:
  assumes D':   ‹D' = pointwise_set D›
      and prem: ‹sep_orthogonal_monoid ψ D›
  shows ‹sep_orthogonal_monoid ((∘) ψ) D'›
  unfolding comp_def
proof
  interpret xx: sep_orthogonal_monoid ψ D using prem .
  fix x y a b c :: ‹'a ⇒ 'b›
  fix a' :: ‹'a ⇒ 'c›
  show ‹x ## y ⟹ (λxa. ψ ((x * y) xa)) = (λxa. ψ (x xa)) * (λx. ψ (y x))›
    by (simp add: fun_eq_iff times_fun sep_disj_fun_def xx.homo_mult)
  show ‹a ## b ⟶ (λx. ψ (a x)) ## (λx. ψ (b x))›
    by (simp add: fun_eq_iff times_fun sep_disj_fun_def D' pointwise_set_def)
  show ‹b ∈ D' ∧ c ∈ D' ⟹ (λx. ψ (b x)) ## a' ⟹
     ((λx. ψ (b x)) * a' = (λx. ψ (c x))) = (∃a. a' = (λx. ψ (a x)) ∧ b * a = c ∧ b ## a ∧ a ∈ D')›
    by (auto simp add: D' fun_eq_iff times_fun sep_disj_fun_def xx.sep_orthogonal pointwise_set_def; metis)
  show ‹1 ∈ D'›
    by (simp add: D' pointwise_set_def xx.one_in_D)
qed

lemma share_orthogonal_homo_pointwise[locale_intro]:
  assumes D':   ‹D' = pointwise_set D›
      and prem: ‹share_orthogonal_homo ψ D›
    shows ‹share_orthogonal_homo ((∘) ψ) D'›
proof (rule share_orthogonal_homo.intro, rule sep_orthogonal_monoid_pointwise,
       rule D', rule share_orthogonal_homo.axioms(1)[OF prem], standard)
  interpret xx: share_orthogonal_homo ψ D using prem .

  fix x y z a b c :: ‹'a ⇒ 'b›
  fix a' :: ‹'a ⇒ 'c›
  fix n :: rat

  show ‹x ∈ D' ⟹ mul_carrier (ψ ∘ x)›
    by (simp add: D' sep_disj_fun_def xx.ψ_mul_carrier pointwise_set_def)
  
  show ‹b ∈ D' ∧ c ∈ D' ⟹ (ψ ∘ b) ## a' ⟹
       0 < n ∧ n ≤ 1 ⟹ (n ⦼ (ψ ∘ b) * a' = (ψ ∘ c))
                        = (∃a''. a' = (1 - n) ⦼ (ψ ∘ b) * (ψ ∘ a'') ∧ b * a'' = c ∧ b ## a'' ∧ a'' ∈ D')›
    by (auto simp add: join_sub_def fun_eq_iff times_fun sep_disj_fun_def xx.share_orthogonal
            share_fun_def pointwise_set_def D'; metis)

  show ‹b ∈ D' ∧ c ∈ D' ⟹ (ψ ∘ b) ## a' ⟹ 1 < n ⟹ ψ ∘ b ≠ 1 ⟹ n ⦼ (ψ ∘ b) * a' ≠ ψ ∘ c›
    by (clarsimp simp add: fun_eq_iff sep_disj_fun_def times_fun_def share_fun_def,
        metis D' mem_Collect_eq pointwise_set_def xx.share_bounded)

qed

lemma sep_orthogonal_monoid_pointwise_eq:
  ‹sep_orthogonal_monoid ((∘) ψ) (pointwise_set D) ⟷ sep_orthogonal_monoid ψ D›
  for ψ :: ‹'b::sep_monoid ⇒ 'c::sep_monoid›
proof
  assume prem: ‹sep_orthogonal_monoid ((∘) ψ :: ('a ⇒ 'b) ⇒ 'a ⇒ 'c) (pointwise_set D)›
  show ‹sep_orthogonal_monoid ψ D›
  proof
    interpret xx: sep_orthogonal_monoid ‹(∘) ψ :: ('a ⇒ 'b) ⇒ 'a ⇒ 'c› ‹(pointwise_set D)› using prem .
    fix x y a b c :: ‹'b› and a2 :: 'c
    show ‹x ## y ⟹ ψ (x * y) = ψ x * ψ y›
      using xx.homo_mult[unfolded sep_disj_fun_def times_fun one_fun_def fun_eq_iff, simplified]
      by meson
    show ‹a ## b ⟶ ψ a ## ψ b›
      using xx.sep_disj_homo_semi[unfolded sep_disj_fun_def times_fun one_fun_def fun_eq_iff, simplified]
      by meson
    show ‹1 ∈ D›
      using xx.one_in_D by (auto simp add: pointwise_set_def)
    show ‹b ∈ D ∧ c ∈ D ⟹ ψ b ## a2 ⟹
            (ψ b * a2 = ψ c) = (∃a'. a2 = ψ a' ∧ b * a' = c ∧ b ## a' ∧ a' ∈ D)›
      using xx.sep_orthogonal[unfolded sep_disj_fun_def times_fun one_fun_def fun_eq_iff,
          where a=‹λ_. a2› and b=‹λ_. b› and c=‹λ_. c›, simplified pointwise_set_def, simplified]
      by auto
  qed
next
  show ‹sep_orthogonal_monoid ψ D ⟹ sep_orthogonal_monoid ((∘) ψ) (pointwise_set D)›
    using sep_orthogonal_monoid_pointwise by blast 
qed

lemma share_orthogonal_homo_pointwise_eq:
  ‹share_orthogonal_homo ((∘) ψ) (pointwise_set D) ⟷ share_orthogonal_homo ψ D›
  for ψ :: ‹'b::sep_algebra ⇒ 'c::share_semimodule›
proof
  assume prem: ‹share_orthogonal_homo ((∘) ψ :: ('a ⇒ 'b) ⇒ 'a ⇒ 'c) (pointwise_set D)›
  show ‹share_orthogonal_homo ψ D›
  proof (rule share_orthogonal_homo.intro[OF share_orthogonal_homo.axioms(1)[OF prem, unfolded sep_orthogonal_monoid_pointwise_eq]],
         standard)
    interpret xx: share_orthogonal_homo ‹((∘) ψ :: ('a ⇒ 'b) ⇒ 'a ⇒ 'c)› ‹(pointwise_set D)› using prem .
    fix x y a b c :: ‹'b› and a2 :: 'c and n :: rat

    show ‹ x ∈ D ⟹ mul_carrier (ψ x) ›
      using xx.ψ_mul_carrier[of ‹λ_. x›, simplified pointwise_set_def, simplified]
      by (auto simp add: sep_disj_fun_def)

    show ‹ b ∈ D ∧ c ∈ D ⟹ ψ b ## a2 ⟹ 0 < n ∧ n ≤ 1 ⟹
            (n ⦼ ψ b * a2 = ψ c) = (∃a'. a2 = (1 - n) ⦼ ψ b * ψ a'∧ b * a' = c ∧ b ## a' ∧ a' ∈ D)›
      by (insert xx.share_orthogonal[where a=‹λ_. a2› and b=‹λ_. b› and c=‹λ_. c›];
          clarsimp simp add: sep_disj_fun_def share_fun_def fun_eq_iff times_fun pointwise_set_def; rule; auto)

    show ‹b ∈ D ∧ c ∈ D ⟹ ψ b ## a2 ⟹ 1 < n ⟹ ψ b ≠ 1 ⟹ n ⦼ ψ b * a2 ≠ ψ c›
      by (insert xx.share_bounded[where a=‹λ_. a2› and b=‹λ_. b› and c=‹λ_. c›];
          clarsimp simp add: sep_disj_fun_def share_fun_def fun_eq_iff times_fun pointwise_set_def)

  qed
next
  show ‹share_orthogonal_homo ψ D ⟹ share_orthogonal_homo ((∘) ψ) (pointwise_set D)›
    using share_orthogonal_homo_pointwise by blast 
qed



subsubsection ‹Subsumption›

lemma discrete_partial_map_subsumption:
  ‹f ≼⇩S⇩L g ⟹ k ∈ dom1 f ⟹ g k = f k›
  for f :: ‹'k ⇒ 'v::discrete_monoid›
  unfolding join_sub_def
  apply (clarsimp simp add: times_fun)
  by (simp add: disjoint_iff dom1_def sep_disj_dom1_disj_disjoint)

lemma discrete_1_fupdt_subsumption:
  ‹ 1(k := v) ≼⇩S⇩L objs
⟹ v ≠ 1
⟹ objs k = v›
  for v :: ‹'v::discrete_monoid›
  using discrete_partial_map_subsumption[where f=‹1(k := v)›]
  by (clarsimp simp add: times_fun)

lemma discrete_partial_map_subsumption_L2:
  ‹ 1(k := v) ≼⇩S⇩L objs
⟹ v ⊆⇩m objs k›
  for v :: ‹'b ⇒ 'c::discrete_semigroup option›
  unfolding join_sub_def map_le_def
  by (clarsimp simp add: times_fun,
      metis fun_upd_same mult_1_class.mult_1_right one_option_def sep_disj_fun_def sep_disj_option_discrete(2))


subsection ‹Fractional SA›

datatype 'a share = Share (perm:rat) (val: 'a)
hide_const (open) val perm

lemma share_exists: ‹Ex  P ⟷ (∃n x. P (Share n x))› by (metis share.exhaust_sel)
lemma share_forall: ‹All P ⟷ (∀n x. P (Share n x))› by (metis share.exhaust_sel)
lemma share_All: ‹(⋀x. PROP P x) ≡ (⋀n x'. PROP (P (Share n x')))› proof
  fix n x' assume ‹(⋀x. PROP P x)› then show ‹PROP P (Share n x')› .
next fix x assume ‹⋀n x'. PROP P (Share n x')›
  from ‹PROP P (Share (share.perm x) (share.val x))› show ‹PROP P x› by simp
qed

subsubsection ‹Instantiating Algebraic Properties›

instantiation share :: (type) sep_magma begin

definition times_share :: "'a share ⇒ 'a share ⇒ 'a share" where
  "times_share x' y' = (case x' of Share n x ⇒ (case y' of Share m y ⇒
    if x = y then Share (n+m) x else undefined))"

lemma times_share[simp]:
  "(Share n x) * (Share m y) = (if x = y then Share (n+m) x else undefined)"
  unfolding times_share_def by simp_all

definition sep_disj_share :: "'a share ⇒ 'a share ⇒ bool" where
  "sep_disj_share x' y' ⟷ (case x' of Share n x ⇒
    (case y' of Share m y ⇒ 0 < n ∧ 0 < m ∧ x = y))"

lemma sep_disj_share[simp]:
  "(Share n x) ## (Share m y) ⟷ 0 < n ∧ 0 < m ∧ x = y"
  unfolding sep_disj_share_def by simp_all

instance ..
end

instance share :: (type) strict_positive_sep_magma
  by (standard; case_tac a; case_tac b; simp)

instantiation share :: (mul_carrier) mul_carrier begin

definition mul_carrier_share :: ‹'a share ⇒ bool›
  where ‹mul_carrier_share x = (case x of Share n x' ⇒ 0 < n ∧ mul_carrier x')›

lemma mul_carrier_share[simp]:
  ‹mul_carrier (Share n x) ⟷ 0 < n ∧ mul_carrier x›
  unfolding mul_carrier_share_def
  by simp

instance ..

end

instance share :: (sep_carrier) sep_carrier
  by (standard; case_tac a; case_tac b; simp)

instance share :: (type) sep_ab_semigroup proof
  fix x y z :: "'a share"
  show "x ## y ⟹ x * y = y * x" by (cases x; cases y) (simp add: add.commute)
  show "x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)"
    by (cases x; cases y; cases z) (simp add: add.assoc)
  show "x ## y * z ⟹ y ## z ⟹ x ## y"
    by (cases x; cases y; cases z; simp)
  show "x ## y * z ⟹ y ## z ⟹ x * y ## z"
    by (cases x; cases y; cases z)
       (simp add: ab_semigroup_add_class.add_ac(1) order_less_le)
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    unfolding join_sub_def
    apply (clarsimp; cases x; cases y; clarsimp)
    by (metis add.commute add_cancel_left_left add_le_cancel_left le_add_same_cancel1 less_le_not_le nle_le sep_disj_share share.exhaust share.inject share.sel(2) times_share)
  show "x ## y ⟹ y ## x" by (cases x; cases y) (simp add: add.commute)
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z›
    by (cases x; cases y; cases z; simp)
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z›
    by (cases x; cases y; cases z; simp)
qed

instance share :: (type) sep_disj_distrib
  by (standard; case_tac a; case_tac b; case_tac c; simp)

instantiation share :: (type) share begin

definition share_share :: "rat ⇒ 'a share ⇒ 'a share"
  where ‹share_share n x = (case x of Share m x' ⇒ Share (n*m) x')›

lemma share_share[simp]: ‹share n (Share m x) = Share (n*m) x›
  unfolding share_share_def by simp

instance by (standard; case_tac x; simp add: share_share_def mult.assoc mult_le_one)

end

instance share :: (type) share_inj
  by (standard; case_tac x; case_tac y; simp)

instance share :: (sep_carrier) share_nun_semimodule proof
  fix x y :: ‹'a share›
  fix n n' m :: rat

  show ‹0 < n ⟹ share n x ## y = x ## y›
    by (cases x; cases y; simp add: zero_less_mult_iff)
  show ‹mul_carrier x ⟹ x ## x›
    by (cases x; simp)
  show ‹0 < n ⟹ 0 < m ⟹ share n x * share m x = share (n + m) x›
    by (cases x; cases y; simp add: distrib_right)
  show ‹0 < n ⟹ x ## y ⟹ share n x * share n y = share n (x * y)›
    by (cases x; cases y; simp add: distrib_left)
  show ‹0 < n ∧ n < 1 ⟹ mul_carrier x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x›
    by (cases x; cases y; simp add: join_sub_def share_exists;
        metis add.commute add_le_same_cancel1 diff_add_cancel linorder_not_le mult_1_class.mult_1_left mult_less_cancel_right)
  show ‹0 < n ⟹ mul_carrier x ⟹ mul_carrier (n ⦼ x)›
    by (cases x; simp)
qed

instance share :: (type) sep_cancel
  by (standard; case_tac a; case_tac b; case_tac c; simp)


subsubsection ‹Homomorphism of ‹map_share››

lemma homo_sep_disj_map_share[simp]:
  ‹ homo_sep_disj (map_share f)›
  unfolding homo_sep_disj_def
  by (clarsimp simp add: share_forall)

lemma closed_homo_sep_disj_map_share[simp]:
  ‹ inj f
⟹ closed_homo_sep_disj (map_share f) ›
  unfolding closed_homo_sep_disj_def inj_def
  by (clarsimp simp add: share_forall; blast)

lemma homo_sep_mult_map_share[simp]:
  ‹ homo_sep_mult (map_share f) ›
  unfolding homo_sep_mult_def
  by (clarsimp simp add: share_forall)

lemma homo_sep_map_share[simp]:
  ‹ homo_sep (map_share f) ›
  unfolding homo_sep_def
  by clarsimp

lemma closed_homo_sep_map_share[simp]:
  ‹ inj f
⟹ closed_homo_sep (map_share f) ›
  unfolding closed_homo_sep_def
  by (clarsimp simp add: share_forall)

subsubsection ‹‹Share› as an Embedding Homomorphism›

lemma homo_mul_carrier_Share_discrete[simp]:
  ‹ 0 < n ⟹ homo_mul_carrier (Share n) ›
  unfolding homo_mul_carrier_def
  by clarsimp

lemma homo_sep_disj_Share_discrete[simp]:
  ‹ 0 < n ⟹ homo_sep_disj (Share n :: 'a::discrete_semigroup ⇒ 'a share) ›
  unfolding homo_sep_disj_def
  by clarsimp

lemma
  ‹ 0 < n ⟹ closed_homo_sep_disj (Share n) ›
  unfolding closed_homo_sep_disj_def
  apply clarsimp (*TODO: maybe we shall introduce an 'agreement' class?*)
  oops

lemma homo_sep_mult_Share_discrete[simp]:
  ‹ 0 < n ⟹ homo_sep_mult (Share n :: 'a::discrete_semigroup ⇒ 'a share) ›
  unfolding homo_sep_mult_def
  by clarsimp

lemma homo_sep_Share_discrete[simp]:
  ‹ 0 < n ⟹ homo_sep (Share n :: 'a::discrete_semigroup ⇒ 'a share) ›
  unfolding homo_sep_def
  by clarsimp



subsubsection ‹Convert a function to sharing or back›

abbreviation ‹to_share ≡ map_option (Share 1)›
abbreviation ‹strip_share ≡ map_option share.val›

lemma share_orthogonal_homo_to_share[locale_witness]:
  ‹share_orthogonal_homo (to_share::'a::{sep_carrier, discrete_semigroup} option ⇒ 'a share option) (Collect mul_carrier)›
proof
  fix x y z a b c :: ‹'a option›
  fix xx yy aa bb cc :: ‹'a›
  fix a' a2 :: ‹'a share option›
  fix n :: rat
  show ‹x ## y ⟹ to_share (x * y) = to_share x * to_share y› by (cases x; cases y; simp)
  show ‹a ## b ⟶ to_share a ## to_share b› by simp
  show ‹b ∈ Collect mul_carrier ∧ c ∈ Collect mul_carrier ⟹
        to_share b ## a' ⟹
       (to_share b * a' = to_share c) = (∃a. a' = to_share a ∧ b * a = c ∧ b ## a ∧ a ∈ Collect mul_carrier)›
    apply (cases a'; cases b; cases c; simp add: split_option_ex)
    subgoal for a'' by (cases a''; simp) .
  show ‹(1::'a option) ∈ Collect mul_carrier› by simp
  (* show ‹inj to_share›
    by (rule, simp, metis option.inj_map_strong share.inject) *)
  show ‹x ∈ Collect mul_carrier ⟹ mul_carrier (to_share x)› by (cases x; simp)
  show ‹b ∈ Collect mul_carrier ∧ c ∈ Collect mul_carrier ⟹
        to_share b ## a2 ⟹ 0 < n ∧ n ≤ 1 ⟹
        (n ⦼ to_share b * a2 = to_share c) = (∃a'. a2 = (1 - n) ⦼ to_share b * to_share a' ∧ b * a' = c ∧ b ## a' ∧ a' ∈ Collect mul_carrier)›
    apply (cases a2; cases b; cases c; simp add: share_option_def)
    apply (cases ‹n < 1›; simp)
    apply (smt (verit, ccfv_SIG) diff_add_cancel diff_gt_0_iff_gt sep_cancel sep_disj_commuteI sep_disj_multD2 sep_disj_multI2 sep_disj_share sep_mult_commute times_share)
    by (metis join_strict_positivity sep_disj_distrib_left sep_disj_share zero_less_one)

  show ‹b ∈ Collect mul_carrier ∧ c ∈ Collect mul_carrier ⟹ to_share b ## a2 ⟹ 1 < n ⟹ to_share b ≠ 1 ⟹
        n ⦼ to_share b * a2 ≠ to_share c›
    by (cases a2; cases b; cases c; simp; case_tac a; simp)
  
qed


lemma to_share_kernel_is_1[locale_witness]:
  ‹ 1 ∈ D
⟹ simple_homo_mul to_share D›
  by (simp add: simple_homo_mul_def)

lemma strip_share_Share[simp]:
  ‹strip_share (map_option (Share n) x) = x›
  by (cases x; simp)

lemma map_option_funcomp_1[simp]:
  ‹map_option f o 1 = 1›
  unfolding fun_eq_iff by simp

lemma strip_share_share_funcomp[simp]:
  ‹strip_share o map_option (Share n) = id›
  ‹strip_share o (map_option (Share n) o f) = f›
  by (simp add: fun_eq_iff)+

lemma strip_share_fun_mult:
 ‹f ## g ⟹ strip_share o (f * g) = (strip_share o f) ++ (strip_share o g)›
  unfolding fun_eq_iff times_fun map_add_def times_option_def
        times_share_def comp_def sep_disj_fun_def sep_disj_share_def sep_disj_option_def
  apply (clarsimp split: option.split share.split)
  subgoal premises prems for x
    by (insert prems(1)[THEN spec[where x=x]] prems(2,3,4), simp) .

lemma strip_share_share[simp]:
  ‹0 < n ⟹ strip_share (share n x) = strip_share x›
  by (cases x; simp; case_tac a; simp)

lemma strip_share_fun_share[simp]:
  ‹0 < n ⟹ strip_share o share n f = strip_share o f›
  unfolding fun_eq_iff share_fun_def by simp


interpretation to_share_homo_one: homo_one to_share
  by standard simp

lemma to_share_eq_1_iff[simp]:
  ‹to_share x = 1 ⟷ x = 1› by simp

lemma to_share_funcomp_eq_1_iff[simp]:
  ‹to_share o f = 1 ⟷ f = 1› by (simp add: fun_eq_iff)

lemma to_share_total_disjoint:
  ‹g ## (to_share o h) ⟹
  to_share o f = g * (to_share o h) ⟹ dom g ∩ dom (to_share o h) = {}›
  unfolding fun_eq_iff times_fun times_share_def times_option_def
      sep_disj_fun_def sep_disj_option_def sep_disj_share_def
  apply auto
  subgoal premises prems for x y z
    using prems(1)[THEN spec[where x = x]]
          prems(2)[THEN spec[where x = x]]
          prems(3,4)
    by (cases y, simp)
  done

lemma map_option_funcomp_map_add:
  ‹(map_option f o (g ++ h)) = (map_option f o g) ++ (map_option f o h)›
  unfolding fun_eq_iff map_add_def by (clarsimp simp add: fun_eq_iff split: option.split)

(* lemma to_share_funcomp_map_add: (*deprecated*)
  ‹to_share o (f ++ g) = (to_share o f) ++ (to_share o g)›
  unfolding fun_eq_iff map_add_def by (auto split: option.split) *)


lemma to_share_wand_homo:
  ‹ a ## (to_share o b)
⟹ a * (to_share o b) = to_share ∘ y
⟷ (∃a'. a = to_share o a' ∧ a' * b = y ∧ a' ## b)›
  for a :: ‹'a ⇒ 'b::discrete_semigroup share option›
  unfolding times_fun fun_eq_iff sep_disj_fun_def all_conj_distrib[symmetric]
  apply (simp, subst choice_iff[symmetric])
  apply (rule; clarsimp)
  subgoal premises prems for x
    apply (insert prems[THEN spec[where x=x]])
    apply (cases ‹b x›; cases ‹a x›; cases ‹y x›; simp)
    by (metis add_cancel_left_left less_numeral_extra(3) sep_disj_share share.collapse share.sel(1) times_share)
  subgoal premises prems for x
    apply (insert prems[THEN spec[where x=x]])
    by (cases ‹b x›; cases ‹a x›; cases ‹y x›; clarsimp) .

lemma to_share_funcomp_sep_disj_I:
  ‹a ## b ⟹ (to_share o a) ## (to_share o b)›
  for a :: ‹'a ⇒ 'b::discrete_semigroup option›
  unfolding sep_disj_fun_def apply simp
   apply clarsimp subgoal premises prems for x
    apply (insert prems[THEN spec[where x=x]])
    by (cases ‹a x›; cases ‹b x›; simp) .

lemma pointwise_to_share_bij[simp]:
  ‹to_share ∘ x = to_share ∘ y ⟷ x = y›
  unfolding fun_eq_iff
  by (simp, metis strip_share_Share)


subsection ‹Non-sepable Semigroup›

(*TODO: rename this to discrete injector or other*)

datatype 'a discrete = discrete (dest: 'a)
hide_const (open) dest

lemma split_discrete_all: ‹All P ⟷ (∀x. P (discrete x))› by (metis discrete.exhaust)
lemma split_discrete_ex : ‹Ex P ⟷ (∃x. P (discrete x))› by (metis discrete.exhaust)
lemma split_discrete_meta_all: ‹Pure.all P ≡ (⋀x. PROP P (discrete x))›
proof
  fix x
  assume ‹⋀x. PROP P x›
  then show ‹PROP P (discrete x)› .
next
  fix x :: ‹'a discrete›
  assume ‹(⋀x. PROP P (discrete x))›
  note this[of ‹discrete.dest x›, simplified]
  then show ‹PROP P x› .
qed

lemma inj_discrete[simp]:
  ‹inj discrete›
  unfolding inj_def by simp

instantiation discrete :: (type) discrete_semigroup begin
definition ‹sep_disj_discrete (x :: 'a discrete) (y :: 'a discrete) = False›
definition share_discrete :: ‹rat ⇒ 'a discrete ⇒ 'a discrete›
  where [simp]: ‹share_discrete _ x = x›
definition times_discrete :: ‹'a discrete ⇒ 'a discrete ⇒ 'a discrete›
  where [simp]: ‹times_discrete x y = undefined›
instance by (standard; case_tac x; simp; case_tac y; simp add: sep_disj_discrete_def)
end

instantiation discrete :: (type) sep_carrier begin
definition mul_carrier_discrete :: ‹'a discrete ⇒ bool›
  where [simp]: ‹mul_carrier_discrete = (λ_. True)›
instance by (standard; simp)
end

instance discrete :: (type) sep_cancel by (standard; case_tac a; case_tac b; case_tac c; simp)

instance discrete :: (type) sep_disj_distrib by (standard; case_tac a; case_tac b; case_tac c; simp)

instance discrete :: (type) ab_semigroup_mult
  by (standard; case_tac a; case_tac b; simp)

instance discrete :: (type) strict_positive_sep_magma
  by (standard; case_tac a; case_tac b; simp)


lemma cancl_sep_orthogonal_monoid__map_option_discrete:
  ‹ inj_on (map_option f) D
⟹ None ∈ D
⟹ cancl_sep_orthogonal_monoid (map_option f) D›
  for f :: ‹'a discrete ⇒ 'b discrete›
  by (standard,
      (case_tac x; case_tac y; simp),
      (case_tac a; case_tac b; simp),
      (case_tac b; case_tac a; case_tac c; auto simp add: inj_on_def; force),
      simp)


subsection ‹Agreement›

datatype 'a agree = agree 'a

lemma agree_forall: ‹All P ⟷ (∀x. P (agree x))› by (metis agree.exhaust)
lemma agree_exists: ‹Ex P  ⟷ (∃x. P (agree x))› by (metis agree.exhaust)

instantiation agree :: (type) sep_magma begin
definition times_agree :: ‹'a agree ⇒ 'a agree ⇒ 'a agree›
  where [simp]: ‹times_agree x y = x›
definition sep_disj_agree :: ‹'a agree ⇒ 'a agree ⇒ bool›
  where [simp]: ‹sep_disj_agree x y ⟷ x = y›

instance ..
end

instantiation agree :: (mul_carrier) mul_carrier begin

definition mul_carrier_agree :: ‹'a agree ⇒ bool›
  where ‹mul_carrier_agree = pred_agree mul_carrier›

lemma mul_carrier_agree:
  ‹mul_carrier (agree x) ⟷ mul_carrier x›
  unfolding mul_carrier_agree_def
  by simp

instance ..
end

instance agree :: (sep_carrier) sep_carrier
  by (standard; simp)

instantiation agree :: (sep_carrier) share_nun_semimodule begin

definition share_agree :: ‹rat ⇒ 'a agree ⇒ 'a agree›
  where [simp]: ‹share_agree _ x = x›

instance proof
  fix x y z :: ‹'a agree›
  fix n n' m :: rat
  show ‹x ## y ⟹ x * y = y * x› by (case_tac x; case_tac y; simp)
  show ‹x ## y ⟹ x * y ## z ⟹ x * y * z = x * (y * z)› by (case_tac x; case_tac y; simp)
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y› unfolding join_sub_def by simp
  show ‹x ## y * z ⟹ y ## z ⟹ x ## y› by (case_tac x; case_tac y; case_tac z; simp)
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z› by (case_tac x; case_tac y; case_tac z; simp)
  show ‹0 < n ⟹ 0 < m ⟹ share n (share m x) = share (n * m) x› by (cases x; simp)
  show ‹share 1 x = x› by (cases x; simp)
  show ‹0 < n ⟹ 0 < m ⟹ share n x * share m x = share (n + m) x› by (cases x; simp)
  show ‹0 < n ⟹ x ## y ⟹ share n x * share n y = share n (x * y)› by (cases x; simp)
  show ‹0 < n ∧ n < 1 ⟹ mul_carrier x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x› by (cases x; simp)
  show ‹x ## y ⟹ y ## x› by (cases x; cases y; simp)
  show ‹x * y ## z ⟹ x ## y ⟹ y ## z› by (cases x; cases y; cases z; simp)
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z› by (cases x; cases y; cases z; simp)
  show ‹0 < n ⟹ share n x ## y = x ## y› by (cases x; cases y; simp)
  show ‹mul_carrier x ⟹ x ## x› by (cases x; simp)
  show ‹0 < n ⟹ mul_carrier x ⟹ mul_carrier (n ⦼ x)› by (cases x; simp)
qed
end

instance agree :: (type) sep_disj_distrib
  by (standard; case_tac a; case_tac b; case_tac c; simp)

instance agree :: (type) sep_cancel
  by (standard; case_tac a; case_tac c; case_tac b; simp)



end