Theory Kleene_Algebra.Kleene_Algebra

(* Title:      Kleene Algebra
   Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

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"
(*nitpick [expect=genuine]*)
  oops

lemma "x  x = x"
(*nitpick [expect=genuine]*)
  oops

text ‹Next we show that starred elements are transitive.›

lemma star_trans_eq [simp]: "x  x = x"
proof (rule order.antisym) ― ‹this splits an equation into two inequalities›
  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"
(*nitpick [expect=genuine]*)
  oops

lemma "x  z  y  z + x  y  y"
(*nitpick [expect=genuine]*)
  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"
(*nitpick [expect=genuine]*)
  oops

lemma "x  x"
(*nitpick [expect=genuine]*)
  oops

lemma "x  x  x"
(*nitpick [expect=genuine]*)
  oops

lemma "1 + x  x = x"
(*nitpick [expect=genuine]*)
  oops

lemma "x  z  z  y  x  z  z  y"
(*nitpick [expect=genuine]*)
  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"
(*nitpick [expect=genuine]*)
  oops

end (* left_near_kleene_algebra *)


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"
(*nitpick [expect=genuine]*)
  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)"
(*nitpick [expect=genuine]*)
  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"
(*nitpick [expect=genuine]*)
  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"
(*nitpick [expect=genuine]*)
  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"
(*nitpick [expect=genuine]*)
  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"
(*nitpick [expect=genuine]*)
  oops

lemma "y  x  x  y  (x + y)  x  y"
  (* nitpick [expect=genuine] *) 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"
(*nitpick [expect=genuine]*)
  oops

lemma "(x  y)  x = x  (y  x)"
(*nitpick [expect=genuine]*)
  oops

lemma "x  x = x  x = 1 + x"
(* nitpick [expect=genuine] *) 
  oops

end (* left_pre_kleene_algebra *)


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)

(*
text {*
For the following two lemmas, Isabelle could neither find a
counterexample nor a proof automatically.
*}

lemma "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x ≤ y ⋅ z"
  -- "unfortunately, no counterexample found"
oops

lemma star_sim3: "z ⋅ x = y ⋅ z ⟹ z ⋅ x = y ⋅ z"
  -- "we conjecture that this is not provable"
oops
*)

end (* left_kleene_algebra *)


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 (* left_kleene_algebra_zerol *)


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 (* kleene_algebra *)

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 (* commutative_kleene_algebra *)

end