# Theory Partial_Semigroup_Models

```(* Title: Models of Partial Semigroups
Author: Brijesh Dongol, Victor Gomes, Ian J Hayes, Georg Struth
Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
Georg Struth <g.struth@sheffield.ac.uk>
*)

section ‹Models of Partial Semigroups›

theory Partial_Semigroup_Models
imports Partial_Semigroups

begin

text ‹So far this section collects three models that we need for applications. Other interesting models might be
added in the future. These might include binary relations, formal power series and matrices, paths in graphs under fusion,
program traces with alternating state and action symbols under fusion, partial orders under series and parallel products.›

subsection ‹Partial Monoids of Segments and Intervals›

text ‹Segments of a partial order are sub partial orders between two points. Segments generalise
intervals in that intervals are segments in linear orders. We formalise segments and intervals as pairs,
where the first coordinate is smaller than the second one. Algebras of segments and intervals are interesting
in Rota's work on the foundations of combinatorics as well as for interval logics and duration calculi.›

text ‹First we define the subtype of ordered pairs of one single type.›

typedef 'a dprod = "{(x::'a, y::'a). True}"
by simp

setup_lifting type_definition_dprod

text ‹Such pairs form partial semigroups and partial monoids with respect to fusion.›

instantiation dprod :: (type) partial_semigroup
begin

lift_definition D_dprod :: "'a dprod ⇒ 'a dprod ⇒ bool" is "λx y. (snd x = fst y)" .

lift_definition times_dprod :: "'a dprod ⇒ 'a dprod ⇒ 'a dprod" is "λx y. (fst x, snd y)"
by simp

instance
by standard (transfer, force)+

end

instantiation "dprod" :: (type) partial_monoid
begin

lift_definition E_dprod :: "'a dprod set" is "{x. fst x = snd x}"
by simp

instance
by standard (transfer,force)+

end

text ‹Next we define the type of segments.›

typedef (overloaded) 'a segment = "{x::('a::order × 'a::order). fst x ≤ snd x}"
by force

setup_lifting type_definition_segment

text ‹Segments form partial monoids as well.›

instantiation segment :: (order) partial_monoid
begin

lift_definition E_segment :: "'a segment set" is "{x. fst x = snd x}"
by simp

lift_definition D_segment :: "'a::order segment ⇒ 'a segment ⇒ bool"
is "λx y. (snd x = fst y)" .

lift_definition times_segment :: "'a::order segment ⇒ 'a segment ⇒ 'a segment"
is "λx y. if snd x = fst y then (fst x, snd y) else x"
by auto

instance
by standard (transfer, force)+

end

text ‹Next we define the function segm that maps segments-as-pairs to segments-as-sets.›

definition segm :: "'a::order segment ⇒ 'a set" where
"segm x = {y. fst (Rep_segment x) ≤ y ∧ y ≤ snd (Rep_segment x)}"

thm Rep_segment

lemma segm_sub_morph: "snd (Rep_segment x) = fst (Rep_segment y) ⟹ segm x ∪ segm y ≤ segm (x ⋅ y)"
apply (simp add: segm_def times_segment.rep_eq, safe)
using Rep_segment dual_order.trans apply blast
by (metis (mono_tags, lifting) Rep_segment dual_order.trans mem_Collect_eq)

text ‹The function segm is not generally a morphism.›

lemma "snd (Rep_segment x) = fst (Rep_segment y) ⟹ segm x ∪ segm y = segm (x ⋅ y)" (* nitpick [expect=genuine] *)
oops

text ‹Intervals are segments over orders that satisfy Halpern and Shoham's  linear order property. This
is still more general than linearity of the poset.›

class lip_order = order +
assumes lip: "x ≤ y ⟹ (∀v w. (x ≤ v ∧ v ≤ y ∧ x ≤ w ∧ w ≤ y ⟶ v ≤ w ∨ w ≤ v))"

text ‹The function segm is now a morphism.›

lemma segm_morph: "snd (Rep_segment x::('a::lip_order × 'a::lip_order)) = fst (Rep_segment y)
⟹ segm x ∪ segm y = segm (x ⋅ y)"
apply (transfer, clarsimp simp add: Abs_segment_inverse lip, safe)
apply force+
by (meson lip order_trans)

subsection ‹Cancellative PAM's of Partial Functions›

text ‹We show that partial functions under disjoint union form a positive cancellative PAM.
This is interesting for modeling the heap in separation logic.›

type_synonym 'a pfun = "'a ⇒ 'a option"

definition ortho :: "'a pfun ⇒ 'a pfun ⇒ bool"
where "ortho f g ≡ dom f ∩ dom g = {}"

lemma pfun_comm: "ortho x y ⟹ x ++ y = y ++ x"
by (force simp: ortho_def intro!: map_add_comm)

lemma pfun_canc: "ortho z x ⟹ ortho z y ⟹ z ++ x = z ++ y ⟹ x = y"
apply (auto simp: ortho_def map_add_def option.case_eq_if fun_eq_iff)
by (metis domIff dom_restrict option.collapse restrict_map_def)

interpretation pfun: positive_cancellative_pam_one map_add ortho "{Map.empty}" Map.empty
apply (standard, auto simp: ortho_def pfun_canc)

subsection ‹PAM's of Disjoint Unions of Sets›

text ‹This simple disjoint union construction underlies important compositions of graphs or partial orders,
in particular in the context of complete joins and disjoint unions of graphs and of series and parallel products
of partial orders.›

instantiation set :: (type) pas
begin

definition D_set :: "'a set ⇒ 'a set ⇒ bool" where
"D_set x y ≡ x ∩ y = {}"

definition times_set :: "'a set ⇒ 'a set ⇒ 'a set" where
"times_set x y = x ∪ y"

instance
by standard (auto simp: D_set_def times_set_def)

end

instantiation set :: (type) pam
begin

definition E_set :: "'a set set" where
"E_set = {{}}"

instance
by standard (auto simp: D_set_def times_set_def E_set_def)

end

end

```