Theory Modal_Kleene_Algebra_Converse

(* 
Title: Modal Kleene Algebra with converse
Author: Cameron Calk, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Modal Kleene algebra with converse›

theory "Modal_Kleene_Algebra_Converse"
  imports Modal_Kleene_Algebra_Var Kleene_Algebra_Converse

begin

text ‹Here we mainly study the interaction of converse with domain and codomain.›

subsection ‹Involutive modal Kleene algebras›

class involutive_domain_semiring = domain_semiring + involutive_dioid

begin

notation domain_op ("dom")

lemma strong_conv_conv: "dom x ≤ x ⋅ x⇧∘ ⟹ x ≤ x ⋅ x⇧∘ ⋅ x"
proof-
  assume h: "dom x ≤ x ⋅ x⇧∘"
  have "x = dom x ⋅ x"
    by simp
  also have "… ≤  x ⋅ x⇧∘ ⋅ x"
    using h local.mult_isor by presburger
  finally show ?thesis.
qed

end

class involutive_dr_modal_semiring  = dr_modal_semiring + involutive_dioid

class involutive_dr_modal_kleene_algebra = involutive_dr_modal_semiring + kleene_algebra


subsection ‹Modal semirings algebras with converse›

class dr_modal_semiring_converse = dr_modal_semiring + dioid_converse

begin

lemma d_conv [simp]: "(dom x)⇧∘ = dom x"
proof-
  have "dom x ≤ dom x ⋅ (dom x)⇧∘ ⋅ dom x"
    by (simp add: local.strong_gelfand)
  also have  "… ≤ 1 ⋅ (dom x)⇧∘ ⋅ 1"
    by (simp add: local.subid_conv)
  finally have a: "dom x ≤ (dom x)⇧∘"
    by simp
  hence "(dom x)⇧∘ ≤ dom x"
    by (simp add: local.inv_adj)
  thus ?thesis
    using a by auto
qed

lemma cod_conv: "(cod x)⇧∘ = cod x"
  by (metis d_conv local.dc_compat)

lemma d_conv_cod [simp]: "dom (x⇧∘) = cod x"
proof-
  have "dom (x⇧∘) = dom ((x ⋅ cod x)⇧∘)"
    by simp
  also have "… = dom ((cod x)⇧∘ ⋅ x⇧∘)"
    using local.inv_contrav by presburger
  also have "… = dom (cod x ⋅ x⇧∘)"
    by (simp add: cod_conv)
  also have "… = dom (dom (cod x) ⋅ x⇧∘)"
    by simp
  also have "… = dom (cod x) ⋅ dom (x⇧∘)"
    using local.dsg3 by blast
  also have "… = cod x ⋅ dom (x⇧∘)"
    by simp
  also have "… = cod x ⋅ cod (dom (x⇧∘))"
    by simp
  also have "… = cod (x ⋅ cod (dom (x⇧∘)))"
    using local.rdual.dsg3 by presburger
  also have "… = cod (x ⋅ dom (x⇧∘))"
    by simp
  also have "… = cod ((x⇧∘)⇧∘ ⋅ (dom (x⇧∘))⇧∘)"
    by simp
  also have "… = cod ((dom (x⇧∘) ⋅ x⇧∘)⇧∘)"
    using local.inv_contrav by presburger
  also have "… = cod ((x⇧∘)⇧∘)"
    by simp
  also have "… = cod x"
    by simp
  finally show ?thesis.
qed

lemma cod_conv_d: "cod (x⇧∘) = dom x"
  by (metis d_conv_cod local.inv_invol)

lemma "dom y = y ⟹ fd (x⇧∘) y = bd x y"
proof-
  assume h: "dom y = y"
  have "fd (x⇧∘) y = dom (x⇧∘ ⋅ dom y)"
    by (simp add: local.fd_def)
  also have "… = dom ((dom y ⋅ x)⇧∘)"
    by simp
  also have "… = cod (dom y ⋅ x)"
    using d_conv_cod by blast
  also have "… = bd x y"
    by (simp add: h local.bd_def)
  finally show ?thesis.
qed

lemma "dom y = y ⟹ bd (x⇧∘) y = fd x y"
  by (metis cod_conv_d d_conv local.bd_def local.fd_def local.inv_contrav)

end


subsection ‹Modal Kleene algebras with converse›

class dr_modal_kleene_algebra_converse = dr_modal_semiring_converse + kleene_algebra

class dr_modal_semiring_strong_converse = involutive_dr_modal_semiring + 
  assumes weak_dom_def: "dom x ≤ x ⋅ x⇧∘"
  and weak_cod_def: "cod x ≤ x⇧∘ ⋅ x"

subclass (in dr_modal_semiring_strong_converse) dr_modal_semiring_converse
  by unfold_locales (metis local.ddual.mult_isol_var local.dsg1 local.eq_refl local.weak_dom_def)

class dr_modal_kleene_algebra_strong_converse = dr_modal_semiring_strong_converse + kleene_algebra

end