Theory Phi_Algebras.Algebras

theory Algebras
  imports Main HOL.Rat
    "Phi_Statespace.StateFun" "Phi_Document.Base" "HOL-Library.Product_Plus"
    "HOL-Library.Finite_Map"
  abbrevs "!!" = "!!"
begin

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

section ‹Algebra Structures›

subsection ‹Preliminary Structures›

subsubsection ‹Homomorphism-like›

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

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

locale homo_mult = homo_one φ
  for φ :: " 'a::{one,times} ⇒ 'b::{one,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 =
  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; simp)

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

thm add_nonneg_nonneg

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

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 = x * y ∧ x ## y)›
end

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

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

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_intuitive = sep_magma +
  assumes sep_disj_intuitive_right[simp]: ‹b ## c ⟹ a ## b * c ⟷ a ## b ∧ a ## c›
  assumes sep_disj_intuitive_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_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.mult_1_right local.sep_magma_1_left sep_magma.join_sub_def)
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 = x * y)›

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 apply standard
  by (metis local.mult_1_right local.positive_mult local.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:
  ‹r ## y ⟹ x ≼⇩S⇩L y ⟹ r * x ≼⇩S⇩L r * y›
  unfolding join_sub_def
  by (clarsimp, metis local.sep_disj_commuteI local.sep_disj_multI1 local.sep_mult_commute)

(*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_multD1 local.sep_disj_multI1 local.sep_mult_assoc sep_mult_left_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 Algebra›

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_sep_semigroup = sep_disj + times +
  assumes discrete_sep_disj[simp]: "x ## y ⟷ x = y"
    and discrete_mult[simp]: "x * y = (if x = y then x else undefined)"
begin
subclass sep_magma .
subclass sep_ab_semigroup proof
  fix x y z :: 'a
  show ‹x ## y ⟹ x * y = y * x› by simp
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y› unfolding 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 nonsepable_semigroup = sep_disj + times +
  assumes nonsepable_disj[simp]: "¬ x ## y"
begin
subclass sep_magma .
subclass sep_ab_semigroup by (standard; simp add: local.join_sub_def)
end

class nonsepable_monoid = sep_disj + mult_1 +
  assumes nonsepable_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.nonsepable_disj_1)
  show ‹x ## y * z ⟹ y ## z ⟹ x * y ## z›
    by (metis local.mult_1_left local.nonsepable_disj_1)
  show ‹x ≼⇩S⇩L y ⟹ y ≼⇩S⇩L x ⟹ x = y›
    unfolding join_sub_def apply clarsimp
    by (metis local.mult_1_left)
  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.nonsepable_disj_1)
  show ‹x * y ## z ⟹ x ## y ⟹ x ## y * z›
    by (metis local.mult_1_right local.nonsepable_disj_1)
  show ‹x ## y ⟹ y ## x›
    using local.nonsepable_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_multI1 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.›

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)

class share = raw_share + ― ‹share algebra for semigroup, where unit ‹1› is not defined›
  assumes share_share_not0: ‹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_not0 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_sep_disj = share + comm_sep_disj +
  assumes share_sep_disj_left[simp]: ‹0 < n ⟹ share n x ## y ⟷ x ## y›
