Theory Kleene_Algebra_Models
section ‹Models of Kleene Algebras›
theory Kleene_Algebra_Models
imports Kleene_Algebra Dioid_Models
begin
text ‹We now show that most of the models considered for dioids are
also Kleene algebras. Some of the dioid models cannot be expanded, for
instance max-plus and min-plus semirings, but we do not formalise this
fact. We also currently do not show that formal powerseries and
matrices form Kleene algebras.
The interpretation proofs for some of the following models are quite
similar. One could, perhaps, abstract out common reasoning in the
future.›
subsection ‹Preliminary Lemmas›
text ‹We first prove two induction-style statements for dioids that
are useful for establishing the full induction laws. In the future
these will live in a theory file on finite sums for Kleene
algebras.›
context dioid_one_zero
begin
lemma power_inductl: "z + x ⋅ y ≤ y ⟹ (x ^ n) ⋅ z ≤ y"
proof (induct n)
case 0 show ?case
using "0.prems" by auto
case Suc thus ?case
by (auto, metis mult.assoc mult_isol order_trans)
qed
lemma power_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ (x ^ n) ≤ y"
proof (induct n)
case 0 show ?case
using "0.prems" by auto
case Suc
{
fix n
assume "z + y ⋅ x ≤ y ⟹ z ⋅ x ^ n ≤ y"
and "z + y ⋅ x ≤ y"
hence "z ⋅ x ^ n ≤ y"
by auto
also have "z ⋅ x ^ Suc n = z ⋅ x ⋅ x ^ n"
by (metis mult.assoc power_Suc)
moreover have "... = (z ⋅ x ^ n) ⋅ x"
by (metis mult.assoc power_commutes)
moreover have "... ≤ y ⋅ x"
by (metis calculation(1) mult_isor)
moreover have "... ≤ y"
using ‹z + y ⋅ x ≤ y› by auto
ultimately have "z ⋅ x ^ Suc n ≤ y" by auto
}
thus ?case
by (metis Suc)
qed
end
subsection ‹The Powerset Kleene Algebra over a Monoid›
text ‹We now show that the powerset dioid forms a Kleene
algebra. The Kleene star is defined as in language theory.›
lemma Un_0_Suc: "(⋃n. f n) = f 0 ∪ (⋃n. f (Suc n))"
by auto (metis not0_implies_Suc)
instantiation set :: (monoid_mult) kleene_algebra
begin
definition star_def: "X⇧⋆ = (⋃n. X ^ n)"
lemma star_elim: "x ∈ X⇧⋆ ⟷ (∃k. x ∈ X ^ k)"
by (simp add: star_def)
lemma star_contl: "X ⋅ Y⇧⋆ = (⋃n. X ⋅ Y ^ n)"
by (auto simp add: star_elim c_prod_def)
lemma star_contr: "X⇧⋆ ⋅ Y = (⋃n. X ^ n ⋅ Y)"
by (auto simp add: star_elim c_prod_def)
instance
proof
fix X Y Z :: "'a set"
show "1 + X ⋅ X⇧⋆ ⊆ X⇧⋆"
proof -
have "1 + X ⋅ X⇧⋆ = (X ^ 0) ∪ (⋃n. X ^ (Suc n))"
by (auto simp add: star_def c_prod_def plus_set_def one_set_def)
also have "... = (⋃n. X ^ n)"
by (metis Un_0_Suc)
also have "... = X⇧⋆"
by (simp only: star_def)
finally show ?thesis
by (metis subset_refl)
qed
next
fix X Y Z :: "'a set"
assume hyp: "Z + X ⋅ Y ⊆ Y"
show "X⇧⋆ ⋅ Z ⊆ Y"
by (simp add: star_contr SUP_le_iff) (meson hyp dioid_one_zero_class.power_inductl)
next
fix X Y Z :: "'a set"
assume hyp: "Z + Y ⋅ X ⊆ Y"
show "Z ⋅ X⇧⋆ ⊆ Y"
by (simp add: star_contl SUP_le_iff) (meson dioid_one_zero_class.power_inductr hyp)
qed
end
subsection ‹Language Kleene Algebras›
text ‹We now specialise this fact to languages.›
interpretation lan_kleene_algebra: kleene_algebra "(+)" "(⋅)" "1::'a lan" "0" "(⊆)" "(⊂)" star ..
subsection ‹Regular Languages›
text ‹{\ldots} and further to regular languages. For the sake of
simplicity we just copy in the axiomatisation of regular expressions
by Krauss and Nipkow~\<^cite>‹"krauss12regular"›.›