Theory Modal_Kleene_Algebra_Models

(* Title:      Models of Modal Kleene Algebras
   Author:     Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
   Maintainer: Walter Guttmann <walter.guttman at canterbury.ac.nz>
               Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Models of Modal Kleene Algebras›

theory Modal_Kleene_Algebra_Models
imports Kleene_Algebra.Kleene_Algebra_Models
  Modal_Kleene_Algebra

begin

text ‹
  This section develops the relation model. We also briefly develop the trace model for
  antidomain Kleene algebras, but not for antirange or full modal Kleene algebras.
  The reason is that traces are implemented as lists; we therefore expect tedious inductive
  proofs in the presence of range. The language model is not particularly interesting.
›

definition rel_ad :: "'a rel ⇒ 'a rel" where
  "rel_ad R = {(x,x) | x. ¬ (∃y. (x,y) ∈ R)}"

interpretation rel_antidomain_kleene_algebra: antidomain_kleene_algebra rel_ad "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl
by unfold_locales (auto simp: rel_ad_def)

definition trace_a :: "('p, 'a) trace set ⇒ ('p, 'a) trace set" where
  "trace_a X = {(p,[]) | p. ¬ (∃x. x ∈ X ∧ p = first x)}"

interpretation trace_antidomain_kleene_algebra: antidomain_kleene_algebra trace_a "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)" t_star
proof
  show "⋀x. t_prod (trace_a x) x = t_zero"
    by (auto simp: trace_a_def t_prod_def t_fusion_def t_zero_def)
  show "⋀x y. trace_a (t_prod x y) ∪ trace_a (t_prod x (trace_a (trace_a y))) = trace_a (t_prod x (trace_a (trace_a y)))"
    by (auto simp: trace_a_def t_prod_def t_fusion_def)
  show "⋀x. trace_a (trace_a x) ∪ trace_a x = t_one"
    by (auto simp: trace_a_def t_one_def)
qed

text ‹The trace model should be extended to cover modal Kleene algebras in the future.›

definition rel_ar :: "'a rel ⇒ 'a rel" where
  "rel_ar R = {(y,y) | y. ¬ (∃x. (x,y) ∈ R)}"

interpretation rel_antirange_kleene_algebra: antirange_semiring "(∪)" "(O)" Id "{}" rel_ar "(⊆)" "(⊂)"
apply unfold_locales
apply (simp_all add: rel_ar_def)
by auto

interpretation rel_modal_kleene_algebra: modal_kleene_algebra "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl rel_ad rel_ar
apply standard
apply (metis (no_types, lifting) rel_antidomain_kleene_algebra.a_d_closed rel_antidomain_kleene_algebra.a_one rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.am5_lem rel_antidomain_kleene_algebra.am6_lem rel_antidomain_kleene_algebra.apd_d_def rel_antidomain_kleene_algebra.dka.dns1 rel_antidomain_kleene_algebra.dpdz.dom_one rel_antirange_kleene_algebra.ardual.a_comm' rel_antirange_kleene_algebra.ardual.a_d_closed rel_antirange_kleene_algebra.ardual.a_mul_d' rel_antirange_kleene_algebra.ardual.a_mult_idem rel_antirange_kleene_algebra.ardual.a_zero rel_antirange_kleene_algebra.ardual.ads_d_def rel_antirange_kleene_algebra.ardual.am6_lem rel_antirange_kleene_algebra.ardual.apd_d_def rel_antirange_kleene_algebra.ardual.s4)
by (metis rel_antidomain_kleene_algebra.a_zero rel_antidomain_kleene_algebra.addual.ars1 rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.am5_lem rel_antidomain_kleene_algebra.am6_lem rel_antidomain_kleene_algebra.ds.ddual.mult_oner rel_antidomain_kleene_algebra.s4 rel_antirange_kleene_algebra.ardual.ads_d_def rel_antirange_kleene_algebra.ardual.am6_lem rel_antirange_kleene_algebra.ardual.apd1 rel_antirange_kleene_algebra.ardual.dpdz.dns1'')

end