(*    and   share_sep_disj_refl[simp]:  ‹n ≠ 0 ⟹ m ≠ 0 ⟹ share n x ## share m x› *)
begin

(* lemma share_sep_disj_refl_1 [simp]:
  ‹m ≠ 0 ⟹ x ## share m x›  ‹m ≠ 0 ⟹ share m x ## x›
  by (metis share_left_one share_sep_disj_refl)+ *)

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_semimodule_sep = share_sep_disj + sep_ab_semigroup +
  assumes share_sep_left_distrib_0:  ‹0 < n ⟹ 0 < m ⟹ x ## 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 ⟹ x ## x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x›
begin
lemma self_disj_I: ‹x ## y ⟹ x ## x ⟹ y ## y ⟹ x * y ## x * y›
  by (smt (verit, best) less_numeral_extra(1) local.sep_disj_commuteI local.sep_disj_multI2 local.sep_mult_assoc local.sep_mult_commute local.share_sep_disj_left local.share_sep_left_distrib_0 local.share_sep_right_distrib_0 zero_less_two)
end

class share_module_sep = share_sep_disj + share_one + sep_algebra +
  assumes share_sep_left_distrib:  ‹0 ≤ n ⟹ 0 ≤ m ⟹ x ## 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 ⟹ x ## x ⟹ share n x ≼⇩S⇩L x›
begin

subclass share_semimodule_sep proof
  fix x y :: 'a
  fix n m :: rat
  show ‹0 < n ⟹ 0 < m ⟹ x ## 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 ⟹ x ## x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x›
    by (simp add: local.share_sub)
qed
end

class share_semimodule_mult = share_one + monoid_mult +
  assumes share_left_distrib:  ‹0 ≤ n ⟹ 0 ≤ m ⟹ share n x * share m x = share (n+m) x›
    and   share_right_distrib: ‹0 ≤ n ⟹ share n x * share n y = share n (x * y)›

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

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

class share_resistence_sep_assms = raw_share + sep_disj + times +
  assumes share_resistence_sep_mult[simp]: ‹x ## x ⟹ x * x = x›

class share_resistence_semimodule_sep = share_resistence_semi + sep_disj + sep_ab_semigroup + share_resistence_sep_assms
begin
subclass share_semimodule_sep by (standard; simp add: join_sub_def)
end

class share_resistence_module_sep = share_resistence + sep_disj + sep_algebra + share_resistence_sep_assms
begin
subclass share_module_sep apply (standard; clarsimp simp add: join_sub_def)
  by (metis local.mult_1_left local.sep_magma_1_right)
end

subsection ‹Homomorphisms›

locale homo_sep_disj_total =
  fixes ψ :: ‹'a::sep_disj ⇒ 'b::sep_disj›
  assumes sep_disj_homo[iff]: ‹ψ a ## ψ b ⟷ a ## b›

lemma homo_sep_disj_total_comp:
  ‹ homo_sep_disj_total f
⟹ homo_sep_disj_total g
⟹ homo_sep_disj_total (f o g)›
  unfolding homo_sep_disj_total_def
  by simp

locale homo_sep_disj_semi =
  fixes ψ :: ‹'a::sep_disj ⇒ 'b::sep_disj›
  assumes sep_disj_homo_semi[simp]: ‹a ## b ⟶ ψ a ## ψ b› (* TODO: improve this to be a ⟷ ! *)

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›
  assumes homo_join_sub: ‹ψ x ≼⇩S⇩L ψ y ⟷ x ≼⇩S⇩L y›

locale homo_sep = homo_sep_mult ψ + homo_sep_disj_semi ψ
  for ψ :: ‹'a::sep_magma ⇒ 'b::sep_magma›

lemma homo_sep_comp:
  ‹homo_sep f ⟹ homo_sep g ⟹ homo_sep (f o g)›
  unfolding homo_sep_mult_def homo_sep_disj_semi_def homo_sep_def
  by simp

locale homo_sep_wand = homo_sep ψ
  for ψ :: ‹'a::sep_magma ⇒ 'b::sep_magma›
+ assumes homo_sep_wand: ‹a ## ψ b ⟹ a * ψ b = ψ c ⟷ (∃a'. a = ψ a' ∧ a' * b = c ∧ a' ## b)›
begin

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

end

locale homo_sep_wand_1 = homo_sep_wand ψ
  for ψ :: ‹'a::sep_magma_1 ⇒ 'b::sep_magma_1›
begin

sublocale homo_one ψ
  apply standard
  by (metis homo_sep_wand mult_1_class.mult_1_left mult_1_class.mult_1_right sep_magma_1_right)

end


lemma homo_sep_wand_comp:
  ‹homo_sep_wand f ⟹ homo_sep_wand g ⟹ homo_sep_wand (f o g)›
  unfolding homo_sep_wand_def homo_sep_wand_axioms_def
  apply (simp add: homo_sep_comp)
  using homo_sep.axioms(2) homo_sep_disj_semi.sep_disj_homo_semi by blast

lemma homo_sep_wand_1_comp:
  ‹homo_sep_wand_1 f ⟹ homo_sep_wand_1 g ⟹ homo_sep_wand_1 (f o g)›
  unfolding homo_sep_wand_1_def using homo_sep_wand_comp .


locale kernel_is_1 =
  fixes ψ :: " 'a::one ⇒ 'b::one"
  assumes inj_at_1: ‹∀x. ψ x = 1 ⟷ x = 1›

lemma kernel_is_1_comp:
  ‹kernel_is_1 f ⟹ kernel_is_1 g ⟹ kernel_is_1 (f o g)›
  unfolding kernel_is_1_def by simp

locale homo_sep_wand_monoid = homo_sep_wand_1 ψ
  for ψ :: ‹'a::sep_monoid ⇒ 'b::sep_monoid›
begin

sublocale kernel_is_1 ψ
  apply standard
  by (metis homo_join_sub homo_sep_wand join_sub.bot_least join_sub.le_bot mult_1_class.mult_1_left sep_magma_1_right)

end

lemma homo_sep_wand_monoid_comp:
  ‹homo_sep_wand_monoid f ⟹ homo_sep_wand_monoid g ⟹ homo_sep_wand_monoid (f o g)›
  unfolding homo_sep_wand_monoid_def using homo_sep_wand_1_comp .


(*
locale homo_sep_wand_1 = homo_sep_wand ψ
  for ψ :: ‹'a::sep_magma_1 ⇒ 'b::sep_magma_1›
begin
end *)

text ‹Insertion homomorphism from a separation algebra to a separation permission semimodule.›

locale perm_ins_homo = homo_sep_wand_monoid ψ
  for ψ :: ‹'a::sep_algebra ⇒ 'b::share_module_sep›
+ assumes join_sub_share_join_sub_whole: ‹0 < n ∧ n ≤ 1 ⟹ share n (ψ x) ≼⇩S⇩L ψ y ⟷ x ≼⇩S⇩L y›
    and   inj_ψ[simp]: ‹inj ψ›
    and   ψ_self_disj: ‹ψ x ## ψ x›
begin

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


end

locale perm_ins_homo_L =
  fixes ψ :: ‹'a::sep_algebra ⇒ 'b::share_module_sep›
  assumes perm_ins_homo': ‹id perm_ins_homo ψ›
begin
sublocale perm_ins_homo using perm_ins_homo'[simplified] .
end 

(*
lemma perm_ins_homo'_id[intro!,simp]:
  ‹perm_ins_homo' F ⟹ id perm_ins_homo' F›
  by simp*)

(*
lemma
  ‹perm_ins_homo' f ⟹ homo_sep_wand g ∧ inj_at_1 g ⟹ perm_ins_homo' (f o g)›
  unfolding perm_ins_homo'_def perm_ins_homo'_axioms_def
  apply (simp add: inj_at_1_comp homo_sep_wand_comp) *)



(* class unital_mult = plus + one +
  assumes unital_add_left[simp]: "1 * x = x"
    and unital_add_right[simp]: "x * 1 = x"

subclass (in monoid_mult) unital_mult .. simp_all *)


section ‹Instances of Algebras›

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

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 :: (type) one begin
definition [simp]: "one_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 :: (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_nonsepable[simp]:
  ‹x ## Some y ⟷ x = None›
  ‹Some y ## x ⟷ x = None›
  for y :: ‹'a :: nonsepable_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


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(1))
     apply (metis times_option_not_none(1))
    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


