Theory Quantale_Models

(* Title: Models of Quantales
   Author: Georg Struth
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Models of Quantales›

theory Quantale_Models
  imports Quantales
  "Dioid_Models_New"

begin

text ‹Most of the models in this section expand those of dioids (and hence Kleene algebras). They really belong here, 
because quantales form a stronger setting than dioids or Kleene algebras. They are, however, subsumed by the general lifting
results of partial semigroups and monoids from another AFP entry~\<^cite>‹"DongolGHS17"›.›


subsection ‹Quantales of Booleans›

instantiation bool :: bool_ab_unital_quantale
begin
  
definition "one_bool = True"
  
definition "times_bool = (∧)"

instance
  by intro_classes (auto simp: times_bool_def one_bool_def)

end
  
lemma bool_sep_eq_conj [simp]: "((x :: bool) * y) = (x ∧ y)"
  by (auto simp: times_bool_def)
  
lemma bool_impl_eq [simp]: "(x :: bool) → y = -x ⊔ y"
  by (clarsimp simp: bres_def)
  
subsection ‹Powerset Quantales of Semigroups and Monoids›

instance set :: (semigroup_mult) quantale
  by intro_classes (auto simp: times_set_def)

text ‹With the definition of products on powersets (from the component of models of dioids) one
can prove the following mixed distributivity law.›

lemma comp_dist_mix: "⨆(X::'a::quantale set) ⋅ ⨆Y = ⨆(X ⋅ Y)"
proof-
  have "⨆X ⋅ ⨆Y = (⨆x ∈ X. ⨆y ∈ Y. x ⋅ y)"
    by (metis (no_types, lifting) SUP_cong Sup_distl Sup_distr)
  also have "... = ⨆{⨆{x ⋅ y|y. y ∈ Y} |x. x ∈ X}"
    by (simp add: setcompr_eq_image)
  also have "... = ⨆{x ⋅ y |x y. x ∈ X ∧ y ∈ Y}"
    apply (rule antisym)
     apply (rule Sup_least, smt Collect_mono Sup_subset_mono mem_Collect_eq)
    by (rule Sup_least, smt Sup_upper calculation mem_Collect_eq psrpq.mult_isol_var)
  finally show ?thesis
    by (simp add: times_set_def)
qed

text ‹Powerset quantales of monoids can nevertheless be formalised as instances.›

instance set :: (monoid_mult) unital_quantale..


text ‹There is much more to this example. In fact, every quantale can be represented, up to isomorphism, 
as a certain quotient of a powerset quantale over some semigroup~\<^cite>‹"Rosenthal90"›. This representation theorem is 
formalised in the section on nuclei.›


subsection ‹Language, Relation, Trace and Path Quantales›

text ‹The language quantale is implcit in the powerset quantale over a semigroup or monoid. The free list monoid has
already been linked with the class of monoid as an instance in Isabelle's dioid components~\<^cite>‹"ArmstrongSW13"›. I provide an alternative
interpretation. In all of the following locale statements, an interpretation for Sup-quantales fails, due to the occurance of some low level
less operations in the underlying model...›

interpretation lan_quantale: unital_quantale "1::'a lan" "(⋅)" Inf Sup inf "(⊆)" "(⊂)" sup "0" UNIV
  by unfold_locales (simp_all add: Inf_lower Inter_greatest Sup_upper Sup_least zero_set_def Sup_distr Sup_distl)

text ‹The relation quantale follows.›

interpretation rel_quantale: unital_quantale Id relcomp Inf Sup inf "(⊆)" "(⊂)" sup "{}" "UNIV"
  by (unfold_locales, auto) 

text ‹Traces alternate between state and action symbols, the first and last symbol of a trace being state symbols.
They can be associated with behaviours of automata or executions of programs.›

interpretation trace_quantale: unital_quantale t_one t_prod Inf Sup inf "(⊆)" "(⊂)" sup t_zero UNIV
  by unfold_locales (auto simp: Inf_lower Inf_greatest Sup_upper Sup_least t_zero_def t_prod_def t_fusion_def)

text ‹The final model corresponds to paths as sequences of states of an automata, transition system or graph.›

interpretation path_quantale: unital_quantale p_one p_prod Inter Union "(∩)" "(⊆)" "(⊂)" "(∪)" "{}" UNIV
  by unfold_locales (auto simp: p_prod_def)

text ‹Rosenthal's book contains a wealth of other examples. Many of them come from ring theory 
(e.g. the additive subgroups of a ring form a quantale and so do the left, right and two-sided ideals). Others are based
on the interval $[0,\infty]$. The first line of models was the original motivation for the study of quantales, the second 
one is important to Lawvere's categorical generalisation of metric spaces. These examples are left for future consideration.›

end