Theory Action_Algebra
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"
by (simp add: local.resrI)
lemma residual_l_refl: "1 ≤ x ← x"
by (simp add: local.reslI)
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⇧⋆"
by (simp add: local.star_rtc2)
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"
by (simp add: local.resl_galois)
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"
by (simp add: local.resl_galois)
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"
by (simp add: resr_galois)
hence "x⇧⋆ ≤ (y → y)⇧⋆"
by (fact star_mon)
hence "x⇧⋆ ≤ y → y"
by (metis order_trans residual_r_pure_induction)
hence "y ⋅ x⇧⋆ ≤ y"
by (simp add: local.resr_galois)
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"
by (simp add: local.star_inductl)
show "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
by (simp add: star_inductr)
qed
end
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"
by (simp add: local.resr_galois)
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
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
by (unfold_locales, metis add.commute less_eq_def order_refl star_ext star_plus_one star_trans_eq, metis add.assoc add.commute star_rtc_least)
end
sublocale action_algebra ⊆ action_algebra_var
by (unfold_locales, metis star_unfoldl, metis star_inductl, metis star_inductr)
end