instantiation option :: (sep_semigroup) sep_semigroup begin
instance 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
end

instantiation option :: (sep_ab_semigroup) sep_ab_semigroup begin
instance 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
end

instantiation option :: (sep_ab_semigroup) sep_algebra begin
instance ..
end


instantiation option :: (share) share begin

definition ‹share_option n = (if 0 < n then map_option (share n) else (λ_. None))›

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 by (standard; simp add: share_option_def; case_tac x; simp add: share_share_not0)
end

instantiation option :: (sep_disj_intuitive) sep_disj_intuitive begin
instance 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
end

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

instantiation option :: (share_sep_disj) share_sep_disj begin
instance by (standard; case_tac x; simp add: share_option_def; case_tac y;
             simp add: share_sep_left_distrib_0 order_less_le)
end

instantiation option :: (share_semimodule_sep) share_module_sep begin
instance proof
  fix n m :: rat
  fix x y :: ‹'a option›
  show ‹0 ≤ n ⟹ 0 ≤ m ⟹ x ## 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 ∧ n ≤ 1 ⟹ x ## 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 sep_disj_option(2) share_left_one times_option(3))
    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 mult_1_class.mult_1_left sep_magma_1_right)
    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_nonsepable_semigroup_sub_join[simp]:
  ‹Some x ≼⇩S⇩L X ⟷ X = Some x›
  for x :: ‹'a::nonsepable_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



subsection ‹Product›

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

instantiation prod :: (one, one) one begin
definition "one_prod = (1,1)"
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 :: (numeral, numeral) numeral begin
instance ..
end

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)

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

instantiation prod :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult begin
instance by standard simp
end

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

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

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

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

instantiation prod :: (sep_disj_intuitive,sep_disj_intuitive) sep_disj_intuitive begin
instance by (standard; case_tac a; case_tac b; case_tac c; simp; blast)
end

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

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

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

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

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

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

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

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

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

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

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

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

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›

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

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

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

instantiation list :: (type) no_inverse begin
instance by (standard, simp add: times_list_def) blast
end

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

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

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 :: (type) sep_monoid begin
instance by (standard; clarsimp simp add: times_list_def join_sub_def)
end

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



subsection ‹Function›

