# Theory Action_Algebra

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

theory Action_Algebra
imports "../Residuated_Lattices/Residuated_Lattices" Kleene_Algebra.Kleene_Algebra
begin

text ‹Action algebras have been defined and discussed in œ
Pratt's paper on \emph{Action Logic and Pure
Induction}~\<^cite>‹"pratt90action"›. They are expansions of Kleene
algebras by operations of left and right residuation. They are
interesting, first because most models of Kleene algebras, e.g.
relations, traces, paths and languages, possess the residuated
structure, and second because, in this setting, the Kleene star can be
defined equationally.

Action algebras can be based on residuated
semilattices. Many important properties of action
algebras already arise at this level.›

text ‹We can define an action algebra as a residuated join
semilattice that is also a dioid. Following Pratt, we also add a star
operation that is axiomatised as a reflexive transitive closure
operation.
›

class action_algebra = residuated_sup_lgroupoid + dioid_one_zero + star_op +
assumes star_rtc1: "1 + x⇧⋆ ⋅ x⇧⋆ + x ≤ x⇧⋆"
and star_rtc2: "1 + y ⋅ y + x ≤ y ⟹ x⇧⋆ ≤ y"
begin

lemma plus_sup: "(+) = (⊔)"
by (rule ext)+ (simp add: local.join.sup_unique)

text ‹We first prove a reflexivity property for residuals.›

lemma residual_r_refl: "1 ≤ x → x"

lemma residual_l_refl: "1 ≤ x ← x"

text ‹We now derive pure induction laws for residuals.›

lemma residual_l_pure_induction: "(x ← x)⇧⋆ ≤ x ← x"
proof -
have "1 + (x ← x) ⋅ (x ← x) + (x ← x) ≤ (x ← x)"
using local.resl_antitoner local.resl_galois mult_assoc by auto
thus ?thesis
by (fact star_rtc2)
qed

lemma residual_r_pure_induction: "(x → x)⇧⋆ ≤ x → x"
proof -
have "1 + (x → x) ⋅ (x → x) + (x → x) ≤ (x → x)"
using local.resr_antitonel local.resr_galois mult_assoc apply clarsimp
by (metis local.mult_oner residual_r_refl)
thus ?thesis
by (fact star_rtc2)
qed

text ‹Next we show that every action algebra is a Kleene
algebra. First, we derive the star unfold law and the star induction
laws in action algebra. Then we prove a subclass statement.›

lemma star_unfoldl: "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
proof -
have "x ⋅ x⇧⋆ ≤ x⇧⋆"
by (meson local.dual_order.trans local.join.le_sup_iff local.mult_isor local.star_rtc1)
thus ?thesis
using local.star_rtc1 by auto
qed

lemma star_mon [intro]: "x ≤ y ⟹ x⇧⋆ ≤ y⇧⋆"
proof -
assume "x ≤ y"
hence "x ≤ y⇧⋆"
by (meson local.dual_order.trans local.join.le_supE local.star_rtc1)
hence "1 + x + y⇧⋆ ⋅ y⇧⋆ ≤ y⇧⋆"
using local.star_rtc1 by auto
thus "x⇧⋆ ≤ y⇧⋆"
qed

lemma star_subdist': "x⇧⋆ ≤ (x + y)⇧⋆"
by force

lemma star_inductl: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
proof -
assume hyp: "z + x ⋅ y ≤ y"
hence "x ≤ y ← y"
hence "x⇧⋆ ≤ (y ← y)⇧⋆"
by (fact star_mon)
hence "x⇧⋆ ≤ y ← y"
using local.order_trans residual_l_pure_induction by blast
hence "x⇧⋆ ⋅ y ≤ y"
thus "x⇧⋆ ⋅ z ≤ y"
by (meson hyp local.dual_order.trans local.join.le_supE local.mult_isol)
qed

lemma star_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
proof -
assume hyp: "z + y ⋅ x ≤ y"
hence "x ≤ y → y"
hence "x⇧⋆ ≤ (y → y)⇧⋆"
by (fact star_mon)
hence "x⇧⋆ ≤ y → y"
by (metis order_trans residual_r_pure_induction)
hence "y ⋅ x⇧⋆ ≤ y"
thus "z ⋅ x⇧⋆ ≤ y"
by (meson hyp local.join.le_supE local.order_trans local.resl_galois)
qed

subclass kleene_algebra
proof
fix x y z
show "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
using local.star_unfoldl by blast
show "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
show "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
qed

end (* action_algebra *)

subsection ‹Equational Action Algebras›

text ‹The induction axioms of Kleene algebras are universal Horn
formulas. This is unavoidable, because due to a well known result of
Redko, there is no finite equational axiomatisation for the equational
theory of regular expressions.

Action algebras, in contrast, admit a finite equational
axiomatization, as Pratt has shown. We now formalise this
result. Consequently, the equational action algebra axioms, which
imply those based on Galois connections, which in turn imply those of
Kleene algebras, are complete with respect to the equational theory of
regular expressions. However, this completeness result does not
account for residuation.›

class equational_action_algebra = residuated_sup_lgroupoid + dioid_one_zero + star_op +
assumes star_ax: "1 + x⇧⋆ ⋅ x⇧⋆ + x ≤ x⇧⋆"
and star_subdist: "x⇧⋆ ≤ (x + y)⇧⋆"
and right_pure_induction: "(x → x)⇧⋆ ≤ x → x"
begin

text ‹We now show that the equational axioms of action algebra
satisfy those based on the Galois connections. Since we can use our
correspondence between the two variants of residuated semilattice, it
remains to derive the second reflexive transitive closure axiom for
the star, essentially copying Pratt's proof step by step. We then
prove a subclass statement.›

lemma star_rtc_2: "1 + y ⋅ y + x ≤ y ⟹ x⇧⋆ ≤ y"
proof -
assume "1 + y ⋅ y + x ≤ y"
hence "1 ≤ y" and "x ≤ y" and "y ⋅ y ≤ y"
by auto
hence "y ≤ y → y" and "x ≤ y → y"
using local.order_trans by blast+
hence "x⇧⋆ ≤ (y → y)⇧⋆"
by (metis local.join.sup.absorb2 local.star_subdist)
hence "x⇧⋆ ≤ y → y"
by (metis order_trans right_pure_induction)
hence "y ⋅ x⇧⋆ ≤ y"
thus "x⇧⋆ ≤ y"
by (metis ‹1 ≤ y› local.dual_order.trans local.mult_onel local.resl_galois)
qed

subclass action_algebra
by (unfold_locales, metis star_ax, metis star_rtc_2)

end (* equational_action_algebra *)

text ‹
Conversely, every action algebra satisfies the equational axioms of
equational action algebras.

Because the subclass relation must be acyclic in Isabelle, we can only
establish this for the corresponding locales. Again this proof is
based on the residuated semilattice result.
›

sublocale action_algebra ⊆ equational_action_algebra
by (unfold_locales, metis star_rtc1, metis star_subdist, metis residual_r_pure_induction)

subsection ‹Another Variant›

text ‹Finally we show that Pratt and Kozen's star axioms generate
precisely the same theory.›

class action_algebra_var = residuated_sup_lgroupoid + dioid_one_zero + star_op +
assumes star_unfold': "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
and star_inductl': "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
and star_inductr': "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆  ≤ y"
begin

subclass kleene_algebra
by (unfold_locales, metis star_unfold', metis star_inductl', metis star_inductr')

subclass action_algebra