(* 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" 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 (* 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" 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 (* 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 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