paragraph ‹Instantiations of Algebra›

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


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[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 (in homo_zero) fun_updt_single_point[simp]:
  ‹φ o 0(i := x) = 0(i := φ x)›
  unfolding fun_eq_iff by simp

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



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

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

instantiation "fun" :: (type, semigroup_mult) semigroup_mult begin
instance apply standard
  by (simp add: mult.assoc times_fun_def)
end

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

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

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

lemma sep_disj_fun_nonsepable:
  ‹f x = Some v ⟹ f ## g ⟹ g x = None›
  ‹f x = Some v ⟹ g ## f ⟹ g x = None›
  for v :: ‹'a :: nonsepable_semigroup›
  by (metis sep_disj_fun sep_disj_option_nonsepable)+


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

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

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

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

instantiation "fun" :: (type,sep_semigroup) sep_semigroup begin
instance 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
end

instantiation "fun" :: (type,sep_ab_semigroup) sep_ab_semigroup begin
instance 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
end

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

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

instantiation "fun" :: (type,sep_disj_intuitive) sep_disj_intuitive begin
instance by (standard; simp add: sep_disj_fun_def times_fun; blast)
end

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

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


instantiation "fun" :: (type,monoid_add) monoid_add begin
instance 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
end

instantiation "fun" :: (type,comm_monoid_add) comm_monoid_add begin
instance 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
end


paragraph ‹Multiplication with Function Update›

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

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

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

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

lemma times_fupdt_1_fupdt_1[simp]:
  "(f * 1(k := x))(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]:
  "(f * 1(k := x))(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 ⟹ (f * 1(k' := x))(k:=1) = f(k:=1) * 1(k' := x)" for f :: "'a ⇒ 'b::monoid_mult"
  unfolding fun_upd_def fun_eq_iff times_fun_def by simp

lemma [simp]:
  "k' ≠ k ⟹ (f * 1(k' := x))(k:=1) = f(k:=1) * 1(k' := x)" 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 = f(k:=1) * 1(k:= f k)" 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_monoid"
  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_monoid"
  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_monoid"
  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 .


paragraph ‹Share›

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

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

instance by (standard; simp add: share_fun_def fun_eq_iff share_share_not0)
end

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

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

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

instantiation "fun" :: (type, share_module_sep) share_module_sep begin
instance apply (standard; simp_all add: share_fun_def fun_eq_iff times_fun_def share_sep_left_distrib
      sep_disj_fun_def share_sep_right_distrib join_sub_def)
  subgoal premises prems for n x proof -
    have t1: ‹∀a. share n (x a) ≼⇩S⇩L (x a)›
      by (simp add: prems share_sub)
    show ?thesis apply (insert t1; clarsimp simp add: join_sub_def)
      by metis
  qed .
end

instantiation "fun" :: (type, share_semimodule_mult) share_semimodule_mult begin
instance by standard (simp_all add: share_fun_def fun_eq_iff times_fun_def share_left_distrib share_right_distrib)
end

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


(*
paragraph ‹Complete Permission›

ML ‹
structure ML_Attribute = Generic_Data (
  type T = Thm.attribute option
  val empty : T = NONE
  fun merge (a,_) = a
)
›

attribute_setup ML_attr = ‹Scan.peek (fn ctxt => Parse.ML_source >> (fn src =>
  ML_Context.expression (Input.pos_of src)
    ( ML_Lex.read "Context.>> (ML_Attribute.put (SOME (Thm.rule_attribute [] (("
    @ ML_Lex.read_source src
    @ ML_Lex.read ") o Context.proof_of))))") ctxt
  |> ML_Attribute.get |> the
))›
 *)

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:
  ‹fmlookup (f * g) x = fmlookup f x * fmlookup g x› by (transfer; simp)
end

instantiation "fmap" :: (type,one) one begin
context includes fmap.lifting begin
lift_definition one_fmap :: ‹('a, 'b) fmap› is "(λ(x::'a). (1::'b option))" by simp
instance ..
end
end

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

instance "fmap" :: (type,mult_1) mult_1
  including fmap.lifting
  by (standard; 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

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

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


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

subsection ‹Set›

definition Inhabited :: " 'a set ⇒ bool" where  "Inhabited S = (∃p. p ∈ S)"

lemma Inhabited_I:
  ‹x ∈ S ⟹ Inhabited S›
  unfolding Inhabited_def ..

lemma Inhabited_cong[cong]:
  ‹X ≡ X ⟹ Inhabited X ≡ Inhabited X› .


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

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:
  ‹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 set_mult_inhabited[elim!]:
  ‹Inhabited (S * T) ⟹ (Inhabited S ⟹ Inhabited T ⟹ C) ⟹ C›
  unfolding Inhabited_def times_set_def by (simp, blast)

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+

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

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_intuitive) sep_disj_intuitive 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

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

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

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

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

lemma set_plus_inhabited[elim!]:
  ‹Inhabited (S + T) ⟹ (Inhabited S ⟹ C) ⟹ (Inhabited T ⟹ C) ⟹ C›
  unfolding Inhabited_def times_set_def by (simp, blast)

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

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

instantiation set :: (sep_ab_semigroup) ordered_comm_semiring begin
instance apply standard
  apply (simp add: zero_set_def plus_set_def times_set_def)
  using mult.commute apply blast
  by simp
end

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

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 :: nonsepable_semigroup)"
  unfolding sep_disj_fun_def sep_disj_option_def disjoint_iff
  by (smt (verit, ccfv_SIG) domD domIff nonsepable_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 :: nonsepable_semigroup)"
  using disjoint_iff sep_disj_partial_map_disjoint by fastforce

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


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

