Theory Omega_Algebra

(* Title:      Omega 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 ‹Omega Algebras›

theory Omega_Algebra
imports Kleene_Algebra
begin

text ‹
\emph{Omega algebras}~\<^cite>‹"cohen00omega"› extend Kleene algebras by an
$\omega$-operation that axiomatizes infinite iteration (just like the
Kleene star axiomatizes finite iteration).
›


subsection ‹Left Omega Algebras›

text ‹
In this section we consider \emph{left omega algebras}, i.e., omega
algebras based on left Kleene algebras. Surprisingly, we are still
looking for statements mentioning~$\omega$ that are true in omega
algebras, but do not already hold in left omega algebras.
›

class left_omega_algebra = left_kleene_algebra_zero + omega_op +
  assumes omega_unfold: "x⇧^ω ≤ x ⋅ x⇧^ω"
  and omega_coinduct: "y ≤ z + x ⋅ y ⟹ y ≤ x⇧^ω + x⇧^⋆ ⋅ z"
begin

text ‹First we prove some variants of the coinduction axiom.›

lemma omega_coinduct_var1: "y ≤ 1 + x ⋅ y ⟹ y ≤ x⇧^ω + x⇧^⋆"
  using local.omega_coinduct by fastforce

lemma  omega_coinduct_var2: "y ≤ x ⋅ y ⟹ y ≤ x⇧^ω"
  by (metis add.commute add_zero_l annir omega_coinduct)

lemma omega_coinduct_eq: "y = z + x ⋅ y ⟹ y ≤ x⇧^ω + x⇧^⋆ ⋅ z"
  by (simp add: local.omega_coinduct)

lemma omega_coinduct_eq_var1: "y = 1 + x ⋅ y ⟹ y ≤ x⇧^ω + x⇧^⋆"
  by (simp add: omega_coinduct_var1)

lemma  omega_coinduct_eq_var2: "y = x ⋅ y ⟹ y ≤ x⇧^ω"
  by (simp add: omega_coinduct_var2)

lemma "y = x ⋅ y + z ⟹ y = x⇧^⋆ ⋅ z + x⇧^ω"
  (* nitpick [expect=genuine] -- "2-element counterexample" *)
oops

lemma "y = 1 + x ⋅ y ⟹ y = x⇧^ω + x⇧^⋆"
  (* nitpick [expect=genuine] -- "3-element counterexample" *)
oops

lemma "y = x ⋅ y ⟹ y = x⇧^ω"
  (* nitpick [expect=genuine] -- "2-element counterexample" *)
oops

text ‹Next we strengthen the unfold law to an equation.›

lemma omega_unfold_eq [simp]: "x ⋅ x⇧^ω = x⇧^ω"
proof (rule order.antisym)
  have "x ⋅ x⇧^ω ≤ x ⋅ x ⋅ x⇧^ω"
    by (simp add: local.mult_isol local.omega_unfold mult_assoc)
  thus "x ⋅ x⇧^ω ≤ x⇧^ω"
    by (simp add: mult_assoc omega_coinduct_var2)
  show  "x⇧^ω ≤ x ⋅ x⇧^ω"
    by (fact omega_unfold)
qed

lemma omega_unfold_var: "z + x ⋅ x⇧^ω ≤ x⇧^ω + x⇧^⋆ ⋅ z"
  by (simp add: local.omega_coinduct)

lemma "z + x ⋅ x⇧^ω = x⇧^ω + x⇧^⋆ ⋅ z"
  (* nitpick [expect=genuine] -- "4-element counterexample" *)
oops

text ‹We now prove subdistributivity and isotonicity of omega.›

lemma omega_subdist: "x⇧^ω ≤ (x + y)⇧^ω"
proof -
  have "x⇧^ω ≤ (x + y) ⋅ x⇧^ω"
    by simp
  thus ?thesis
    by (rule omega_coinduct_var2)
qed

lemma omega_iso: "x ≤ y ⟹ x⇧^ω ≤ y⇧^ω"
  by (metis less_eq_def omega_subdist)

lemma omega_subdist_var: "x⇧^ω + y⇧^ω ≤ (x + y)⇧^ω"
  by (simp add: omega_iso)

lemma zero_omega [simp]: "0⇧^ω = 0"
  by (metis annil omega_unfold_eq)

text ‹The next lemma is another variant of omega unfold›

lemma star_omega_1 [simp]: "x⇧^⋆ ⋅ x⇧^ω = x⇧^ω"
proof (rule order.antisym)
  have "x ⋅ x⇧^ω ≤ x⇧^ω"
    by simp
  thus "x⇧^⋆ ⋅ x⇧^ω ≤ x⇧^ω"
    by simp
  show "x⇧^ω ≤ x⇧^⋆ ⋅ x⇧^ω"
    using local.star_inductl_var_eq2 by auto
qed

text ‹The next lemma says that~@{term "1⇧^ω"} is the maximal element
of omega algebra. We therefore baptise it~$\top$.›

lemma max_element: "x ≤ 1⇧^ω"
  by (simp add: omega_coinduct_eq_var2)

definition top (‹⊤›)
  where "⊤ = 1⇧^ω"

lemma star_omega_3 [simp]: "(x⇧^⋆)⇧^ω = ⊤"
proof -
  have "1 ≤ x⇧^⋆"
    by (fact star_ref)
  hence "⊤ ≤ (x⇧^⋆)⇧^ω"
    by (simp add: omega_iso top_def)
  thus ?thesis
    by (simp add: local.order.antisym max_element top_def)
qed

text ‹The following lemma is strange since it is counterintuitive
that one should be able to append something after an infinite
iteration.›

lemma omega_1: "x⇧^ω ⋅ y ≤ x⇧^ω"
proof -
  have "x⇧^ω ⋅ y ≤ x ⋅ x⇧^ω ⋅ y"
    by simp
  thus ?thesis
    by (metis mult.assoc omega_coinduct_var2)
qed

lemma "x⇧^ω ⋅ y = x⇧^ω"
  (*nitpick [expect=genuine] -- "2-element counterexample"*)
oops

lemma omega_sup_id: "1 ≤ y ⟹ x⇧^ω ⋅ y = x⇧^ω"
  using order.eq_iff local.mult_isol omega_1 by fastforce

lemma omega_top [simp]: "x⇧^ω ⋅ ⊤ = x⇧^ω"
  by (simp add: max_element omega_sup_id top_def)

lemma supid_omega: "1 ≤ x ⟹ x⇧^ω = ⊤"
  by (simp add: local.order.antisym max_element omega_iso top_def)

lemma "x⇧^ω = ⊤ ⟹ 1 ≤ x"
  (* nitpick [expect=genuine] -- "4-element counterexample" *)
oops

text ‹Next we prove a simulation law for the omega operation›

lemma omega_simulation: "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧^ω ≤ y⇧^ω"
proof -
  assume hyp: "z ⋅ x ≤ y ⋅ z"
  have "z ⋅ x⇧^ω = z ⋅ x ⋅ x⇧^ω"
    by (simp add: mult_assoc)
  also have "... ≤ y ⋅ z ⋅ x⇧^ω"
    by (simp add: hyp local.mult_isor)
  finally show "z ⋅ x⇧^ω ≤ y⇧^ω"
    by (simp add: mult_assoc omega_coinduct_var2)
qed

lemma "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧^ω ≤ y⇧^ω ⋅ z"
  (* nitpick [expect=genuine] -- "4-element counterexample" *)
oops

lemma "y ⋅ z  ≤ z ⋅ x ⟹ y⇧^ω ≤ z ⋅ x⇧^ω"
  (* nitpick [expect=genuine] -- "2-element counterexample" *)
oops

lemma "y ⋅ z  ≤ z ⋅ x ⟹ y⇧^ω ⋅ z ≤ x⇧^ω"
  (* nitpick [expect=genuine] -- "4-element counterexample" *)
oops

text ‹Next we prove transitivity of omega elements.›

lemma omega_omega: "(x⇧^ω)⇧^ω ≤ x⇧^ω"
  by (metis omega_1 omega_unfold_eq)

(*
lemma "x⇧^ω ⋅ x⇧^ω = x⇧^ω"
nitpick -- "no proof, no counterexample"

lemma "(x⇧^ω)⇧^ω = x⇧^ω"
nitpick -- "no proof, no counterexample"
*)

text ‹The next lemmas are axioms of Wagner's complete axiomatisation
for omega-regular languages~\<^cite>‹"wagner77omega"›, but in a slightly
different setting.›

lemma wagner_1 [simp]: "(x ⋅ x⇧^⋆)⇧^ω = x⇧^ω"
proof (rule order.antisym)
  have "(x ⋅ x⇧^⋆)⇧^ω = x ⋅ x⇧^⋆ ⋅ x ⋅ x⇧^⋆ ⋅ (x ⋅ x⇧^⋆)⇧^ω"
    by (metis mult.assoc omega_unfold_eq)
  also have "... = x ⋅ x ⋅ x⇧^⋆ ⋅ x⇧^⋆ ⋅ (x ⋅ x⇧^⋆)⇧^ω"
    by (simp add: local.star_slide_var mult_assoc)
  also have "... = x ⋅ x ⋅ x⇧^⋆ ⋅ (x ⋅ x⇧^⋆)⇧^ω"
    by (simp add: mult_assoc)
  also have "... = x ⋅ (x ⋅ x⇧^⋆)⇧^ω"
    by (simp add: mult_assoc)
  thus "(x ⋅ x⇧^⋆)⇧^ω ≤ x⇧^ω"
    using calculation omega_coinduct_eq_var2 by auto
   show "x⇧^ω ≤ (x ⋅ x⇧^⋆)⇧^ω"
    by (simp add: mult_assoc omega_coinduct_eq_var2)
qed

lemma wagner_2_var: "x ⋅ (y ⋅ x)⇧^ω ≤ (x ⋅ y)⇧^ω"
proof -
  have "x ⋅ y ⋅ x ≤ x ⋅ y ⋅ x"
    by auto
  thus "x ⋅ (y ⋅ x)⇧^ω ≤ (x ⋅ y)⇧^ω"
    by (simp add: mult_assoc omega_simulation)
qed

lemma wagner_2 [simp]: "x ⋅ (y ⋅ x)⇧^ω = (x ⋅ y)⇧^ω"
proof (rule order.antisym)
  show "x ⋅ (y ⋅ x)⇧^ω ≤ (x ⋅ y)⇧^ω"
    by (rule wagner_2_var)
  have "(x ⋅ y)⇧^ω = x ⋅ y ⋅ (x ⋅ y)⇧^ω"
    by simp
  thus "(x ⋅ y)⇧^ω ≤ x ⋅ (y ⋅ x)⇧^ω"
    by (metis mult.assoc mult_isol wagner_2_var)
qed

text ‹
This identity is called~(A8) in Wagner's paper.
›

lemma wagner_3:
assumes "x ⋅ (x + y)⇧^ω + z = (x + y)⇧^ω"
shows "(x + y)⇧^ω = x⇧^ω + x⇧^⋆ ⋅ z"
proof (rule order.antisym)
  show  "(x + y)⇧^ω ≤ x⇧^ω + x⇧^⋆ ⋅ z"
    using assms local.join.sup_commute omega_coinduct_eq by auto
  have "x⇧^⋆ ⋅ z ≤ (x + y)⇧^ω"
    using assms local.join.sup_commute local.star_inductl_eq by auto
  thus "x⇧^ω + x⇧^⋆ ⋅ z ≤ (x + y)⇧^ω"
    by (simp add: omega_subdist)
qed

text ‹
This identity is called~(R4) in Wagner's paper.
›

lemma wagner_1_var [simp]: "(x⇧^⋆ ⋅ x)⇧^ω = x⇧^ω"
  by (simp add: local.star_slide_var)

lemma star_omega_4 [simp]: "(x⇧^ω)⇧^⋆ = 1 + x⇧^ω"
proof (rule order.antisym)
  have "(x⇧^ω)⇧^⋆ = 1 + x⇧^ω ⋅ (x⇧^ω)⇧^⋆"
    by simp
  also have "... ≤ 1 + x⇧^ω ⋅ ⊤"
    by (simp add: omega_sup_id)
  finally show "(x⇧^ω)⇧^⋆ ≤ 1 + x⇧^ω"
    by simp
  show "1 + x⇧^ω ≤ (x⇧^ω)⇧^⋆"
    by simp
qed

lemma star_omega_5 [simp]: "x⇧^ω ⋅ (x⇧^ω)⇧^⋆ = x⇧^ω"
proof (rule order.antisym)
  show "x⇧^ω ⋅ (x⇧^ω)⇧^⋆ ≤ x⇧^ω"
    by (rule omega_1)
  show "x⇧^ω ≤ x⇧^ω ⋅ (x⇧^ω)⇧^⋆"
    by (simp add: omega_sup_id)
qed

text ‹The next law shows how omegas below a sum can be unfolded.›

lemma omega_sum_unfold: "x⇧^ω + x⇧^⋆ ⋅ y ⋅ (x + y)⇧^ω = (x + y)⇧^ω"
proof -
  have "(x + y)⇧^ω = x ⋅ (x + y)⇧^ω + y ⋅ (x+y)⇧^ω"
    by (metis distrib_right omega_unfold_eq)
  thus ?thesis
    by (metis mult.assoc wagner_3)
qed

text ‹
The next two lemmas apply induction and coinduction to this law.
›

lemma omega_sum_unfold_coind: "(x + y)⇧^ω ≤ (x⇧^⋆ ⋅ y)⇧^ω + (x⇧^⋆ ⋅ y)⇧^⋆ ⋅ x⇧^ω"
  by (simp add: omega_coinduct_eq omega_sum_unfold)

lemma omega_sum_unfold_ind: "(x⇧^⋆ ⋅ y)⇧^⋆ ⋅ x⇧^ω ≤ (x + y)⇧^ω"
  by (simp add: local.star_inductl_eq omega_sum_unfold)

lemma wagner_1_gen: "(x ⋅ y⇧^⋆)⇧^ω ≤ (x + y)⇧^ω"
proof -
  have "(x ⋅ y⇧^⋆)⇧^ω ≤ ((x + y) ⋅ (x + y)⇧^⋆)⇧^ω"
    using local.join.le_sup_iff local.join.sup.cobounded1 local.mult_isol_var local.star_subdist_var omega_iso by presburger
  thus ?thesis
    by (metis wagner_1)
qed

lemma wagner_1_var_gen: "(x⇧^⋆ ⋅ y)⇧^ω ≤ (x + y)⇧^ω"
proof -
  have "(x⇧^⋆ ⋅ y)⇧^ω = x⇧^⋆ ⋅ (y ⋅ x⇧^⋆)⇧^ω"
    by simp
  also have "... ≤ x⇧^⋆ ⋅ (x + y)⇧^ω"
    by (metis add.commute mult_isol wagner_1_gen)
  also have "... ≤ (x + y)⇧^⋆ ⋅ (x + y)⇧^ω"
    using local.mult_isor local.star_subdist by auto
  thus ?thesis
    by (metis calculation order_trans star_omega_1)
qed

text ‹The next lemma is a variant of the denest law for the star at
the level of omega.›

lemma omega_denest [simp]: "(x + y)⇧^ω = (x⇧^⋆ ⋅ y)⇧^ω + (x⇧^⋆ ⋅ y)⇧^⋆ ⋅ x⇧^ω"
proof (rule order.antisym)
  show "(x + y)⇧^ω ≤ (x⇧^⋆ ⋅ y)⇧^ω + (x⇧^⋆ ⋅ y)⇧^⋆ ⋅ x⇧^ω"
    by (rule omega_sum_unfold_coind)
  have "(x⇧^⋆ ⋅ y)⇧^ω ≤  (x + y)⇧^ω"
    by (rule wagner_1_var_gen)
  hence "(x⇧^⋆ ⋅ y)⇧^⋆ ⋅ x⇧^ω ≤ (x + y)⇧^ω"
    by (simp add: omega_sum_unfold_ind)
  thus "(x⇧^⋆ ⋅ y)⇧^ω + (x⇧^⋆ ⋅ y)⇧^⋆ ⋅ x⇧^ω ≤ (x + y)⇧^ω"
    by (simp add: wagner_1_var_gen)
qed

text ‹The next lemma yields a separation theorem for infinite
iteration in the presence of a quasicommutation property. A
nondeterministic loop over~@{term x} and~@{term y} can be refined into
separate infinite loops over~@{term x} and~@{term y}.›

lemma omega_sum_refine:
  assumes "y ⋅ x ≤ x ⋅ (x + y)⇧^⋆"
  shows "(x + y)⇧^ω = x⇧^ω + x⇧^⋆ ⋅ y⇧^ω"
proof (rule order.antisym)
  have a: "y⇧^⋆ ⋅ x ≤ x ⋅ (x + y)⇧^⋆"
    using assms local.quasicomm_var by blast
  have "(x + y)⇧^ω = y⇧^ω + y⇧^⋆ ⋅ x ⋅ (x + y)⇧^ω"
    by (metis add.commute omega_sum_unfold)
  also have "... ≤ y⇧^ω + x ⋅ (x + y)⇧^⋆ ⋅ (x + y)⇧^ω"
    using a local.join.sup_mono local.mult_isol_var by blast
  also have "... ≤ x ⋅ (x + y)⇧^ω + y⇧^ω"
    using local.eq_refl local.join.sup_commute mult_assoc star_omega_1 by presburger
  finally show "(x + y)⇧^ω ≤ x⇧^ω + x⇧^⋆ ⋅ y⇧^ω"
    by (metis add_commute local.omega_coinduct)
  have "x⇧^ω + x⇧^⋆ ⋅ y⇧^ω ≤ (x + y)⇧^ω + (x + y)⇧^⋆ ⋅ (x + y)⇧^ω"
    using local.join.sup.cobounded2 local.join.sup.mono local.mult_isol_var local.star_subdist omega_iso omega_subdist by presburger
  thus "x⇧^ω + x⇧^⋆ ⋅ y⇧^ω ≤ (x + y)⇧^ω"
    by (metis local.join.sup_idem star_omega_1)
qed

text ‹The following theorem by Bachmair and
Dershowitz~\<^cite>‹"bachmair86commutation"› is a corollary.›

lemma bachmair_dershowitz:
  assumes "y ⋅ x ≤ x ⋅ (x + y)⇧^⋆"
  shows "(x + y)⇧^ω = 0 ⟷ x⇧^ω + y⇧^ω = 0"
  by (metis add_commute assms local.annir local.join.le_bot local.no_trivial_inverse omega_subdist omega_sum_refine)

text ‹
The next lemmas consider an abstract variant of the empty word
property from language theory and match it with the absence of
infinite iteration~\<^cite>‹"struth12regeq"›.
›

definition (in dioid_one_zero) ewp
where "ewp x ≡ ¬(∀y. y ≤ x ⋅ y ⟶ y = 0)"

lemma ewp_super_id1: "0 ≠ 1 ⟹ 1 ≤ x ⟹ ewp x"
  by (metis ewp_def mult_oner)

lemma "0 ≠ 1 ⟹ 1 ≤ x ⟷ ewp x"
  (* nitpick [expect=genuine] -- "3-element counterexample" *)
oops

text ‹The next facts relate the absence of the empty word property
with the absence of infinite iteration.›

lemma ewp_neg_and_omega: "¬ ewp x ⟷ x⇧^ω = 0"
proof
  assume "¬ ewp x"
  hence "∀ y. y ≤ x ⋅ y ⟶ y = 0"
    by (meson ewp_def)
  thus "x⇧^ω = 0"
    by simp
next
  assume "x⇧^ω = 0"
  hence "∀ y. y ≤ x ⋅ y ⟶ y = 0"
    using local.join.le_bot local.omega_coinduct_var2 by blast
  thus "¬ ewp x"
    by (meson ewp_def)
qed

lemma ewp_alt1: "(∀z. x⇧^ω ≤ x⇧^⋆ ⋅ z) ⟷ (∀y z. y ≤ x ⋅ y + z ⟶ y ≤ x⇧^⋆ ⋅ z)"
  by (metis add_comm less_eq_def omega_coinduct omega_unfold_eq order_prop)

lemma ewp_alt: "x⇧^ω = 0 ⟷ (∀y z. y ≤ x ⋅ y + z ⟶ y ≤ x⇧^⋆ ⋅ z)"
  by (metis annir order.antisym ewp_alt1 join.bot_least)

text ‹So we have obtained a condition for Arden's lemma in omega
algebra.›

lemma omega_super_id1: "0 ≠ 1 ⟹ 1 ≤ x ⟹ x⇧^ω ≠ 0"
  using ewp_neg_and_omega ewp_super_id1 by blast

lemma omega_super_id2: "0 ≠ 1 ⟹ x⇧^ω = 0 ⟹ ¬(1 ≤ x)"
  using omega_super_id1 by blast

text ‹The next lemmas are abstract versions of Arden's lemma from
language theory.›

lemma ardens_lemma_var:
  assumes "x⇧^ω = 0" 
  and "z + x ⋅ y = y"
  shows "x⇧^⋆ ⋅ z = y"
proof -
  have "y ≤ x⇧^ω + x⇧^⋆ ⋅ z"
    by (simp add: assms(2) local.omega_coinduct_eq)
  hence "y ≤ x⇧^⋆ ⋅ z"
    by (simp add: assms(1))
  thus "x⇧^⋆ ⋅ z = y"
    by (simp add: assms(2) order.eq_iff local.star_inductl_eq)
qed

lemma ardens_lemma: "¬ ewp x ⟹ z + x ⋅ y = y ⟹ x⇧^⋆ ⋅ z = y"
  by (simp add: ardens_lemma_var ewp_neg_and_omega)

lemma ardens_lemma_equiv:
  assumes "¬ ewp x"
  shows "z + x ⋅ y = y ⟷ x⇧^⋆ ⋅ z = y"
  by (metis ardens_lemma_var assms ewp_neg_and_omega local.conway.dagger_unfoldl_distr mult_assoc)

lemma ardens_lemma_var_equiv: "x⇧^ω = 0 ⟹ (z + x ⋅ y = y ⟷ x⇧^⋆ ⋅ z = y)"
  by (simp add: ardens_lemma_equiv ewp_neg_and_omega)

lemma arden_conv1: "(∀y z. z + x ⋅ y = y ⟶ x⇧^⋆ ⋅ z = y) ⟹ ¬ ewp x"
  by (metis add_zero_l annir ewp_neg_and_omega omega_unfold_eq)

lemma arden_conv2: "(∀y z. z + x ⋅ y = y ⟶ x⇧^⋆ ⋅ z = y) ⟹ x⇧^ω = 0"
  using arden_conv1 ewp_neg_and_omega by blast

lemma arden_var3: "(∀y z. z + x ⋅ y = y ⟶ x⇧^⋆ ⋅ z = y) ⟷ x⇧^ω = 0"
  using arden_conv2 ardens_lemma_var by blast

end

subsection ‹Omega Algebras›

class omega_algebra = kleene_algebra + left_omega_algebra

end