(* 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 (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)