Theory Partial_Semigroup_Models
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)"
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 (simp add: segm_def times_segment_def)
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)