lemma nonsepable_semigroup_sepdisj_fun:
  ‹a ## 1(k ↦ x) ⟹ a ## 1(k := any)›
  for x :: ‹'b::nonsepable_semigroup›
  unfolding sep_disj_fun_def
  by (metis fun_upd_other fun_upd_same sep_magma_1_right sep_disj_option_nonsepable(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 f = dom f"
  by (metis 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 (f * 1(k:=v))) ⟷ finite (dom1 f)"
  for f :: "'a ⇒ 'b :: sep_monoid"
proof -
  have "dom1 (f * 1(k:=v)) = dom1 f ∨ dom1 (f * 1(k:=v)) = insert k (dom1 f)
    ∨ dom1 (f * 1(k:=v)) = 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::nonsepable_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) = f * 1(k:= v)" 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) = f * 1(k:= v)"
  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 perm_ins_homo_pointwise:
  assumes prem: ‹perm_ins_homo ψ›
  shows ‹perm_ins_homo ((∘) ψ)›
  unfolding comp_def
proof
  interpret xx: perm_ins_homo ψ using prem .

  fix x y z a b c :: ‹'c ⇒ 'a›
  fix a' :: ‹'c ⇒ 'b›
  fix n :: rat
  show ‹a ## b ⟶ (λx. ψ (a x)) ## (λx. ψ (b x))›
    by (simp add: fun_eq_iff times_fun sep_disj_fun_def)
  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' ## (λx. ψ (b x)) ⟹
     (a' * (λx. ψ (b x)) = (λx. ψ (c x))) = (∃a. a' = (λx. ψ (a x)) ∧ a * b = c ∧ a ## b)›
    by (simp add: fun_eq_iff times_fun sep_disj_fun_def xx.homo_sep_wand
            all_conj_distrib[symmetric], subst choice_iff[symmetric]; blast)

  show ‹inj (λg x. ψ (g x))›
    by (rule, simp add: fun_eq_iff inj_eq)
  (* show ‹∀x. ((λxa. ψ (x xa)) = 1) = (x = 1)›
    by (simp add: one_fun_def fun_eq_iff) *)
  show ‹(λxa. ψ (x xa)) ## (λxa. ψ (x xa))›
    by (simp add: sep_disj_fun_def xx.ψ_self_disj)

  have t2[unfolded join_sub_def]:
      ‹(∀n x y. 0 < n ∧ n ≤ 1 ⟶ (share n (ψ x) ≼⇩S⇩L ψ y) = (x ≼⇩S⇩L y))›
    using xx.join_sub_share_join_sub_whole by blast

  show ‹0 < n ∧ n ≤ 1 ⟹ (n :⩥ (λxa. ψ (x xa)) ≼⇩S⇩L (λx. ψ (y x))) = (x ≼⇩S⇩L y)›
    apply (simp add: join_sub_def fun_eq_iff times_fun sep_disj_fun_def share_fun_def
        all_conj_distrib[symmetric],
        subst choice_iff[symmetric], subst choice_iff[symmetric])
    using t2 by simp
qed

lemma perm_ins_homo_pointwise_eq[iff]:
  ‹perm_ins_homo ((∘) ψ) ⟷ perm_ins_homo ψ›
  for ψ :: ‹'b::sep_algebra ⇒ 'c::share_module_sep›
proof
  fix ψ :: ‹'b::sep_algebra ⇒ 'c::share_module_sep›
  assume prem: ‹perm_ins_homo ((∘) ψ :: ('a ⇒ 'b) ⇒ 'a ⇒ 'c)›
  show ‹perm_ins_homo ψ›
  proof
    interpret xx: perm_ins_homo ‹((∘) ψ :: ('a ⇒ 'b) ⇒ 'a ⇒ 'c)› using prem .
    fix x y a b c :: ‹'b› and a2 :: 'c and n :: rat
    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 ‹a2 ## ψ b ⟹ (a2 * ψ b = ψ c) = (∃a'. a2 = ψ a' ∧ a' * b = c ∧ a' ## b)›
      using xx.homo_sep_wand[unfolded sep_disj_fun_def times_fun one_fun_def fun_eq_iff,
          where a=‹λ_. a2› and b=‹λ_. b› and c=‹λ_. c›, simplified]
      by auto
    show ‹inj ψ›
      by (metis (no_types, opaque_lifting) fun_upd_comp inj_def mult_1_class.mult_1_left one_fun times_fupdt_1_apply_sep xx.inj_ψ)
    show ‹ψ x ## ψ x›
      by (metis fun_sep_disj_imply_v fun_upd_comp xx.ψ_self_disj)

    have x1[simp]: ‹⋀k v x. ψ ((1(k := v)) x) = (1(k := ψ v)) x›
      by (metis comp_apply fun_upd_apply one_fun xx.homo_one)
    have x2[simp]: ‹⋀k a b. (1(k := a) ≼⇩S⇩L 1(k := b)) ⟷ a ≼⇩S⇩L (b::'x::sep_algebra)›
      unfolding join_sub_def
      by (metis fun_1upd_homo_right1 fun_sep_disj_1_fupdt(1) fun_upd_same fun_upd_triv)
    have ‹∀(x::'a ⇒ 'b) y. 0 < n ∧ n ≤ 1 ⟶ (n :⩥ (λxa. ψ (x xa)) ≼⇩S⇩L (λx. ψ (y x))) = (x ≼⇩S⇩L y)›
      using xx.join_sub_share_join_sub_whole[unfolded sep_disj_fun_def times_fun one_fun_def fun_eq_iff comp_def, simplified]
      by fastforce
    then have ‹0 < n ∧ n ≤ 1 ⟶ (∀(x::'a ⇒ 'b) y. (n :⩥ (λxa. ψ (x xa)) ≼⇩S⇩L (λx. ψ (y x))) = (x ≼⇩S⇩L y))›
      by blast
    from this[THEN mp, THEN spec[where x=‹1(undefined := x)›], THEN spec[where x=‹1(undefined := y)›],
          simplified x1 x2 share_1_fupdt]
    show ‹0 < n ∧ n ≤ 1 ⟹ (n :⩥ ψ x ≼⇩S⇩L ψ y) = (x ≼⇩S⇩L y)› .
  qed
next
  show ‹perm_ins_homo ψ ⟹ perm_ins_homo ((∘) ψ)›
    using perm_ins_homo_pointwise .
qed



subsubsection ‹Subsumption›

lemma nonsepable_partial_map_subsumption:
  ‹f ≼⇩S⇩L g ⟹ k ∈ dom1 f ⟹ g k = f k›
  for f :: ‹'k ⇒ 'v::nonsepable_monoid›
  unfolding join_sub_def
  apply (clarsimp simp add: times_fun)
  by (metis disjoint_dom1_eq_1(1) mult_1_class.mult_1_left sep_disj_commute sep_disj_dom1_disj_disjoint)

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

lemma nonsepable_partial_map_subsumption_L2:
  ‹ 1(k := v) ≼⇩S⇩L objs
⟹ v ⊆⇩m objs k›
  for v :: ‹'b ⇒ 'c::nonsepable_semigroup option›
  unfolding join_sub_def map_le_def
  apply (clarsimp simp add: times_fun)
  by (metis (mono_tags, opaque_lifting) fun_upd_same mult_1_class.mult_1_left one_option_def sep_disj_fun_def sep_disj_partial_map_some_none)


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

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

instantiation share :: (type) sep_ab_semigroup begin
instance 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
end

instantiation share :: (type) sep_disj_intuitive begin
instance by (standard; case_tac a; case_tac b; case_tac c; simp)
end

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

instantiation share :: (type) share_semimodule_sep begin
instance 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 ‹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 ⟹ x ## x ⟹ share n x ≼⇩S⇩L x ∨ share n x = x›
    apply (cases x; cases y; simp add: join_sub_def share_exists)
    by (metis add.commute add_le_same_cancel1 diff_add_cancel linorder_not_le mult_1_class.mult_1_left mult_less_cancel_right)
qed
end



subsubsection ‹Convert a function to sharing or back›

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

lemma perm_ins_homo_to_share[iff]:
  ‹perm_ins_homo (to_share::'a::nonsepable_semigroup option ⇒ 'a share option)›
proof
  fix x y z a b c :: ‹'a option›
  fix a' :: ‹'a share option›
  fix n :: rat
  show ‹a ## b ⟶ to_share a ## to_share b› by (cases a; cases b; simp)
  show ‹x ## y ⟹ to_share (x * y) = to_share x * to_share y› by (cases x; cases y; simp)
  show ‹a' ## to_share b ⟹
       (a' * to_share b = to_share c) = (∃a. a' = to_share a ∧ a * b = c ∧ a ## b)›
    apply (cases a'; cases b; cases c; simp add: split_option_ex)
    subgoal for a'' by (cases a''; simp) .
  show ‹inj to_share›
    by (rule, simp, metis option.inj_map_strong share.inject)
  show ‹to_share x ## to_share x› by (cases x; simp)
  show ‹0 < n ∧ n ≤ 1 ⟹ (n :⩥ to_share x ≼⇩S⇩L to_share y) = (x ≼⇩S⇩L y)›
    apply (cases a'; cases x; cases y; simp add: join_sub_def split_option_ex share_forall share_exists
          share_All)
    apply (metis add.commute add_le_same_cancel1 diff_add_cancel linorder_not_le nle_le)
    by (metis Orderings.order_eq_iff diff_add_cancel less_add_same_cancel2 linorder_le_less_linear)
qed


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

lemma to_share_funcomp_1[simp]:
  ‹to_share 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 to_share_funcomp_map_add:
  ‹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::nonsepable_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::nonsepable_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 to_share_ringop_id[simp]:
  ‹to_share ∘ x = to_share ∘ y ⟷ x = y›
  unfolding fun_eq_iff
  by (simp, metis strip_share_Share)


subsection ‹Non-sepable Semigroup›

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

instantiation nosep :: (type) nonsepable_semigroup begin
definition ‹sep_disj_nosep (x :: 'a nosep) (y :: 'a nosep) = False›
definition share_nosep :: ‹rat ⇒ 'a nosep ⇒ 'a nosep›
  where [simp]: ‹share_nosep _ x = x›
definition times_nosep :: ‹'a nosep ⇒ 'a nosep ⇒ 'a nosep›
  where [simp]: ‹times_nosep x y = undefined›
instance by (standard; case_tac x; simp; case_tac y; simp add: sep_disj_nosep_def)
end

instance nosep :: (type) sep_disj_intuitive by (standard; case_tac a; case_tac b; case_tac c; simp)

instance nosep :: (type) ab_semigroup_mult
  by (standard; case_tac a; case_tac b; simp; case_tac c; 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 :: (type) share_semimodule_sep 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 ⟹ x ## 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)
qed
end

instantiation agree :: (type) sep_disj_intuitive begin
instance by (standard; case_tac a; case_tac b; case_tac c; simp)
end


section ‹Interpretation of Fictional Separation›

subsection ‹Algebric Structure›

text ‹
  Referring to Fictional Separation Logic~\cite{FSL}, the interpretation of fictional separation
  maps a fictional resource to a set of concrete resource.
  The interpretation can be any map to set that preserves ‹1›, the unit of the separation algebra.›

definition Interpretation :: "('a::one ⇒ 'b::one set) ⇒ bool"
  where "Interpretation ℐ ⟷ ℐ 1 = 1"

typedef (overloaded) ('a::one,'b::one) interp
    = ‹Collect (Interpretation :: ('a ⇒ 'b set) ⇒ bool)›
  morphisms ℐ Interp
  by (rule exI[where x = ‹λ_. 1›]) (simp add:sep_mult_commute Interpretation_def)

text ‹Type ‹('a,'b) interp› encapsulating the 1-preserving condition, represents an interpretation.
\<^const>‹ℐ› activates the interpretation; \<^const>‹Interp› constructs an interpretation by checking
the 1-preserving condition.
\[@{thm Interp_inverse[simplified]}\]›

lemmas Interp_inverse[simp] = Interp_inverse[simplified]

lemma Interp_one[simp]: "ℐ I 1 = 1"
  using Interpretation_def ℐ by blast


subsection ‹Instances›


subsubsection ‹Function, pointwise›

definition "ℱ_fun' I = Interp (λf. prod (λx. ℐ (I x) (f x)) (dom1 f))"

lemma ℱ_fun'_ℐ[simp]: "ℐ (ℱ_fun' I) = (λf. prod (λx. ℐ (I x) (f x)) (dom1 f))"
  unfolding ℱ_fun'_def by (rule Interp_inverse) (simp add: Interpretation_def)

lemma ℱ_fun'_split:
  " finite (dom1 f)
⟹ ℐ (ℱ_fun' I) f = ℐ (ℱ_fun' I) (f(k:=1)) * ℐ (I k) (f k)
   ∧ ℐ (ℱ_fun' I) (f(k:=1)) ## ℐ (I k) (f k)"
  for f :: "'a ⇒ 'b::sep_algebra"
  by simp (smt (verit, best) Interp_one dom1_upd fun_upd_triv mult.comm_neutral mult.commute prod.insert_remove)


definition "ℱ_fun I = ℱ_fun' (λ_. I)"

lemma ℱ_fun_ℐ[simp]: "ℐ (ℱ_fun I) = (λf. prod (ℐ I o f) (dom1 f))"
  unfolding ℱ_fun_def by simp

lemma ℱ_fun_split:
  " finite (dom1 f)
⟹ ℐ (ℱ_fun I) f = ℐ (ℱ_fun I) (f(k:=1)) * ℐ I (f k)
  ∧ ℐ (ℱ_fun I) (f(k:=1)) ## ℐ I (f k)"
  for f :: "'a ⇒ 'b::sep_algebra"
  unfolding ℱ_fun_def using ℱ_fun'_split .

lemma ℱ_interp_fun_ℐ_1_fupdt[simp]: "ℐ (ℱ_fun I) (1(k:=v)) = ℐ I v" by simp


definition "ℱ_pointwise I = Interp (λf. {g. ∀x. g x ∈ ℐ I (f x) })"

lemma ℱ_pointwise_ℐ[simp]:
  "ℐ (ℱ_pointwise I) = (λf. {g. ∀x. g x ∈ ℐ I (f x) })"
  unfolding ℱ_pointwise_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def one_fun_def fun_eq_iff)


definition "ℱ_pointwise' I = Interp (λf. {g. ∀x. g x ∈ ℐ (I x) (f x) })"

lemma ℱ_pointwise'_ℐ[simp]:
  "ℐ (ℱ_pointwise' I) = (λf. {g. ∀x. g x ∈ ℐ (I x) (f x) })"
  unfolding ℱ_pointwise'_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def one_fun_def fun_eq_iff)



subsubsection ‹Pairwise›

definition "ℱ_pair I1 I2 = Interp (λ(x,y). ℐ I1 x * ℐ I2 y) "

lemma ℱ_pair_ℐ[simp]: "ℐ (ℱ_pair I1 I2) = (λ(x,y). ℐ I1 x * ℐ I2 y)"
  for I1 :: "('a::one,'b::sep_monoid) interp"
  unfolding ℱ_pair_def
  by (rule Interp_inverse) (simp add: Interpretation_def one_prod_def)

notation ℱ_pair (infixl "∙⇩ℱ" 50)


subsubsection ‹Option›

definition "ℱ_option I = Interp (case_option 1 I)"

lemma ℱ_option_ℐ[simp]: "ℐ (ℱ_option I) = (case_option 1 I)"
  unfolding ℱ_option_def
  by (rule Interp_inverse) (simp add: Interpretation_def)


definition "ℱ_optionwise I = Interp (λx. case x of Some x' ⇒ Some ` I x' | _ ⇒ {None})"

lemma ℱ_optionwise_ℐ[simp]:
  "ℐ (ℱ_optionwise I) = (λx. case x of Some x' ⇒ Some ` I x' | _ ⇒ {None})"
  unfolding ℱ_optionwise_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def)


(* subsubsection ‹Partiality›

definition "fine I = Interp (case_fine (ℐ I) {})"
lemma fine_ℐ[simp]: "ℐ (fine I) = case_fine (ℐ I) {}"
  unfolding fine_def by (rule Interp_inverse) (simp add: Interpretation_def one_fine_def)

definition "defined I = Interp (λx. Fine ` ℐ I x)"
lemma defined_ℐ[simp]: "ℐ (defined I) = (λx. Fine ` ℐ I x)"
  unfolding defined_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def one_fine_def)

definition "partialwise I = ℱ_fine (defined I)"
lemma partialwise_ℐ[simp]: "ℐ (partialwise I) (Fine x) = { Fine y |y. y ∈ ℐ I x }"
  unfolding partialwise_def by auto
*)

subsubsection ‹Exact Itself›

definition [simp]: "ℱ_it' x = {x}"

definition "ℱ_it = Interp ℱ_it'"

lemma ℱ_it_ℐ[simp]: "ℐ ℱ_it = ℱ_it'"
  unfolding ℱ_it_def
  by (rule Interp_inverse) (simp add: Interpretation_def one_set_def)



subsubsection ‹Functional Fiction›

definition ‹ℱ_functional ψ = Interp (λx. {y. x = ψ y})›

lemma (in kernel_is_1) ℱ_functional_ℐ[simp]:
  ‹ℐ (ℱ_functional ψ) = (λx. {y. x = ψ y})›
  unfolding ℱ_functional_def
  by (rule Interp_inverse, simp add: Interpretation_def one_set_def set_eq_iff inj_at_1)

lemma map_option_inj_at_1[simp]:
  ‹kernel_is_1 (map_option f)›
  unfolding one_option_def kernel_is_1_def
  by (simp add: split_option_all)


definition "ℱ_share s = (case s of Share w v ⇒ if w = 1 then {v} else {})"

lemma ℱ_share_ℐ[simp]: "ℱ_share (Share w v) = (if w = 1 then {v} else {})"
  unfolding ℱ_share_def by simp

(* lemma In_ficion_fine [simp]:
  ‹x ∈ (case some_fine of Fine y ⇒ f y | Undef ⇒ {})
        ⟷ (∃y. some_fine = Fine y ∧ x ∈ f y)›
  by (cases some_fine; simp)
*)

subsubsection ‹Agreement›

definition ‹ℱ_agree = (λx. case x of agree x' ⇒ {x'})›



end