Theory Partial_Semigroup_Models

(* Title: Models of Partial Semigroups
   Author: Brijesh Dongol, Victor Gomes, Ian J Hayes, Georg Struth
   Maintainer: Victor Gomes <>
               Georg Struth <> 

section ‹Models of Partial Semigroups›

theory Partial_Semigroup_Models
  imports Partial_Semigroups
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

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

  by standard (transfer, force)+


instantiation "dprod" :: (type) partial_monoid

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

  by standard (transfer,force)+

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

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

  by standard (transfer, force)+
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] *)

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)

interpretation pfun: positive_cancellative_pam_one map_add ortho "{Map.empty}" Map.empty
  apply (standard, auto simp: ortho_def pfun_canc)
  by (simp_all add: inf_commute map_add_comm 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

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"

  by standard (auto simp: D_set_def times_set_def)


instantiation set :: (type) pam

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

  by standard (auto simp: D_set_def times_set_def E_set_def)