Theory Kleene_Algebra.Dioid_Models
section ‹Models of Dioids›
theory Dioid_Models
imports Dioid HOL.Real
begin
text ‹In this section we consider some well known models of
dioids. These so far include the powerset dioid over a monoid,
languages, binary relations, sets of traces, sets paths (in a graph),
as well as the min-plus and the max-plus semirings. Most of these
models are taken from an article about Kleene algebras with
domain~\<^cite>‹"desharnaismoellerstruth06kad"›.
The advantage of formally linking these models with the abstract
axiomatisations of dioids is that all abstract theorems are
automatically available in all models. It therefore makes sense to
establish models for the strongest possible axiomatisations (whereas
theorems should be proved for the weakest ones).›
subsection ‹The Powerset Dioid over a Monoid›
text ‹We assume a multiplicative monoid and define the usual complex
product on sets of elements. We formalise the well known result that
this lifting induces a dioid.›
instantiation set :: (monoid_mult) monoid_mult
begin
definition one_set_def:
"1 = {1}"
definition c_prod_def:
"A ⋅ B = {u * v | u v. u ∈ A ∧ v ∈ B}"
instance
proof
fix X Y Z :: "'a set"
show "X ⋅ Y ⋅ Z = X ⋅ (Y ⋅ Z)"
by (auto simp add: c_prod_def) (metis mult.assoc)+
show "1 ⋅ X = X"
by (simp add: one_set_def c_prod_def)
show "X ⋅ 1 = X"
by (simp add: one_set_def c_prod_def)
qed
end
instantiation set :: (monoid_mult) dioid_one_zero
begin
definition zero_set_def:
"0 = {}"
definition plus_set_def:
"A + B = A ∪ B"
instance
proof
fix X Y Z :: "'a set"
show "X + Y + Z = X + (Y + Z)"
by (simp add: Un_assoc plus_set_def)
show "X + Y = Y + X"
by (simp add: Un_commute plus_set_def)
show "(X + Y) ⋅ Z = X ⋅ Z + Y ⋅ Z"
by (auto simp add: plus_set_def c_prod_def)
show "1 ⋅ X = X"
by (simp add: one_set_def c_prod_def)
show "X ⋅ 1 = X"
by (simp add: one_set_def c_prod_def)
show "0 + X = X"
by (simp add: plus_set_def zero_set_def)
show "0 ⋅ X = 0"
by (simp add: c_prod_def zero_set_def)
show "X ⋅ 0 = 0"
by (simp add: c_prod_def zero_set_def)
show "X ⊆ Y ⟷ X + Y = Y"
by (simp add: plus_set_def subset_Un_eq)
show "X ⊂ Y ⟷ X ⊆ Y ∧ X ≠ Y"
by (fact psubset_eq)
show "X + X = X"
by (simp add: Un_absorb plus_set_def)
show "X ⋅ (Y + Z) = X ⋅ Y + X ⋅ Z"
by (auto simp add: plus_set_def c_prod_def)
qed
end
subsection ‹Language Dioids›
text ‹Language dioids arise as special cases of the monoidal lifting
because sets of words form free monoids. Moreover, monoids of words
are isomorphic to monoids of lists under append.
To show that languages form dioids it therefore suffices to show that
sets of lists closed under append and multiplication with the empty
word form a (multiplicative) monoid. Isabelle then does the rest of the work
automatically. Infix~‹@› denotes word
concatenation.›
instantiation list :: (type) monoid_mult
begin
definition times_list_def:
"xs * ys ≡ xs @ ys"
definition one_list_def:
"1 ≡ []"
instance proof
fix xs ys zs :: "'a list"
show "xs * ys * zs = xs * (ys * zs)"
by (simp add: times_list_def)
show "1 * xs = xs"
by (simp add: one_list_def times_list_def)
show "xs * 1 = xs"
by (simp add: one_list_def times_list_def)
qed
end
text ‹Languages as sets of lists have already been formalised in
Isabelle in various places. We can now obtain much of their algebra
for free.›
type_synonym 'a lan = "'a list set"
interpretation lan_dioid: dioid_one_zero "(+)" "(⋅)" "1::'a lan" "0" "(⊆)" "(⊂)" ..
subsection ‹Relation Dioids›
text ‹We now show that binary relations under union, relational
composition, the identity relation, the empty relation and set
inclusion form dioids. Due to the well developed relation library of
Isabelle this is entirely trivial.›