Theory Modal_Kleene_Algebra
section ‹Modal Kleene Algebras›
text ‹This section studies laws that relate antidomain and antirange semirings and Kleene algebra,
notably Galois connections and conjugations as those studied in~\<^cite>‹"MoellerStruth" and "DesharnaisStruthSCP"›.›
theory Modal_Kleene_Algebra
imports Range_Semiring
begin
class modal_semiring = antidomain_semiring + antirange_semiring +
assumes domrange [simp]: "d (r x) = r x"
and rangedom [simp]: "r (d x) = d x"
begin
text ‹These axioms force that the domain algebra and the range algebra coincide.›
lemma domrangefix: "d x = x ⟷ r x = x"
by (metis domrange rangedom)
lemma box_diamond_galois_1:
assumes "d p = p" and "d q = q"
shows "⟨x| p ≤ q ⟷ p ≤ |x] q"
proof -
have "⟨x| p ≤ q ⟷ p ⋅ x ≤ x ⋅ q"
by (metis assms domrangefix local.ardual.ds.fdemodalisation2 local.ars_r_def)
thus ?thesis
by (metis assms fbox_demodalisation3)
qed
lemma box_diamond_galois_2:
assumes "d p = p" and "d q = q"
shows "|x⟩ p ≤ q ⟷ p ≤ [x| q"
proof -
have "|x⟩ p ≤ q ⟷ x ⋅ p ≤ q ⋅ x"
by (metis assms local.ads_d_def local.ds.fdemodalisation2)
thus ?thesis
by (metis assms domrangefix local.ardual.fbox_demodalisation3)
qed
lemma diamond_conjugation_var_1:
assumes "d p = p" and "d q = q"
shows "|x⟩ p ≤ ad q ⟷ ⟨x| q ≤ ad p"
proof -
have "|x⟩ p ≤ ad q ⟷ x ⋅ p ≤ ad q ⋅ x"
by (metis assms local.ads_d_def local.ds.fdemodalisation2)
also have "... ⟷ q ⋅ x ≤ x ⋅ ad p"
by (metis assms local.ads_d_def local.kat_1_equiv_opp)
finally show ?thesis
by (metis assms box_diamond_galois_1 local.ads_d_def local.fbox_demodalisation3)
qed
lemma diamond_conjungation_aux:
assumes "d p = p" and "d q = q"
shows "⟨x| p ≤ ad q ⟷ q ⋅ ⟨x| p = 0"
apply standard
apply (metis assms(2) local.a_antitone' local.a_gla local.ads_d_def)
proof -
assume a1: "q ⋅ ⟨x| p = zero_class.zero"
have "ad (ad q) = q"
using assms(2) local.ads_d_def by fastforce
then show "⟨x| p ≤ ad q"
using a1
by (metis a_closure' a_gla ardual.a_subid_aux1' bdia_def
dnsz.dsg4 dpdz.dsg1 dpdz.dsg3 ds.dsr4 order.trans)
qed
lemma diamond_conjugation:
assumes "d p = p" and "d q = q"
shows "p ⋅ |x⟩ q = 0 ⟷ q ⋅ ⟨x| p = 0"
proof -
have "p ⋅ |x⟩ q = 0 ⟷ |x⟩ q ≤ ad p"
by (metis assms(1) local.a_gla local.ads_d_def local.am2 local.fdia_def)
also have "... ⟷ ⟨x| p ≤ ad q"
by (simp add: assms diamond_conjugation_var_1)
finally show ?thesis
by (simp add: assms diamond_conjungation_aux)
qed
lemma box_conjugation_var_1:
assumes "d p = p" and "d q = q"
shows "ad p ≤ [x| q ⟷ ad q ≤ |x] p"
by (metis assms box_diamond_galois_1 box_diamond_galois_2 diamond_conjugation_var_1 local.ads_d_def)
lemma box_diamond_cancellation_1: "d p = p ⟹ p ≤ |x] ⟨x| p"
using box_diamond_galois_1 domrangefix local.ars_r_def local.bdia_def by fastforce
lemma box_diamond_cancellation_2: "d p = p ⟹ p ≤ [x| |x⟩ p"
by (metis box_diamond_galois_2 local.ads_d_def local.dpdz.domain_invol local.eq_refl local.fdia_def)
lemma box_diamond_cancellation_3: "d p = p ⟹ |x⟩ [x| p ≤ p"
using box_diamond_galois_2 domrangefix local.ardual.fdia_fbox_de_morgan_2 local.ars_r_def local.bbox_def local.bdia_def by auto
lemma box_diamond_cancellation_4: "d p = p ⟹ ⟨x| |x] p ≤ p"
using box_diamond_galois_1 local.ads_d_def local.fbox_def local.fdia_def local.fdia_fbox_de_morgan_2 by auto
end
class modal_kleene_algebra = modal_semiring + kleene_algebra
begin
subclass antidomain_kleene_algebra ..
subclass antirange_kleene_algebra ..
end
end