Theory Kleene_Algebra
section ‹Kleene Algebras›
theory Kleene_Algebra
imports Conway
begin
subsection ‹Left Near Kleene Algebras›
text ‹Extending the hierarchy developed in @{theory Kleene_Algebra.Dioid} we now
add an operation of Kleene star, finite iteration, or reflexive
transitive closure to variants of Dioids. Since a multiplicative unit
is needed for defining the star we only consider variants with~$1$;
$0$ can be added separately. We consider the left star induction axiom
and the right star induction axiom independently since in some
applications, e.g., Salomaa's axioms, probabilistic Kleene algebras,
or completeness proofs with respect to the equational theoy of regular
expressions and regular languages, the right star induction axiom is
not needed or not valid.
We start with near dioids, then consider pre-dioids and finally
dioids. It turns out that many of the known laws of Kleene algebras
hold already in these more general settings. In fact, all our
equational theorems have been proved within left Kleene algebras, as
expected.
Although most of the proofs in this file could be fully automated by
Sledgehammer and Metis, we display step-wise proofs as they would
appear in a text book. First, this file may then be useful as a
reference manual on Kleene algebra. Second, it is better protected
against changes in the underlying theories and supports easy
translation of proofs into other settings.›
class left_near_kleene_algebra = near_dioid_one + star_op +
assumes star_unfoldl: "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
and star_inductl: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
begin
text ‹First we prove two immediate consequences of the unfold
axiom. The first one states that starred elements are reflexive.›
lemma star_ref [simp]: "1 ≤ x⇧⋆"
using star_unfoldl by auto
text ‹Reflexivity of starred elements implies, by definition of the
order, that~$1$ is an additive unit for starred elements.›
lemma star_plus_one [simp]: "1 + x⇧⋆ = x⇧⋆"
using less_eq_def star_ref by blast
lemma star_1l [simp]: "x ⋅ x⇧⋆ ≤ x⇧⋆"
using star_unfoldl by auto
lemma "x⇧⋆ ⋅ x ≤ x⇧⋆"
oops
lemma "x ⋅ x⇧⋆ = x⇧⋆"
oops
text ‹Next we show that starred elements are transitive.›
lemma star_trans_eq [simp]: "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
proof (rule order.antisym)
have "x⇧⋆ + x ⋅ x⇧⋆ ≤ x⇧⋆"
by auto
thus "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by (simp add: star_inductl)
next show "x⇧⋆ ≤ x⇧⋆ ⋅ x⇧⋆"
using mult_isor star_ref by fastforce
qed
lemma star_trans: "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
text ‹We now derive variants of the star induction axiom.›
lemma star_inductl_var: "x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ y ≤ y"
proof -
assume "x ⋅ y ≤ y"
hence "y + x ⋅ y ≤ y"
by simp
thus "x⇧⋆ ⋅ y ≤ y"
by (simp add: star_inductl)
qed
lemma star_inductl_var_equiv [simp]: "x⇧⋆ ⋅ y ≤ y ⟷ x ⋅ y ≤ y"
proof
assume "x ⋅ y ≤ y"
thus "x⇧⋆ ⋅ y ≤ y"
by (simp add: star_inductl_var)
next
assume "x⇧⋆ ⋅ y ≤ y"
hence "x⇧⋆ ⋅ y = y"
by (metis order.eq_iff mult_1_left mult_isor star_ref)
moreover hence "x ⋅ y = x ⋅ x⇧⋆ ⋅ y"
by (simp add: mult.assoc)
moreover have "... ≤ x⇧⋆ ⋅ y"
by (metis mult_isor star_1l)
ultimately show "x ⋅ y ≤ y"
by auto
qed
lemma star_inductl_var_eq: "x ⋅ y = y ⟹ x⇧⋆ ⋅ y ≤ y"
by (metis order.eq_iff star_inductl_var)
lemma star_inductl_var_eq2: "y = x ⋅ y ⟹ y = x⇧⋆ ⋅ y"
proof -
assume hyp: "y = x ⋅ y"
hence "y ≤ x⇧⋆ ⋅ y"
using mult_isor star_ref by fastforce
thus "y = x⇧⋆ ⋅ y"
using hyp order.eq_iff by auto
qed
lemma "y = x ⋅ y ⟷ y = x⇧⋆ ⋅ y"
oops
lemma "x⇧⋆ ⋅ z ≤ y ⟹ z + x ⋅ y ≤ y"
oops
lemma star_inductl_one: "1 + x ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"
using star_inductl by force
lemma star_inductl_star: "x ⋅ y⇧⋆ ≤ y⇧⋆ ⟹ x⇧⋆ ≤ y⇧⋆"
by (simp add: star_inductl_one)
lemma star_inductl_eq: "z + x ⋅ y = y ⟹ x⇧⋆ ⋅ z ≤ y"
by (simp add: star_inductl)
text ‹We now prove two facts related to~$1$.›
lemma star_subid: "x ≤ 1 ⟹ x⇧⋆ = 1"
proof -
assume "x ≤ 1"
hence "1 + x ⋅ 1 ≤ 1"
by simp
hence "x⇧⋆ ≤ 1"
by (metis mult_oner star_inductl)
thus "x⇧⋆ = 1"
by (simp add: order.antisym)
qed
lemma star_one [simp]: "1⇧⋆ = 1"
by (simp add: star_subid)
text ‹We now prove a subdistributivity property for the star (which
is equivalent to isotonicity of star).›
lemma star_subdist: "x⇧⋆ ≤ (x + y)⇧⋆"
proof -
have "x ⋅ (x + y)⇧⋆ ≤ (x + y) ⋅ (x + y)⇧⋆"
by simp
also have "... ≤ (x + y)⇧⋆"
by (metis star_1l)
thus ?thesis
using calculation order_trans star_inductl_star by blast
qed
lemma star_subdist_var: "x⇧⋆ + y⇧⋆ ≤ (x + y)⇧⋆"
using join.sup_commute star_subdist by force
lemma star_iso [intro]: "x ≤ y ⟹ x⇧⋆ ≤ y⇧⋆"
by (metis less_eq_def star_subdist)
text ‹We now prove some more simple properties.›
lemma star_invol [simp]: "(x⇧⋆)⇧⋆ = x⇧⋆"
proof (rule order.antisym)
have "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (fact star_trans_eq)
thus "(x⇧⋆)⇧⋆ ≤ x⇧⋆"
by (simp add: star_inductl_star)
have"(x⇧⋆)⇧⋆ ⋅ (x⇧⋆)⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (fact star_trans)
hence "x ⋅ (x⇧⋆)⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (meson star_inductl_var_equiv)
thus "x⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (simp add: star_inductl_star)
qed
lemma star2 [simp]: "(1 + x)⇧⋆ = x⇧⋆"
proof (rule order.antisym)
show "x⇧⋆ ≤ (1 + x)⇧⋆"
by auto
have "x⇧⋆ + x ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
thus "(1 + x)⇧⋆ ≤ x⇧⋆"
by (simp add: star_inductl_star)
qed
lemma "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
oops
lemma "x ≤ x⇧⋆"
oops
lemma "x⇧⋆ ⋅ x ≤ x⇧⋆"
oops
lemma "1 + x ⋅ x⇧⋆ = x⇧⋆"
oops
lemma "x ⋅ z ≤ z ⋅ y ⟹ x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
oops
text ‹The following facts express inductive conditions that are used
to show that @{term "(x + y)⇧⋆"} is the greatest term that can be built
from~@{term x} and~@{term y}.›
lemma prod_star_closure: "x ≤ z⇧⋆ ⟹ y ≤ z⇧⋆ ⟹ x ⋅ y ≤ z⇧⋆"
proof -
assume assm: "x ≤ z⇧⋆" "y ≤ z⇧⋆"
hence "y + z⇧⋆ ⋅ z⇧⋆ ≤ z⇧⋆"
by simp
hence "z⇧⋆ ⋅ y ≤ z⇧⋆"
by (simp add: star_inductl)
also have "x ⋅ y ≤ z⇧⋆ ⋅ y"
by (simp add: assm mult_isor)
thus "x ⋅ y ≤ z⇧⋆"
using calculation order.trans by blast
qed
lemma star_star_closure: "x⇧⋆ ≤ z⇧⋆ ⟹ (x⇧⋆)⇧⋆ ≤ z⇧⋆"
by (metis star_invol)
lemma star_closed_unfold: "x⇧⋆ = x ⟹ x = 1 + x ⋅ x"
by (metis star_plus_one star_trans_eq)
lemma "x⇧⋆ = x ⟷ x = 1 + x ⋅ x"
oops
end
subsection ‹Left Pre-Kleene Algebras›
class left_pre_kleene_algebra = left_near_kleene_algebra + pre_dioid_one
begin
text ‹We first prove that the star operation is extensive.›
lemma star_ext [simp]: "x ≤ x⇧⋆"
proof -
have "x ≤ x ⋅ x⇧⋆"
by (metis mult_oner mult_isol star_ref)
thus ?thesis
by (metis order_trans star_1l)
qed
text ‹We now prove a right star unfold law.›
lemma star_1r [simp]: "x⇧⋆ ⋅ x ≤ x⇧⋆"
proof -
have "x + x ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
thus ?thesis
by (fact star_inductl)
qed
lemma star_unfoldr: "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
by simp
lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
oops
text ‹Next we prove a simulation law for the star. It is
instrumental in proving further properties.›
lemma star_sim1: "x ⋅ z ≤ z ⋅ y ⟹ x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
proof -
assume "x ⋅ z ≤ z ⋅ y"
hence "x ⋅ z ⋅ y⇧⋆ ≤ z ⋅ y ⋅ y⇧⋆"
by (simp add: mult_isor)
also have "... ≤ z ⋅ y⇧⋆"
by (simp add: mult_isol mult_assoc)
finally have "x ⋅ z ⋅ y⇧⋆ ≤ z ⋅ y⇧⋆"
by simp
hence "z + x ⋅ z ⋅ y⇧⋆ ≤ z ⋅ y⇧⋆"
by (metis join.sup_least mult_isol mult_oner star_ref)
thus "x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
by (simp add: star_inductl mult_assoc)
qed
text ‹The next lemma is used in omega algebras to prove, for
instance, Bachmair and Dershowitz's separation of termination
theorem~\<^cite>‹"bachmair86commutation"›. The property at the left-hand
side of the equivalence is known as \emph{quasicommutation}.›
lemma quasicomm_var: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ ⟷ y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
proof
assume "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
thus "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
using star_sim1 by force
next
assume "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
thus "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
by (meson mult_isor order_trans star_ext)
qed
lemma star_slide1: "(x ⋅ y)⇧⋆ ⋅ x ≤ x ⋅ (y ⋅ x)⇧⋆"
by (simp add: mult_assoc star_sim1)
lemma "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
oops
lemma star_slide_var1: "x⇧⋆ ⋅ x ≤ x ⋅ x⇧⋆"
by (simp add: star_sim1)
text ‹We now show that the (left) star unfold axiom can be strengthened to an equality.›
lemma star_unfoldl_eq [simp]: "1 + x ⋅ x⇧⋆ = x⇧⋆"
proof (rule order.antisym)
show "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
by (fact star_unfoldl)
have "1 + x ⋅ (1 + x ⋅ x⇧⋆) ≤ 1 + x ⋅ x⇧⋆"
by (meson join.sup_mono eq_refl mult_isol star_unfoldl)
thus "x⇧⋆ ≤ 1 + x ⋅ x⇧⋆"
by (simp add: star_inductl_one)
qed
lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
oops
text ‹Next we relate the star and the reflexive transitive closure
operation.›
lemma star_rtc1_eq [simp]: "1 + x + x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (simp add: join.sup.absorb2)
lemma star_rtc1: "1 + x + x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
lemma star_rtc2: "1 + x ⋅ x ≤ x ⟷ x = x⇧⋆"
proof
assume "1 + x ⋅ x ≤ x"
thus "x = x⇧⋆"
by (simp add: order.eq_iff local.star_inductl_one)
next
assume "x = x⇧⋆"
thus "1 + x ⋅ x ≤ x"
using local.star_closed_unfold by auto
qed
lemma star_rtc3: "1 + x ⋅ x = x ⟷ x = x⇧⋆"
by (metis order_refl star_plus_one star_rtc2 star_trans_eq)
lemma star_rtc_least: "1 + x + y ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"
proof -
assume "1 + x + y ⋅ y ≤ y"
hence "1 + x ⋅ y ≤ y"
by (metis join.le_sup_iff mult_isol_var star_trans_eq star_rtc2)
thus "x⇧⋆ ≤ y"
by (simp add: star_inductl_one)
qed
lemma star_rtc_least_eq: "1 + x + y ⋅ y = y ⟹ x⇧⋆ ≤ y"
by (simp add: star_rtc_least)
lemma "1 + x + y ⋅ y ≤ y ⟷ x⇧⋆ ≤ y"
oops
text ‹The next lemmas are again related to closure conditions›
lemma star_subdist_var_1: "x ≤ (x + y)⇧⋆"
by (meson join.sup.boundedE star_ext)
lemma star_subdist_var_2: "x ⋅ y ≤ (x + y)⇧⋆"
by (meson join.sup.boundedE prod_star_closure star_ext)
lemma star_subdist_var_3: "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by (simp add: prod_star_closure star_iso)
text ‹We now prove variants of sum-elimination laws under a star.
These are also known a denesting laws or as sum-star laws.›
lemma star_denest [simp]: "(x + y)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
proof (rule order.antisym)
have "x + y ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis join.sup.bounded_iff mult_1_right mult_isol_var mult_onel star_ref star_ext)
thus "(x + y)⇧⋆ ≤ (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (fact star_iso)
have "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by (fact star_subdist_var_3)
thus "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
by (simp add: prod_star_closure star_inductl_star)
qed
lemma star_sum_var [simp]: "(x⇧⋆ + y⇧⋆)⇧⋆ = (x + y)⇧⋆"
by simp
lemma star_denest_var [simp]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x + y)⇧⋆"
proof (rule order.antisym)
have "1 ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis mult_isol_var mult_oner star_ref)
moreover have "x ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (simp add: mult_isor)
moreover have "y ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis mult_isol_var mult_onel star_1l star_ref)
ultimately have "1 + (x + y) ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by auto
thus "(x + y)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis mult.assoc mult_oner star_inductl)
have "(y ⋅ x⇧⋆)⇧⋆ ≤ (y⇧⋆ ⋅ x⇧⋆)⇧⋆"
by (simp add: mult_isol_var star_iso)
hence "(y ⋅ x⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
by (metis add.commute star_denest)
moreover have "x⇧⋆ ≤ (x + y)⇧⋆"
by (fact star_subdist)
ultimately show "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
using prod_star_closure by blast
qed
lemma star_denest_var_2 [simp]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by simp
lemma star_denest_var_3 [simp]: "x⇧⋆ ⋅ (y⇧⋆ ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by simp
lemma star_denest_var_4 [ac_simps]: "(y⇧⋆ ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (metis add_comm star_denest)
lemma star_denest_var_5 [ac_simps]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = y⇧⋆ ⋅ (x ⋅ y⇧⋆)⇧⋆"
by (simp add: star_denest_var_4)
lemma "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
oops
lemma star_denest_var_6 [simp]: "x⇧⋆ ⋅ y⇧⋆ ⋅ (x + y)⇧⋆ = (x + y)⇧⋆"
using mult_assoc by simp
lemma star_denest_var_7 [simp]: "(x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ = (x + y)⇧⋆"
proof (rule order.antisym)
have "(x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (simp add: mult_assoc)
thus "(x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by simp
have "1 ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by (metis dual_order.trans mult_1_left mult_isor star_ref)
moreover have "(x + y) ⋅ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
using mult_isor star_1l by presburger
ultimately have "1 + (x + y) ⋅ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by simp
thus "(x + y)⇧⋆ ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by (metis mult.assoc star_inductl_one)
qed
lemma star_denest_var_8 [simp]: "x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (simp add: mult_assoc)
lemma star_denest_var_9 [simp]: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
using star_denest_var_7 by simp
text ‹The following statements are well known from term
rewriting. They are all variants of the Church-Rosser theorem in
Kleene algebra~\<^cite>‹"struth06churchrosser"›. But first we prove a law
relating two confluence properties.›
lemma confluence_var [iff]: "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟷ y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
proof
assume "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
thus "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
using star_sim1 by fastforce
next
assume "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
thus "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (meson mult_isor order_trans star_ext)
qed
lemma church_rosser [intro]: "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
proof (rule order.antisym)
assume "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
hence "x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆) ≤ x⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ⋅ y⇧⋆"
by (metis mult_isol mult_isor mult.assoc)
hence "x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆) ≤ x⇧⋆ ⋅ y⇧⋆"
by (simp add: mult_assoc)
moreover have "1 ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis dual_order.trans mult_1_right mult_isol star_ref)
ultimately have "1 + x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆) ≤ x⇧⋆ ⋅ y⇧⋆"
by simp
hence "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (simp add: star_inductl_one)
thus "(x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by simp
thus "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by simp
qed
lemma church_rosser_var: "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by fastforce
lemma church_rosser_to_confluence: "(x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis add_comm order.eq_iff star_subdist_var_3)
lemma church_rosser_equiv: "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟷ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
using church_rosser_to_confluence order.eq_iff by blast
lemma confluence_to_local_confluence: "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆"
by (meson mult_isol_var order_trans star_ext)
lemma "y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
oops
lemma "y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
oops
text ‹
More variations could easily be proved. The last counterexample shows
that Newman's lemma needs a wellfoundedness assumption. This is well
known.
›
text ‹The next lemmas relate the reflexive transitive closure and
the transitive closure.›
lemma sup_id_star1: "1 ≤ x ⟹ x ⋅ x⇧⋆ = x⇧⋆"
proof -
assume "1 ≤ x"
hence " x⇧⋆ ≤ x ⋅ x⇧⋆"
using mult_isor by fastforce
thus "x ⋅ x⇧⋆ = x⇧⋆"
by (simp add: order.eq_iff)
qed
lemma sup_id_star2: "1 ≤ x ⟹ x⇧⋆ ⋅ x = x⇧⋆"
by (metis order.antisym mult_isol mult_oner star_1r)
lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
oops
lemma "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
oops
lemma "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
oops
end
subsection ‹Left Kleene Algebras›
class left_kleene_algebra = left_pre_kleene_algebra + dioid_one
begin
text ‹In left Kleene algebras the non-fact @{prop "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"}
is a good challenge for counterexample generators. A model of left
Kleene algebras in which the right star induction law does not hold
has been given by Kozen~\<^cite>‹"kozen90kleene"›.›
text ‹We now show that the right unfold law becomes an equality.›
lemma star_unfoldr_eq [simp]: "1 + x⇧⋆ ⋅ x = x⇧⋆"
proof (rule order.antisym)
show "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
by (fact star_unfoldr)
have "1 + x ⋅ (1 + x⇧⋆ ⋅ x) = 1 + (1 + x ⋅ x⇧⋆) ⋅ x"
using distrib_left distrib_right mult_1_left mult_1_right mult_assoc by presburger
also have "... = 1 + x⇧⋆ ⋅ x"
by simp
finally show "x⇧⋆ ≤ 1 + x⇧⋆ ⋅ x"
by (simp add: star_inductl_one)
qed
text ‹The following more complex unfold law has been used as an
axiom, called prodstar, by Conway~\<^cite>‹"conway71regular"›.›
lemma star_prod_unfold [simp]: "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y = (x ⋅ y)⇧⋆"
proof (rule order.antisym)
have "(x ⋅ y)⇧⋆ = 1 + (x ⋅ y)⇧⋆ ⋅ x ⋅ y"
by (simp add: mult_assoc)
thus "(x ⋅ y)⇧⋆ ≤ 1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y"
by (metis join.sup_mono mult_isor order_refl star_slide1)
have "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ≤ 1 + x ⋅ y ⋅ (x ⋅ y)⇧⋆"
by (metis join.sup_mono eq_refl mult.assoc mult_isol star_slide1)
thus "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ≤ (x ⋅ y)⇧⋆"
by simp
qed
text ‹The slide laws, which have previously been inequalities, now
become equations.›
lemma star_slide [ac_simps]: "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
proof -
have "x ⋅ (y ⋅ x)⇧⋆ = x ⋅ (1 + y ⋅ (x ⋅ y)⇧⋆ ⋅ x)"
by simp
also have "... = (1 + x ⋅ y ⋅ (x ⋅ y)⇧⋆) ⋅ x"
by (simp add: distrib_left mult_assoc)
finally show ?thesis
by simp
qed
lemma star_slide_var [ac_simps]: "x⇧⋆ ⋅ x = x ⋅ x⇧⋆"
by (metis mult_onel mult_oner star_slide)
lemma star_sum_unfold_var [simp]: "1 + x⇧⋆ ⋅ (x + y)⇧⋆ ⋅ y⇧⋆ = (x + y)⇧⋆"
by (metis star_denest star_denest_var_3 star_denest_var_4 star_plus_one star_slide)
text ‹The following law shows how starred sums can be unfolded.›
lemma star_sum_unfold [simp]: "x⇧⋆ + x⇧⋆ ⋅ y ⋅ (x + y)⇧⋆ = (x + y)⇧⋆"
proof -
have "(x + y)⇧⋆ = x⇧⋆ ⋅ (y ⋅ x⇧⋆ )⇧⋆"
by simp
also have "... = x⇧⋆ ⋅ (1 + y ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆ )⇧⋆)"
by simp
also have "... = x⇧⋆ ⋅ (1 + y ⋅ (x + y)⇧⋆)"
by (simp add: mult.assoc)
finally show ?thesis
by (simp add: distrib_left mult_assoc)
qed
text ‹The following property appears in process algebra.›
lemma troeger: "(x + y)⇧⋆ ⋅ z = x⇧⋆ ⋅ (y ⋅ (x + y)⇧⋆ ⋅ z + z)"
proof -
have "(x + y)⇧⋆ ⋅ z = x⇧⋆ ⋅ z + x⇧⋆ ⋅ y ⋅ (x + y)⇧⋆ ⋅ z"
by (metis (full_types) distrib_right star_sum_unfold)
thus ?thesis
by (simp add: add_commute distrib_left mult_assoc)
qed
text ‹The following properties are related to a property from
propositional dynamic logic which has been attributed to Albert
Meyer~\<^cite>‹"harelkozentiuryn00dynamic"›. Here we prove it as a theorem
of Kleene algebra.›
lemma star_square: "(x ⋅ x)⇧⋆ ≤ x⇧⋆"
proof -
have "x ⋅ x ⋅ x⇧⋆ ≤ x⇧⋆"
by (simp add: prod_star_closure)
thus ?thesis
by (simp add: star_inductl_star)
qed
lemma meyer_1 [simp]: "(1 + x) ⋅ (x ⋅ x)⇧⋆ = x⇧⋆"
proof (rule order.antisym)
have "x ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ = x ⋅ (x ⋅ x)⇧⋆ + x ⋅ x ⋅ (x ⋅ x)⇧⋆"
by (simp add: distrib_left)
also have "... ≤ x ⋅ (x ⋅ x)⇧⋆ + (x ⋅ x)⇧⋆"
using join.sup_mono star_1l by blast
finally have "x ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (simp add: join.sup_commute)
moreover have "1 ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
using join.sup.coboundedI1 by auto
ultimately have "1 + x ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by auto
thus "x⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (simp add: star_inductl_one mult_assoc)
show "(1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ x⇧⋆"
by (simp add: prod_star_closure star_square)
qed
text ‹The following lemma says that transitive elements are equal to
their transitive closure.›
lemma tc: "x ⋅ x ≤ x ⟹ x⇧⋆ ⋅ x = x"
proof -
assume "x ⋅ x ≤ x"
hence "x + x ⋅ x ≤ x"
by simp
hence "x⇧⋆ ⋅ x ≤ x"
by (fact star_inductl)
thus "x⇧⋆ ⋅ x = x"
by (metis mult_isol mult_oner star_ref star_slide_var order.eq_iff)
qed
lemma tc_eq: "x ⋅ x = x ⟹ x⇧⋆ ⋅ x = x"
by (auto intro: tc)
text ‹The next fact has been used by Boffa~\<^cite>‹"boffa90remarque"› to
axiomatise the equational theory of regular expressions.›
lemma boffa_var: "x ⋅ x ≤ x ⟹ x⇧⋆ = 1 + x"
proof -
assume "x ⋅ x ≤ x"
moreover have "x⇧⋆ = 1 + x⇧⋆ ⋅ x"
by simp
ultimately show "x⇧⋆ = 1 + x"
by (simp add: tc)
qed
lemma boffa: "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
by (auto intro: boffa_var)
end
subsection ‹Left Kleene Algebras with Zero›
text ‹
There are applications where only a left zero is assumed, for instance
in the context of total correctness and for demonic refinement
algebras~\<^cite>‹"vonwright04refinement"›.
›
class left_kleene_algebra_zerol = left_kleene_algebra + dioid_one_zerol
begin
sublocale conway: near_conway_base_zerol star
by standard (simp_all add: local.star_slide)
lemma star_zero [simp]: "0⇧⋆ = 1"
by (rule local.conway.zero_dagger)
text ‹
In principle,~$1$ could therefore be defined from~$0$ in this setting.
›
end
class left_kleene_algebra_zero = left_kleene_algebra_zerol + dioid_one_zero
subsection ‹Pre-Kleene Algebras›
text ‹Pre-Kleene algebras are essentially probabilistic Kleene
algebras~\<^cite>‹"mciverweber05pka"›. They have a weaker right star
unfold axiom. We are still looking for theorems that could be proved
in this setting.›
class pre_kleene_algebra = left_pre_kleene_algebra +
assumes weak_star_unfoldr: "z + y ⋅ (x + 1) ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
subsection ‹Kleene Algebras›
class kleene_algebra_zerol = left_kleene_algebra_zerol +
assumes star_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
begin
lemma star_sim2: "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧⋆ ≤ y⇧⋆ ⋅ z"
proof -
assume "z ⋅ x ≤ y ⋅ z"
hence "y⇧⋆ ⋅ z ⋅ x ≤ y⇧⋆ ⋅ y ⋅ z"
using mult_isol mult_assoc by auto
also have "... ≤ y⇧⋆ ⋅ z"
by (simp add: mult_isor)
finally have "y⇧⋆ ⋅ z ⋅ x ≤ y⇧⋆ ⋅ z"
by simp
moreover have "z ≤ y⇧⋆ ⋅ z"
using mult_isor star_ref by fastforce
ultimately have "z + y⇧⋆ ⋅ z ⋅ x ≤ y⇧⋆ ⋅ z"
by simp
thus "z ⋅ x⇧⋆ ≤ y⇧⋆ ⋅ z"
by (simp add: star_inductr)
qed
sublocale conway: pre_conway star
by standard (simp add: star_sim2)
lemma star_inductr_var: "y ⋅ x ≤ y ⟹ y ⋅ x⇧⋆ ≤ y"
by (simp add: star_inductr)
lemma star_inductr_var_equiv: "y ⋅ x ≤ y ⟷ y ⋅ x⇧⋆ ≤ y"
by (meson order_trans mult_isol star_ext star_inductr_var)
lemma star_sim3: "z ⋅ x = y ⋅ z ⟹ z ⋅ x⇧⋆ = y⇧⋆ ⋅ z"
by (simp add: order.eq_iff star_sim1 star_sim2)
lemma star_sim4: "x ⋅ y ≤ y ⋅ x ⟹ x⇧⋆ ⋅ y⇧⋆ ≤ y⇧⋆ ⋅ x⇧⋆"
by (auto intro: star_sim1 star_sim2)
lemma star_inductr_eq: "z + y ⋅ x = y ⟹ z ⋅ x⇧⋆ ≤ y"
by (auto intro: star_inductr)
lemma star_inductr_var_eq: "y ⋅ x = y ⟹ y ⋅ x⇧⋆ ≤ y"
by (auto intro: star_inductr_var)
lemma star_inductr_var_eq2: "y ⋅ x = y ⟹ y ⋅ x⇧⋆ = y"
by (metis mult_onel star_one star_sim3)
lemma bubble_sort: "y ⋅ x ≤ x ⋅ y ⟹ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by (fastforce intro: star_sim4)
lemma independence1: "x ⋅ y = 0 ⟹ x⇧⋆ ⋅ y = y"
proof -
assume "x ⋅ y = 0"
moreover have "x⇧⋆ ⋅ y = y + x⇧⋆ ⋅ x ⋅ y"
by (metis distrib_right mult_onel star_unfoldr_eq)
ultimately show "x⇧⋆ ⋅ y = y"
by (metis add_0_left add.commute join.sup_ge1 order.eq_iff star_inductl_eq)
qed
lemma independence2: "x ⋅ y = 0 ⟹ x ⋅ y⇧⋆ = x"
by (metis annil mult_onel star_sim3 star_zero)
lemma lazycomm_var: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ + y ⟷ y ⋅ x⇧⋆ ≤ x ⋅ (x + y)⇧⋆ + y"
proof
let ?t = "x ⋅ (x + y)⇧⋆"
assume hyp: "y ⋅ x ≤ ?t + y"
have "(?t + y) ⋅ x = ?t ⋅ x + y ⋅ x"
by (fact distrib_right)
also have "... ≤ ?t ⋅ x + ?t + y"
using hyp join.sup.coboundedI2 join.sup_assoc by auto
also have "... ≤ ?t + y"
using eq_refl join.sup_least join.sup_mono mult_isol prod_star_closure star_subdist_var_1 mult_assoc by presburger
finally have "y + (?t + y) ⋅ x ≤ ?t + y"
by simp
thus "y ⋅ x⇧⋆ ≤ x ⋅ (x + y)⇧⋆ + y"
by (fact star_inductr)
next
assume "y ⋅ x⇧⋆ ≤ x ⋅ (x + y)⇧⋆ + y"
thus "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ + y"
using dual_order.trans mult_isol star_ext by blast
qed
lemma arden_var: "(∀y v. y ≤ x ⋅ y + v ⟶ y ≤ x⇧⋆ ⋅ v) ⟹ z = x ⋅ z + w ⟹ z = x⇧⋆ ⋅ w"
by (auto simp: add_comm order.eq_iff star_inductl_eq)
lemma "(∀x y. y ≤ x ⋅ y ⟶ y = 0) ⟹ y ≤ x ⋅ y + z ⟹ y ≤ x⇧⋆ ⋅ z"
by (metis eq_refl mult_onel)
end
text ‹Finally, here come the Kleene algebras \`a~la
Kozen~\<^cite>‹"kozen94complete"›. We only prove quasi-identities in this
section. Since left Kleene algebras are complete with respect to the
equational theory of regular expressions and regular languages, all
identities hold already without the right star induction axiom.›
class kleene_algebra = left_kleene_algebra_zero +
assumes star_inductr': "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
begin
subclass kleene_algebra_zerol
by standard (simp add: star_inductr')
sublocale conway_zerol: conway star ..
text ‹
The next lemma shows that opposites of Kleene algebras (i.e., Kleene
algebras with the order of multiplication swapped) are again Kleene
algebras.
›
lemma dual_kleene_algebra:
"class.kleene_algebra (+) (⊙) 1 0 (≤) (<) star"
proof
fix x y z :: 'a
show "(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis opp_mult_def distrib_left)
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
by (fact add_zerol)
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "x + x = x"
by (fact add_idem)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "z ⊙ x ≤ z ⊙ (x + y)"
by (metis mult_isor opp_mult_def order_prop)
show "1 + x ⊙ x⇧⋆ ≤ x⇧⋆"
by (metis opp_mult_def order_refl star_slide_var star_unfoldl_eq)
show "z + x ⊙ y ≤ y ⟹ x⇧⋆ ⊙ z ≤ y"
by (metis opp_mult_def star_inductr)
show "z + y ⊙ x ≤ y ⟹ z ⊙ x⇧⋆ ≤ y"
by (metis opp_mult_def star_inductl)
qed
end
text ‹We finish with some properties on (multiplicatively)
commutative Kleene algebras. A chapter in Conway's
book~\<^cite>‹"conway71regular"› is devoted to this topic.›
class commutative_kleene_algebra = kleene_algebra +
assumes mult_comm [ac_simps]: "x ⋅ y = y ⋅ x"
begin
lemma conway_c3 [simp]: "(x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
using church_rosser mult_comm by auto
lemma conway_c4: "(x⇧⋆ ⋅ y)⇧⋆ = 1 + x⇧⋆ ⋅ y⇧⋆ ⋅ y"
by (metis conway_c3 star_denest_var star_prod_unfold)
lemma cka_1: "(x ⋅ y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis conway_c3 star_invol star_iso star_subdist_var_2)
lemma cka_2 [simp]: "x⇧⋆ ⋅ (x⇧⋆ ⋅ y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by (metis conway_c3 mult_comm star_denest_var)
lemma conway_c4_var [simp]: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by (metis conway_c3 star_invol)
lemma conway_c2_var: "(x ⋅ y)⇧⋆ ⋅ x ⋅ y ⋅ y⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ y⇧⋆"
by (metis mult_isor star_1r mult_assoc)
lemma conway_c2 [simp]: "(x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) = x⇧⋆ ⋅ y⇧⋆"
proof (rule order.antisym)
show "(x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis cka_1 conway_c3 prod_star_closure star_ext star_sum_var)
have "x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) = x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + 1 + y ⋅ y⇧⋆)"
by (simp add: add_assoc)
also have "... = x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y ⋅ y⇧⋆)"
by (simp add: add_commute)
also have "... = (x ⋅ y)⇧⋆ ⋅ (x ⋅ x⇧⋆) + (x ⋅ y)⇧⋆ ⋅ x ⋅ y ⋅ y⇧⋆"
using distrib_left mult_comm mult_assoc by force
also have "... ≤ (x ⋅ y)⇧⋆ ⋅ x⇧⋆ + (x ⋅ y)⇧⋆ ⋅ x ⋅ y ⋅ y⇧⋆"
using add_iso mult_isol by force
also have "... ≤ (x ⋅ y)⇧⋆ ⋅ x⇧⋆ + (x ⋅ y)⇧⋆ ⋅ y⇧⋆"
using conway_c2_var join.sup_mono by blast
also have "... = (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by (simp add: distrib_left)
finally have "x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)" .
moreover have "y⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by (metis dual_order.trans join.sup_ge2 mult_1_left mult_isor star_ref)
ultimately have "y⇧⋆ + x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by simp
thus "x⇧⋆ ⋅ y⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by (simp add: mult.assoc star_inductl)
qed
end
end