Theory Kleene_Algebras
section ‹Kleene Algebras›
text ‹
Kleene algebras have been axiomatised by Kozen to describe the equational theory of regular languages \<^cite>‹"Kozen1994"›.
Binary relations are another important model.
This theory implements variants of Kleene algebras based on idempotent left semirings \<^cite>‹"Moeller2007"›.
The weakening of some semiring axioms allows the treatment of further computation models.
The presented algebras are special cases of iterings, so many results can be inherited.
›
theory Kleene_Algebras
imports Iterings
begin
text ‹
We start with left Kleene algebras, which use the left unfold and left induction axioms of Kleene algebras.
›
class star =
fixes star :: "'a ⇒ 'a" (‹_⇧⋆› [100] 100)
class left_kleene_algebra = idempotent_left_semiring + star +
assumes star_left_unfold : "1 ⊔ y * y⇧⋆ ≤ y⇧⋆"
assumes star_left_induct : "z ⊔ y * x ≤ x ⟶ y⇧⋆ * z ≤ x"
begin
unbundle no trancl_syntax
abbreviation tc (‹_⇧+› [100] 100) where "tc x ≡ x * x⇧⋆"
lemma star_left_unfold_equal:
"1 ⊔ x * x⇧⋆ = x⇧⋆"
by (metis sup_right_isotone order.antisym mult_right_isotone mult_1_right star_left_induct star_left_unfold)
text ‹
This means that for some properties of Kleene algebras, only one inequality can be derived, as exemplified by the following sliding rule.
›
lemma star_left_slide:
"(x * y)⇧⋆ * x ≤ x * (y * x)⇧⋆"
by (metis mult_assoc mult_left_sub_dist_sup mult_1_right star_left_induct star_left_unfold_equal)
lemma star_isotone:
"x ≤ y ⟹ x⇧⋆ ≤ y⇧⋆"
by (metis sup_right_isotone mult_left_isotone order_trans star_left_unfold mult_1_right star_left_induct)
lemma star_sup_1:
"(x ⊔ y)⇧⋆ = x⇧⋆ * (y * x⇧⋆)⇧⋆"
proof (rule order.antisym)
have "y * x⇧⋆ * (y * x⇧⋆)⇧⋆ ≤ (y * x⇧⋆)⇧⋆"
using sup_right_divisibility star_left_unfold_equal by auto
also have "... ≤ x⇧⋆ * (y * x⇧⋆)⇧⋆"
using mult_left_isotone sup_left_divisibility star_left_unfold_equal by fastforce
finally have "(x ⊔ y) * (x⇧⋆ * (y * x⇧⋆)⇧⋆) ≤ x⇧⋆ * (y * x⇧⋆)⇧⋆"
by (metis le_supI mult_right_dist_sup mult_right_sub_dist_sup_right mult_assoc star_left_unfold_equal)
hence "1 ⊔ (x ⊔ y) * (x⇧⋆ * (y * x⇧⋆)⇧⋆) ≤ x⇧⋆ * (y * x⇧⋆)⇧⋆"
using reflexive_mult_closed star_left_unfold by auto
thus "(x ⊔ y)⇧⋆ ≤ x⇧⋆ * (y * x⇧⋆)⇧⋆"
using star_left_induct by force
next
have "x⇧⋆ * (y * x⇧⋆)⇧⋆ ≤ x⇧⋆ * (y * (x ⊔ y)⇧⋆)⇧⋆"
by (simp add: mult_right_isotone star_isotone)
also have "... ≤ x⇧⋆ * ((x ⊔ y) * (x ⊔ y)⇧⋆)⇧⋆"
by (simp add: mult_right_isotone mult_right_sub_dist_sup_right star_isotone)
also have "... ≤ x⇧⋆ * (x ⊔ y)⇧⋆⇧⋆"
using mult_right_isotone star_left_unfold star_isotone by auto
also have "... ≤ (x ⊔ y)⇧⋆ * (x ⊔ y)⇧⋆⇧⋆"
by (simp add: mult_left_isotone star_isotone)
also have "... ≤ (x ⊔ y)⇧⋆"
by (metis sup.bounded_iff mult_1_right star_left_induct star_left_unfold)
finally show "x⇧⋆ * (y * x⇧⋆)⇧⋆ ≤ (x ⊔ y)⇧⋆"
by simp
qed
lemma plus_transitive:
"x⇧+ * x⇧+ ≤ x⇧+"
by (metis mult_right_isotone star_left_induct sup_absorb2 sup_ge2 mult_assoc star_left_unfold_equal)
end
text ‹
We now show that left Kleene algebras form iterings.
A sublocale is used instead of a subclass, because iterings use a different iteration operation.
›
left_kleene_algebra < star: left_conway_semiring where circ = star
apply unfold_locales
apply (rule star_left_unfold_equal)
apply (rule star_left_slide)
by (rule star_sup_1)
context left_kleene_algebra
begin
text ‹
A number of lemmas in this class are taken from Georg Struth's Kleene algebra theory \<^cite>‹"ArmstrongGomesStruthWeber2016"›.
›
lemma star_sub_one:
"x ≤ 1 ⟹ x⇧⋆ = 1"
by (metis sup_right_isotone order.eq_iff le_iff_sup mult_1_right star.circ_plus_one star_left_induct)
lemma star_one:
"1⇧⋆ = 1"
by (simp add: star_sub_one)
lemma star_left_induct_mult:
"x * y ≤ y ⟹ x⇧⋆ * y ≤ y"
by (simp add: star_left_induct)
lemma star_left_induct_mult_iff:
"x * y ≤ y ⟷ x⇧⋆ * y ≤ y"
using mult_left_isotone order_trans star.circ_increasing star_left_induct_mult by blast
lemma star_involutive:
"x⇧⋆ = x⇧⋆⇧⋆"
using star.circ_circ_sup star_sup_1 star_one by auto
lemma star_sup_one:
"(1 ⊔ x)⇧⋆ = x⇧⋆"
using star.circ_circ_sup star_involutive by auto
lemma star_plus_loops:
"x⇧⋆ ⊔ 1 = x⇧+ ⊔ 1"
using star.circ_plus_one star_left_unfold_equal sup_commute by auto
lemma star_left_induct_equal:
"z ⊔ x * y = y ⟹ x⇧⋆ * z ≤ y"
by (simp add: star_left_induct)
lemma star_left_induct_mult_equal:
"x * y = y ⟹ x⇧⋆ * y ≤ y"
by (simp add: star_left_induct_mult)
lemma star_star_upper_bound:
"x⇧⋆ ≤ z⇧⋆ ⟹ x⇧⋆⇧⋆ ≤ z⇧⋆"
using star_involutive by auto
lemma star_simulation_left:
assumes "x * z ≤ z * y"
shows "x⇧⋆ * z ≤ z * y⇧⋆"
proof -
have "x * z * y⇧⋆ ≤ z * y * y⇧⋆"
by (simp add: assms mult_left_isotone)
also have "... ≤ z * y⇧⋆"
by (simp add: mult_right_isotone star.left_plus_below_circ mult_assoc)
finally have "z ⊔ x * z * y⇧⋆ ≤ z * y⇧⋆"
using star.circ_back_loop_prefixpoint by auto
thus ?thesis
by (simp add: star_left_induct mult_assoc)
qed
lemma quasicomm_1:
"y * x ≤ x * (x ⊔ y)⇧⋆ ⟷ y⇧⋆ * x ≤ x * (x ⊔ y)⇧⋆"
by (metis mult_isotone order_refl order_trans star.circ_increasing star_involutive star_simulation_left)
lemma star_rtc_3:
"1 ⊔ x ⊔ y * y = y ⟹ x⇧⋆ ≤ y"
by (metis sup.bounded_iff le_iff_sup mult_left_sub_dist_sup_left mult_1_right star_left_induct_mult_iff star.circ_sub_dist)
lemma star_decompose_1:
"(x ⊔ y)⇧⋆ = (x⇧⋆ * y⇧⋆)⇧⋆"
apply (rule order.antisym)
apply (simp add: star.circ_sup_2)
using star.circ_sub_dist_3 star_isotone star_involutive by fastforce
lemma star_sum:
"(x ⊔ y)⇧⋆ = (x⇧⋆ ⊔ y⇧⋆)⇧⋆"
using star_decompose_1 star_involutive by auto
lemma star_decompose_3:
"(x⇧⋆ * y⇧⋆)⇧⋆ = x⇧⋆ * (y * x⇧⋆)⇧⋆"
using star_sup_1 star_decompose_1 by auto
text ‹
In contrast to iterings, we now obtain that the iteration operation results in least fixpoints.
›
lemma star_loop_least_fixpoint:
"y * x ⊔ z = x ⟹ y⇧⋆ * z ≤ x"
by (simp add: sup_commute star_left_induct_equal)
lemma star_loop_is_least_fixpoint:
"is_least_fixpoint (λx . y * x ⊔ z) (y⇧⋆ * z)"
by (simp add: is_least_fixpoint_def star.circ_loop_fixpoint star_loop_least_fixpoint)
lemma star_loop_mu:
"μ (λx . y * x ⊔ z) = y⇧⋆ * z"
by (metis least_fixpoint_same star_loop_is_least_fixpoint)
lemma affine_has_least_fixpoint:
"has_least_fixpoint (λx . y * x ⊔ z)"
by (metis has_least_fixpoint_def star_loop_is_least_fixpoint)
lemma star_outer_increasing:
"x ≤ y⇧⋆ * x * y⇧⋆"
by (metis star.circ_back_loop_prefixpoint star.circ_loop_fixpoint sup.boundedE)
end
text ‹
We next add the right induction rule, which allows us to strengthen many inequalities of left Kleene algebras to equalities.
›
class strong_left_kleene_algebra = left_kleene_algebra +
assumes star_right_induct: "z ⊔ x * y ≤ x ⟶ z * y⇧⋆ ≤ x"
begin
lemma star_plus:
"y⇧⋆ * y = y * y⇧⋆"
proof (rule order.antisym)
show "y⇧⋆ * y ≤ y * y⇧⋆"
by (simp add: star.circ_plus_sub)
next
have "y⇧⋆ * y * y ≤ y⇧⋆ * y"
by (simp add: mult_left_isotone star.right_plus_below_circ)
hence "y ⊔ y⇧⋆ * y * y ≤ y⇧⋆ * y"
by (simp add: star.circ_mult_increasing_2)
thus "y * y⇧⋆ ≤ y⇧⋆ * y"
using star_right_induct by blast
qed
lemma star_slide:
"(x * y)⇧⋆ * x = x * (y * x)⇧⋆"
proof (rule order.antisym)
show "(x * y)⇧⋆ * x ≤ x * (y * x)⇧⋆"
by (rule star_left_slide)
next
have "x ⊔ (x * y)⇧⋆ * x * y * x ≤ (x * y)⇧⋆ * x"
by (metis (full_types) sup.commute eq_refl star.circ_loop_fixpoint mult.assoc star_plus)
thus "x * (y * x)⇧⋆ ≤ (x * y)⇧⋆ * x"
by (simp add: mult_assoc star_right_induct)
qed
lemma star_simulation_right:
assumes "z * x ≤ y * z"
shows "z * x⇧⋆ ≤ y⇧⋆ * z"
proof -
have "y⇧⋆ * z * x ≤ y⇧⋆ * z"
by (metis assms dual_order.trans mult_isotone mult_left_sub_dist_sup_right star.circ_loop_fixpoint star.circ_transitive_equal sup.cobounded1 mult_assoc)
thus ?thesis
by (metis le_supI star.circ_loop_fixpoint star_right_induct sup.cobounded2)
qed
end
text ‹
Again we inherit results from the itering hierarchy.
›
sublocale strong_left_kleene_algebra < star: itering_1 where circ = star
apply unfold_locales
apply (simp add: star_slide)
by (simp add: star_simulation_right)
context strong_left_kleene_algebra
begin
lemma star_right_induct_mult:
"y * x ≤ y ⟹ y * x⇧⋆ ≤ y"
by (simp add: star_right_induct)
lemma star_right_induct_mult_iff:
"y * x ≤ y ⟷ y * x⇧⋆ ≤ y"
using mult_right_isotone order_trans star.circ_increasing star_right_induct_mult by blast
lemma star_simulation_right_equal:
"z * x = y * z ⟹ z * x⇧⋆ = y⇧⋆ * z"
by (metis order.eq_iff star_simulation_left star_simulation_right)
lemma star_simulation_star:
"x * y ≤ y * x ⟹ x⇧⋆ * y⇧⋆ ≤ y⇧⋆ * x⇧⋆"
by (simp add: star_simulation_left star_simulation_right)
lemma star_right_induct_equal:
"z ⊔ y * x = y ⟹ z * x⇧⋆ ≤ y"
by (simp add: star_right_induct)
lemma star_right_induct_mult_equal:
"y * x = y ⟹ y * x⇧⋆ ≤ y"
by (simp add: star_right_induct_mult)
lemma star_back_loop_least_fixpoint:
"x * y ⊔ z = x ⟹ z * y⇧⋆ ≤ x"
by (simp add: sup_commute star_right_induct_equal)
lemma star_back_loop_is_least_fixpoint:
"is_least_fixpoint (λx . x * y ⊔ z) (z * y⇧⋆)"
proof (unfold is_least_fixpoint_def, rule conjI)
have "(z * y⇧⋆ * y ⊔ z) * y ≤ z * y⇧⋆ * y ⊔ z"
using le_supI1 mult_left_isotone star.circ_back_loop_prefixpoint by auto
hence "z * y⇧⋆ ≤ z * y⇧⋆ * y ⊔ z"
by (simp add: star_right_induct)
thus "z * y⇧⋆ * y ⊔ z = z * y⇧⋆"
using order.antisym star.circ_back_loop_prefixpoint by auto
next
show "∀x. x * y ⊔ z = x ⟶ z * y⇧⋆ ≤ x"
by (simp add: star_back_loop_least_fixpoint)
qed
lemma star_back_loop_mu:
"μ (λx . x * y ⊔ z) = z * y⇧⋆"
by (metis least_fixpoint_same star_back_loop_is_least_fixpoint)
lemma star_square:
"x⇧⋆ = (1 ⊔ x) * (x * x)⇧⋆"
proof -
let ?f = "λy . y * x ⊔ 1"
have 1: "isotone ?f"
by (metis sup_left_isotone isotone_def mult_left_isotone)
have "?f ∘ ?f = (λy . y * (x * x) ⊔ (1 ⊔ x))"
by (simp add: sup_assoc sup_commute mult_assoc mult_right_dist_sup o_def)
thus ?thesis
using 1 by (metis mu_square mult_left_one star_back_loop_mu has_least_fixpoint_def star_back_loop_is_least_fixpoint)
qed
lemma star_square_2:
"x⇧⋆ = (x * x)⇧⋆ * (x ⊔ 1)"
proof -
have "(1 ⊔ x) * (x * x)⇧⋆ = (x * x)⇧⋆ * 1 ⊔ x * (x * x)⇧⋆"
using mult_right_dist_sup by force
thus ?thesis
by (metis (no_types) order.antisym mult_left_sub_dist_sup star.circ_square_2 star_slide sup_commute star_square)
qed
lemma star_circ_simulate_right_plus:
assumes "z * x ≤ y * y⇧⋆ * z ⊔ w"
shows "z * x⇧⋆ ≤ y⇧⋆ * (z ⊔ w * x⇧⋆)"
proof -
have "(z ⊔ w * x⇧⋆) * x ≤ z * x ⊔ w * x⇧⋆"
using mult_right_dist_sup star.circ_back_loop_prefixpoint sup_right_isotone by auto
also have "... ≤ y * y⇧⋆ * z ⊔ w ⊔ w * x⇧⋆"
using assms sup_left_isotone by blast
also have "... ≤ y * y⇧⋆ * z ⊔ w * x⇧⋆"
using le_supI1 star.circ_back_loop_prefixpoint sup_commute by auto
also have "... ≤ y⇧⋆ * (z ⊔ w * x⇧⋆)"
by (metis sup.bounded_iff mult_isotone mult_left_isotone mult_left_one mult_left_sub_dist_sup_left star.circ_reflexive star.left_plus_below_circ)
finally have "y⇧⋆ * (z ⊔ w * x⇧⋆) * x ≤ y⇧⋆ * (z ⊔ w * x⇧⋆)"
by (metis mult_assoc mult_right_isotone star.circ_transitive_equal)
thus ?thesis
by (metis sup.bounded_iff star_right_induct mult_left_sub_dist_sup_left star.circ_loop_fixpoint)
qed
lemma transitive_star:
"x * x ≤ x ⟹ x⇧⋆ = 1 ⊔ x"
by (metis order.antisym star.circ_mult_increasing_2 star.circ_plus_same star_left_induct_mult star_left_unfold_equal)
lemma star_sup_2:
assumes "x * x ≤ x"
and "x * y ≤ x"
shows "(x ⊔ y)⇧⋆ = y⇧⋆ * (x ⊔ 1)"
proof -
have "(x ⊔ y)⇧⋆ = y⇧⋆ * (x * y⇧⋆)⇧⋆"
by (simp add: star.circ_decompose_6 star_sup_1)
also have "... = y⇧⋆ * x⇧⋆"
using assms(2) dual_order.antisym star.circ_back_loop_prefixpoint star_right_induct_mult by fastforce
also have "... = y⇧⋆ * (x ⊔ 1)"
by (simp add: assms(1) sup_commute transitive_star)
finally show ?thesis
.
qed
end
text ‹
The following class contains a generalisation of Kleene algebras, which lacks the right zero axiom.
›
class left_zero_kleene_algebra = idempotent_left_zero_semiring + strong_left_kleene_algebra
begin
lemma star_star_absorb:
"y⇧⋆ * (y⇧⋆ * x)⇧⋆ * y⇧⋆ = (y⇧⋆ * x)⇧⋆ * y⇧⋆"
by (metis star.circ_transitive_equal star_slide mult_assoc)
lemma star_circ_simulate_left_plus:
assumes "x * z ≤ z * y⇧⋆ ⊔ w"
shows "x⇧⋆ * z ≤ (z ⊔ x⇧⋆ * w) * y⇧⋆"
proof -
have "x * (x⇧⋆ * (w * y⇧⋆)) ≤ x⇧⋆ * (w * y⇧⋆)"
by (metis (no_types) mult_right_sub_dist_sup_left star.circ_loop_fixpoint mult_assoc)
hence "x * ((z ⊔ x⇧⋆ * w) * y⇧⋆) ≤ x * z * y⇧⋆ ⊔ x⇧⋆ * w * y⇧⋆"
using mult_left_dist_sup mult_right_dist_sup sup_right_isotone mult_assoc by presburger
also have "... ≤ (z * y⇧⋆ ⊔ w) * y⇧⋆ ⊔ x⇧⋆ * w * y⇧⋆"
using assms mult_isotone semiring.add_right_mono by blast
also have "... = z * y⇧⋆ ⊔ w * y⇧⋆ ⊔ x⇧⋆ * w * y⇧⋆"
by (simp add: mult_right_dist_sup star.circ_transitive_equal mult_assoc)
also have "... = (z ⊔ w ⊔ x⇧⋆ * w) * y⇧⋆"
by (simp add: mult_right_dist_sup)
also have "... = (z ⊔ x⇧⋆ * w) * y⇧⋆"
by (metis sup_assoc sup_ge2 le_iff_sup star.circ_loop_fixpoint)
finally show ?thesis
by (metis sup.bounded_iff mult_left_sub_dist_sup_left mult_1_right star.circ_right_unfold_1 star_left_induct)
qed
lemma star_one_sup_below:
"x * y⇧⋆ * (1 ⊔ z) ≤ x * (y ⊔ z)⇧⋆"
proof -
have "y⇧⋆ * z ≤ (y ⊔ z)⇧⋆"
using sup_ge2 order_trans star.circ_increasing star.circ_mult_upper_bound star.circ_sub_dist by blast
hence "y⇧⋆ ⊔ y⇧⋆ * z ≤ (y ⊔ z)⇧⋆"
by (simp add: star.circ_sup_upper_bound star.circ_sub_dist)
hence "y⇧⋆ * (1 ⊔ z) ≤ (y ⊔ z)⇧⋆"
by (simp add: mult_left_dist_sup)
thus ?thesis
by (metis mult_right_isotone mult_assoc)
qed
text ‹
The following theorem is similar to the puzzle where persons insert themselves always in the middle between two groups of people in a line.
Here, however, items in the middle annihilate each other, leaving just one group of items behind.
›
lemma cancel_separate:
assumes "x * y ≤ 1"
shows "x⇧⋆ * y⇧⋆ ≤ x⇧⋆ ⊔ y⇧⋆"
proof -
have "x * y⇧⋆ = x ⊔ x * y * y⇧⋆"
by (metis mult_assoc mult_left_dist_sup mult_1_right star_left_unfold_equal)
also have "... ≤ x ⊔ y⇧⋆"
by (meson assms dual_order.trans order.refl star.circ_mult_upper_bound star.circ_reflexive sup_right_isotone)
also have "... ≤ x⇧⋆ ⊔ y⇧⋆"
using star.circ_increasing sup_left_isotone by auto
finally have 1: "x * y⇧⋆ ≤ x⇧⋆ ⊔ y⇧⋆"
.
have "x * (x⇧⋆ ⊔ y⇧⋆) = x * x⇧⋆ ⊔ x * y⇧⋆"
by (simp add: mult_left_dist_sup)
also have "... ≤ x⇧⋆ ⊔ y⇧⋆"
using 1 by (metis sup.bounded_iff sup_ge1 order_trans star.left_plus_below_circ)
finally have 2: "x * (x⇧⋆ ⊔ y⇧⋆) ≤ x⇧⋆ ⊔ y⇧⋆"
.
have "y⇧⋆ ≤ x⇧⋆ ⊔ y⇧⋆"
by simp
hence "y⇧⋆ ⊔ x * (x⇧⋆ ⊔ y⇧⋆) ≤ x⇧⋆ ⊔ y⇧⋆"
using 2 sup.bounded_iff by blast
thus ?thesis
by (metis star_left_induct)
qed
lemma star_separate:
assumes "x * y = bot"
and "y * y = bot"
shows "(x ⊔ y)⇧⋆ = x⇧⋆ ⊔ y * x⇧⋆"
proof -
have 1: "y⇧⋆ = 1 ⊔ y"
using assms(2) by (simp add: transitive_star)
have "(x ⊔ y)⇧⋆ = y⇧⋆ * (x * y⇧⋆)⇧⋆"
by (simp add: star.circ_decompose_6 star_sup_1)
also have "... = y⇧⋆ * (x * (1 ⊔ y * y⇧⋆))⇧⋆"
by (simp add: star_left_unfold_equal)
also have "... = (1 ⊔ y) * x⇧⋆"
using 1 by (simp add: assms mult_left_dist_sup)
also have "... = x⇧⋆ ⊔ y * x⇧⋆"
by (simp add: mult_right_dist_sup)
finally show ?thesis
.
qed
end
text ‹
We can now inherit from the strongest variant of iterings.
›
sublocale left_zero_kleene_algebra < star: itering where circ = star
apply unfold_locales
apply (metis star.circ_sup_9)
apply (metis star.circ_mult_1)
apply (simp add: star_circ_simulate_right_plus)
by (simp add: star_circ_simulate_left_plus)
context left_zero_kleene_algebra
begin
lemma star_absorb:
"x * y = bot ⟹ x * y⇧⋆ = x"
by (metis sup.bounded_iff antisym_conv star.circ_back_loop_prefixpoint star.circ_elimination)
lemma star_separate_2:
assumes "x * z⇧+ * y = bot"
and "y * z⇧+ * y = bot"
and "z * x = bot"
shows "(x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆ = z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
proof -
have 1: "x⇧⋆ * z⇧+ * y = z⇧+ * y"
by (metis assms mult_assoc mult_1_left mult_left_zero star.circ_zero star_simulation_right_equal)
have 2: "z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
by (simp add: mult_right_isotone star.left_plus_below_circ)
have "z⇧⋆ * z⇧+ * y * x⇧⋆ ≤ z⇧⋆ * y * x⇧⋆"
by (metis mult_left_isotone star.left_plus_below_circ star.right_plus_circ star_plus)
also have "... ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆)"
by (simp add: mult_assoc mult_left_sub_dist_sup_right)
also have "... ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
using sup_right_divisibility star.circ_back_loop_fixpoint by blast
finally have 3: "z⇧⋆ * z⇧+ * y * x⇧⋆ ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
.
have "z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆ * (z * (1 ⊔ y * x⇧⋆)) = z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ ⊔ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ * y * x⇧⋆"
by (metis mult_1_right semiring.distrib_left star.circ_plus_same mult_assoc)
also have "... = z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ ⊔ z⇧⋆ * (1 ⊔ y) * x⇧⋆ * z⇧+ * y * x⇧⋆"
by (simp add: semiring.distrib_right mult_assoc)
also have "... = z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ ⊔ z⇧⋆ * (1 ⊔ y) * z⇧+ * y * x⇧⋆"
using 1 by (simp add: mult_assoc)
also have "... = z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ ⊔ z⇧⋆ * z⇧+ * y * x⇧⋆ ⊔ z⇧⋆ * y * z⇧+ * y * x⇧⋆"
using mult_left_dist_sup mult_right_dist_sup sup_assoc by auto
also have "... = z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧+ ⊔ z⇧⋆ * z⇧+ * y * x⇧⋆"
by (metis assms(2) mult_left_dist_sup mult_left_zero sup_commute sup_monoid.add_0_left mult_assoc)
also have "... ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
using 2 3 by simp
finally have "(x⇧⋆ ⊔ y * x⇧⋆) ⊔ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆ * (z * (1 ⊔ y * x⇧⋆)) ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
by (simp add: star_outer_increasing)
hence 4: "(x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆ ≤ z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆"
by (simp add: star_right_induct)
have 5: "(x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆ ≤ (x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆"
by (metis sup_ge1 mult_right_isotone mult_1_right star_isotone)
have "z * (x⇧⋆ ⊔ y * x⇧⋆) = z * x⇧⋆ ⊔ z * y * x⇧⋆"
by (simp add: mult_assoc mult_left_dist_sup)
also have "... = z ⊔ z * y * x⇧⋆"
by (simp add: assms star_absorb)
also have "... = z * (1 ⊔ y * x⇧⋆)"
by (simp add: mult_assoc mult_left_dist_sup)
also have "... ≤ (z * (1 ⊔ y * x⇧⋆))⇧⋆"
by (simp add: star.circ_increasing)
also have "... ≤ (x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆"
by (metis le_supE mult_right_sub_dist_sup_left star.circ_loop_fixpoint)
finally have "z * (x⇧⋆ ⊔ y * x⇧⋆) ≤ (x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆"
.
hence "z * (x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆ ≤ (x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆"
by (metis mult_assoc mult_left_isotone star.circ_transitive_equal)
hence "z⇧⋆ * (x⇧⋆ ⊔ y * x⇧⋆) * z⇧⋆ ≤ (x⇧⋆ ⊔ y * x⇧⋆) * (z * (1 ⊔ y * x⇧⋆))⇧⋆"
using 5 by (metis star_left_induct sup.bounded_iff mult_assoc)
thus ?thesis
using 4 by (simp add: antisym)
qed
lemma cancel_separate_eq:
"x * y ≤ 1 ⟹ x⇧⋆ * y⇧⋆ = x⇧⋆ ⊔ y⇧⋆"
by (metis order.antisym cancel_separate star.circ_plus_one star.circ_sup_sub_sup_one_1 star_involutive)
lemma cancel_separate_1:
assumes "x * y ≤ 1"
shows "(x ⊔ y)⇧⋆ = y⇧⋆ * x⇧⋆"
proof -
have "y⇧⋆ * x⇧⋆ * y = y⇧⋆ * x⇧⋆ * x * y ⊔ y⇧⋆ * y"
by (metis mult_right_dist_sup star.circ_back_loop_fixpoint)
also have "... ≤ y⇧⋆ * x⇧⋆ ⊔ y⇧⋆ * y"
by (metis assms semiring.add_right_mono mult_right_isotone mult_1_right mult_assoc)
also have "... ≤ y⇧⋆ * x⇧⋆ ⊔ y⇧⋆"
using semiring.add_left_mono star.right_plus_below_circ by simp
also have "... = y⇧⋆ * x⇧⋆"
by (metis star.circ_back_loop_fixpoint sup.left_idem sup_commute)
finally have "y⇧⋆ * x⇧⋆ * y ≤ y⇧⋆ * x⇧⋆"
by simp
hence "y⇧⋆ * x⇧⋆ * (x ⊔ y) ≤ y⇧⋆ * x⇧⋆ * x ⊔ y⇧⋆ * x⇧⋆"
using mult_left_dist_sup order_lesseq_imp by fastforce
also have "... = y⇧⋆ * x⇧⋆"
by (metis star.circ_back_loop_fixpoint sup.left_idem)
finally have "(x ⊔ y)⇧⋆ ≤ y⇧⋆ * x⇧⋆"
by (metis star.circ_decompose_7 star_right_induct_mult sup_commute)
thus ?thesis
using order.antisym star.circ_sub_dist_3 sup_commute by fastforce
qed
lemma plus_sup:
"(x ⊔ y)⇧+ = (x⇧⋆ * y)⇧⋆ * x⇧+ ⊔ (x⇧⋆ * y)⇧+"
by (metis semiring.distrib_left star.circ_sup_9 star_plus mult_assoc)
lemma plus_half_bot:
"x * y * x = bot ⟹ (x * y)⇧+ = x * y"
by (metis star_absorb star_slide mult_assoc)
lemma cancel_separate_1_sup:
assumes "x * y ≤ 1"
and "y * x ≤ 1"
shows "(x ⊔ y)⇧⋆ = x⇧⋆ ⊔ y⇧⋆"
by (simp add: assms cancel_separate_1 cancel_separate_eq sup_commute)
text ‹Lemma ‹star_separate_3› was contributed by Nicolas Robinson-O'Brien.›
lemma star_separate_3:
assumes "y * x⇧⋆ * y ≤ y"
shows "(x ⊔ y)⇧⋆ = x⇧⋆ ⊔ x⇧⋆ * y * x⇧⋆"
proof (rule order.antisym)
have "x⇧⋆ * y * (x⇧⋆ * y)⇧⋆ * x⇧⋆ ≤ x⇧⋆ * y * x⇧⋆"
by (metis assms mult_left_isotone mult_right_isotone star_right_induct_mult mult_assoc)
thus "(x ⊔ y)⇧⋆ ≤ x⇧⋆ ⊔ x⇧⋆ * y * x⇧⋆"
by (metis order.antisym semiring.add_left_mono star.circ_sup_2 star.circ_sup_sub star.circ_unfold_sum star_decompose_3 star_slide mult_assoc)
next
show "x⇧⋆ ⊔ x⇧⋆ * y * x⇧⋆ ≤ (x ⊔ y)⇧⋆"
using mult_isotone star.circ_increasing star.circ_sub_dist star.circ_sup_9 by auto
qed
end
text ‹
A Kleene algebra is obtained by requiring an idempotent semiring.
›
class kleene_algebra = left_zero_kleene_algebra + idempotent_semiring
text ‹
The following classes are variants of Kleene algebras expanded by an additional iteration operation.
This is useful to study the Kleene star in computation models that do not use least fixpoints in the refinement order as the semantics of recursion.
›
class left_kleene_conway_semiring = left_kleene_algebra + left_conway_semiring
begin
lemma star_below_circ:
"x⇧⋆ ≤ x⇧∘"
by (metis circ_left_unfold mult_1_right order_refl star_left_induct)
lemma star_zero_below_circ_mult:
"x⇧⋆ * bot ≤ x⇧∘ * y"
by (simp add: mult_isotone star_below_circ)
lemma star_mult_circ:
"x⇧⋆ * x⇧∘ = x⇧∘"
by (metis sup_right_divisibility order.antisym circ_left_unfold star_left_induct_mult star.circ_loop_fixpoint)
lemma circ_mult_star:
"x⇧∘ * x⇧⋆ = x⇧∘"
by (metis sup_assoc sup.bounded_iff circ_left_unfold circ_rtc_2 order.eq_iff left_plus_circ star.circ_sup_sub star.circ_back_loop_prefixpoint star.circ_increasing star_below_circ star_mult_circ star_sup_one)
lemma circ_star:
"x⇧∘⇧⋆ = x⇧∘"
by (metis order.antisym circ_reflexive circ_transitive_equal star.circ_increasing star.circ_sup_one_right_unfold star_left_induct_mult_equal)
lemma star_circ:
"x⇧⋆⇧∘ = x⇧∘⇧∘"
by (metis order.antisym circ_circ_sup circ_sub_dist le_iff_sup star.circ_rtc_2 star_below_circ)
lemma circ_sup_3:
"(x⇧∘ * y⇧∘)⇧⋆ ≤ (x ⊔ y)⇧∘"
using circ_star circ_sub_dist_3 star_isotone by fastforce
end
class left_zero_kleene_conway_semiring = left_zero_kleene_algebra + itering
begin
subclass left_kleene_conway_semiring ..
lemma circ_isolate:
"x⇧∘ = x⇧∘ * bot ⊔ x⇧⋆"
by (metis sup_commute order.antisym circ_sup_upper_bound circ_mult_star circ_simulate_absorb star.left_plus_below_circ star_below_circ zero_right_mult_decreasing)
lemma circ_isolate_mult:
"x⇧∘ * y = x⇧∘ * bot ⊔ x⇧⋆ * y"
by (metis circ_isolate mult_assoc mult_left_zero mult_right_dist_sup)
lemma circ_isolate_mult_sub:
"x⇧∘ * y ≤ x⇧∘ ⊔ x⇧⋆ * y"
by (metis sup_left_isotone circ_isolate_mult zero_right_mult_decreasing)
lemma circ_sub_decompose:
"(x⇧∘ * y)⇧∘ ≤ (x⇧⋆ * y)⇧∘ * x⇧∘"
proof -
have "x⇧⋆ * y ⊔ x⇧∘ * bot = x⇧∘ * y"
by (metis sup.commute circ_isolate_mult)
hence "(x⇧⋆ * y)⇧∘ * x⇧∘ = ((x⇧∘ * y)⇧∘ ⊔ x⇧∘)⇧⋆"
by (metis circ_star circ_sup_9 circ_sup_mult_zero star_decompose_1)
thus ?thesis
by (metis circ_star le_iff_sup star.circ_decompose_7 star.circ_unfold_sum)
qed
lemma circ_sup_4:
"(x ⊔ y)⇧∘ = (x⇧⋆ * y)⇧∘ * x⇧∘"
apply (rule order.antisym)
apply (metis circ_sup circ_sub_decompose circ_transitive_equal mult_assoc mult_left_isotone)
by (metis circ_sup circ_isotone mult_left_isotone star_below_circ)
lemma circ_sup_5:
"(x⇧∘ * y)⇧∘ * x⇧∘ = (x⇧⋆ * y)⇧∘ * x⇧∘"
using circ_sup_4 circ_sup_9 by auto
lemma plus_circ:
"(x⇧⋆ * x)⇧∘ = x⇧∘"
by (metis sup_idem circ_sup_4 circ_decompose_7 circ_star star.circ_decompose_5 star.right_plus_circ)
end
text ‹
The following classes add a greatest element.
›
class bounded_left_kleene_algebra = bounded_idempotent_left_semiring + left_kleene_algebra
sublocale bounded_left_kleene_algebra < star: bounded_left_conway_semiring where circ = star ..
class bounded_left_zero_kleene_algebra = bounded_idempotent_left_semiring + left_zero_kleene_algebra
sublocale bounded_left_zero_kleene_algebra < star: bounded_itering where circ = star ..
class bounded_kleene_algebra = bounded_idempotent_semiring + kleene_algebra
sublocale bounded_kleene_algebra < star: bounded_itering where circ = star ..
text ‹
We conclude with an alternative axiomatisation of Kleene algebras.
›
class kleene_algebra_var = idempotent_semiring + star +
assumes star_left_unfold_var : "1 ⊔ y * y⇧⋆ ≤ y⇧⋆"
assumes star_left_induct_var : "y * x ≤ x ⟶ y⇧⋆ * x ≤ x"
assumes star_right_induct_var : "x * y ≤ x ⟶ x * y⇧⋆ ≤ x"
begin
subclass kleene_algebra
apply unfold_locales
apply (rule star_left_unfold_var)
apply (meson sup.bounded_iff mult_right_isotone order_trans star_left_induct_var)
by (meson sup.bounded_iff mult_left_isotone order_trans star_right_induct_var)
end
end