Theory Kleene_Algebra_Converse
section ‹Kleene algebra with converse›
theory "Kleene_Algebra_Converse"
imports Kleene_Algebra.Kleene_Algebra
begin
text ‹We start from involutive dioids and Kleene algebra and then add a so-called strong Gelfand property
to obtain an operation of converse that is closer to algebras of paths and relations.›
subsection ‹Involutive Kleene algebra›
class invol_op =
fixes invol :: "'a ⇒ 'a" ("_⇧∘" [101] 100)
class involutive_dioid = dioid_one_zero + invol_op +
assumes inv_invol [simp]: "(x⇧∘)⇧∘ = x"
and inv_contrav [simp]: "(x ⋅ y)⇧∘ = y⇧∘ ⋅ x⇧∘"
and inv_sup [simp]: "(x + y)⇧∘ = x⇧∘ + y⇧∘"
begin
lemma inv_zero [simp]: "0⇧∘ = 0"
proof-
have "0⇧∘ = (0⇧∘ ⋅ 0)⇧∘"
by simp
also have "… = 0⇧∘ ⋅ (0⇧∘)⇧∘"
using local.inv_contrav by blast
also have "… = 0⇧∘ ⋅ 0"
by simp
also have "… = 0"
by simp
finally show ?thesis.
qed
lemma inv_one [simp]: "1⇧∘ = 1"
proof-
have "1⇧∘ = 1⇧∘ ⋅ (1⇧∘)⇧∘"
by simp
also have "… = (1⇧∘ ⋅ 1)⇧∘"
using local.inv_contrav by presburger
also have "… = (1⇧∘)⇧∘"
by simp
also have "… = 1"
by simp
finally show ?thesis.
qed
lemma inv_iso: "x ≤ y ⟹ x⇧∘ ≤ y⇧∘"
by (metis local.inv_sup local.less_eq_def)
lemma inv_adj: "(x⇧∘ ≤ y) = (x ≤ y⇧∘)"
using inv_iso by fastforce
end
text ‹Here is an equivalent axiomatisation from Doornbos, Backhouse and van der Woude's paper
on a calculational approach to mathematical induction.›
class involutive_dioid_alt = dioid_one_zero +
fixes inv_alt :: "'a ⇒ 'a"
assumes inv_alt: "(inv_alt x ≤ y) = (x ≤ inv_alt y)"
and inv_alt_contrav [simp]: "inv_alt (x ⋅ y) = inv_alt y ⋅ inv_alt x"
begin
lemma inv_alt_invol [simp]: "inv_alt (inv_alt x) = x"
proof-
have "inv_alt (inv_alt x) ≤ x"
by (simp add: inv_alt)
thus ?thesis
by (meson inv_alt order_antisym)
qed
lemma inv_alt_add: "inv_alt (x + y) = inv_alt x + inv_alt y"
proof-
{fix z
have "(inv_alt (x + y) ≤ z) = (x + y ≤ inv_alt z)"
by (simp add: inv_alt)
also have "… = (x ≤ inv_alt z ∧ y ≤ inv_alt z)"
by simp
also have "… = (inv_alt x ≤ z ∧ inv_alt y ≤ z)"
by (simp add: inv_alt)
also have "… = (inv_alt x + inv_alt y ≤ z)"
by force
finally have "(inv_alt (x + y) ≤ z) = (inv_alt x + inv_alt y ≤ z)".}
thus ?thesis
using order_antisym by blast
qed
sublocale altinv: involutive_dioid _ _ _ _ _ _ inv_alt
by unfold_locales (simp_all add: inv_alt_add)
end
sublocale involutive_dioid ⊆ altinv: involutive_dioid_alt _ _ _ _ _ _ invol
by unfold_locales (simp_all add: local.inv_adj)
class involutive_kleene_algebra = involutive_dioid + kleene_algebra
begin
lemma inv_star: "(x⇧⋆)⇧∘ = (x⇧∘)⇧⋆"
proof (rule order.antisym)
have "((x⇧∘)⇧⋆)⇧∘ = (1 + (x⇧∘)⇧⋆ ⋅ x⇧∘)⇧∘"
by simp
also have "… = 1 + (x⇧∘)⇧∘ ⋅ ((x⇧∘)⇧⋆)⇧∘"
using local.inv_contrav local.inv_one local.inv_sup by presburger
finally have "1 + x ⋅ ((x⇧∘)⇧⋆)⇧∘ ≤ ((x⇧∘)⇧⋆)⇧∘"
by simp
hence "x⇧⋆ ≤ ((x⇧∘)⇧⋆)⇧∘"
using local.star_inductl by force
thus "(x⇧⋆)⇧∘ ≤ (x⇧∘)⇧⋆"
by (simp add: local.inv_adj)
next
have "(x⇧⋆)⇧∘ = (1 + x⇧⋆ ⋅ x)⇧∘"
by simp
also have "… = 1 + x⇧∘ ⋅ (x⇧⋆)⇧∘"
using local.inv_contrav local.inv_one local.inv_sup by presburger
finally have "1 + x⇧∘ ⋅ (x⇧⋆)⇧∘ ≤ (x⇧⋆)⇧∘"
by simp
thus "(x⇧∘)⇧⋆ ≤ (x⇧⋆)⇧∘"
using local.star_inductl by force
qed
end
subsection ‹Kleene algebra with converse›
text ‹The name "strong Gelfand property" has been borrowed from Palmigiano and Re.›
class dioid_converse = involutive_dioid +
assumes strong_gelfand: "x ≤ x ⋅ x⇧∘ ⋅ x"
lemma (in dioid_converse) subid_conv: "x ≤ 1 ⟹ x⇧∘ = x"
proof (rule order.antisym)
assume h: "x ≤ 1"
have "x ≤ x ⋅ x⇧∘ ⋅ x"
by (simp add: local.strong_gelfand)
also have "… ≤ 1 ⋅ x⇧∘ ⋅ 1"
using h local.mult_isol_var by blast
also have "… = x⇧∘"
by simp
finally show "x ≤ x⇧∘"
by simp
thus "x⇧∘ ≤ x"
by (simp add: local.inv_adj)
qed
class kleene_algebra_converse = involutive_kleene_algebra + dioid_converse
end