Theory Signatures
section ‹Signatures›
theory Signatures
imports Main
begin
text ‹
Default notation in Isabelle/HOL is occasionally different from
established notation in the relation/algebra community. We use the
latter where possible.
›
notation
times (infixl "⋅" 70)
text ‹
Some classes in our algebraic hierarchy are most naturally defined as
subclasses of two (or more) superclasses that impose different
restrictions on the same parameter(s).
Alas, in Isabelle/HOL, a class cannot have multiple superclasses that
independently declare the same parameter(s). One workaround, which
motivated the following syntactic classes, is to shift the parameter
declaration to a common superclass.
›
class star_op =
fixes star :: "'a ⇒ 'a" ("_⇧⋆" [101] 100)
class omega_op =
fixes omega :: "'a ⇒ 'a" ("_⇧ω" [101] 100)
text ‹
We define a type class that combines addition and the definition of
order in, e.g., semilattices. This class makes the definition of
various other type classes more slick.
›
class plus_ord = plus + ord +
assumes less_eq_def: "x ≤ y ⟷ x + y = y"
and less_def: "x < y ⟷ x ≤ y ∧ x ≠ y"
end
Theory Dioid
section ‹Dioids›
theory Dioid
imports Signatures
begin
subsection ‹Join Semilattices›
text ‹Join semilattices can be axiomatised order-theoretically or
algebraically. A join semilattice (or upper semilattice) is either a
poset in which every pair of elements has a join (or least upper
bound), or a set endowed with an associative, commutative, idempotent
binary operation. It is well known that the order-theoretic definition
induces the algebraic one and vice versa. We start from the algebraic
axiomatisation because it is easily expandable to dioids, using
Isabelle's type class mechanism.
In Isabelle/HOL, a type class @{class semilattice_sup} is available.
Alas, we cannot use this type class because we need the symbol~‹+› for the join operation in the dioid expansion and subclass
proofs in Isabelle/HOL require the two type classes involved to have
the same fixed signature.
Using {\em add\_assoc} as a name for the first assumption in class
{\em join\_semilattice} would lead to name clashes: we will later
define classes that inherit from @{class semigroup_add}, which
provides its own assumption {\em add\_assoc}, and prove that these are
subclasses of {\em join\_semilattice}. Hence the primed name.
›
class join_semilattice = plus_ord +
assumes add_assoc' [ac_simps]: "(x + y) + z = x + (y + z)"
and add_comm [ac_simps] : "x + y = y + x"
and add_idem [simp]: "x + x = x"
begin
lemma add_left_comm [ac_simps]: "y + (x + z) = x + (y + z)"
using local.add_assoc' local.add_comm by auto
lemma add_left_idem [ac_simps]: "x + (x + y) = x + y"
unfolding add_assoc' [symmetric] by simp
text ‹The definition @{term "x ≤ y ⟷ x + y = y"} of the order is
hidden in class @{class plus_ord}.
We show some simple order-based properties of semilattices. The
first one states that every semilattice is a partial order.›
subclass order
proof
fix x y z :: 'a
show "x < y ⟷ x ≤ y ∧ ¬ y ≤ x"
using local.add_comm local.less_def local.less_eq_def by force
show "x ≤ x"
by (simp add: local.less_eq_def)
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
by (metis add_assoc' less_eq_def)
show "x ≤ y ⟹ y ≤ x ⟹ x = y"
by (simp add: local.add_comm local.less_eq_def)
qed
text ‹Next we show that joins are least upper bounds.›
sublocale join: semilattice_sup "(+)"
by (unfold_locales; simp add: ac_simps local.less_eq_def)
text ‹Next we prove that joins are isotone (order preserving).›
lemma add_iso: "x ≤ y ⟹ x + z ≤ y + z"
using join.sup_mono by blast
text ‹
The next lemma links the definition of order as @{term "x ≤ y ⟷ x + y = y"}
with a perhaps more conventional one known, e.g., from arithmetics.
›
lemma order_prop: "x ≤ y ⟷ (∃z. x + z = y)"
proof
assume "x ≤ y"
hence "x + y = y"
by (simp add: less_eq_def)
thus "∃z. x + z = y"
by auto
next
assume "∃z. x + z = y"
then obtain c where "x + c = y"
by auto
hence "x + c ≤ y"
by simp
thus "x ≤ y"
by simp
qed
end
subsection ‹Join Semilattices with an Additive Unit›
text ‹We now expand join semilattices by an additive unit~$0$. Is
the least element with respect to the order, and therefore often
denoted by~‹⊥›. Semilattices with a least element are often
called \emph{bounded}.›
class join_semilattice_zero = join_semilattice + zero +
assumes add_zero_l [simp]: "0 + x = x"
begin
subclass comm_monoid_add
by (unfold_locales, simp_all add: add_assoc') (simp add: add_comm)
sublocale join: bounded_semilattice_sup_bot "(+)" "(≤)" "(<)" 0
by unfold_locales (simp add: local.order_prop)
lemma no_trivial_inverse: "x ≠ 0 ⟹ ¬(∃y. x + y = 0)"
by (metis local.add_0_right local.join.sup_left_idem)
end
subsection ‹Near Semirings›
text ‹\emph{Near semirings} (also called seminearrings) are
generalisations of near rings to the semiring case. They have been
studied, for instance, in G.~Pilz's book~\cite{pilz83nearrings} on
near rings. According to his definition, a near semiring consists of
an additive and a multiplicative semigroup that interact via a single
distributivity law (left or right). The additive semigroup is not
required to be commutative. The definition is influenced by partial
transformation semigroups.
We only consider near semirings in which addition is commutative, and
in which the right distributivity law holds. We call such near
semirings \emph{abelian}.›
class ab_near_semiring = ab_semigroup_add + semigroup_mult +
assumes distrib_right' [simp]: "(x + y) ⋅ z = x ⋅ z + y ⋅ z"
subclass (in semiring) ab_near_semiring
by (unfold_locales, metis distrib_right)
class ab_pre_semiring = ab_near_semiring +
assumes subdistl_eq: "z ⋅ x + z ⋅ (x + y) = z ⋅ (x + y)"
subsection ‹Variants of Dioids›
text ‹A \emph{near dioid} is an abelian near semiring in which
addition is idempotent. This generalises the notion of (additively)
idempotent semirings by dropping one distributivity law. Near dioids
are a starting point for process algebras.
By modelling variants of dioids as variants of semirings in which
addition is idempotent we follow the tradition of
Birkhoff~\cite{birkhoff67lattices}, but deviate from the definitions
in Gondran and Minoux's book~\cite{gondran10graphs}.›
class near_dioid = ab_near_semiring + plus_ord +
assumes add_idem' [simp]: "x + x = x"
begin
text ‹Since addition is idempotent, the additive (commutative)
semigroup reduct of a near dioid is a semilattice. Near dioids are
therefore ordered by the semilattice order.›
subclass join_semilattice
by unfold_locales (auto simp add: add.commute add.left_commute)
text ‹It follows that multiplication is right-isotone (but not
necessarily left-isotone).›
lemma mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
proof -
assume "x ≤ y"
hence "x + y = y"
by (simp add: less_eq_def)
hence "(x + y) ⋅ z = y ⋅ z"
by simp
thus "x ⋅ z ≤ y ⋅ z"
by (simp add: less_eq_def)
qed
lemma "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
oops
text ‹The next lemma states that, in every near dioid, left
isotonicity and left subdistributivity are equivalent.›
lemma mult_isol_equiv_subdistl:
"(∀x y z. x ≤ y ⟶ z ⋅ x ≤ z ⋅ y) ⟷ (∀x y z. z ⋅ x ≤ z ⋅ (x + y))"
by (metis local.join.sup_absorb2 local.join.sup_ge1)
text ‹The following lemma is relevant to propositional Hoare logic.›
lemma phl_cons1: "x ≤ w ⟹ w ⋅ y ≤ y ⋅ z ⟹ x ⋅ y ≤ y ⋅ z"
using dual_order.trans mult_isor by blast
end
text ‹We now make multiplication in near dioids left isotone, which
is equivalent to left subdistributivity, as we have seen. The
corresponding structures form the basis of probabilistic Kleene
algebras~\cite{mciverweber05pka} and game
algebras~\cite{venema03gamealgebra}. We are not aware that these
structures have a special name, so we baptise them \emph{pre-dioids}.
We do not explicitly define pre-semirings since we have no application
for them.›
class pre_dioid = near_dioid +
assumes subdistl: "z ⋅ x ≤ z ⋅ (x + y)"
begin
text ‹Now, obviously, left isotonicity follows from left subdistributivity.›
lemma subdistl_var: "z ⋅ x + z ⋅ y ≤ z ⋅ (x + y)"
using local.mult_isol_equiv_subdistl local.subdistl by auto
subclass ab_pre_semiring
apply unfold_locales
by (simp add: local.join.sup_absorb2 local.subdistl)
lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
proof -
assume "x ≤ y"
hence "x + y = y"
by (simp add: less_eq_def)
also have "z ⋅ x + z ⋅ y ≤ z ⋅ (x + y)"
using subdistl_var by blast
moreover have "... = z ⋅ y"
by (simp add: calculation)
ultimately show "z ⋅ x ≤ z ⋅ y"
by auto
qed
lemma mult_isol_var: "u ≤ x ⟹ v ≤ y ⟹ u ⋅ v ≤ x ⋅ y"
by (meson local.dual_order.trans local.mult_isor mult_isol)
lemma mult_double_iso: "x ≤ y ⟹ w ⋅ x ⋅ z ≤ w ⋅ y ⋅ z"
by (simp add: local.mult_isor mult_isol)
text ‹The following lemmas are relevant to propositional Hoare logic.›
lemma phl_cons2: "w ≤ x ⟹ z ⋅ y ≤ y ⋅ w ⟹ z ⋅ y ≤ y ⋅ x"
using local.order_trans mult_isol by blast
lemma phl_seq:
assumes "p ⋅ x ≤ x ⋅ r"
and "r ⋅ y ≤ y ⋅ q"
shows "p ⋅ (x ⋅ y) ≤ x ⋅ y ⋅ q"
proof -
have "p ⋅ x ⋅ y ≤ x ⋅ r ⋅ y"
using assms(1) mult_isor by blast
thus ?thesis
by (metis assms(2) order_prop order_trans subdistl mult_assoc)
qed
lemma phl_cond:
assumes "u ⋅ v ≤ v ⋅ u ⋅ v" and "u ⋅ w ≤ w ⋅ u ⋅ w"
and "⋀x y. u ⋅ (x + y) ≤ u ⋅ x + u ⋅ y"
and "u ⋅ v ⋅ x ≤ x ⋅ z" and "u ⋅ w ⋅ y ≤ y ⋅ z"
shows "u ⋅ (v ⋅ x + w ⋅ y) ≤ (v ⋅ x + w ⋅ y) ⋅ z"
proof -
have a: "u ⋅ v ⋅ x ≤ v ⋅ x ⋅ z" and b: "u ⋅ w ⋅ y ≤ w ⋅ y ⋅ z"
by (metis assms mult_assoc phl_seq)+
have "u ⋅ (v ⋅ x + w ⋅ y) ≤ u ⋅ v ⋅ x + u ⋅ w ⋅ y"
using assms(3) mult_assoc by auto
also have "... ≤ v ⋅ x ⋅ z + w ⋅ y ⋅ z"
using a b join.sup_mono by blast
finally show ?thesis
by simp
qed
lemma phl_export1:
assumes "x ⋅ y ≤ y ⋅ x ⋅ y"
and "(x ⋅ y) ⋅ z ≤ z ⋅ w"
shows "x ⋅ (y ⋅ z) ≤ (y ⋅ z) ⋅ w"
proof -
have "x ⋅ y ⋅ z ≤ y ⋅ x ⋅ y ⋅ z"
by (simp add: assms(1) mult_isor)
thus ?thesis
using assms(1) assms(2) mult_assoc phl_seq by auto
qed
lemma phl_export2:
assumes "z ⋅ w ≤ w ⋅ z ⋅ w"
and "x ⋅ y ≤ y ⋅ z"
shows "x ⋅ (y ⋅ w) ≤ y ⋅ w ⋅ (z ⋅ w)"
proof -
have "x ⋅ y ⋅ w ≤ y ⋅ z ⋅ w"
using assms(2) mult_isor by blast
thus ?thesis
by (metis assms(1) dual_order.trans order_prop subdistl mult_assoc)
qed
end
text ‹By adding a full left distributivity law we obtain semirings
(which are already available in Isabelle/HOL as @{class semiring})
from near semirings, and dioids from near dioids. Dioids are therefore
idempotent semirings.›
class dioid = near_dioid + semiring
subclass (in dioid) pre_dioid
by unfold_locales (simp add: local.distrib_left)
subsection ‹Families of Nearsemirings with a Multiplicative Unit›
text ‹Multiplicative units are important, for instance, for defining
an operation of finite iteration or Kleene star on dioids. We do not
introduce left and right units separately since we have no application
for this.›
class ab_near_semiring_one = ab_near_semiring + one +
assumes mult_onel [simp]: "1 ⋅ x = x"
and mult_oner [simp]: "x ⋅ 1 = x"
begin
subclass monoid_mult
by (unfold_locales, simp_all)
end
class ab_pre_semiring_one = ab_near_semiring_one + ab_pre_semiring
class near_dioid_one = near_dioid + ab_near_semiring_one
begin
text ‹The following lemma is relevant to propositional Hoare logic.›
lemma phl_skip: "x ⋅ 1 ≤ 1 ⋅ x"
by simp
end
text ‹For near dioids with one, it would be sufficient to require
$1+1=1$. This implies @{term "x+x=x"} for arbitray~@{term x} (but that
would lead to annoying redundant proof obligations in mutual
subclasses of @{class near_dioid_one} and @{class near_dioid} later).
›
class pre_dioid_one = pre_dioid + near_dioid_one
class dioid_one = dioid + near_dioid_one
subclass (in dioid_one) pre_dioid_one ..
subsection ‹Families of Nearsemirings with Additive Units›
text ‹
We now axiomatise an additive unit~$0$ for nearsemirings. The zero is
usually required to satisfy annihilation properties with respect to
multiplication. Due to applications we distinguish a zero which is
only a left annihilator from one that is also a right annihilator.
More briefly, we call zero either a left unit or a unit.
Semirings and dioids with a right zero only can be obtained from those
with a left unit by duality.
›
class ab_near_semiring_one_zerol = ab_near_semiring_one + zero +
assumes add_zerol [simp]: "0 + x = x"
and annil [simp]: "0 ⋅ x = 0"
begin
text ‹Note that we do not require~$0 \neq 1$.›
lemma add_zeror [simp]: "x + 0 = x"
by (subst add_commute) simp
end
class ab_pre_semiring_one_zerol = ab_near_semiring_one_zerol + ab_pre_semiring
begin
text ‹The following lemma shows that there is no point defining pre-semirings separately from dioids.›
lemma "1 + 1 = 1"
proof -
have "1 + 1 = 1 ⋅ 1 + 1 ⋅ (1 + 0)"
by simp
also have "... = 1 ⋅ (1 + 0)"
using subdistl_eq by presburger
finally show ?thesis
by simp
qed
end
class near_dioid_one_zerol = near_dioid_one + ab_near_semiring_one_zerol
subclass (in near_dioid_one_zerol) join_semilattice_zero
by (unfold_locales, simp)
class pre_dioid_one_zerol = pre_dioid_one + ab_near_semiring_one_zerol
subclass (in pre_dioid_one_zerol) near_dioid_one_zerol ..
class semiring_one_zerol = semiring + ab_near_semiring_one_zerol
class dioid_one_zerol = dioid_one + ab_near_semiring_one_zerol
subclass (in dioid_one_zerol) pre_dioid_one_zerol ..
text ‹We now make zero also a right annihilator.›
class ab_near_semiring_one_zero = ab_near_semiring_one_zerol +
assumes annir [simp]: "x ⋅ 0 = 0"
class semiring_one_zero = semiring + ab_near_semiring_one_zero
class near_dioid_one_zero = near_dioid_one_zerol + ab_near_semiring_one_zero
class pre_dioid_one_zero = pre_dioid_one_zerol + ab_near_semiring_one_zero
subclass (in pre_dioid_one_zero) near_dioid_one_zero ..
class dioid_one_zero = dioid_one_zerol + ab_near_semiring_one_zero
subclass (in dioid_one_zero) pre_dioid_one_zero ..
subclass (in dioid_one_zero) semiring_one_zero ..
subsection ‹Duality by Opposition›
text ‹
Swapping the order of multiplication in a semiring (or dioid) gives
another semiring (or dioid), called its \emph{dual} or
\emph{opposite}.
›
definition (in times) opp_mult (infixl "⊙" 70)
where "x ⊙ y ≡ y ⋅ x"
lemma (in semiring_1) dual_semiring_1:
"class.semiring_1 1 (⊙) (+) 0"
by unfold_locales (auto simp add: opp_mult_def mult.assoc distrib_right distrib_left)
lemma (in dioid_one_zero) dual_dioid_one_zero:
"class.dioid_one_zero (+) (⊙) 1 0 (≤) (<)"
by unfold_locales (auto simp add: opp_mult_def mult.assoc distrib_right distrib_left)
subsection ‹Selective Near Semirings›
text ‹In this section we briefly sketch a generalisation of the
notion of \emph{dioid}. Some important models, e.g. max-plus and
min-plus semirings, have that property.›
class selective_near_semiring = ab_near_semiring + plus_ord +
assumes select: "x + y = x ∨ x + y = y"
begin
lemma select_alt: "x + y ∈ {x,y}"
by (simp add: local.select)
text ‹It follows immediately that every selective near semiring is a near dioid.›
subclass near_dioid
by (unfold_locales, meson select)
text ‹Moreover, the order in a selective near semiring is obviously linear.›
subclass linorder
by (unfold_locales, metis add.commute join.sup.orderI select)
end
class selective_semiring = selective_near_semiring + semiring_one_zero
begin
subclass dioid_one_zero ..
end
end
Theory 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.›
interpretation rel_dioid: dioid_one_zero "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)"
by (unfold_locales, auto)
interpretation rel_monoid: monoid_mult Id "(O)" ..
subsection ‹Trace Dioids›
text ‹Traces have been considered, for instance, by
Kozen~\cite{kozen00hoare} in the context of Kleene algebras with
tests. Intuitively, a trace is an execution sequence of a labelled
transition system from some state to some other state, in which state
labels and action labels alternate, and which begin and end with a
state label.
Traces generalise words: words can be obtained from traces by
forgetting state labels. Similarly, sets of traces generalise
languages.
In this section we show that sets of traces under union, an
appropriately defined notion of complex product, the set of all traces
of length zero, the empty set of traces and set inclusion form a
dioid.
We first define the notion of trace and the product of traces, which
has been called \emph{fusion product} by Kozen.›
type_synonym ('p, 'a) trace = "'p × ('a × 'p) list"
definition first :: "('p, 'a) trace ⇒ 'p" where
"first = fst"
lemma first_conv [simp]: "first (p, xs) = p"
by (unfold first_def, simp)
fun last :: "('p, 'a) trace ⇒ 'p" where
"last (p, []) = p"
| "last (_, xs) = snd (List.last xs)"
lemma last_append [simp]: "last (p, xs @ ys) = last (last (p, xs), ys)"
proof (cases xs)
show "xs = [] ⟹ last (p, xs @ ys) = last (last (p, xs), ys)"
by simp
show "⋀a list. xs = a # list ⟹
last (p, xs @ ys) = last (last (p, xs), ys)"
proof (cases ys)
show "⋀a list. ⟦xs = a # list; ys = []⟧
⟹ last (p, xs @ ys) = last (last (p, xs), ys)"
by simp
show "⋀a list aa lista. ⟦xs = a # list; ys = aa # lista⟧
⟹ last (p, xs @ ys) = last (last (p, xs), ys)"
by simp
qed
qed
text ‹The fusion product is a partial operation. It is undefined if
the last element of the first trace and the first element of the
second trace are different. If these elements are the same, then the
fusion product removes the first element from the second trace and
appends the resulting object to the first trace.›
definition t_fusion :: "('p, 'a) trace ⇒ ('p, 'a) trace ⇒ ('p, 'a) trace" where
"t_fusion x y ≡ if last x = first y then (fst x, snd x @ snd y) else undefined"
text ‹We now show that the first element and the last element of a
trace are a left and right unit for that trace and prove some other
auxiliary lemmas.›
lemma t_fusion_leftneutral [simp]: "t_fusion (first x, []) x = x"
by (cases x, simp add: t_fusion_def)
lemma fusion_rightneutral [simp]: "t_fusion x (last x, []) = x"
by (simp add: t_fusion_def)
lemma first_t_fusion [simp]: "last x = first y ⟹ first (t_fusion x y) = first x"
by (simp add: first_def t_fusion_def)
lemma last_t_fusion [simp]: "last x = first y ⟹ last (t_fusion x y) = last y"
by (simp add: first_def t_fusion_def)
text ‹Next we show that fusion of traces is associative.›
lemma t_fusion_assoc [simp]:
"⟦ last x = first y; last y = first z ⟧ ⟹ t_fusion x (t_fusion y z) = t_fusion (t_fusion x y) z"
by (cases x, cases y, cases z, simp add: t_fusion_def)
subsection ‹Sets of Traces›
text ‹We now lift the fusion product to a complex product on sets of
traces. This operation is total.›
no_notation
times (infixl "⋅" 70)
definition t_prod :: "('p, 'a) trace set ⇒ ('p, 'a) trace set ⇒ ('p, 'a) trace set" (infixl "⋅" 70)
where "X ⋅ Y = {t_fusion u v| u v. u ∈ X ∧ v ∈ Y ∧ last u = first v}"
text ‹Next we define the empty set of traces and the set of traces
of length zero as the multiplicative unit of the trace dioid.›
definition t_zero :: "('p, 'a) trace set" where
"t_zero ≡ {}"
definition t_one :: "('p, 'a) trace set" where
"t_one ≡ ⋃p. {(p, [])}"
text ‹We now provide elimination rules for trace products.›
lemma t_prod_iff:
"w ∈ X⋅Y ⟷ (∃u v. w = t_fusion u v ∧ u ∈ X ∧ v ∈ Y ∧ last u = first v)"
by (unfold t_prod_def) auto
lemma t_prod_intro [simp, intro]:
"⟦ u ∈ X; v ∈ Y; last u = first v ⟧ ⟹ t_fusion u v ∈ X⋅Y"
by (meson t_prod_iff)
lemma t_prod_elim [elim]:
"w ∈ X⋅Y ⟹ ∃u v. w = t_fusion u v ∧ u ∈ X ∧ v ∈ Y ∧ last u = first v"
by (meson t_prod_iff)
text ‹Finally we prove the interpretation statement that sets of traces
under union and the complex product based on trace fusion together
with the empty set of traces and the set of traces of length one forms
a dioid.›
interpretation trace_dioid: dioid_one_zero "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)"
apply unfold_locales
apply (auto simp add: t_prod_def t_one_def t_zero_def t_fusion_def)
apply (metis last_append)
apply (metis last_append append_assoc)
done
no_notation
t_prod (infixl "⋅" 70)
subsection ‹The Path Diod›
text ‹The next model we consider are sets of paths in a graph. We
consider two variants, one that contains the empty path and one that
doesn't. The former leads to more difficult proofs and a more involved
specification of the complex product. We start with paths that include
the empty path. In this setting, a path is a list of nodes.›
subsection ‹Path Models with the Empty Path›
type_synonym 'a path = "'a list"
text ‹Path fusion is defined similarly to trace
fusion. Mathematically it should be a partial operation. The fusion of
two empty paths yields the empty path; the fusion between a non-empty
path and an empty one is undefined; the fusion of two non-empty paths
appends the tail of the second path to the first one.
We need to use a total alternative and make sure that undefined paths
do not contribute to the complex product.›
fun p_fusion :: "'a path ⇒ 'a path ⇒ 'a path" where
"p_fusion [] _ = []"
| "p_fusion _ [] = []"
| "p_fusion ps (q # qs) = ps @ qs"
lemma p_fusion_assoc:
"p_fusion ps (p_fusion qs rs) = p_fusion (p_fusion ps qs) rs"
proof (induct rs)
case Nil show ?case
by (metis p_fusion.elims p_fusion.simps(2))
case Cons show ?case
proof (induct qs)
case Nil show ?case
by (metis neq_Nil_conv p_fusion.simps(1) p_fusion.simps(2))
case Cons show ?case
proof -
have "∀ps. ([] = ps ∨ hd ps # tl ps = ps) ∧ ((∀q qs. q # qs ≠ ps) ∨ [] ≠ ps)"
using list.collapse by fastforce
moreover hence "∀ps q qs. p_fusion ps (q # qs) = ps @ qs ∨ [] = ps"
by (metis p_fusion.simps(3))
ultimately show ?thesis
by (metis (no_types) Cons_eq_appendI append_eq_appendI p_fusion.simps(1) p_fusion.simps(3))
qed
qed
qed
text ‹This lemma overapproximates the real situation, but it holds
in all cases where path fusion should be defined.›
lemma p_fusion_last:
assumes "List.last ps = hd qs"
and "ps ≠ []"
and "qs ≠ []"
shows "List.last (p_fusion ps qs) = List.last qs"
by (metis (hide_lams, no_types) List.last.simps List.last_append append_Nil2 assms list.sel(1) neq_Nil_conv p_fusion.simps(3))
lemma p_fusion_hd: "⟦ps ≠ []; qs ≠ []⟧ ⟹ hd (p_fusion ps qs) = hd ps"
by (metis list.exhaust p_fusion.simps(3) append_Cons list.sel(1))
lemma nonempty_p_fusion: "⟦ps ≠ []; qs ≠ []⟧ ⟹ p_fusion ps qs ≠ []"
by (metis list.exhaust append_Cons p_fusion.simps(3) list.simps(2))
text ‹We now define a condition that filters out undefined paths in
the complex product.›
abbreviation p_filter :: "'a path ⇒ 'a path ⇒ bool" where
"p_filter ps qs ≡ ((ps = [] ∧ qs = []) ∨ (ps ≠ [] ∧ qs ≠ [] ∧ (List.last ps) = hd qs))"
no_notation
times (infixl "⋅" 70)
definition p_prod :: "'a path set ⇒ 'a path set ⇒ 'a path set" (infixl "⋅" 70)
where "X ⋅ Y = {rs . ∃ps ∈ X. ∃qs ∈ Y. rs = p_fusion ps qs ∧ p_filter ps qs}"
lemma p_prod_iff:
"ps ∈ X ⋅ Y ⟷ (∃qs rs. ps = p_fusion qs rs ∧ qs ∈ X ∧ rs ∈ Y ∧ p_filter qs rs)"
by (unfold p_prod_def) auto
text ‹Due to the complexity of the filter condition, proving
properties of complex products can be tedious.›
lemma p_prod_assoc: "(X ⋅ Y) ⋅ Z = X ⋅ (Y ⋅ Z)"
proof (rule set_eqI)
fix ps
show "ps ∈ (X ⋅ Y) ⋅ Z ⟷ ps ∈ X ⋅ (Y ⋅ Z)"
proof (cases ps)
case Nil thus ?thesis
by auto (metis nonempty_p_fusion p_prod_iff)+
next
case Cons thus ?thesis
by (auto simp add: p_prod_iff) (metis (hide_lams, mono_tags) nonempty_p_fusion p_fusion_assoc p_fusion_hd p_fusion_last)+
qed
qed
text ‹We now define the multiplicative unit of the path dioid as the
set of all paths of length one, including the empty path, and show the
unit laws with respect to the path product.›
definition p_one :: "'a path set" where
"p_one ≡ {p . ∃q::'a. p = [q]} ∪ {[]}"
lemma p_prod_onel [simp]: "p_one ⋅ X = X"
proof (rule set_eqI)
fix ps
show "ps ∈ p_one ⋅ X ⟷ ps ∈ X"
proof (cases ps)
case Nil thus ?thesis
by (auto simp add: p_one_def p_prod_def, metis nonempty_p_fusion not_Cons_self)
next
case Cons thus ?thesis
by (auto simp add: p_one_def p_prod_def, metis append_Cons append_Nil list.sel(1) neq_Nil_conv p_fusion.simps(3), metis Cons_eq_appendI list.sel(1) last_ConsL list.simps(3) p_fusion.simps(3) self_append_conv2)
qed
qed
lemma p_prod_oner [simp]: "X ⋅ p_one = X"
proof (rule set_eqI)
fix ps
show "ps ∈ X ⋅ p_one ⟷ ps ∈ X"
proof (cases ps)
case Nil thus ?thesis
by (auto simp add: p_one_def p_prod_def, metis nonempty_p_fusion not_Cons_self2, metis p_fusion.simps(1))
next
case Cons thus ?thesis
by (auto simp add: p_one_def p_prod_def, metis append_Nil2 neq_Nil_conv p_fusion.simps(3), metis list.sel(1) list.simps(2) p_fusion.simps(3) self_append_conv)
qed
qed
text ‹Next we show distributivity laws at the powerset level.›
lemma p_prod_distl: "X ⋅ (Y ∪ Z) = X ⋅ Y ∪ X ⋅ Z"
proof (rule set_eqI)
fix ps
show "ps ∈ X ⋅ (Y ∪ Z) ⟷ ps ∈ X ⋅ Y ∪ X ⋅ Z"
by (cases ps) (auto simp add: p_prod_iff)
qed
lemma p_prod_distr: "(X ∪ Y) ⋅ Z = X ⋅ Z ∪ Y ⋅ Z"
proof (rule set_eqI)
fix ps
show "ps ∈ (X ∪ Y) ⋅ Z ⟷ ps ∈ X ⋅ Z ∪ Y ⋅ Z"
by (cases ps) (auto simp add: p_prod_iff)
qed
text ‹Finally we show that sets of paths under union, the complex
product, the unit set and the empty set form a dioid.›
interpretation path_dioid: dioid_one_zero "(∪)" "(⋅)" p_one "{}" "(⊆)" "(⊂)"
proof
fix x y z :: "'a path set"
show "x ∪ y ∪ z = x ∪ (y ∪ z)"
by auto
show "x ∪ y = y ∪ x"
by auto
show "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
by (fact p_prod_assoc)
show "(x ∪ y) ⋅ z = x ⋅ z ∪ y ⋅ z"
by (fact p_prod_distr)
show "p_one ⋅ x = x"
by (fact p_prod_onel)
show "x ⋅ p_one = x"
by (fact p_prod_oner)
show "{} ∪ x = x"
by auto
show "{} ⋅ x = {}"
by (metis all_not_in_conv p_prod_iff)
show "x ⋅ {} = {}"
by (metis all_not_in_conv p_prod_iff)
show "(x ⊆ y) = (x ∪ y = y)"
by auto
show "(x ⊂ y) = (x ⊆ y ∧ x ≠ y)"
by auto
show "x ∪ x = x"
by auto
show "x ⋅ (y ∪ z) = x ⋅ y ∪ x ⋅ z"
by (fact p_prod_distl)
qed
no_notation
p_prod (infixl "⋅" 70)
subsection ‹Path Models without the Empty Path›
text ‹We now build a model of paths that does not include the empty
path and therefore leads to a simpler complex product.›
datatype 'a ppath = Node 'a | Cons 'a "'a ppath"
primrec pp_first :: "'a ppath ⇒ 'a" where
"pp_first (Node x) = x"
| "pp_first (Cons x _) = x"
primrec pp_last :: "'a ppath ⇒ 'a" where
"pp_last (Node x) = x"
| "pp_last (Cons _ xs) = pp_last xs"
text ‹The path fusion product (although we define it as a total
funcion) should only be applied when the last element of the first
argument is equal to the first element of the second argument.›
primrec pp_fusion :: "'a ppath ⇒ 'a ppath ⇒ 'a ppath" where
"pp_fusion (Node x) ys = ys"
| "pp_fusion (Cons x xs) ys = Cons x (pp_fusion xs ys)"
text ‹We now go through the same steps as for traces and paths
before, showing that the first and last element of a trace a left or
right unit for that trace and that the fusion product on traces is
associative.›
lemma pp_fusion_leftneutral [simp]: "pp_fusion (Node (pp_first x)) x = x"
by simp
lemma pp_fusion_rightneutral [simp]: "pp_fusion x (Node (pp_last x)) = x"
by (induct x) simp_all
lemma pp_first_pp_fusion [simp]:
"pp_last x = pp_first y ⟹ pp_first (pp_fusion x y) = pp_first x"
by (induct x) simp_all
lemma pp_last_pp_fusion [simp]:
"pp_last x = pp_first y ⟹ pp_last (pp_fusion x y) = pp_last y"
by (induct x) simp_all
lemma pp_fusion_assoc [simp]:
"⟦ pp_last x = pp_first y; pp_last y = pp_first z ⟧ ⟹ pp_fusion x (pp_fusion y z) = pp_fusion (pp_fusion x y) z"
by (induct x) simp_all
text ‹We now lift the path fusion product to a complex product on
sets of paths. This operation is total.›
definition pp_prod :: "'a ppath set ⇒ 'a ppath set ⇒ 'a ppath set" (infixl "⋅" 70)
where "X⋅Y = {pp_fusion u v| u v. u ∈ X ∧ v ∈ Y ∧ pp_last u = pp_first v}"
text ‹Next we define the set of paths of length one as the
multiplicative unit of the path dioid.›
definition pp_one :: "'a ppath set" where
"pp_one ≡ range Node"
text ‹We again provide an
elimination rule.›
lemma pp_prod_iff:
"w ∈ X⋅Y ⟷ (∃u v. w = pp_fusion u v ∧ u ∈ X ∧ v ∈ Y ∧ pp_last u = pp_first v)"
by (unfold pp_prod_def) auto
interpretation ppath_dioid: dioid_one_zero "(∪)" "(⋅)" pp_one "{}" "(⊆)" "(⊂)"
proof
fix x y z :: "'a ppath set"
show "x ∪ y ∪ z = x ∪ (y ∪ z)"
by auto
show "x ∪ y = y ∪ x"
by auto
show "x ⋅ y ⋅ z = x ⋅ (y ⋅ z)"
by (auto simp add: pp_prod_def, metis pp_first_pp_fusion pp_fusion_assoc, metis pp_last_pp_fusion)
show "(x ∪ y) ⋅ z = x ⋅ z ∪ y ⋅ z"
by (auto simp add: pp_prod_def)
show "pp_one ⋅ x = x"
by (auto simp add: pp_one_def pp_prod_def, metis pp_fusion.simps(1) pp_last.simps(1) rangeI)
show "x ⋅ pp_one = x"
by (auto simp add: pp_one_def pp_prod_def, metis pp_first.simps(1) pp_fusion_rightneutral rangeI)
show "{} ∪ x = x"
by auto
show "{} ⋅ x = {}"
by (simp add: pp_prod_def)
show "x ⋅ {} = {}"
by (simp add: pp_prod_def)
show "x ⊆ y ⟷ x ∪ y = y"
by auto
show "x ⊂ y ⟷ x ⊆ y ∧ x ≠ y"
by auto
show "x ∪ x = x"
by auto
show "x ⋅ (y ∪ z) = x ⋅ y ∪ x ⋅ z"
by (auto simp add: pp_prod_def)
qed
no_notation
pp_prod (infixl "⋅" 70)
subsection ‹The Distributive Lattice Dioid›
text ‹A bounded distributive lattice is a distributive lattice with
a least and a greatest element. Using Isabelle's lattice theory file
we define a bounded distributive lattice as an axiomatic type class
and show, using a sublocale statement, that every bounded distributive
lattice is a dioid with one and zero.›
class bounded_distributive_lattice = bounded_lattice + distrib_lattice
sublocale bounded_distributive_lattice ⊆ dioid_one_zero sup inf top bot less_eq
proof
fix x y z
show "sup (sup x y) z = sup x (sup y z)"
by (fact sup_assoc)
show "sup x y = sup y x"
by (fact sup.commute)
show "inf (inf x y) z = inf x (inf y z)"
by (metis inf.commute inf.left_commute)
show "inf (sup x y) z = sup (inf x z) (inf y z)"
by (fact inf_sup_distrib2)
show "inf top x = x"
by simp
show "inf x top = x"
by simp
show "sup bot x = x"
by simp
show "inf bot x = bot"
by simp
show "inf x bot = bot"
by simp
show "(x ≤ y) = (sup x y = y)"
by (fact le_iff_sup)
show "(x < y) = (x ≤ y ∧ x ≠ y)"
by auto
show "sup x x = x"
by simp
show "inf x (sup y z) = sup (inf x y) (inf x z)"
by (fact inf_sup_distrib1)
qed
subsection ‹The Boolean Dioid›
text ‹In this section we show that the booleans form a dioid,
because the booleans form a bounded distributive lattice.›
instantiation bool :: bounded_distributive_lattice
begin
instance ..
end
interpretation boolean_dioid: dioid_one_zero sup inf True False less_eq less
by (unfold_locales, simp_all add: inf_bool_def sup_bool_def)
subsection ‹The Max-Plus Dioid›
text ‹The following dioids have important applications in
combinatorial optimisations, control theory, algorithm design and
computer networks.›
text ‹A definition of reals extended with~‹+∞› {\em
and}~‹-∞› may be found in {\em
HOL/Library/Extended\_Real.thy}. Alas, we require separate extensions
with either~‹+∞› or~‹-∞›.›
text ‹The carrier set of the max-plus semiring is the set of real
numbers extended by minus infinity. The operation of addition is
maximum, the operation of multiplication is addition, the additive
unit is minus infinity and the multiplicative unit is zero.›
datatype mreal = mreal real | MInfty
fun mreal_max where
"mreal_max (mreal x) (mreal y) = mreal (max x y)"
| "mreal_max x MInfty = x"
| "mreal_max MInfty y = y"
lemma mreal_max_simp_3 [simp]: "mreal_max MInfty y = y"
by (cases y, simp_all)
fun mreal_plus where
"mreal_plus (mreal x) (mreal y) = mreal (x + y)"
| "mreal_plus _ _ = MInfty"
text ‹We now show that the max plus-semiring satisfies the axioms of
selective semirings, from which it follows that it satisfies the dioid
axioms.›
instantiation mreal :: selective_semiring
begin
definition zero_mreal_def:
"0 ≡ MInfty"
definition one_mreal_def:
"1 ≡ mreal 0"
definition plus_mreal_def:
"x + y ≡ mreal_max x y"
definition times_mreal_def:
"x * y ≡ mreal_plus x y"
definition less_eq_mreal_def:
"(x::mreal) ≤ y ≡ x + y = y"
definition less_mreal_def:
"(x::mreal) < y ≡ x ≤ y ∧ x ≠ y"
instance
proof
fix x y z :: mreal
show "x + y + z = x + (y + z)"
by (cases x, cases y, cases z, simp_all add: plus_mreal_def)
show "x + y = y + x"
by (cases x, cases y, simp_all add: plus_mreal_def)
show "x * y * z = x * (y * z)"
by (cases x, cases y, cases z, simp_all add: times_mreal_def)
show "(x + y) * z = x * z + y * z"
by (cases x, cases y, cases z, simp_all add: plus_mreal_def times_mreal_def)
show "1 * x = x"
by (cases x, simp_all add: one_mreal_def times_mreal_def)
show "x * 1 = x"
by (cases x, simp_all add: one_mreal_def times_mreal_def)
show "0 + x = x"
by (cases x, simp_all add: plus_mreal_def zero_mreal_def)
show "0 * x = 0"
by (cases x, simp_all add: times_mreal_def zero_mreal_def)
show "x * 0 = 0"
by (cases x, simp_all add: times_mreal_def zero_mreal_def)
show "x ≤ y ⟷ x + y = y"
by (metis less_eq_mreal_def)
show "x < y ⟷ x ≤ y ∧ x ≠ y"
by (metis less_mreal_def)
show "x + y = x ∨ x + y = y"
by (cases x, cases y, simp_all add: plus_mreal_def, metis linorder_le_cases max.absorb_iff2 max.absorb1)
show "x * (y + z) = x * y + x * z"
by (cases x, cases y, cases z, simp_all add: plus_mreal_def times_mreal_def) qed
end
subsection ‹The Min-Plus Dioid›
text ‹The min-plus dioid is also known as {\em tropical
semiring}. Here we need to add a positive infinity to the real
numbers. The procedere follows that of max-plus semirings.›
datatype preal = preal real | PInfty
fun preal_min where
"preal_min (preal x) (preal y) = preal (min x y)"
| "preal_min x PInfty = x"
| "preal_min PInfty y = y"
lemma preal_min_simp_3 [simp]: "preal_min PInfty y = y"
by (cases y, simp_all)
fun preal_plus where
"preal_plus (preal x) (preal y) = preal (x + y)"
| "preal_plus _ _ = PInfty"
instantiation preal :: selective_semiring
begin
definition zero_preal_def:
"0 ≡ PInfty"
definition one_preal_def:
"1 ≡ preal 0"
definition plus_preal_def:
"x + y ≡ preal_min x y"
definition times_preal_def:
"x * y ≡ preal_plus x y"
definition less_eq_preal_def:
"(x::preal) ≤ y ≡ x + y = y"
definition less_preal_def:
"(x::preal) < y ≡ x ≤ y ∧ x ≠ y"
instance
proof
fix x y z :: preal
show "x + y + z = x + (y + z)"
by (cases x, cases y, cases z, simp_all add: plus_preal_def)
show "x + y = y + x"
by (cases x, cases y, simp_all add: plus_preal_def)
show "x * y * z = x * (y * z)"
by (cases x, cases y, cases z, simp_all add: times_preal_def)
show "(x + y) * z = x * z + y * z"
by (cases x, cases y, cases z, simp_all add: plus_preal_def times_preal_def)
show "1 * x = x"
by (cases x, simp_all add: one_preal_def times_preal_def)
show "x * 1 = x"
by (cases x, simp_all add: one_preal_def times_preal_def)
show "0 + x = x"
by (cases x, simp_all add: plus_preal_def zero_preal_def)
show "0 * x = 0"
by (cases x, simp_all add: times_preal_def zero_preal_def)
show "x * 0 = 0"
by (cases x, simp_all add: times_preal_def zero_preal_def)
show "x ≤ y ⟷ x + y = y"
by (metis less_eq_preal_def)
show "x < y ⟷ x ≤ y ∧ x ≠ y"
by (metis less_preal_def)
show "x + y = x ∨ x + y = y"
by (cases x, cases y, simp_all add: plus_preal_def, metis linorder_le_cases min.absorb2 min.absorb_iff1)
show "x * (y + z) = x * y + x * z"
by (cases x, cases y, cases z, simp_all add: plus_preal_def times_preal_def) qed
end
text ‹Variants of min-plus and max-plus semirings can easily be
obtained. Here we formalise the min-plus semiring over the natural
numbers as an example.›
datatype pnat = pnat nat | PInfty
fun pnat_min where
"pnat_min (pnat x) (pnat y) = pnat (min x y)"
| "pnat_min x PInfty = x"
| "pnat_min PInfty x = x"
lemma pnat_min_simp_3 [simp]: "pnat_min PInfty y = y"
by (cases y, simp_all)
fun pnat_plus where
"pnat_plus (pnat x) (pnat y) = pnat (x + y)"
| "pnat_plus _ _ = PInfty"
instantiation pnat :: selective_semiring
begin
definition zero_pnat_def:
"0 ≡ PInfty"
definition one_pnat_def:
"1 ≡ pnat 0"
definition plus_pnat_def:
"x + y ≡ pnat_min x y"
definition times_pnat_def:
"x * y ≡ pnat_plus x y"
definition less_eq_pnat_def:
"(x::pnat) ≤ y ≡ x + y = y"
definition less_pnat_def:
"(x::pnat) < y ≡ x ≤ y ∧ x ≠ y"
lemma zero_pnat_top: "(x::pnat) ≤ 1"
by (cases x, simp_all add: less_eq_pnat_def plus_pnat_def one_pnat_def)
instance
proof
fix x y z :: pnat
show "x + y + z = x + (y + z)"
by (cases x, cases y, cases z, simp_all add: plus_pnat_def)
show "x + y = y + x"
by (cases x, cases y, simp_all add: plus_pnat_def)
show "x * y * z = x * (y * z)"
by (cases x, cases y, cases z, simp_all add: times_pnat_def)
show "(x + y) * z = x * z + y * z"
by (cases x, cases y, cases z, simp_all add: plus_pnat_def times_pnat_def)
show "1 * x = x"
by (cases x, simp_all add: one_pnat_def times_pnat_def)
show "x * 1 = x"
by (cases x, simp_all add: one_pnat_def times_pnat_def)
show "0 + x = x"
by (cases x, simp_all add: plus_pnat_def zero_pnat_def)
show "0 * x = 0"
by (cases x, simp_all add: times_pnat_def zero_pnat_def)
show "x * 0 = 0"
by (cases x, simp_all add: times_pnat_def zero_pnat_def)
show "x ≤ y ⟷ x + y = y"
by (metis less_eq_pnat_def)
show "x < y ⟷ x ≤ y ∧ x ≠ y"
by (metis less_pnat_def)
show "x + y = x ∨ x + y = y"
by (cases x, cases y, simp_all add: plus_pnat_def, metis linorder_le_cases min.absorb2 min.absorb_iff1)
show "x * (y + z) = x * y + x * z"
by (cases x, cases y, cases z, simp_all add: plus_pnat_def times_pnat_def)
qed
end
end
Theory Matrix
section ‹Matrices›
theory Matrix
imports "HOL-Library.Word" Dioid
begin
text ‹In this section we formalise a perhaps more natural version of
matrices of fixed dimension ($m \times n$-matrices). It is well known
that such matrices over a Kleene algebra form a Kleene
algebra~\cite{conway71regular}.›
subsection ‹Type Definition›
typedef (overloaded) 'a atMost = "{..<LENGTH('a::len)}"
by auto
declare Rep_atMost_inject [simp]
lemma UNIV_atMost:
"(UNIV::'a atMost set) = Abs_atMost ` {..<LENGTH('a::len)}"
apply auto
apply (rule Abs_atMost_induct)
apply auto
done
lemma finite_UNIV_atMost [simp]: "finite (UNIV::('a::len) atMost set)"
by (simp add: UNIV_atMost)
text ‹Our matrix type is similar to \mbox{‹'a^'n^'m›} from
{\em HOL/Multivariate\_Analysis/Finite\_Cartesian\_Product.thy}, but
(i)~we explicitly define a type constructor for matrices and square
matrices, and (ii)~in the definition of operations, e.g., matrix
multiplication, we impose weaker sort requirements on the element
type.›
context notes [[typedef_overloaded]]
begin
datatype ('a,'m,'n) matrix = Matrix "'m atMost ⇒ 'n atMost ⇒ 'a"
datatype ('a,'m) sqmatrix = SqMatrix "'m atMost ⇒ 'm atMost ⇒ 'a"
end
fun sqmatrix_of_matrix where
"sqmatrix_of_matrix (Matrix A) = SqMatrix A"
fun matrix_of_sqmatrix where
"matrix_of_sqmatrix (SqMatrix A) = Matrix A"
subsection ‹0 and 1›
instantiation matrix :: (zero,type,type) zero
begin
definition zero_matrix_def: "0 ≡ Matrix (λi j. 0)"
instance ..
end
instantiation sqmatrix :: (zero,type) zero
begin
definition zero_sqmatrix_def: "0 ≡ SqMatrix (λi j. 0)"
instance ..
end
text ‹Tricky sort issues: compare @{term one_matrix} with @{term
one_sqmatrix} \dots›
instantiation matrix :: ("{zero,one}",len,len) one
begin
definition one_matrix_def:
"1 ≡ Matrix (λi j. if Rep_atMost i = Rep_atMost j then 1 else 0)"
instance ..
end
instantiation sqmatrix :: ("{zero,one}",type) one
begin
definition one_sqmatrix_def:
"1 ≡ SqMatrix (λi j. if i = j then 1 else 0)"
instance ..
end
subsection ‹Matrix Addition›
fun matrix_plus where
"matrix_plus (Matrix A) (Matrix B) = Matrix (λi j. A i j + B i j)"
instantiation matrix :: (plus,type,type) plus
begin
definition plus_matrix_def: "A + B ≡ matrix_plus A B"
instance ..
end
lemma plus_matrix_def' [simp]:
"Matrix A + Matrix B = Matrix (λi j. A i j + B i j)"
by (simp add: plus_matrix_def)
instantiation sqmatrix :: (plus,type) plus
begin
definition plus_sqmatrix_def:
"A + B ≡ sqmatrix_of_matrix (matrix_of_sqmatrix A + matrix_of_sqmatrix B)"
instance ..
end
lemma plus_sqmatrix_def' [simp]:
"SqMatrix A + SqMatrix B = SqMatrix (λi j. A i j + B i j)"
by (simp add: plus_sqmatrix_def)
lemma matrix_add_0_right [simp]:
"A + 0 = (A::('a::monoid_add,'m,'n) matrix)"
by (cases A, simp add: zero_matrix_def)
lemma matrix_add_0_left [simp]:
"0 + A = (A::('a::monoid_add,'m,'n) matrix)"
by (cases A, simp add: zero_matrix_def)
lemma matrix_add_commute [simp]:
"(A::('a::ab_semigroup_add,'m,'n) matrix) + B = B + A"
by (cases A, cases B, simp add: add.commute)
lemma matrix_add_assoc:
"(A::('a::semigroup_add,'m,'n) matrix) + B + C = A + (B + C)"
by (cases A, cases B, cases C, simp add: add.assoc)
lemma matrix_add_left_commute [simp]:
"(A::('a::ab_semigroup_add,'m,'n) matrix) + (B + C) = B + (A + C)"
by (metis matrix_add_assoc matrix_add_commute)
lemma sqmatrix_add_0_right [simp]:
"A + 0 = (A::('a::monoid_add,'m) sqmatrix)"
by (cases A, simp add: zero_sqmatrix_def)
lemma sqmatrix_add_0_left [simp]:
"0 + A = (A::('a::monoid_add,'m) sqmatrix)"
by (cases A, simp add: zero_sqmatrix_def)
lemma sqmatrix_add_commute [simp]:
"(A::('a::ab_semigroup_add,'m) sqmatrix) + B = B + A"
by (cases A, cases B, simp add: add.commute)
lemma sqmatrix_add_assoc:
"(A::('a::semigroup_add,'m) sqmatrix) + B + C = A + (B + C)"
by (cases A, cases B, cases C, simp add: add.assoc)
lemma sqmatrix_add_left_commute [simp]:
"(A::('a::ab_semigroup_add,'m) sqmatrix) + (B + C) = B + (A + C)"
by (metis sqmatrix_add_commute sqmatrix_add_assoc)
subsection ‹Order (via Addition)›
instantiation matrix :: (plus,type,type) plus_ord
begin
definition less_eq_matrix_def:
"(A::('a, 'b, 'c) matrix) ≤ B ≡ A + B = B"
definition less_matrix_def:
"(A::('a, 'b, 'c) matrix) < B ≡ A ≤ B ∧ A ≠ B"
instance
proof
fix A B :: "('a, 'b, 'c) matrix"
show "A ≤ B ⟷ A + B = B"
by (metis less_eq_matrix_def)
show "A < B ⟷ A ≤ B ∧ A ≠ B"
by (metis less_matrix_def)
qed
end
instantiation sqmatrix :: (plus,type) plus_ord
begin
definition less_eq_sqmatrix_def:
"(A::('a, 'b) sqmatrix) ≤ B ≡ A + B = B"
definition less_sqmatrix_def:
"(A::('a, 'b) sqmatrix) < B ≡ A ≤ B ∧ A ≠ B"
instance
proof
fix A B :: "('a, 'b) sqmatrix"
show "A ≤ B ⟷ A + B = B"
by (metis less_eq_sqmatrix_def)
show "A < B ⟷ A ≤ B ∧ A ≠ B"
by (metis less_sqmatrix_def)
qed
end
subsection ‹Matrix Multiplication›
fun matrix_times :: "('a::{comm_monoid_add,times},'m,'k) matrix ⇒ ('a,'k,'n) matrix ⇒ ('a,'m,'n) matrix" where
"matrix_times (Matrix A) (Matrix B) = Matrix (λi j. sum (λk. A i k * B k j) (UNIV::'k atMost set))"
notation matrix_times (infixl "*⇩M" 70)
instantiation sqmatrix :: ("{comm_monoid_add,times}",type) times
begin
definition times_sqmatrix_def:
"A * B = sqmatrix_of_matrix (matrix_of_sqmatrix A *⇩M matrix_of_sqmatrix B)"
instance ..
end
lemma times_sqmatrix_def' [simp]:
"SqMatrix A * SqMatrix B = SqMatrix (λi j. sum (λk. A i k * B k j) (UNIV::'k atMost set))"
by (simp add: times_sqmatrix_def)
lemma matrix_mult_0_right [simp]:
"(A::('a::{comm_monoid_add,mult_zero},'m,'n) matrix) *⇩M 0 = 0"
by (cases A, simp add: zero_matrix_def)
lemma matrix_mult_0_left [simp]:
"0 *⇩M (A::('a::{comm_monoid_add,mult_zero},'m,'n) matrix) = 0"
by (cases A, simp add: zero_matrix_def)
lemma sum_delta_r_0 [simp]:
"⟦ finite S; j ∉ S ⟧ ⟹ (∑k∈S. f k * (if k = j then 1 else (0::'b::{semiring_0,monoid_mult}))) = 0"
by (induct S rule: finite_induct, auto)
lemma sum_delta_r_1 [simp]:
"⟦ finite S; j ∈ S ⟧ ⟹ (∑k∈S. f k * (if k = j then 1 else (0::'b::{semiring_0,monoid_mult}))) = f j"
by (induct S rule: finite_induct, auto)
lemma matrix_mult_1_right [simp]:
"(A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) *⇩M 1 = A"
by (cases A, simp add: one_matrix_def)
lemma sum_delta_l_0 [simp]:
"⟦ finite S; i ∉ S ⟧ ⟹ (∑k∈S. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = 0"
by (induct S rule: finite_induct, auto)
lemma sum_delta_l_1 [simp]:
"⟦ finite S; i ∈ S ⟧ ⟹ (∑k∈S. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = f i j"
by (induct S rule: finite_induct, auto)
lemma matrix_mult_1_left [simp]:
"1 *⇩M (A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) = A"
by (cases A, simp add: one_matrix_def)
lemma matrix_mult_assoc:
"(A::('a::semiring_0,'m,'n) matrix) *⇩M B *⇩M C = A *⇩M (B *⇩M C)"
apply (cases A)
apply (cases B)
apply (cases C)
apply (simp add: sum_distrib_right sum_distrib_left mult.assoc)
apply (subst sum.swap)
apply (rule refl)
done
lemma matrix_mult_distrib_left:
"(A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) *⇩M (B + C) = A *⇩M B + A *⇩M C"
by (cases A, cases B, cases C, simp add: distrib_left sum.distrib)
lemma matrix_mult_distrib_right:
"((A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) + B) *⇩M C = A *⇩M C + B *⇩M C"
by (cases A, cases B, cases C, simp add: distrib_right sum.distrib)
lemma sqmatrix_mult_0_right [simp]:
"(A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) * 0 = 0"
by (cases A, simp add: zero_sqmatrix_def)
lemma sqmatrix_mult_0_left [simp]:
"0 * (A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) = 0"
by (cases A, simp add: zero_sqmatrix_def)
lemma sqmatrix_mult_1_right [simp]:
"(A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) * 1 = A"
by (cases A, simp add: one_sqmatrix_def)
lemma sqmatrix_mult_1_left [simp]:
"1 * (A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) = A"
by (cases A, simp add: one_sqmatrix_def)
lemma sqmatrix_mult_assoc:
"(A::('a::{semiring_0,monoid_mult},'m) sqmatrix) * B * C = A * (B * C)"
apply (cases A)
apply (cases B)
apply (cases C)
apply (simp add: sum_distrib_right sum_distrib_left mult.assoc)
apply (subst sum.swap)
apply (rule refl)
done
lemma sqmatrix_mult_distrib_left:
"(A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) * (B + C) = A * B + A * C"
by (cases A, cases B, cases C, simp add: distrib_left sum.distrib)
lemma sqmatrix_mult_distrib_right:
"((A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) + B) * C = A * C + B * C"
by (cases A, cases B, cases C, simp add: distrib_right sum.distrib)
subsection ‹Square-Matrix Model of Dioids›
text ‹The following subclass proofs are necessary to connect parts
of our algebraic hierarchy to the hierarchy found in the Isabelle/HOL
library.›
subclass (in ab_near_semiring_one_zerol) comm_monoid_add
proof
fix a :: 'a
show "0 + a = a"
by (fact add_zerol)
qed
subclass (in semiring_one_zero) semiring_0
proof
fix a :: 'a
show "0 * a = 0"
by (fact annil)
show "a * 0 = 0"
by (fact annir)
qed
subclass (in ab_near_semiring_one) monoid_mult ..
instantiation sqmatrix :: (dioid_one_zero,len) dioid_one_zero
begin
instance
proof
fix A B C :: "('a, 'b) sqmatrix"
show "A + B + C = A + (B + C)"
by (fact sqmatrix_add_assoc)
show "A + B = B + A"
by (fact sqmatrix_add_commute)
show "A * B * C = A * (B * C)"
by (fact sqmatrix_mult_assoc)
show "(A + B) * C = A * C + B * C"
by (fact sqmatrix_mult_distrib_right)
show "1 * A = A"
by (fact sqmatrix_mult_1_left)
show "A * 1 = A"
by (fact sqmatrix_mult_1_right)
show "0 + A = A"
by (fact sqmatrix_add_0_left)
show "0 * A = 0"
by (fact sqmatrix_mult_0_left)
show "A * 0 = 0"
by (fact sqmatrix_mult_0_right)
show "A + A = A"
by (cases A, simp)
show "A * (B + C) = A * B + A * C"
by (fact sqmatrix_mult_distrib_left)
qed
end
subsection ‹Kleene Star for Matrices›
text ‹We currently do not implement the Kleene star of matrices,
since this is complicated.›
end
Theory Conway
section ‹Conway Algebras›
theory Conway
imports Dioid
begin
text ‹
We define a weak regular algebra which can serve as a common basis for Kleene algebra and demonic reginement algebra.
It is closely related to an axiomatisation given by Conway~\cite{conway71regular}.
›
class dagger_op =
fixes dagger :: "'a ⇒ 'a" ("_⇧†" [101] 100)
subsection‹Near Conway Algebras›
class near_conway_base = near_dioid_one + dagger_op +
assumes dagger_denest: "(x + y)⇧† = (x⇧† ⋅ y)⇧† ⋅ x⇧†"
and dagger_prod_unfold [simp]: "1 + x ⋅ (y ⋅ x)⇧† ⋅ y = (x ⋅ y)⇧†"
begin
lemma dagger_unfoldl_eq [simp]: "1 + x ⋅ x⇧† = x⇧†"
by (metis dagger_prod_unfold mult_1_left mult_1_right)
lemma dagger_unfoldl: "1 + x ⋅ x⇧† ≤ x⇧†"
by auto
lemma dagger_unfoldr_eq [simp]: "1 + x⇧† ⋅ x = x⇧†"
by (metis dagger_prod_unfold mult_1_right mult_1_left)
lemma dagger_unfoldr: "1 + x⇧† ⋅ x ≤ x⇧†"
by auto
lemma dagger_unfoldl_distr [simp]: "y + x ⋅ x⇧† ⋅ y = x⇧† ⋅ y"
by (metis distrib_right' mult_1_left dagger_unfoldl_eq)
lemma dagger_unfoldr_distr [simp]: "y + x⇧† ⋅ x ⋅ y = x⇧† ⋅ y"
by (metis dagger_unfoldr_eq distrib_right' mult_1_left mult.assoc)
lemma dagger_refl: "1 ≤ x⇧†"
using dagger_unfoldl local.join.sup.bounded_iff by blast
lemma dagger_plus_one [simp]: "1 + x⇧† = x⇧†"
by (simp add: dagger_refl local.join.sup_absorb2)
lemma star_1l: "x ⋅ x⇧† ≤ x⇧†"
using dagger_unfoldl local.join.sup.bounded_iff by blast
lemma star_1r: "x⇧† ⋅ x ≤ x⇧†"
using dagger_unfoldr local.join.sup.bounded_iff by blast
lemma dagger_ext: "x ≤ x⇧†"
by (metis dagger_unfoldl_distr local.join.sup.boundedE star_1r)
lemma dagger_trans_eq [simp]: "x⇧† ⋅ x⇧† = x⇧†"
by (metis dagger_unfoldr_eq local.dagger_denest local.join.sup.idem mult_assoc)
lemma dagger_subdist: "x⇧† ≤ (x + y)⇧†"
by (metis dagger_unfoldr_distr local.dagger_denest local.order_prop)
lemma dagger_subdist_var: "x⇧† + y⇧† ≤ (x + y)⇧†"
using dagger_subdist local.join.sup_commute by fastforce
lemma dagger_iso [intro]: "x ≤ y ⟹ x⇧† ≤ y⇧†"
by (metis less_eq_def dagger_subdist)
lemma star_square: "(x ⋅ x)⇧† ≤ x⇧†"
by (metis dagger_plus_one dagger_subdist dagger_trans_eq dagger_unfoldr_distr dagger_denest
distrib_right' order.eq_iff join.sup_commute less_eq_def mult_onel mult_assoc)
lemma dagger_rtc1_eq [simp]: "1 + x + x⇧† ⋅ x⇧† = x⇧†"
by (simp add: local.dagger_ext local.dagger_refl local.join.sup_absorb2)
text ‹Nitpick refutes the next lemmas.›
lemma " y + y ⋅ x⇧† ⋅ x = y ⋅ x⇧†"
oops
lemma "y ⋅ x⇧† = y + y ⋅ x ⋅ x⇧†"
oops
lemma "(x + y)⇧† = x⇧† ⋅ (y ⋅ x⇧†)⇧†"
oops
lemma "(x⇧†)⇧† = x⇧†"
oops
lemma "(1 + x)⇧⋆ = x⇧⋆"
oops
lemma "x⇧† ⋅ x = x ⋅ x⇧†"
oops
end
subsection‹Pre-Conway Algebras›
class pre_conway_base = near_conway_base + pre_dioid_one
begin
lemma dagger_subdist_var_3: "x⇧† ⋅ y⇧† ≤ (x + y)⇧†"
using local.dagger_subdist_var local.mult_isol_var by fastforce
lemma dagger_subdist_var_2: "x ⋅ y ≤ (x + y)⇧†"
by (meson dagger_subdist_var_3 local.dagger_ext local.mult_isol_var local.order.trans)
lemma dagger_sum_unfold [simp]: "x⇧† + x⇧† ⋅ y ⋅ (x + y)⇧† = (x + y)⇧†"
by (metis local.dagger_denest local.dagger_unfoldl_distr mult_assoc)
end
subsection ‹Conway Algebras›
class conway_base = pre_conway_base + dioid_one
begin
lemma troeger: "(x + y)⇧† ⋅ z = x⇧† ⋅ (y ⋅ (x + y)⇧† ⋅ z + z)"
proof -
have "(x + y)⇧† ⋅ z = x⇧† ⋅ z + x⇧† ⋅ y ⋅ (x + y)⇧† ⋅ z"
by (metis dagger_sum_unfold local.distrib_right')
thus ?thesis
by (metis add_commute local.distrib_left mult_assoc)
qed
lemma dagger_slide_var1: "x⇧† ⋅ x ≤ x ⋅ x⇧†"
by (metis local.dagger_unfoldl_distr local.dagger_unfoldr_eq local.distrib_left order.eq_iff local.mult_1_right mult_assoc)
lemma dagger_slide_var1_eq: "x⇧† ⋅ x = x ⋅ x⇧†"
by (metis local.dagger_unfoldl_distr local.dagger_unfoldr_eq local.distrib_left local.mult_1_right mult_assoc)
lemma dagger_slide_eq: "(x ⋅ y)⇧† ⋅ x = x ⋅ (y ⋅ x)⇧†"
proof -
have "(x ⋅ y)⇧† ⋅ x = x + x ⋅ (y ⋅ x)⇧† ⋅ y ⋅ x"
by (metis local.dagger_prod_unfold local.distrib_right' local.mult_onel)
also have "... = x ⋅ (1 + (y ⋅ x)⇧† ⋅ y ⋅ x)"
using local.distrib_left local.mult_1_right mult_assoc by presburger
finally show ?thesis
by (simp add: mult_assoc)
qed
end
subsection ‹Conway Algebras with Zero›
class near_conway_base_zerol = near_conway_base + near_dioid_one_zerol
begin
lemma dagger_annil [simp]: "1 + x ⋅ 0 = (x ⋅ 0)⇧†"
by (metis annil dagger_unfoldl_eq mult.assoc)
lemma zero_dagger [simp]: "0⇧† = 1"
by (metis add_0_right annil dagger_annil)
end
class pre_conway_base_zerol = near_conway_base_zerol + pre_dioid
class conway_base_zerol = pre_conway_base_zerol + dioid
subclass (in pre_conway_base_zerol) pre_conway_base ..
subclass (in conway_base_zerol) conway_base ..
context conway_base_zerol
begin
lemma "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧† ≤ y⇧† ⋅ z"
oops
end
subsection ‹Conway Algebras with Simulation›
class near_conway = near_conway_base +
assumes dagger_simr: "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧† ≤ y⇧† ⋅ z"
begin
lemma dagger_slide_var: "x ⋅ (y ⋅ x)⇧† ≤ (x ⋅ y)⇧† ⋅ x"
by (metis eq_refl dagger_simr mult.assoc)
text ‹Nitpick refutes the next lemma.›
lemma dagger_slide: "x ⋅ (y ⋅ x)⇧† = (x ⋅ y)⇧† ⋅ x"
oops
text ‹
We say that $y$ preserves $x$ if $x \cdot y \cdot x = x \cdot y$ and $!x \cdot y \cdot !x = !x \cdot y$. This definition is taken
from Solin~\cite{Solin11}. It is useful for program transformation.
›
lemma preservation1: "x ⋅ y ≤ x ⋅ y ⋅ x ⟹ x ⋅ y⇧† ≤ (x ⋅ y + z)⇧† ⋅ x"
proof -
assume "x ⋅ y ≤ x ⋅ y ⋅ x"
hence "x ⋅ y ≤ (x ⋅ y + z) ⋅ x"
by (simp add: local.join.le_supI1)
thus ?thesis
by (simp add: local.dagger_simr)
qed
end
class near_conway_zerol = near_conway + near_dioid_one_zerol
class pre_conway = near_conway + pre_dioid_one
begin
subclass pre_conway_base ..
lemma dagger_slide: "x ⋅ (y ⋅ x)⇧† = (x ⋅ y)⇧† ⋅ x"
by (metis add.commute dagger_prod_unfold join.sup_least mult_1_right mult.assoc subdistl dagger_slide_var dagger_unfoldl_distr order.antisym)
lemma dagger_denest2: "(x + y)⇧† = x⇧† ⋅ (y ⋅ x⇧†)⇧†"
by (metis dagger_denest dagger_slide)
lemma preservation2: "y ⋅ x ≤ y ⟹ (x ⋅ y)⇧† ⋅ x ≤ x ⋅ y⇧†"
by (metis dagger_slide local.dagger_iso local.mult_isol)
lemma preservation1_eq: "x ⋅ y ≤ x ⋅ y ⋅ x ⟹ y ⋅ x ≤ y ⟹ (x ⋅ y)⇧† ⋅ x = x ⋅ y⇧†"
by (simp add: local.dagger_simr order.eq_iff preservation2)
end
class pre_conway_zerol = near_conway_zerol + pre_dioid_one_zerol
begin
subclass pre_conway ..
end
class conway = pre_conway + dioid_one
class conway_zerol = pre_conway + dioid_one_zerol
begin
subclass conway_base ..
text ‹Nitpick refutes the next lemmas.›
lemma "1 = 1⇧†"
oops
lemma "(x⇧†)⇧† = x⇧†"
oops
lemma dagger_denest_var [simp]: "(x + y)⇧† = (x⇧† ⋅ y⇧†)⇧†"
oops
lemma star2 [simp]: "(1 + x)⇧† = x⇧†"
oops
end
end
Theory Kleene_Algebra
section ‹Kleene Algebras›
theory Kleene_Algebra
imports Conway
begin
subsection ‹Left Near Kleene Algebras›
text ‹Extending the hierarchy developed in @{theory Kleene_Algebra.Dioid} we now
add an operation of Kleene star, finite iteration, or reflexive
transitive closure to variants of Dioids. Since a multiplicative unit
is needed for defining the star we only consider variants with~$1$;
$0$ can be added separately. We consider the left star induction axiom
and the right star induction axiom independently since in some
applications, e.g., Salomaa's axioms, probabilistic Kleene algebras,
or completeness proofs with respect to the equational theoy of regular
expressions and regular languages, the right star induction axiom is
not needed or not valid.
We start with near dioids, then consider pre-dioids and finally
dioids. It turns out that many of the known laws of Kleene algebras
hold already in these more general settings. In fact, all our
equational theorems have been proved within left Kleene algebras, as
expected.
Although most of the proofs in this file could be fully automated by
Sledgehammer and Metis, we display step-wise proofs as they would
appear in a text book. First, this file may then be useful as a
reference manual on Kleene algebra. Second, it is better protected
against changes in the underlying theories and supports easy
translation of proofs into other settings.›
class left_near_kleene_algebra = near_dioid_one + star_op +
assumes star_unfoldl: "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
and star_inductl: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
begin
text ‹First we prove two immediate consequences of the unfold
axiom. The first one states that starred elements are reflexive.›
lemma star_ref [simp]: "1 ≤ x⇧⋆"
using star_unfoldl by auto
text ‹Reflexivity of starred elements implies, by definition of the
order, that~$1$ is an additive unit for starred elements.›
lemma star_plus_one [simp]: "1 + x⇧⋆ = x⇧⋆"
using less_eq_def star_ref by blast
lemma star_1l [simp]: "x ⋅ x⇧⋆ ≤ x⇧⋆"
using star_unfoldl by auto
lemma "x⇧⋆ ⋅ x ≤ x⇧⋆"
oops
lemma "x ⋅ x⇧⋆ = x⇧⋆"
oops
text ‹Next we show that starred elements are transitive.›
lemma star_trans_eq [simp]: "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
proof (rule order.antisym)
have "x⇧⋆ + x ⋅ x⇧⋆ ≤ x⇧⋆"
by auto
thus "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by (simp add: star_inductl)
next show "x⇧⋆ ≤ x⇧⋆ ⋅ x⇧⋆"
using mult_isor star_ref by fastforce
qed
lemma star_trans: "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
text ‹We now derive variants of the star induction axiom.›
lemma star_inductl_var: "x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ y ≤ y"
proof -
assume "x ⋅ y ≤ y"
hence "y + x ⋅ y ≤ y"
by simp
thus "x⇧⋆ ⋅ y ≤ y"
by (simp add: star_inductl)
qed
lemma star_inductl_var_equiv [simp]: "x⇧⋆ ⋅ y ≤ y ⟷ x ⋅ y ≤ y"
proof
assume "x ⋅ y ≤ y"
thus "x⇧⋆ ⋅ y ≤ y"
by (simp add: star_inductl_var)
next
assume "x⇧⋆ ⋅ y ≤ y"
hence "x⇧⋆ ⋅ y = y"
by (metis order.eq_iff mult_1_left mult_isor star_ref)
moreover hence "x ⋅ y = x ⋅ x⇧⋆ ⋅ y"
by (simp add: mult.assoc)
moreover have "... ≤ x⇧⋆ ⋅ y"
by (metis mult_isor star_1l)
ultimately show "x ⋅ y ≤ y"
by auto
qed
lemma star_inductl_var_eq: "x ⋅ y = y ⟹ x⇧⋆ ⋅ y ≤ y"
by (metis order.eq_iff star_inductl_var)
lemma star_inductl_var_eq2: "y = x ⋅ y ⟹ y = x⇧⋆ ⋅ y"
proof -
assume hyp: "y = x ⋅ y"
hence "y ≤ x⇧⋆ ⋅ y"
using mult_isor star_ref by fastforce
thus "y = x⇧⋆ ⋅ y"
using hyp order.eq_iff by auto
qed
lemma "y = x ⋅ y ⟷ y = x⇧⋆ ⋅ y"
oops
lemma "x⇧⋆ ⋅ z ≤ y ⟹ z + x ⋅ y ≤ y"
oops
lemma star_inductl_one: "1 + x ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"
using star_inductl by force
lemma star_inductl_star: "x ⋅ y⇧⋆ ≤ y⇧⋆ ⟹ x⇧⋆ ≤ y⇧⋆"
by (simp add: star_inductl_one)
lemma star_inductl_eq: "z + x ⋅ y = y ⟹ x⇧⋆ ⋅ z ≤ y"
by (simp add: star_inductl)
text ‹We now prove two facts related to~$1$.›
lemma star_subid: "x ≤ 1 ⟹ x⇧⋆ = 1"
proof -
assume "x ≤ 1"
hence "1 + x ⋅ 1 ≤ 1"
by simp
hence "x⇧⋆ ≤ 1"
by (metis mult_oner star_inductl)
thus "x⇧⋆ = 1"
by (simp add: order.antisym)
qed
lemma star_one [simp]: "1⇧⋆ = 1"
by (simp add: star_subid)
text ‹We now prove a subdistributivity property for the star (which
is equivalent to isotonicity of star).›
lemma star_subdist: "x⇧⋆ ≤ (x + y)⇧⋆"
proof -
have "x ⋅ (x + y)⇧⋆ ≤ (x + y) ⋅ (x + y)⇧⋆"
by simp
also have "... ≤ (x + y)⇧⋆"
by (metis star_1l)
thus ?thesis
using calculation order_trans star_inductl_star by blast
qed
lemma star_subdist_var: "x⇧⋆ + y⇧⋆ ≤ (x + y)⇧⋆"
using join.sup_commute star_subdist by force
lemma star_iso [intro]: "x ≤ y ⟹ x⇧⋆ ≤ y⇧⋆"
by (metis less_eq_def star_subdist)
text ‹We now prove some more simple properties.›
lemma star_invol [simp]: "(x⇧⋆)⇧⋆ = x⇧⋆"
proof (rule order.antisym)
have "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (fact star_trans_eq)
thus "(x⇧⋆)⇧⋆ ≤ x⇧⋆"
by (simp add: star_inductl_star)
have"(x⇧⋆)⇧⋆ ⋅ (x⇧⋆)⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (fact star_trans)
hence "x ⋅ (x⇧⋆)⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (meson star_inductl_var_equiv)
thus "x⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (simp add: star_inductl_star)
qed
lemma star2 [simp]: "(1 + x)⇧⋆ = x⇧⋆"
proof (rule order.antisym)
show "x⇧⋆ ≤ (1 + x)⇧⋆"
by auto
have "x⇧⋆ + x ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
thus "(1 + x)⇧⋆ ≤ x⇧⋆"
by (simp add: star_inductl_star)
qed
lemma "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
oops
lemma "x ≤ x⇧⋆"
oops
lemma "x⇧⋆ ⋅ x ≤ x⇧⋆"
oops
lemma "1 + x ⋅ x⇧⋆ = x⇧⋆"
oops
lemma "x ⋅ z ≤ z ⋅ y ⟹ x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
oops
text ‹The following facts express inductive conditions that are used
to show that @{term "(x + y)⇧⋆"} is the greatest term that can be built
from~@{term x} and~@{term y}.›
lemma prod_star_closure: "x ≤ z⇧⋆ ⟹ y ≤ z⇧⋆ ⟹ x ⋅ y ≤ z⇧⋆"
proof -
assume assm: "x ≤ z⇧⋆" "y ≤ z⇧⋆"
hence "y + z⇧⋆ ⋅ z⇧⋆ ≤ z⇧⋆"
by simp
hence "z⇧⋆ ⋅ y ≤ z⇧⋆"
by (simp add: star_inductl)
also have "x ⋅ y ≤ z⇧⋆ ⋅ y"
by (simp add: assm mult_isor)
thus "x ⋅ y ≤ z⇧⋆"
using calculation order.trans by blast
qed
lemma star_star_closure: "x⇧⋆ ≤ z⇧⋆ ⟹ (x⇧⋆)⇧⋆ ≤ z⇧⋆"
by (metis star_invol)
lemma star_closed_unfold: "x⇧⋆ = x ⟹ x = 1 + x ⋅ x"
by (metis star_plus_one star_trans_eq)
lemma "x⇧⋆ = x ⟷ x = 1 + x ⋅ x"
oops
end
subsection ‹Left Pre-Kleene Algebras›
class left_pre_kleene_algebra = left_near_kleene_algebra + pre_dioid_one
begin
text ‹We first prove that the star operation is extensive.›
lemma star_ext [simp]: "x ≤ x⇧⋆"
proof -
have "x ≤ x ⋅ x⇧⋆"
by (metis mult_oner mult_isol star_ref)
thus ?thesis
by (metis order_trans star_1l)
qed
text ‹We now prove a right star unfold law.›
lemma star_1r [simp]: "x⇧⋆ ⋅ x ≤ x⇧⋆"
proof -
have "x + x ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
thus ?thesis
by (fact star_inductl)
qed
lemma star_unfoldr: "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
by simp
lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
oops
text ‹Next we prove a simulation law for the star. It is
instrumental in proving further properties.›
lemma star_sim1: "x ⋅ z ≤ z ⋅ y ⟹ x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
proof -
assume "x ⋅ z ≤ z ⋅ y"
hence "x ⋅ z ⋅ y⇧⋆ ≤ z ⋅ y ⋅ y⇧⋆"
by (simp add: mult_isor)
also have "... ≤ z ⋅ y⇧⋆"
by (simp add: mult_isol mult_assoc)
finally have "x ⋅ z ⋅ y⇧⋆ ≤ z ⋅ y⇧⋆"
by simp
hence "z + x ⋅ z ⋅ y⇧⋆ ≤ z ⋅ y⇧⋆"
by (metis join.sup_least mult_isol mult_oner star_ref)
thus "x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
by (simp add: star_inductl mult_assoc)
qed
text ‹The next lemma is used in omega algebras to prove, for
instance, Bachmair and Dershowitz's separation of termination
theorem~\cite{bachmair86commutation}. The property at the left-hand
side of the equivalence is known as \emph{quasicommutation}.›
lemma quasicomm_var: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ ⟷ y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
proof
assume "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
thus "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
using star_sim1 by force
next
assume "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
thus "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
by (meson mult_isor order_trans star_ext)
qed
lemma star_slide1: "(x ⋅ y)⇧⋆ ⋅ x ≤ x ⋅ (y ⋅ x)⇧⋆"
by (simp add: mult_assoc star_sim1)
lemma "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
oops
lemma star_slide_var1: "x⇧⋆ ⋅ x ≤ x ⋅ x⇧⋆"
by (simp add: star_sim1)
text ‹We now show that the (left) star unfold axiom can be strengthened to an equality.›
lemma star_unfoldl_eq [simp]: "1 + x ⋅ x⇧⋆ = x⇧⋆"
proof (rule order.antisym)
show "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
by (fact star_unfoldl)
have "1 + x ⋅ (1 + x ⋅ x⇧⋆) ≤ 1 + x ⋅ x⇧⋆"
by (meson join.sup_mono eq_refl mult_isol star_unfoldl)
thus "x⇧⋆ ≤ 1 + x ⋅ x⇧⋆"
by (simp add: star_inductl_one)
qed
lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
oops
text ‹Next we relate the star and the reflexive transitive closure
operation.›
lemma star_rtc1_eq [simp]: "1 + x + x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
by (simp add: join.sup.absorb2)
lemma star_rtc1: "1 + x + x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
by simp
lemma star_rtc2: "1 + x ⋅ x ≤ x ⟷ x = x⇧⋆"
proof
assume "1 + x ⋅ x ≤ x"
thus "x = x⇧⋆"
by (simp add: order.eq_iff local.star_inductl_one)
next
assume "x = x⇧⋆"
thus "1 + x ⋅ x ≤ x"
using local.star_closed_unfold by auto
qed
lemma star_rtc3: "1 + x ⋅ x = x ⟷ x = x⇧⋆"
by (metis order_refl star_plus_one star_rtc2 star_trans_eq)
lemma star_rtc_least: "1 + x + y ⋅ y ≤ y ⟹ x⇧⋆ ≤ y"
proof -
assume "1 + x + y ⋅ y ≤ y"
hence "1 + x ⋅ y ≤ y"
by (metis join.le_sup_iff mult_isol_var star_trans_eq star_rtc2)
thus "x⇧⋆ ≤ y"
by (simp add: star_inductl_one)
qed
lemma star_rtc_least_eq: "1 + x + y ⋅ y = y ⟹ x⇧⋆ ≤ y"
by (simp add: star_rtc_least)
lemma "1 + x + y ⋅ y ≤ y ⟷ x⇧⋆ ≤ y"
oops
text ‹The next lemmas are again related to closure conditions›
lemma star_subdist_var_1: "x ≤ (x + y)⇧⋆"
by (meson join.sup.boundedE star_ext)
lemma star_subdist_var_2: "x ⋅ y ≤ (x + y)⇧⋆"
by (meson join.sup.boundedE prod_star_closure star_ext)
lemma star_subdist_var_3: "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by (simp add: prod_star_closure star_iso)
text ‹We now prove variants of sum-elimination laws under a star.
These are also known a denesting laws or as sum-star laws.›
lemma star_denest [simp]: "(x + y)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
proof (rule order.antisym)
have "x + y ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis join.sup.bounded_iff mult_1_right mult_isol_var mult_onel star_ref star_ext)
thus "(x + y)⇧⋆ ≤ (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (fact star_iso)
have "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by (fact star_subdist_var_3)
thus "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
by (simp add: prod_star_closure star_inductl_star)
qed
lemma star_sum_var [simp]: "(x⇧⋆ + y⇧⋆)⇧⋆ = (x + y)⇧⋆"
by simp
lemma star_denest_var [simp]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x + y)⇧⋆"
proof (rule order.antisym)
have "1 ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis mult_isol_var mult_oner star_ref)
moreover have "x ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (simp add: mult_isor)
moreover have "y ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis mult_isol_var mult_onel star_1l star_ref)
ultimately have "1 + (x + y) ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by auto
thus "(x + y)⇧⋆ ≤ x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆"
by (metis mult.assoc mult_oner star_inductl)
have "(y ⋅ x⇧⋆)⇧⋆ ≤ (y⇧⋆ ⋅ x⇧⋆)⇧⋆"
by (simp add: mult_isol_var star_iso)
hence "(y ⋅ x⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
by (metis add.commute star_denest)
moreover have "x⇧⋆ ≤ (x + y)⇧⋆"
by (fact star_subdist)
ultimately show "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
using prod_star_closure by blast
qed
lemma star_denest_var_2 [simp]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by simp
lemma star_denest_var_3 [simp]: "x⇧⋆ ⋅ (y⇧⋆ ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by simp
lemma star_denest_var_4 [ac_simps]: "(y⇧⋆ ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (metis add_comm star_denest)
lemma star_denest_var_5 [ac_simps]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = y⇧⋆ ⋅ (x ⋅ y⇧⋆)⇧⋆"
by (simp add: star_denest_var_4)
lemma "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
oops
lemma star_denest_var_6 [simp]: "x⇧⋆ ⋅ y⇧⋆ ⋅ (x + y)⇧⋆ = (x + y)⇧⋆"
using mult_assoc by simp
lemma star_denest_var_7 [simp]: "(x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ = (x + y)⇧⋆"
proof (rule order.antisym)
have "(x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (simp add: mult_assoc)
thus "(x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by simp
have "1 ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by (metis dual_order.trans mult_1_left mult_isor star_ref)
moreover have "(x + y) ⋅ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
using mult_isor star_1l by presburger
ultimately have "1 + (x + y) ⋅ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by simp
thus "(x + y)⇧⋆ ≤ (x + y)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆"
by (metis mult.assoc star_inductl_one)
qed
lemma star_denest_var_8 [simp]: "x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
by (simp add: mult_assoc)
lemma star_denest_var_9 [simp]: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ = (x⇧⋆ ⋅ y⇧⋆)⇧⋆"
using star_denest_var_7 by simp
text ‹The following statements are well known from term
rewriting. They are all variants of the Church-Rosser theorem in
Kleene algebra~\cite{struth06churchrosser}. But first we prove a law
relating two confluence properties.›
lemma confluence_var [iff]: "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟷ y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
proof
assume "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
thus "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
using star_sim1 by fastforce
next
assume "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
thus "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (meson mult_isor order_trans star_ext)
qed
lemma church_rosser [intro]: "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
proof (rule order.antisym)
assume "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
hence "x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆) ≤ x⇧⋆ ⋅ x⇧⋆ ⋅ y⇧⋆ ⋅ y⇧⋆"
by (metis mult_isol mult_isor mult.assoc)
hence "x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆) ≤ x⇧⋆ ⋅ y⇧⋆"
by (simp add: mult_assoc)
moreover have "1 ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis dual_order.trans mult_1_right mult_isol star_ref)
ultimately have "1 + x⇧⋆ ⋅ y⇧⋆ ⋅ (x⇧⋆ ⋅ y⇧⋆) ≤ x⇧⋆ ⋅ y⇧⋆"
by simp
hence "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (simp add: star_inductl_one)
thus "(x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by simp
thus "x⇧⋆ ⋅ y⇧⋆ ≤ (x + y)⇧⋆"
by simp
qed
lemma church_rosser_var: "y ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by fastforce
lemma church_rosser_to_confluence: "(x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis add_comm order.eq_iff star_subdist_var_3)
lemma church_rosser_equiv: "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟷ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
using church_rosser_to_confluence order.eq_iff by blast
lemma confluence_to_local_confluence: "y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆"
by (meson mult_isol_var order_trans star_ext)
lemma "y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ y⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
oops
lemma "y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
oops
text ‹
More variations could easily be proved. The last counterexample shows
that Newman's lemma needs a wellfoundedness assumption. This is well
known.
›
text ‹The next lemmas relate the reflexive transitive closure and
the transitive closure.›
lemma sup_id_star1: "1 ≤ x ⟹ x ⋅ x⇧⋆ = x⇧⋆"
proof -
assume "1 ≤ x"
hence " x⇧⋆ ≤ x ⋅ x⇧⋆"
using mult_isor by fastforce
thus "x ⋅ x⇧⋆ = x⇧⋆"
by (simp add: order.eq_iff)
qed
lemma sup_id_star2: "1 ≤ x ⟹ x⇧⋆ ⋅ x = x⇧⋆"
by (metis order.antisym mult_isol mult_oner star_1r)
lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
oops
lemma "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
oops
lemma "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
oops
end
subsection ‹Left Kleene Algebras›
class left_kleene_algebra = left_pre_kleene_algebra + dioid_one
begin
text ‹In left Kleene algebras the non-fact @{prop "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"}
is a good challenge for counterexample generators. A model of left
Kleene algebras in which the right star induction law does not hold
has been given by Kozen~\cite{kozen90kleene}.›
text ‹We now show that the right unfold law becomes an equality.›
lemma star_unfoldr_eq [simp]: "1 + x⇧⋆ ⋅ x = x⇧⋆"
proof (rule order.antisym)
show "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
by (fact star_unfoldr)
have "1 + x ⋅ (1 + x⇧⋆ ⋅ x) = 1 + (1 + x ⋅ x⇧⋆) ⋅ x"
using distrib_left distrib_right mult_1_left mult_1_right mult_assoc by presburger
also have "... = 1 + x⇧⋆ ⋅ x"
by simp
finally show "x⇧⋆ ≤ 1 + x⇧⋆ ⋅ x"
by (simp add: star_inductl_one)
qed
text ‹The following more complex unfold law has been used as an
axiom, called prodstar, by Conway~\cite{conway71regular}.›
lemma star_prod_unfold [simp]: "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y = (x ⋅ y)⇧⋆"
proof (rule order.antisym)
have "(x ⋅ y)⇧⋆ = 1 + (x ⋅ y)⇧⋆ ⋅ x ⋅ y"
by (simp add: mult_assoc)
thus "(x ⋅ y)⇧⋆ ≤ 1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y"
by (metis join.sup_mono mult_isor order_refl star_slide1)
have "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ≤ 1 + x ⋅ y ⋅ (x ⋅ y)⇧⋆"
by (metis join.sup_mono eq_refl mult.assoc mult_isol star_slide1)
thus "1 + x ⋅ (y ⋅ x)⇧⋆ ⋅ y ≤ (x ⋅ y)⇧⋆"
by simp
qed
text ‹The slide laws, which have previously been inequalities, now
become equations.›
lemma star_slide [ac_simps]: "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
proof -
have "x ⋅ (y ⋅ x)⇧⋆ = x ⋅ (1 + y ⋅ (x ⋅ y)⇧⋆ ⋅ x)"
by simp
also have "... = (1 + x ⋅ y ⋅ (x ⋅ y)⇧⋆) ⋅ x"
by (simp add: distrib_left mult_assoc)
finally show ?thesis
by simp
qed
lemma star_slide_var [ac_simps]: "x⇧⋆ ⋅ x = x ⋅ x⇧⋆"
by (metis mult_onel mult_oner star_slide)
lemma star_sum_unfold_var [simp]: "1 + x⇧⋆ ⋅ (x + y)⇧⋆ ⋅ y⇧⋆ = (x + y)⇧⋆"
by (metis star_denest star_denest_var_3 star_denest_var_4 star_plus_one star_slide)
text ‹The following law shows how starred sums can be unfolded.›
lemma star_sum_unfold [simp]: "x⇧⋆ + x⇧⋆ ⋅ y ⋅ (x + y)⇧⋆ = (x + y)⇧⋆"
proof -
have "(x + y)⇧⋆ = x⇧⋆ ⋅ (y ⋅ x⇧⋆ )⇧⋆"
by simp
also have "... = x⇧⋆ ⋅ (1 + y ⋅ x⇧⋆ ⋅ (y ⋅ x⇧⋆ )⇧⋆)"
by simp
also have "... = x⇧⋆ ⋅ (1 + y ⋅ (x + y)⇧⋆)"
by (simp add: mult.assoc)
finally show ?thesis
by (simp add: distrib_left mult_assoc)
qed
text ‹The following property appears in process algebra.›
lemma troeger: "(x + y)⇧⋆ ⋅ z = x⇧⋆ ⋅ (y ⋅ (x + y)⇧⋆ ⋅ z + z)"
proof -
have "(x + y)⇧⋆ ⋅ z = x⇧⋆ ⋅ z + x⇧⋆ ⋅ y ⋅ (x + y)⇧⋆ ⋅ z"
by (metis (full_types) distrib_right star_sum_unfold)
thus ?thesis
by (simp add: add_commute distrib_left mult_assoc)
qed
text ‹The following properties are related to a property from
propositional dynamic logic which has been attributed to Albert
Meyer~\cite{harelkozentiuryn00dynamic}. Here we prove it as a theorem
of Kleene algebra.›
lemma star_square: "(x ⋅ x)⇧⋆ ≤ x⇧⋆"
proof -
have "x ⋅ x ⋅ x⇧⋆ ≤ x⇧⋆"
by (simp add: prod_star_closure)
thus ?thesis
by (simp add: star_inductl_star)
qed
lemma meyer_1 [simp]: "(1 + x) ⋅ (x ⋅ x)⇧⋆ = x⇧⋆"
proof (rule order.antisym)
have "x ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ = x ⋅ (x ⋅ x)⇧⋆ + x ⋅ x ⋅ (x ⋅ x)⇧⋆"
by (simp add: distrib_left)
also have "... ≤ x ⋅ (x ⋅ x)⇧⋆ + (x ⋅ x)⇧⋆"
using join.sup_mono star_1l by blast
finally have "x ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (simp add: join.sup_commute)
moreover have "1 ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
using join.sup.coboundedI1 by auto
ultimately have "1 + x ⋅ (1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by auto
thus "x⇧⋆ ≤ (1 + x) ⋅ (x ⋅ x)⇧⋆"
by (simp add: star_inductl_one mult_assoc)
show "(1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ x⇧⋆"
by (simp add: prod_star_closure star_square)
qed
text ‹The following lemma says that transitive elements are equal to
their transitive closure.›
lemma tc: "x ⋅ x ≤ x ⟹ x⇧⋆ ⋅ x = x"
proof -
assume "x ⋅ x ≤ x"
hence "x + x ⋅ x ≤ x"
by simp
hence "x⇧⋆ ⋅ x ≤ x"
by (fact star_inductl)
thus "x⇧⋆ ⋅ x = x"
by (metis mult_isol mult_oner star_ref star_slide_var order.eq_iff)
qed
lemma tc_eq: "x ⋅ x = x ⟹ x⇧⋆ ⋅ x = x"
by (auto intro: tc)
text ‹The next fact has been used by Boffa~\cite{boffa90remarque} to
axiomatise the equational theory of regular expressions.›
lemma boffa_var: "x ⋅ x ≤ x ⟹ x⇧⋆ = 1 + x"
proof -
assume "x ⋅ x ≤ x"
moreover have "x⇧⋆ = 1 + x⇧⋆ ⋅ x"
by simp
ultimately show "x⇧⋆ = 1 + x"
by (simp add: tc)
qed
lemma boffa: "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
by (auto intro: boffa_var)
end
subsection ‹Left Kleene Algebras with Zero›
text ‹
There are applications where only a left zero is assumed, for instance
in the context of total correctness and for demonic refinement
algebras~\cite{vonwright04refinement}.
›
class left_kleene_algebra_zerol = left_kleene_algebra + dioid_one_zerol
begin
sublocale conway: near_conway_base_zerol star
by standard (simp_all add: local.star_slide)
lemma star_zero [simp]: "0⇧⋆ = 1"
by (rule local.conway.zero_dagger)
text ‹
In principle,~$1$ could therefore be defined from~$0$ in this setting.
›
end
class left_kleene_algebra_zero = left_kleene_algebra_zerol + dioid_one_zero
subsection ‹Pre-Kleene Algebras›
text ‹Pre-Kleene algebras are essentially probabilistic Kleene
algebras~\cite{mciverweber05pka}. They have a weaker right star
unfold axiom. We are still looking for theorems that could be proved
in this setting.›
class pre_kleene_algebra = left_pre_kleene_algebra +
assumes weak_star_unfoldr: "z + y ⋅ (x + 1) ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
subsection ‹Kleene Algebras›
class kleene_algebra_zerol = left_kleene_algebra_zerol +
assumes star_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
begin
lemma star_sim2: "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧⋆ ≤ y⇧⋆ ⋅ z"
proof -
assume "z ⋅ x ≤ y ⋅ z"
hence "y⇧⋆ ⋅ z ⋅ x ≤ y⇧⋆ ⋅ y ⋅ z"
using mult_isol mult_assoc by auto
also have "... ≤ y⇧⋆ ⋅ z"
by (simp add: mult_isor)
finally have "y⇧⋆ ⋅ z ⋅ x ≤ y⇧⋆ ⋅ z"
by simp
moreover have "z ≤ y⇧⋆ ⋅ z"
using mult_isor star_ref by fastforce
ultimately have "z + y⇧⋆ ⋅ z ⋅ x ≤ y⇧⋆ ⋅ z"
by simp
thus "z ⋅ x⇧⋆ ≤ y⇧⋆ ⋅ z"
by (simp add: star_inductr)
qed
sublocale conway: pre_conway star
by standard (simp add: star_sim2)
lemma star_inductr_var: "y ⋅ x ≤ y ⟹ y ⋅ x⇧⋆ ≤ y"
by (simp add: star_inductr)
lemma star_inductr_var_equiv: "y ⋅ x ≤ y ⟷ y ⋅ x⇧⋆ ≤ y"
by (meson order_trans mult_isol star_ext star_inductr_var)
lemma star_sim3: "z ⋅ x = y ⋅ z ⟹ z ⋅ x⇧⋆ = y⇧⋆ ⋅ z"
by (simp add: order.eq_iff star_sim1 star_sim2)
lemma star_sim4: "x ⋅ y ≤ y ⋅ x ⟹ x⇧⋆ ⋅ y⇧⋆ ≤ y⇧⋆ ⋅ x⇧⋆"
by (auto intro: star_sim1 star_sim2)
lemma star_inductr_eq: "z + y ⋅ x = y ⟹ z ⋅ x⇧⋆ ≤ y"
by (auto intro: star_inductr)
lemma star_inductr_var_eq: "y ⋅ x = y ⟹ y ⋅ x⇧⋆ ≤ y"
by (auto intro: star_inductr_var)
lemma star_inductr_var_eq2: "y ⋅ x = y ⟹ y ⋅ x⇧⋆ = y"
by (metis mult_onel star_one star_sim3)
lemma bubble_sort: "y ⋅ x ≤ x ⋅ y ⟹ (x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by (fastforce intro: star_sim4)
lemma independence1: "x ⋅ y = 0 ⟹ x⇧⋆ ⋅ y = y"
proof -
assume "x ⋅ y = 0"
moreover have "x⇧⋆ ⋅ y = y + x⇧⋆ ⋅ x ⋅ y"
by (metis distrib_right mult_onel star_unfoldr_eq)
ultimately show "x⇧⋆ ⋅ y = y"
by (metis add_0_left add.commute join.sup_ge1 order.eq_iff star_inductl_eq)
qed
lemma independence2: "x ⋅ y = 0 ⟹ x ⋅ y⇧⋆ = x"
by (metis annil mult_onel star_sim3 star_zero)
lemma lazycomm_var: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ + y ⟷ y ⋅ x⇧⋆ ≤ x ⋅ (x + y)⇧⋆ + y"
proof
let ?t = "x ⋅ (x + y)⇧⋆"
assume hyp: "y ⋅ x ≤ ?t + y"
have "(?t + y) ⋅ x = ?t ⋅ x + y ⋅ x"
by (fact distrib_right)
also have "... ≤ ?t ⋅ x + ?t + y"
using hyp join.sup.coboundedI2 join.sup_assoc by auto
also have "... ≤ ?t + y"
using eq_refl join.sup_least join.sup_mono mult_isol prod_star_closure star_subdist_var_1 mult_assoc by presburger
finally have "y + (?t + y) ⋅ x ≤ ?t + y"
by simp
thus "y ⋅ x⇧⋆ ≤ x ⋅ (x + y)⇧⋆ + y"
by (fact star_inductr)
next
assume "y ⋅ x⇧⋆ ≤ x ⋅ (x + y)⇧⋆ + y"
thus "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ + y"
using dual_order.trans mult_isol star_ext by blast
qed
lemma arden_var: "(∀y v. y ≤ x ⋅ y + v ⟶ y ≤ x⇧⋆ ⋅ v) ⟹ z = x ⋅ z + w ⟹ z = x⇧⋆ ⋅ w"
by (auto simp: add_comm order.eq_iff star_inductl_eq)
lemma "(∀x y. y ≤ x ⋅ y ⟶ y = 0) ⟹ y ≤ x ⋅ y + z ⟹ y ≤ x⇧⋆ ⋅ z"
by (metis eq_refl mult_onel)
end
text ‹Finally, here come the Kleene algebras \`a~la
Kozen~\cite{kozen94complete}. We only prove quasi-identities in this
section. Since left Kleene algebras are complete with respect to the
equational theory of regular expressions and regular languages, all
identities hold already without the right star induction axiom.›
class kleene_algebra = left_kleene_algebra_zero +
assumes star_inductr': "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
begin
subclass kleene_algebra_zerol
by standard (simp add: star_inductr')
sublocale conway_zerol: conway star ..
text ‹
The next lemma shows that opposites of Kleene algebras (i.e., Kleene
algebras with the order of multiplication swapped) are again Kleene
algebras.
›
lemma dual_kleene_algebra:
"class.kleene_algebra (+) (⊙) 1 0 (≤) (<) star"
proof
fix x y z :: 'a
show "(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"
by (metis mult.assoc opp_mult_def)
show "(x + y) ⊙ z = x ⊙ z + y ⊙ z"
by (metis opp_mult_def distrib_left)
show "1 ⊙ x = x"
by (metis mult_oner opp_mult_def)
show "x ⊙ 1 = x"
by (metis mult_onel opp_mult_def)
show "0 + x = x"
by (fact add_zerol)
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "x + x = x"
by (fact add_idem)
show "x ⊙ (y + z) = x ⊙ y + x ⊙ z"
by (metis distrib_right opp_mult_def)
show "z ⊙ x ≤ z ⊙ (x + y)"
by (metis mult_isor opp_mult_def order_prop)
show "1 + x ⊙ x⇧⋆ ≤ x⇧⋆"
by (metis opp_mult_def order_refl star_slide_var star_unfoldl_eq)
show "z + x ⊙ y ≤ y ⟹ x⇧⋆ ⊙ z ≤ y"
by (metis opp_mult_def star_inductr)
show "z + y ⊙ x ≤ y ⟹ z ⊙ x⇧⋆ ≤ y"
by (metis opp_mult_def star_inductl)
qed
end
text ‹We finish with some properties on (multiplicatively)
commutative Kleene algebras. A chapter in Conway's
book~\cite{conway71regular} is devoted to this topic.›
class commutative_kleene_algebra = kleene_algebra +
assumes mult_comm [ac_simps]: "x ⋅ y = y ⋅ x"
begin
lemma conway_c3 [simp]: "(x + y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
using church_rosser mult_comm by auto
lemma conway_c4: "(x⇧⋆ ⋅ y)⇧⋆ = 1 + x⇧⋆ ⋅ y⇧⋆ ⋅ y"
by (metis conway_c3 star_denest_var star_prod_unfold)
lemma cka_1: "(x ⋅ y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis conway_c3 star_invol star_iso star_subdist_var_2)
lemma cka_2 [simp]: "x⇧⋆ ⋅ (x⇧⋆ ⋅ y)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by (metis conway_c3 mult_comm star_denest_var)
lemma conway_c4_var [simp]: "(x⇧⋆ ⋅ y⇧⋆)⇧⋆ = x⇧⋆ ⋅ y⇧⋆"
by (metis conway_c3 star_invol)
lemma conway_c2_var: "(x ⋅ y)⇧⋆ ⋅ x ⋅ y ⋅ y⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ y⇧⋆"
by (metis mult_isor star_1r mult_assoc)
lemma conway_c2 [simp]: "(x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) = x⇧⋆ ⋅ y⇧⋆"
proof (rule order.antisym)
show "(x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) ≤ x⇧⋆ ⋅ y⇧⋆"
by (metis cka_1 conway_c3 prod_star_closure star_ext star_sum_var)
have "x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) = x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + 1 + y ⋅ y⇧⋆)"
by (simp add: add_assoc)
also have "... = x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y ⋅ y⇧⋆)"
by (simp add: add_commute)
also have "... = (x ⋅ y)⇧⋆ ⋅ (x ⋅ x⇧⋆) + (x ⋅ y)⇧⋆ ⋅ x ⋅ y ⋅ y⇧⋆"
using distrib_left mult_comm mult_assoc by force
also have "... ≤ (x ⋅ y)⇧⋆ ⋅ x⇧⋆ + (x ⋅ y)⇧⋆ ⋅ x ⋅ y ⋅ y⇧⋆"
using add_iso mult_isol by force
also have "... ≤ (x ⋅ y)⇧⋆ ⋅ x⇧⋆ + (x ⋅ y)⇧⋆ ⋅ y⇧⋆"
using conway_c2_var join.sup_mono by blast
also have "... = (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by (simp add: distrib_left)
finally have "x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)" .
moreover have "y⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by (metis dual_order.trans join.sup_ge2 mult_1_left mult_isor star_ref)
ultimately have "y⇧⋆ + x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆) ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by simp
thus "x⇧⋆ ⋅ y⇧⋆ ≤ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
by (simp add: mult.assoc star_inductl)
qed
end
end
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}.›
datatype 'a rexp =
Zero
| One
| Atom 'a
| Plus "'a rexp" "'a rexp"
| Times "'a rexp" "'a rexp"
| Star "'a rexp"
text ‹The interpretation map that induces regular languages as the
images of regular expressions in the set of languages has also been
adapted from there.›
fun lang :: "'a rexp ⇒ 'a lan" where
"lang Zero = 0"
| "lang One = 1"
| "lang (Atom a) = {[a]}"
| "lang (Plus x y) = lang x + lang y"
| "lang (Times x y) = lang x ⋅ lang y"
| "lang (Star x) = (lang x)⇧⋆"
typedef 'a reg_lan = "range lang :: 'a lan set"
by auto
setup_lifting type_definition_reg_lan
instantiation reg_lan :: (type) kleene_algebra
begin
lift_definition star_reg_lan :: "'a reg_lan ⇒ 'a reg_lan"
is star
by (metis (hide_lams, no_types) image_iff lang.simps(6) rangeI)
lift_definition zero_reg_lan :: "'a reg_lan"
is 0
by (metis lang.simps(1) rangeI)
lift_definition one_reg_lan :: "'a reg_lan"
is 1
by (metis lang.simps(2) rangeI)
lift_definition less_eq_reg_lan :: "'a reg_lan ⇒ 'a reg_lan ⇒ bool"
is less_eq .
lift_definition less_reg_lan :: "'a reg_lan ⇒ 'a reg_lan ⇒ bool"
is less .
lift_definition plus_reg_lan :: "'a reg_lan ⇒ 'a reg_lan ⇒ 'a reg_lan"
is plus
by (metis (hide_lams, no_types) image_iff lang.simps(4) rangeI)
lift_definition times_reg_lan :: "'a reg_lan ⇒ 'a reg_lan ⇒ 'a reg_lan"
is times
by (metis (hide_lams, no_types) image_iff lang.simps(5) rangeI)
instance
proof
fix x y z :: "'a reg_lan"
show "x + y + z = x + (y + z)"
by transfer (metis join_semilattice_class.add_assoc')
show "x + y = y + x"
by transfer (metis join_semilattice_class.add_comm)
show "x ⋅ y ⋅ z = x ⋅ (y ⋅ z)"
by transfer (metis semigroup_mult_class.mult.assoc)
show "(x + y) ⋅ z = x ⋅ z + y ⋅ z"
by transfer (metis semiring_class.distrib_right)
show "1 ⋅ x = x"
by transfer (metis monoid_mult_class.mult_1_left)
show "x ⋅ 1 = x"
by transfer (metis monoid_mult_class.mult_1_right)
show "0 + x = x"
by transfer (metis join_semilattice_zero_class.add_zero_l)
show "0 ⋅ x = 0"
by transfer (metis ab_near_semiring_one_zerol_class.annil)
show "x ⋅ 0 = 0"
by transfer (metis ab_near_semiring_one_zero_class.annir)
show "x ≤ y ⟷ x + y = y"
by transfer (metis plus_ord_class.less_eq_def)
show "x < y ⟷ x ≤ y ∧ x ≠ y"
by transfer (metis plus_ord_class.less_def)
show "x + x = x"
by transfer (metis join_semilattice_class.add_idem)
show "x ⋅ (y + z) = x ⋅ y + x ⋅ z"
by transfer (metis semiring_class.distrib_left)
show "z ⋅ x ≤ z ⋅ (x + y)"
by transfer (metis pre_dioid_class.subdistl)
show "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
by transfer (metis star_unfoldl)
show "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
by transfer (metis star_inductl)
show "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
by transfer (metis star_inductr)
qed
end
interpretation reg_lan_kleene_algebra: kleene_algebra "(+)" "(⋅)" "1::'a reg_lan" 0 "(≤)" "(<)" star ..
subsection ‹Relation Kleene Algebras›
text ‹We now show that binary relations form Kleene algebras. While
we could have used the reflexive transitive closure operation as the
Kleene star, we prefer the equivalent definition of the star as the
sum of powers. This essentially allows us to copy previous proofs.›
lemma power_is_relpow: "rel_dioid.power X n = X ^^ n"
proof (induct n)
case 0 show ?case
by (metis rel_dioid.power_0 relpow.simps(1))
case Suc thus ?case
by (metis rel_dioid.power_Suc2 relpow.simps(2))
qed
lemma rel_star_def: "X^* = (⋃n. rel_dioid.power X n)"
by (simp add: power_is_relpow rtrancl_is_UN_relpow)
lemma rel_star_contl: "X O Y^* = (⋃n. X O rel_dioid.power Y n)"
by (metis rel_star_def relcomp_UNION_distrib)
lemma rel_star_contr: "X^* O Y = (⋃n. (rel_dioid.power X n) O Y)"
by (metis rel_star_def relcomp_UNION_distrib2)
interpretation rel_kleene_algebra: kleene_algebra "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl
proof
fix x y z :: "'a rel"
show "Id ∪ x O x⇧* ⊆ x⇧*"
by (metis order_refl r_comp_rtrancl_eq rtrancl_unfold)
next
fix x y z :: "'a rel"
assume "z ∪ x O y ⊆ y"
thus "x⇧* O z ⊆ y"
by (simp only: rel_star_contr, metis (lifting) SUP_le_iff rel_dioid.power_inductl)
next
fix x y z :: "'a rel"
assume "z ∪ y O x ⊆ y"
thus "z O x⇧* ⊆ y"
by (simp only: rel_star_contl, metis (lifting) SUP_le_iff rel_dioid.power_inductr)
qed
subsection ‹Trace Kleene Algebras›
text ‹Again, the proof that sets of traces form Kleene algebras
follows the same schema.›
definition t_star :: "('p, 'a) trace set ⇒ ('p, 'a) trace set" where
"t_star X ≡ ⋃n. trace_dioid.power X n"
lemma t_star_elim: "x ∈ t_star X ⟷ (∃n. x ∈ trace_dioid.power X n)"
by (simp add: t_star_def)
lemma t_star_contl: "t_prod X (t_star Y) = (⋃n. t_prod X (trace_dioid.power Y n))"
by (auto simp add: t_star_elim t_prod_def)
lemma t_star_contr: "t_prod (t_star X) Y = (⋃n. t_prod (trace_dioid.power X n) Y)"
by (auto simp add: t_star_elim t_prod_def)
interpretation trace_kleene_algebra: kleene_algebra "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)" t_star
proof
fix X Y Z :: "('a, 'b) trace set"
show "t_one ∪ t_prod X (t_star X) ⊆ t_star X"
proof -
have "t_one ∪ t_prod X (t_star X) = (trace_dioid.power X 0) ∪ (⋃n. trace_dioid.power X (Suc n))"
by (auto simp add: t_star_def t_prod_def)
also have "... = (⋃n. trace_dioid.power X n)"
by (metis Un_0_Suc)
also have "... = t_star X"
by (metis t_star_def)
finally show ?thesis
by (metis subset_refl)
qed
show "Z ∪ t_prod X Y ⊆ Y ⟹ t_prod (t_star X) Z ⊆ Y"
by (simp only: ball_UNIV t_star_contr SUP_le_iff) (metis trace_dioid.power_inductl)
show "Z ∪ t_prod Y X ⊆ Y ⟹ t_prod Z (t_star X) ⊆ Y"
by (simp only: ball_UNIV t_star_contl SUP_le_iff) (metis trace_dioid.power_inductr)
qed
subsection ‹Path Kleene Algebras›
text ‹We start with paths that include the empty path.›
definition p_star :: "'a path set ⇒ 'a path set" where
"p_star X ≡ ⋃n. path_dioid.power X n"
lemma p_star_elim: "x ∈ p_star X ⟷ (∃n. x ∈ path_dioid.power X n)"
by (simp add: p_star_def)
lemma p_star_contl: "p_prod X (p_star Y) = (⋃n. p_prod X (path_dioid.power Y n))"
apply (auto simp add: p_prod_def p_star_elim)
apply (metis p_fusion.simps(1))
apply metis
apply (metis p_fusion.simps(1) p_star_elim)
apply (metis p_star_elim)
done
lemma p_star_contr: "p_prod (p_star X) Y = (⋃n. p_prod (path_dioid.power X n) Y)"
apply (auto simp add: p_prod_def p_star_elim)
apply (metis p_fusion.simps(1))
apply metis
apply (metis p_fusion.simps(1) p_star_elim)
apply (metis p_star_elim)
done
interpretation path_kleene_algebra: kleene_algebra "(∪)" p_prod p_one "{}" "(⊆)" "(⊂)" p_star
proof
fix X Y Z :: "'a path set"
show "p_one ∪ p_prod X (p_star X) ⊆ p_star X"
proof -
have "p_one ∪ p_prod X (p_star X) = (path_dioid.power X 0) ∪ (⋃n. path_dioid.power X (Suc n))"
by (auto simp add: p_star_def p_prod_def)
also have "... = (⋃n. path_dioid.power X n)"
by (metis Un_0_Suc)
also have "... = p_star X"
by (metis p_star_def)
finally show ?thesis
by (metis subset_refl)
qed
show "Z ∪ p_prod X Y ⊆ Y ⟹ p_prod (p_star X) Z ⊆ Y"
by (simp only: ball_UNIV p_star_contr SUP_le_iff) (metis path_dioid.power_inductl)
show "Z ∪ p_prod Y X ⊆ Y ⟹ p_prod Z (p_star X) ⊆ Y"
by (simp only: ball_UNIV p_star_contl SUP_le_iff) (metis path_dioid.power_inductr)
qed
text ‹We now consider a notion of paths that does not include the
empty path.›
definition pp_star :: "'a ppath set ⇒ 'a ppath set" where
"pp_star X ≡ ⋃n. ppath_dioid.power X n"
lemma pp_star_elim: "x ∈ pp_star X ⟷ (∃n. x ∈ ppath_dioid.power X n)"
by (simp add: pp_star_def)
lemma pp_star_contl: "pp_prod X (pp_star Y) = (⋃n. pp_prod X (ppath_dioid.power Y n))"
by (auto simp add: pp_prod_def pp_star_elim)
lemma pp_star_contr: "pp_prod (pp_star X) Y = (⋃n. pp_prod (ppath_dioid.power X n) Y)"
by (auto simp add: pp_prod_def pp_star_elim)
interpretation ppath_kleene_algebra: kleene_algebra "(∪)" pp_prod pp_one "{}" "(⊆)" "(⊂)" pp_star
proof
fix X Y Z :: "'a ppath set"
show "pp_one ∪ pp_prod X (pp_star X) ⊆ pp_star X"
proof -
have "pp_one ∪ pp_prod X (pp_star X) = (ppath_dioid.power X 0) ∪ (⋃n. ppath_dioid.power X (Suc n))"
by (auto simp add: pp_star_def pp_prod_def)
also have "... = (⋃n. ppath_dioid.power X n)"
by (metis Un_0_Suc)
also have "... = pp_star X"
by (metis pp_star_def)
finally show ?thesis
by (metis subset_refl)
qed
show "Z ∪ pp_prod X Y ⊆ Y ⟹ pp_prod (pp_star X) Z ⊆ Y"
by (simp only: ball_UNIV pp_star_contr SUP_le_iff) (metis ppath_dioid.power_inductl)
show "Z ∪ pp_prod Y X ⊆ Y ⟹ pp_prod Z (pp_star X) ⊆ Y"
by (simp only: ball_UNIV pp_star_contl SUP_le_iff) (metis ppath_dioid.power_inductr)
qed
subsection ‹The Distributive Lattice Kleene Algebra›
text ‹In the case of bounded distributive lattices, the star maps
all elements to to the maximal element.›
definition (in bounded_distributive_lattice) bdl_star :: "'a ⇒ 'a" where
"bdl_star x = top"
sublocale bounded_distributive_lattice ⊆ kleene_algebra sup inf top bot less_eq less bdl_star
proof
fix x y z :: 'a
show "sup top (inf x (bdl_star x)) ≤ bdl_star x"
by (simp add: bdl_star_def)
show "sup z (inf x y) ≤ y ⟹ inf (bdl_star x) z ≤ y"
by (simp add: bdl_star_def)
show "sup z (inf y x) ≤ y ⟹ inf z (bdl_star x) ≤ y"
by (simp add: bdl_star_def)
qed
subsection ‹The Min-Plus Kleene Algebra›
text ‹One cannot define a Kleene star for max-plus and min-plus
algebras that range over the real numbers. Here we define the star for
a min-plus algebra restricted to natural numbers and~$+\infty$. The
resulting Kleene algebra is commutative. Similar variants can be
obtained for max-plus algebras and other algebras ranging over the
positive or negative integers.›
instantiation pnat :: commutative_kleene_algebra
begin
definition star_pnat where
"x⇧⋆ ≡ (1::pnat)"
instance
proof
fix x y z :: pnat
show "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
by (metis star_pnat_def zero_pnat_top)
show "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
by (simp add: star_pnat_def)
show "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
by (simp add: star_pnat_def)
show "x ⋅ y = y ⋅ x"
unfolding times_pnat_def by (cases x, cases y, simp_all)
qed
end
end
Theory Omega_Algebra
section ‹Omega Algebras›
theory Omega_Algebra
imports Kleene_Algebra
begin
text ‹
\emph{Omega algebras}~\cite{cohen00omega} extend Kleene algebras by an
$\omega$-operation that axiomatizes infinite iteration (just like the
Kleene star axiomatizes finite iteration).
›
subsection ‹Left Omega Algebras›
text ‹
In this section we consider \emph{left omega algebras}, i.e., omega
algebras based on left Kleene algebras. Surprisingly, we are still
looking for statements mentioning~$\omega$ that are true in omega
algebras, but do not already hold in left omega algebras.
›
class left_omega_algebra = left_kleene_algebra_zero + omega_op +
assumes omega_unfold: "x⇧ω ≤ x ⋅ x⇧ω"
and omega_coinduct: "y ≤ z + x ⋅ y ⟹ y ≤ x⇧ω + x⇧⋆ ⋅ z"
begin
text ‹First we prove some variants of the coinduction axiom.›
lemma omega_coinduct_var1: "y ≤ 1 + x ⋅ y ⟹ y ≤ x⇧ω + x⇧⋆"
using local.omega_coinduct by fastforce
lemma omega_coinduct_var2: "y ≤ x ⋅ y ⟹ y ≤ x⇧ω"
by (metis add.commute add_zero_l annir omega_coinduct)
lemma omega_coinduct_eq: "y = z + x ⋅ y ⟹ y ≤ x⇧ω + x⇧⋆ ⋅ z"
by (simp add: local.omega_coinduct)
lemma omega_coinduct_eq_var1: "y = 1 + x ⋅ y ⟹ y ≤ x⇧ω + x⇧⋆"
by (simp add: omega_coinduct_var1)
lemma omega_coinduct_eq_var2: "y = x ⋅ y ⟹ y ≤ x⇧ω"
by (simp add: omega_coinduct_var2)
lemma "y = x ⋅ y + z ⟹ y = x⇧⋆ ⋅ z + x⇧ω"
oops
lemma "y = 1 + x ⋅ y ⟹ y = x⇧ω + x⇧⋆"
oops
lemma "y = x ⋅ y ⟹ y = x⇧ω"
oops
text ‹Next we strengthen the unfold law to an equation.›
lemma omega_unfold_eq [simp]: "x ⋅ x⇧ω = x⇧ω"
proof (rule order.antisym)
have "x ⋅ x⇧ω ≤ x ⋅ x ⋅ x⇧ω"
by (simp add: local.mult_isol local.omega_unfold mult_assoc)
thus "x ⋅ x⇧ω ≤ x⇧ω"
by (simp add: mult_assoc omega_coinduct_var2)
show "x⇧ω ≤ x ⋅ x⇧ω"
by (fact omega_unfold)
qed
lemma omega_unfold_var: "z + x ⋅ x⇧ω ≤ x⇧ω + x⇧⋆ ⋅ z"
by (simp add: local.omega_coinduct)
lemma "z + x ⋅ x⇧ω = x⇧ω + x⇧⋆ ⋅ z"
oops
text ‹We now prove subdistributivity and isotonicity of omega.›
lemma omega_subdist: "x⇧ω ≤ (x + y)⇧ω"
proof -
have "x⇧ω ≤ (x + y) ⋅ x⇧ω"
by simp
thus ?thesis
by (rule omega_coinduct_var2)
qed
lemma omega_iso: "x ≤ y ⟹ x⇧ω ≤ y⇧ω"
by (metis less_eq_def omega_subdist)
lemma omega_subdist_var: "x⇧ω + y⇧ω ≤ (x + y)⇧ω"
by (simp add: omega_iso)
lemma zero_omega [simp]: "0⇧ω = 0"
by (metis annil omega_unfold_eq)
text ‹The next lemma is another variant of omega unfold›
lemma star_omega_1 [simp]: "x⇧⋆ ⋅ x⇧ω = x⇧ω"
proof (rule order.antisym)
have "x ⋅ x⇧ω ≤ x⇧ω"
by simp
thus "x⇧⋆ ⋅ x⇧ω ≤ x⇧ω"
by simp
show "x⇧ω ≤ x⇧⋆ ⋅ x⇧ω"
using local.star_inductl_var_eq2 by auto
qed
text ‹The next lemma says that~@{term "1⇧ω"} is the maximal element
of omega algebra. We therefore baptise it~$\top$.›
lemma max_element: "x ≤ 1⇧ω"
by (simp add: omega_coinduct_eq_var2)
definition top ("⊤")
where "⊤ = 1⇧ω"
lemma star_omega_3 [simp]: "(x⇧⋆)⇧ω = ⊤"
proof -
have "1 ≤ x⇧⋆"
by (fact star_ref)
hence "⊤ ≤ (x⇧⋆)⇧ω"
by (simp add: omega_iso top_def)
thus ?thesis
by (simp add: local.order.antisym max_element top_def)
qed
text ‹The following lemma is strange since it is counterintuitive
that one should be able to append something after an infinite
iteration.›
lemma omega_1: "x⇧ω ⋅ y ≤ x⇧ω"
proof -
have "x⇧ω ⋅ y ≤ x ⋅ x⇧ω ⋅ y"
by simp
thus ?thesis
by (metis mult.assoc omega_coinduct_var2)
qed
lemma "x⇧ω ⋅ y = x⇧ω"
oops
lemma omega_sup_id: "1 ≤ y ⟹ x⇧ω ⋅ y = x⇧ω"
using order.eq_iff local.mult_isol omega_1 by fastforce
lemma omega_top [simp]: "x⇧ω ⋅ ⊤ = x⇧ω"
by (simp add: max_element omega_sup_id top_def)
lemma supid_omega: "1 ≤ x ⟹ x⇧ω = ⊤"
by (simp add: local.order.antisym max_element omega_iso top_def)
lemma "x⇧ω = ⊤ ⟹ 1 ≤ x"
oops
text ‹Next we prove a simulation law for the omega operation›
lemma omega_simulation: "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧ω ≤ y⇧ω"
proof -
assume hyp: "z ⋅ x ≤ y ⋅ z"
have "z ⋅ x⇧ω = z ⋅ x ⋅ x⇧ω"
by (simp add: mult_assoc)
also have "... ≤ y ⋅ z ⋅ x⇧ω"
by (simp add: hyp local.mult_isor)
finally show "z ⋅ x⇧ω ≤ y⇧ω"
by (simp add: mult_assoc omega_coinduct_var2)
qed
lemma "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧ω ≤ y⇧ω ⋅ z"
oops
lemma "y ⋅ z ≤ z ⋅ x ⟹ y⇧ω ≤ z ⋅ x⇧ω"
oops
lemma "y ⋅ z ≤ z ⋅ x ⟹ y⇧ω ⋅ z ≤ x⇧ω"
oops
text ‹Next we prove transitivity of omega elements.›
lemma omega_omega: "(x⇧ω)⇧ω ≤ x⇧ω"
by (metis omega_1 omega_unfold_eq)
text ‹The next lemmas are axioms of Wagner's complete axiomatisation
for omega-regular languages~\cite{Wagner77omega}, but in a slightly
different setting.›
lemma wagner_1 [simp]: "(x ⋅ x⇧⋆)⇧ω = x⇧ω"
proof (rule order.antisym)
have "(x ⋅ x⇧⋆)⇧ω = x ⋅ x⇧⋆ ⋅ x ⋅ x⇧⋆ ⋅ (x ⋅ x⇧⋆)⇧ω"
by (metis mult.assoc omega_unfold_eq)
also have "... = x ⋅ x ⋅ x⇧⋆ ⋅ x⇧⋆ ⋅ (x ⋅ x⇧⋆)⇧ω"
by (simp add: local.star_slide_var mult_assoc)
also have "... = x ⋅ x ⋅ x⇧⋆ ⋅ (x ⋅ x⇧⋆)⇧ω"
by (simp add: mult_assoc)
also have "... = x ⋅ (x ⋅ x⇧⋆)⇧ω"
by (simp add: mult_assoc)
thus "(x ⋅ x⇧⋆)⇧ω ≤ x⇧ω"
using calculation omega_coinduct_eq_var2 by auto
show "x⇧ω ≤ (x ⋅ x⇧⋆)⇧ω"
by (simp add: mult_assoc omega_coinduct_eq_var2)
qed
lemma wagner_2_var: "x ⋅ (y ⋅ x)⇧ω ≤ (x ⋅ y)⇧ω"
proof -
have "x ⋅ y ⋅ x ≤ x ⋅ y ⋅ x"
by auto
thus "x ⋅ (y ⋅ x)⇧ω ≤ (x ⋅ y)⇧ω"
by (simp add: mult_assoc omega_simulation)
qed
lemma wagner_2 [simp]: "x ⋅ (y ⋅ x)⇧ω = (x ⋅ y)⇧ω"
proof (rule order.antisym)
show "x ⋅ (y ⋅ x)⇧ω ≤ (x ⋅ y)⇧ω"
by (rule wagner_2_var)
have "(x ⋅ y)⇧ω = x ⋅ y ⋅ (x ⋅ y)⇧ω"
by simp
thus "(x ⋅ y)⇧ω ≤ x ⋅ (y ⋅ x)⇧ω"
by (metis mult.assoc mult_isol wagner_2_var)
qed
text ‹
This identity is called~(A8) in Wagner's paper.
›
lemma wagner_3:
assumes "x ⋅ (x + y)⇧ω + z = (x + y)⇧ω"
shows "(x + y)⇧ω = x⇧ω + x⇧⋆ ⋅ z"
proof (rule order.antisym)
show "(x + y)⇧ω ≤ x⇧ω + x⇧⋆ ⋅ z"
using assms local.join.sup_commute omega_coinduct_eq by auto
have "x⇧⋆ ⋅ z ≤ (x + y)⇧ω"
using assms local.join.sup_commute local.star_inductl_eq by auto
thus "x⇧ω + x⇧⋆ ⋅ z ≤ (x + y)⇧ω"
by (simp add: omega_subdist)
qed
text ‹
This identity is called~(R4) in Wagner's paper.
›
lemma wagner_1_var [simp]: "(x⇧⋆ ⋅ x)⇧ω = x⇧ω"
by (simp add: local.star_slide_var)
lemma star_omega_4 [simp]: "(x⇧ω)⇧⋆ = 1 + x⇧ω"
proof (rule order.antisym)
have "(x⇧ω)⇧⋆ = 1 + x⇧ω ⋅ (x⇧ω)⇧⋆"
by simp
also have "... ≤ 1 + x⇧ω ⋅ ⊤"
by (simp add: omega_sup_id)
finally show "(x⇧ω)⇧⋆ ≤ 1 + x⇧ω"
by simp
show "1 + x⇧ω ≤ (x⇧ω)⇧⋆"
by simp
qed
lemma star_omega_5 [simp]: "x⇧ω ⋅ (x⇧ω)⇧⋆ = x⇧ω"
proof (rule order.antisym)
show "x⇧ω ⋅ (x⇧ω)⇧⋆ ≤ x⇧ω"
by (rule omega_1)
show "x⇧ω ≤ x⇧ω ⋅ (x⇧ω)⇧⋆"
by (simp add: omega_sup_id)
qed
text ‹The next law shows how omegas below a sum can be unfolded.›
lemma omega_sum_unfold: "x⇧ω + x⇧⋆ ⋅ y ⋅ (x + y)⇧ω = (x + y)⇧ω"
proof -
have "(x + y)⇧ω = x ⋅ (x + y)⇧ω + y ⋅ (x+y)⇧ω"
by (metis distrib_right omega_unfold_eq)
thus ?thesis
by (metis mult.assoc wagner_3)
qed
text ‹
The next two lemmas apply induction and coinduction to this law.
›
lemma omega_sum_unfold_coind: "(x + y)⇧ω ≤ (x⇧⋆ ⋅ y)⇧ω + (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω"
by (simp add: omega_coinduct_eq omega_sum_unfold)
lemma omega_sum_unfold_ind: "(x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω ≤ (x + y)⇧ω"
by (simp add: local.star_inductl_eq omega_sum_unfold)
lemma wagner_1_gen: "(x ⋅ y⇧⋆)⇧ω ≤ (x + y)⇧ω"
proof -
have "(x ⋅ y⇧⋆)⇧ω ≤ ((x + y) ⋅ (x + y)⇧⋆)⇧ω"
using local.join.le_sup_iff local.join.sup.cobounded1 local.mult_isol_var local.star_subdist_var omega_iso by presburger
thus ?thesis
by (metis wagner_1)
qed
lemma wagner_1_var_gen: "(x⇧⋆ ⋅ y)⇧ω ≤ (x + y)⇧ω"
proof -
have "(x⇧⋆ ⋅ y)⇧ω = x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧ω"
by simp
also have "... ≤ x⇧⋆ ⋅ (x + y)⇧ω"
by (metis add.commute mult_isol wagner_1_gen)
also have "... ≤ (x + y)⇧⋆ ⋅ (x + y)⇧ω"
using local.mult_isor local.star_subdist by auto
thus ?thesis
by (metis calculation order_trans star_omega_1)
qed
text ‹The next lemma is a variant of the denest law for the star at
the level of omega.›
lemma omega_denest [simp]: "(x + y)⇧ω = (x⇧⋆ ⋅ y)⇧ω + (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω"
proof (rule order.antisym)
show "(x + y)⇧ω ≤ (x⇧⋆ ⋅ y)⇧ω + (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω"
by (rule omega_sum_unfold_coind)
have "(x⇧⋆ ⋅ y)⇧ω ≤ (x + y)⇧ω"
by (rule wagner_1_var_gen)
hence "(x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω ≤ (x + y)⇧ω"
by (simp add: omega_sum_unfold_ind)
thus "(x⇧⋆ ⋅ y)⇧ω + (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω ≤ (x + y)⇧ω"
by (simp add: wagner_1_var_gen)
qed
text ‹The next lemma yields a separation theorem for infinite
iteration in the presence of a quasicommutation property. A
nondeterministic loop over~@{term x} and~@{term y} can be refined into
separate infinite loops over~@{term x} and~@{term y}.›
lemma omega_sum_refine:
assumes "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
shows "(x + y)⇧ω = x⇧ω + x⇧⋆ ⋅ y⇧ω"
proof (rule order.antisym)
have a: "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
using assms local.quasicomm_var by blast
have "(x + y)⇧ω = y⇧ω + y⇧⋆ ⋅ x ⋅ (x + y)⇧ω"
by (metis add.commute omega_sum_unfold)
also have "... ≤ y⇧ω + x ⋅ (x + y)⇧⋆ ⋅ (x + y)⇧ω"
using a local.join.sup_mono local.mult_isol_var by blast
also have "... ≤ x ⋅ (x + y)⇧ω + y⇧ω"
using local.eq_refl local.join.sup_commute mult_assoc star_omega_1 by presburger
finally show "(x + y)⇧ω ≤ x⇧ω + x⇧⋆ ⋅ y⇧ω"
by (metis add_commute local.omega_coinduct)
have "x⇧ω + x⇧⋆ ⋅ y⇧ω ≤ (x + y)⇧ω + (x + y)⇧⋆ ⋅ (x + y)⇧ω"
using local.join.sup.cobounded2 local.join.sup.mono local.mult_isol_var local.star_subdist omega_iso omega_subdist by presburger
thus "x⇧ω + x⇧⋆ ⋅ y⇧ω ≤ (x + y)⇧ω"
by (metis local.join.sup_idem star_omega_1)
qed
text ‹The following theorem by Bachmair and
Dershowitz~\cite{bachmair86commutation} is a corollary.›
lemma bachmair_dershowitz:
assumes "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
shows "(x + y)⇧ω = 0 ⟷ x⇧ω + y⇧ω = 0"
by (metis add_commute assms local.annir local.join.le_bot local.no_trivial_inverse omega_subdist omega_sum_refine)
text ‹
The next lemmas consider an abstract variant of the empty word
property from language theory and match it with the absence of
infinite iteration~\cite{struth12regeq}.
›
definition (in dioid_one_zero) ewp
where "ewp x ≡ ¬(∀y. y ≤ x ⋅ y ⟶ y = 0)"
lemma ewp_super_id1: "0 ≠ 1 ⟹ 1 ≤ x ⟹ ewp x"
by (metis ewp_def mult_oner)
lemma "0 ≠ 1 ⟹ 1 ≤ x ⟷ ewp x"
oops
text ‹The next facts relate the absence of the empty word property
with the absence of infinite iteration.›
lemma ewp_neg_and_omega: "¬ ewp x ⟷ x⇧ω = 0"
proof
assume "¬ ewp x"
hence "∀ y. y ≤ x ⋅ y ⟶ y = 0"
by (meson ewp_def)
thus "x⇧ω = 0"
by simp
next
assume "x⇧ω = 0"
hence "∀ y. y ≤ x ⋅ y ⟶ y = 0"
using local.join.le_bot local.omega_coinduct_var2 by blast
thus "¬ ewp x"
by (meson ewp_def)
qed
lemma ewp_alt1: "(∀z. x⇧ω ≤ x⇧⋆ ⋅ z) ⟷ (∀y z. y ≤ x ⋅ y + z ⟶ y ≤ x⇧⋆ ⋅ z)"
by (metis add_comm less_eq_def omega_coinduct omega_unfold_eq order_prop)
lemma ewp_alt: "x⇧ω = 0 ⟷ (∀y z. y ≤ x ⋅ y + z ⟶ y ≤ x⇧⋆ ⋅ z)"
by (metis annir order.antisym ewp_alt1 join.bot_least)
text ‹So we have obtained a condition for Arden's lemma in omega
algebra.›
lemma omega_super_id1: "0 ≠ 1 ⟹ 1 ≤ x ⟹ x⇧ω ≠ 0"
using ewp_neg_and_omega ewp_super_id1 by blast
lemma omega_super_id2: "0 ≠ 1 ⟹ x⇧ω = 0 ⟹ ¬(1 ≤ x)"
using omega_super_id1 by blast
text ‹The next lemmas are abstract versions of Arden's lemma from
language theory.›
lemma ardens_lemma_var:
assumes "x⇧ω = 0"
and "z + x ⋅ y = y"
shows "x⇧⋆ ⋅ z = y"
proof -
have "y ≤ x⇧ω + x⇧⋆ ⋅ z"
by (simp add: assms(2) local.omega_coinduct_eq)
hence "y ≤ x⇧⋆ ⋅ z"
by (simp add: assms(1))
thus "x⇧⋆ ⋅ z = y"
by (simp add: assms(2) order.eq_iff local.star_inductl_eq)
qed
lemma ardens_lemma: "¬ ewp x ⟹ z + x ⋅ y = y ⟹ x⇧⋆ ⋅ z = y"
by (simp add: ardens_lemma_var ewp_neg_and_omega)
lemma ardens_lemma_equiv:
assumes "¬ ewp x"
shows "z + x ⋅ y = y ⟷ x⇧⋆ ⋅ z = y"
by (metis ardens_lemma_var assms ewp_neg_and_omega local.conway.dagger_unfoldl_distr mult_assoc)
lemma ardens_lemma_var_equiv: "x⇧ω = 0 ⟹ (z + x ⋅ y = y ⟷ x⇧⋆ ⋅ z = y)"
by (simp add: ardens_lemma_equiv ewp_neg_and_omega)
lemma arden_conv1: "(∀y z. z + x ⋅ y = y ⟶ x⇧⋆ ⋅ z = y) ⟹ ¬ ewp x"
by (metis add_zero_l annir ewp_neg_and_omega omega_unfold_eq)
lemma arden_conv2: "(∀y z. z + x ⋅ y = y ⟶ x⇧⋆ ⋅ z = y) ⟹ x⇧ω = 0"
using arden_conv1 ewp_neg_and_omega by blast
lemma arden_var3: "(∀y z. z + x ⋅ y = y ⟶ x⇧⋆ ⋅ z = y) ⟷ x⇧ω = 0"
using arden_conv2 ardens_lemma_var by blast
end
subsection ‹Omega Algebras›
class omega_algebra = kleene_algebra + left_omega_algebra
end
Theory Omega_Algebra_Models
section ‹Models of Omega Algebras›
theory Omega_Algebra_Models
imports Omega_Algebra Kleene_Algebra_Models
begin
text ‹The trace, path and language model are not really interesting
in this setting.›
subsection ‹Relation Omega Algebras›
text ‹In the relational model, the omega of a relation relates all
those elements in the domain of the relation, from which an infinite
chain starts, with all other elements; all other elements are not
related to anything~\cite{hofnerstruth10nontermination}. Thus, the
omega of a relation is most naturally defined coinductively.›
coinductive_set omega :: "('a × 'a) set ⇒ ('a × 'a) set" for R where
"⟦ (x, y) ∈ R; (y, z) ∈ omega R ⟧ ⟹ (x, z) ∈ omega R"
text ‹Isabelle automatically derives a case rule and a coinduction
theorem for @{const omega}. We prove slightly more elegant
variants.›
lemma omega_cases: "(x, z) ∈ omega R ⟹
(⋀y. (x, y) ∈ R ⟹ (y, z) ∈ omega R ⟹ P) ⟹ P"
by (metis omega.cases)
lemma omega_coinduct: "X x z ⟹
(⋀x z. X x z ⟹ ∃y. (x, y) ∈ R ∧ (X y z ∨ (y, z) ∈ omega R)) ⟹
(x, z) ∈ omega R"
by (metis (full_types) omega.coinduct)
lemma omega_weak_coinduct: "X x z ⟹
(⋀x z. X x z ⟹ ∃y. (x, y) ∈ R ∧ X y z) ⟹
(x, z) ∈ omega R"
by (metis omega.coinduct)
interpretation rel_omega_algebra: omega_algebra "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl omega
proof
fix x :: "'a rel"
show "omega x ⊆ x O omega x"
by (auto elim: omega_cases)
next
fix x y z :: "'a rel"
assume *: "y ⊆ z ∪ x O y"
{
fix a b
assume 1: "(a,b) ∈ y" and 2: "(a,b) ∉ x⇧* O z"
have "(a,b) ∈ omega x"
proof (rule omega_weak_coinduct[where X="λa b. (a,b) ∈ x O y ∧ (a,b) ∉ x⇧* O z"])
show "(a,b) ∈ x O y ∧ (a,b) ∉ x⇧* O z"
using "*" "1" "2" by auto
next
fix a c
assume 1: "(a,c) ∈ x O y ∧ (a,c) ∉ x⇧* O z"
then obtain b where 2: "(a,b) ∈ x" and "(b,c) ∈ y"
by auto
then have "(b,c) ∈ x O y"
using "*" "1" by blast
moreover have "(b,c) ∉ x⇧* O z"
using "1" "2" by (meson relcomp.cases relcomp.intros converse_rtrancl_into_rtrancl)
ultimately show "∃b. (a,b) ∈ x ∧ (b,c) ∈ x O y ∧ (b,c) ∉ x⇧* O z"
using "2" by blast
qed
}
then show "y ⊆ omega x ∪ x⇧* O z"
by auto
qed
end
Theory DRA
section ‹Demonic Refinement Algebras›
theory DRA
imports Kleene_Algebra
begin
text ‹
A demonic refinement algebra *DRA)~\cite{vonwright04refinement} is a Kleene algebra without right annihilation plus
an operation for possibly infinite iteration.
›
class dra = kleene_algebra_zerol +
fixes strong_iteration :: "'a ⇒ 'a" ("_⇧∞" [101] 100)
assumes iteration_unfoldl [simp] : "1 + x ⋅ x⇧∞ = x⇧∞"
and coinduction: "y ≤ z + x ⋅ y ⟶ y ≤ x⇧∞ ⋅ z"
and isolation [simp]: "x⇧⋆ + x⇧∞ ⋅ 0 = x⇧∞"
begin
text ‹$\top$ is an abort statement, defined as an infinite skip. It is the maximal element of any DRA.›
abbreviation top_elem :: "'a" ("⊤") where "⊤ ≡ 1⇧∞"
text ‹Simple/basic lemmas about the iteration operator›
lemma iteration_refl: "1 ≤ x⇧∞"
using local.iteration_unfoldl local.order_prop by blast
lemma iteration_1l: "x ⋅ x⇧∞ ≤ x⇧∞"
by (metis local.iteration_unfoldl local.join.sup.cobounded2)
lemma top_ref: "x ≤ ⊤"
proof -
have "x ≤ 1 + 1 ⋅ x"
by simp
thus ?thesis
using local.coinduction by fastforce
qed
lemma it_ext: "x ≤ x⇧∞"
proof -
have "x ≤ x ⋅ x⇧∞"
using iteration_refl local.mult_isol by fastforce
thus ?thesis
by (metis (full_types) local.isolation local.join.sup.coboundedI1 local.star_ext)
qed
lemma it_idem [simp]: "(x⇧∞)⇧∞ = x⇧∞"
oops
lemma top_mult_annil [simp]: "⊤ ⋅ x = ⊤"
by (simp add: local.coinduction local.order.antisym top_ref)
lemma top_add_annil [simp]: "⊤ + x = ⊤"
by (simp add: local.join.sup.absorb1 top_ref)
lemma top_elim: "x ⋅ y ≤ x ⋅ ⊤"
by (simp add: local.mult_isol top_ref)
lemma iteration_unfoldl_distl [simp]: " y + y ⋅ x ⋅ x⇧∞ = y ⋅ x⇧∞"
by (metis distrib_left mult.assoc mult_oner iteration_unfoldl)
lemma iteration_unfoldl_distr [simp]: " y + x ⋅ x⇧∞ ⋅ y = x⇧∞ ⋅ y"
by (metis distrib_right' mult_1_left iteration_unfoldl)
lemma iteration_unfoldl' [simp]: "z ⋅ y + z ⋅ x ⋅ x⇧∞ ⋅ y = z ⋅ x⇧∞ ⋅ y"
by (metis iteration_unfoldl_distl local.distrib_right)
lemma iteration_idem [simp]: "x⇧∞ ⋅ x⇧∞ = x⇧∞"
proof (rule order.antisym)
have "x⇧∞ ⋅ x⇧∞ ≤ 1 + x ⋅ x⇧∞ ⋅ x⇧∞"
by (metis add_assoc iteration_unfoldl_distr local.eq_refl local.iteration_unfoldl local.subdistl_eq mult_assoc)
thus "x⇧∞ ⋅ x⇧∞ ≤ x⇧∞"
using local.coinduction mult_assoc by fastforce
show "x⇧∞ ≤ x⇧∞ ⋅ x⇧∞"
using local.coinduction by auto
qed
lemma iteration_induct: "x ⋅ x⇧∞ ≤ x⇧∞ ⋅ x"
proof -
have "x + x ⋅ (x ⋅ x⇧∞) = x ⋅ x⇧∞"
by (metis (no_types) local.distrib_left local.iteration_unfoldl local.mult_oner)
thus ?thesis
by (simp add: local.coinduction)
qed
lemma iteration_ref_star: "x⇧⋆ ≤ x⇧∞"
by (simp add: local.star_inductl_one)
lemma iteration_subdist: "x⇧∞ ≤ (x + y)⇧∞"
by (metis add_assoc' distrib_right' mult_oner coinduction join.sup_ge1 iteration_unfoldl)
lemma iteration_iso: "x ≤ y ⟹ x⇧∞ ≤ y⇧∞"
using iteration_subdist local.order_prop by auto
lemma iteration_unfoldr [simp]: "1 + x⇧∞ ⋅ x = x⇧∞"
by (metis add_0_left annil eq_refl isolation mult.assoc iteration_idem iteration_unfoldl iteration_unfoldl_distr star_denest star_one star_prod_unfold star_slide tc)
lemma iteration_unfoldr_distl [simp]: " y + y ⋅ x⇧∞ ⋅ x = y ⋅ x⇧∞"
by (metis distrib_left mult.assoc mult_oner iteration_unfoldr)
lemma iteration_unfoldr_distr [simp]: " y + x⇧∞ ⋅ x ⋅ y = x⇧∞ ⋅ y"
by (metis iteration_unfoldl_distr iteration_unfoldr_distl)
lemma iteration_unfold_eq: "x⇧∞ ⋅ x = x ⋅ x⇧∞"
by (metis iteration_unfoldl_distr iteration_unfoldr_distl)
lemma iteration_unfoldr' [simp]: "z ⋅ y + z ⋅ x⇧∞ ⋅ x ⋅ y = z ⋅ x⇧∞ ⋅ y"
by (metis distrib_left mult.assoc iteration_unfoldr_distr)
lemma iteration_double [simp]: "(x⇧∞)⇧∞ = ⊤"
by (simp add: iteration_iso iteration_refl order.eq_iff top_ref)
lemma star_iteration [simp]: "(x⇧⋆)⇧∞ = ⊤"
by (simp add: iteration_iso order.eq_iff top_ref)
lemma iteration_star [simp]: "(x⇧∞)⇧⋆ = x⇧∞"
by (metis (no_types) iteration_idem iteration_refl local.star_inductr_var_eq2 local.sup_id_star1)
lemma iteration_star2 [simp]: "x⇧⋆ ⋅ x⇧∞ = x⇧∞"
proof -
have f1: "(x⇧∞)⇧⋆ ⋅ x⇧⋆ = x⇧∞"
by (metis (no_types) it_ext iteration_induct iteration_star local.bubble_sort local.join.sup.absorb1)
have "x⇧∞ = x⇧∞ ⋅ x⇧∞"
by simp
hence "x⇧⋆ ⋅ x⇧∞ = x⇧⋆ ⋅ (x⇧∞)⇧⋆ ⋅ (x⇧⋆ ⋅ (x⇧∞)⇧⋆)⇧⋆"
using f1 by (metis (no_types) iteration_star local.star_denest_var_4 mult_assoc)
thus ?thesis
using f1 by (metis (no_types) iteration_star local.star_denest_var_4 local.star_denest_var_8)
qed
lemma iteration_zero [simp]: "0⇧∞ = 1"
by (metis add_zeror annil iteration_unfoldl)
lemma iteration_annil [simp]: "(x ⋅ 0)⇧∞ = 1 + x ⋅ 0"
by (metis annil iteration_unfoldl mult.assoc)
lemma iteration_subdenest: "x⇧∞ ⋅ y⇧∞ ≤ (x + y)⇧∞"
by (metis add_commute iteration_idem iteration_subdist local.mult_isol_var)
lemma sup_id_top: "1 ≤ y ⟹ y ⋅ ⊤ = ⊤"
using order.eq_iff local.mult_isol_var top_ref by fastforce
lemma iteration_top [simp]: "x⇧∞ ⋅ ⊤ = ⊤"
by (simp add: iteration_refl sup_id_top)
text ‹Next, we prove some simulation laws for data refinement.›
lemma iteration_sim: "z ⋅ y ≤ x ⋅ z ⟹ z ⋅ y⇧∞ ≤ x⇧∞ ⋅ z"
proof -
assume assms: "z ⋅ y ≤ x ⋅ z"
have "z ⋅ y⇧∞ = z + z ⋅ y ⋅ y⇧∞"
by simp
also have "... ≤ z + x ⋅ z ⋅ y⇧∞"
by (metis assms add.commute add_iso mult_isor)
finally show "z ⋅ y⇧∞ ≤ x⇧∞ ⋅ z"
by (simp add: local.coinduction mult_assoc)
qed
text ‹Nitpick gives a counterexample to the dual simulation law.›
lemma "y ⋅ z ≤ z ⋅ x ⟹ y⇧∞ ⋅ z ≤ z ⋅ x⇧∞"
oops
text ‹Next, we prove some sliding laws.›
lemma iteration_slide_var: "x ⋅ (y ⋅ x)⇧∞ ≤ (x ⋅ y)⇧∞ ⋅ x"
by (simp add: iteration_sim mult_assoc)
lemma iteration_prod_unfold [simp]: "1 + y ⋅ (x ⋅ y)⇧∞ ⋅ x = (y ⋅ x)⇧∞"
proof (rule order.antisym)
have "1 + y ⋅ (x ⋅ y)⇧∞ ⋅ x ≤ 1 + (y ⋅ x)⇧∞ ⋅ y ⋅ x"
using iteration_slide_var local.join.sup_mono local.mult_isor by blast
thus "1 + y ⋅ (x ⋅ y)⇧∞ ⋅ x ≤ (y ⋅ x)⇧∞"
by (simp add: mult_assoc)
have "(y ⋅ x)⇧∞ = 1 + y ⋅ x ⋅ (y ⋅ x)⇧∞"
by simp
thus "(y ⋅ x)⇧∞ ≤ 1 + y ⋅ (x ⋅ y)⇧∞ ⋅ x"
by (metis iteration_sim local.eq_refl local.join.sup.mono local.mult_isol mult_assoc)
qed
lemma iteration_slide: "x ⋅ (y ⋅ x)⇧∞ = (x ⋅ y)⇧∞ ⋅ x"
by (metis iteration_prod_unfold iteration_unfoldl_distr distrib_left mult_1_right mult.assoc)
lemma star_iteration_slide [simp]: " y⇧⋆ ⋅ (x⇧⋆ ⋅ y)⇧∞ = (x⇧⋆ ⋅ y)⇧∞"
by (metis iteration_star2 local.conway.dagger_unfoldl_distr local.join.sup.orderE local.mult_isor local.star_invol local.star_subdist local.star_trans_eq)
text ‹The following laws are called denesting laws.›
lemma iteration_sub_denest: "(x + y)⇧∞ ≤ x⇧∞ ⋅ (y ⋅ x⇧∞)⇧∞"
proof -
have "(x + y)⇧∞ = x ⋅ (x + y)⇧∞ + y ⋅ (x + y)⇧∞ + 1"
by (metis add.commute distrib_right' iteration_unfoldl)
hence "(x + y)⇧∞ ≤ x⇧∞ ⋅ (y ⋅ (x + y)⇧∞ + 1)"
by (metis add_assoc' join.sup_least join.sup_ge1 join.sup_ge2 coinduction)
moreover hence "x⇧∞ ⋅ (y ⋅ (x + y)⇧∞ + 1) ≤ x⇧∞ ⋅ (y ⋅ x⇧∞)⇧∞"
by (metis add_iso mult.assoc mult_isol add.commute coinduction mult_oner mult_isol)
ultimately show ?thesis
using local.order_trans by blast
qed
lemma iteration_denest: "(x + y)⇧∞ = x⇧∞ ⋅ (y ⋅ x⇧∞)⇧∞"
proof -
have "x⇧∞ ⋅ (y ⋅ x⇧∞)⇧∞ ≤ x ⋅ x⇧∞ ⋅ (y ⋅ x⇧∞)⇧∞ + y ⋅ x⇧∞ ⋅ (y ⋅ x⇧∞)⇧∞ + 1"
by (metis add.commute iteration_unfoldl_distr add_assoc' add.commute iteration_unfoldl order_refl)
thus ?thesis
by (metis add.commute iteration_sub_denest order.antisym coinduction distrib_right' iteration_sub_denest mult.assoc mult_oner order.antisym)
qed
lemma iteration_denest2 [simp]: "y⇧⋆ ⋅ x ⋅ (x + y)⇧∞ + y⇧∞ = (x + y)⇧∞"
proof -
have "(x + y)⇧∞ = y⇧∞ ⋅ x ⋅ (y⇧∞ ⋅ x)⇧∞ ⋅ y⇧∞ + y⇧∞"
by (metis add.commute iteration_denest iteration_slide iteration_unfoldl_distr)
also have "... = y⇧⋆ ⋅ x ⋅ (y⇧∞ ⋅ x)⇧∞ ⋅ y⇧∞ + y⇧∞ ⋅ 0 + y⇧∞"
by (metis isolation mult.assoc distrib_right' annil mult.assoc)
also have "... = y⇧⋆ ⋅ x ⋅ (y⇧∞ ⋅ x)⇧∞ ⋅ y⇧∞ + y⇧∞"
by (metis add.assoc distrib_left mult_1_right add_0_left mult_1_right)
finally show ?thesis
by (metis add.commute iteration_denest iteration_slide mult.assoc)
qed
lemma iteration_denest3: "(y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞ = (x + y)⇧∞"
proof (rule order.antisym)
have "(y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞ ≤ (y⇧∞ ⋅ x)⇧∞ ⋅ y⇧∞"
by (simp add: iteration_iso iteration_ref_star local.mult_isor)
thus "(y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞ ≤ (x + y)⇧∞"
by (metis iteration_denest iteration_slide local.join.sup_commute)
have "(x + y)⇧∞ = y⇧∞ + y⇧⋆ ⋅ x ⋅ (x + y)⇧∞"
by (metis iteration_denest2 local.join.sup_commute)
thus "(x + y)⇧∞ ≤ (y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞"
by (simp add: local.coinduction)
qed
text ‹Now we prove separation laws for reasoning about distributed systems in the context of action systems.›
lemma iteration_sep: "y ⋅ x ≤ x ⋅ y ⟹ (x + y)⇧∞ = x⇧∞ ⋅ y⇧∞"
proof -
assume "y ⋅ x ≤ x ⋅ y"
hence "y⇧⋆ ⋅ x ≤ x⋅(x + y)⇧⋆"
by (metis star_sim1 add.commute mult_isol order_trans star_subdist)
hence "y⇧⋆ ⋅ x ⋅ (x + y)⇧∞ + y⇧∞ ≤ x ⋅ (x + y)⇧∞ + y⇧∞"
by (metis mult_isor mult.assoc iteration_star2 join.sup.mono eq_refl)
thus ?thesis
by (metis iteration_denest2 add.commute coinduction add.commute less_eq_def iteration_subdenest)
qed
lemma iteration_sim2: "y ⋅ x ≤ x ⋅ y ⟹ y⇧∞ ⋅ x⇧∞ ≤ x⇧∞ ⋅ y⇧∞"
by (metis add.commute iteration_sep iteration_subdenest)
lemma iteration_sep2: "y ⋅ x ≤ x ⋅ y⇧⋆ ⟹ (x + y)⇧∞ = x⇧∞ ⋅ y⇧∞"
proof -
assume "y ⋅ x ≤ x ⋅ y⇧⋆"
hence "y⇧⋆ ⋅ (y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞ ≤ x⇧∞ ⋅ y⇧⋆ ⋅ y⇧∞"
by (metis mult.assoc mult_isor iteration_sim star_denest_var_2 star_sim1 star_slide_var star_trans_eq tc_eq)
moreover have "x⇧∞ ⋅ y⇧⋆ ⋅ y⇧∞ ≤ x⇧∞ ⋅ y⇧∞"
by (metis eq_refl mult.assoc iteration_star2)
moreover have "(y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞ ≤ y⇧⋆ ⋅ (y⇧⋆ ⋅ x)⇧∞ ⋅ y⇧∞"
by (metis mult_isor mult_onel star_ref)
ultimately show ?thesis
by (metis order.antisym iteration_denest3 iteration_subdenest order_trans)
qed
lemma iteration_sep3: "y ⋅ x ≤ x ⋅ (x + y) ⟹ (x + y)⇧∞ = x⇧∞ ⋅ y⇧∞"
proof -
assume "y ⋅ x ≤ x ⋅ (x + y)"
hence "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
by (metis star_sim1)
hence "y⇧⋆ ⋅ x ⋅ (x + y)⇧∞ + y⇧∞ ≤ x ⋅ (x + y)⇧⋆ ⋅ (x + y)⇧∞ + y⇧∞"
by (metis add_iso mult_isor)
hence "(x + y)⇧∞ ≤ x⇧∞ ⋅ y⇧∞"
by (metis mult.assoc iteration_denest2 iteration_star2 add.commute coinduction)
thus ?thesis
by (metis add.commute less_eq_def iteration_subdenest)
qed
lemma iteration_sep4: "y ⋅ 0 = 0 ⟹ z ⋅ x = 0 ⟹ y ⋅ x ≤ (x + z) ⋅ y⇧⋆ ⟹ (x + y + z)⇧∞ = x⇧∞ ⋅ (y + z)⇧∞"
proof -
assume assms: "y ⋅ 0 = 0" "z ⋅ x = 0" "y ⋅ x ≤ (x + z) ⋅ y⇧⋆"
have "y ⋅ y⇧⋆ ⋅ z ≤ y⇧⋆ ⋅ z ⋅ y⇧⋆"
by (metis mult_isor star_1l mult_oner order_trans star_plus_one subdistl)
have "y⇧⋆ ⋅ z ⋅ x ≤ x ⋅ y⇧⋆ ⋅ z"
by (metis join.bot_least assms(1) assms(2) independence1 mult.assoc)
have "y ⋅ (x + y⇧⋆ ⋅ z) ≤ (x + z) ⋅ y⇧⋆ + y ⋅ y⇧⋆ ⋅ z"
by (metis assms(3) distrib_left mult.assoc add_iso)
also have "... ≤ (x + y⇧⋆ ⋅ z) ⋅ y⇧⋆ + y ⋅ y⇧⋆ ⋅ z"
by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor)
also have "... ≤ (x + y⇧⋆ ⋅ z) ⋅ y⇧⋆ + y⇧⋆ ⋅ z ⋅ y⇧⋆" using ‹y ⋅ y⇧⋆ ⋅ z ≤ y⇧⋆ ⋅ z ⋅ y⇧⋆›
by (metis add.commute add_iso)
finally have "y ⋅ (x + y⇧⋆ ⋅ z) ≤ (x + y⇧⋆ ⋅ z) ⋅ y⇧⋆"
by (metis add.commute add_idem' add.left_commute distrib_right)
moreover have "(x + y + z)⇧∞ ≤ (x + y + y⇧⋆ ⋅ z)⇧∞"
by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor iteration_iso)
moreover have "... = (x + y⇧⋆ ⋅ z)⇧∞ ⋅ y⇧∞"
by (metis add_commute calculation(1) iteration_sep2 local.add_left_comm)
moreover have "... = x⇧∞ ⋅ (y⇧⋆ ⋅ z)⇧∞ ⋅ y⇧∞" using ‹y⇧⋆ ⋅ z ⋅ x ≤ x ⋅ y⇧⋆ ⋅ z›
by (metis iteration_sep mult.assoc)
ultimately have "(x + y + z)⇧∞ ≤ x⇧∞ ⋅ (y + z)⇧∞"
by (metis add.commute mult.assoc iteration_denest3)
thus ?thesis
by (metis add.commute add.left_commute less_eq_def iteration_subdenest)
qed
text ‹Finally, we prove some blocking laws.›
text ‹Nitpick refutes the next lemma.›
lemma "x ⋅ y = 0 ⟹ x⇧∞ ⋅ y = y"
oops
lemma iteration_idep: "x ⋅ y = 0 ⟹ x ⋅ y⇧∞ = x"
by (metis add_zeror annil iteration_unfoldl_distl)
text ‹Nitpick refutes the next lemma.›
lemma "y ⋅ w ≤ x ⋅ y + z ⟹ y ⋅ w⇧∞ ≤ x⇧∞ ⋅ z"
oops
text ‹At the end of this file, we consider a data refinement example from von Wright~\cite{Wright02}.›
lemma data_refinement:
assumes "s' ≤ s ⋅ z" and "z ⋅ e' ≤ e" and "z ⋅ a' ≤ a ⋅ z" and "z ⋅ b ≤ z" and "b⇧∞ = b⇧⋆"
shows "s' ⋅ (a' + b)⇧∞ ⋅ e' ≤ s ⋅ a⇧∞ ⋅ e"
proof -
have "z ⋅ b⇧⋆ ≤ z"
by (metis assms(4) star_inductr_var)
have "(z ⋅ a') ⋅ b⇧⋆ ≤ (a ⋅ z) ⋅ b⇧⋆"
by (metis assms(3) mult.assoc mult_isor)
hence "z ⋅ (a' ⋅ b⇧⋆)⇧∞ ≤ a⇧∞ ⋅ z" using ‹z ⋅ b⇧⋆ ≤ z›
by (metis mult.assoc mult_isol order_trans iteration_sim mult.assoc)
have "s' ⋅ (a' + b)⇧∞ ⋅ e' ≤ s' ⋅ b⇧⋆ ⋅ (a' ⋅ b⇧⋆)⇧∞ ⋅ e'"
by (metis add.commute assms(5) eq_refl iteration_denest mult.assoc)
also have "... ≤ s ⋅ z ⋅ b⇧⋆ ⋅ (a' ⋅ b⇧⋆)⇧∞ ⋅ e'"
by (metis assms(1) mult_isor)
also have "... ≤ s ⋅ z ⋅ (a' ⋅ b⇧⋆)⇧∞ ⋅ e'" using ‹z ⋅ b⇧⋆ ≤ z›
by (metis mult.assoc mult_isol mult_isor)
also have "... ≤ s ⋅ a⇧∞ ⋅ z ⋅ e'" using ‹z ⋅ (a' ⋅ b⇧⋆)⇧∞ ≤ a⇧∞ ⋅ z›
by (metis mult.assoc mult_isol mult_isor)
finally show ?thesis
by (metis assms(2) mult.assoc mult_isol mult.assoc mult_isol order_trans)
qed
end
end
Theory PHL_KA
section ‹Propositional Hoare Logic for Conway and Kleene Algebra›
theory PHL_KA
imports Kleene_Algebra
begin
text ‹This is a minimalist Hoare logic developed in the context of pre-dioids. In near-dioids, the sequencing rule would not be derivable.
Iteration is modelled by a function that needs to satisfy a simulation law.
The main assumtions on pre-dioid elements needed to derive the Hoare rules are preservation properties; an additional distributivity propery is needed
for the conditional rule.
This Hoare logic can be instantated in various ways. It covers notions of
finite and possibly infinite iteration. In this theory, it it specialised to Conway and Kleene algebras.›
class it_pre_dioid = pre_dioid_one +
fixes it :: "'a ⇒ 'a"
assumes it_simr: "y ⋅ x ≤ x ⋅ y ⟹ y ⋅ it x ≤ it x ⋅ y"
begin
lemma phl_while:
assumes "p ⋅ s ≤ s ⋅ p ⋅ s" and "p ⋅ w ≤ w ⋅ p ⋅ w"
and "(p ⋅ s) ⋅ x ≤ x ⋅ p"
shows "p ⋅ (it (s ⋅ x) ⋅ w) ≤ it (s ⋅ x) ⋅ w ⋅ (p ⋅ w)"
proof -
have "p ⋅ s ⋅ x ≤ s ⋅ x ⋅ p"
by (metis assms(1) assms(3) mult.assoc phl_export1)
hence "p ⋅ it (s ⋅ x) ≤ it (s ⋅ x) ⋅ p"
by (simp add: it_simr mult.assoc)
thus ?thesis
using assms(2) phl_export2 by blast
qed
end
text ‹Next we define a Hoare triple to make the format of the rules more explicit.›
context pre_dioid_one
begin
abbreviation (in near_dioid) ht :: "'a ⇒ 'a ⇒ 'a ⇒ bool" ("⦃_⦄_⦃_⦄") where
"⦃x⦄ y ⦃z⦄ ≡ x ⋅ y ≤ y ⋅ z"
lemma ht_phl_skip: "⦃x⦄ 1 ⦃x⦄"
by simp
lemma ht_phl_cons1: "x ≤ w ⟹ ⦃w⦄ y ⦃z⦄ ⟹ ⦃x⦄ y ⦃z⦄"
by (fact phl_cons1)
lemma ht_phl_cons2: "w ≤ x ⟹ ⦃z⦄ y ⦃w⦄ ⟹ ⦃z⦄ y ⦃x⦄"
by (fact phl_cons2)
lemma ht_phl_seq: "⦃p⦄ x ⦃r⦄ ⟹ ⦃r⦄ y ⦃q⦄ ⟹ ⦃p⦄ x ⋅ y ⦃q⦄"
by (fact phl_seq)
lemma ht_phl_cond:
assumes "u ⋅ v ≤ v ⋅ u ⋅ v" and "u ⋅ w ≤ w ⋅ u ⋅ w"
and "⋀x y. u ⋅ (x + y) ≤ u ⋅ x + u ⋅ y"
and "⦃u ⋅ v⦄ x ⦃z⦄" and "⦃u ⋅ w⦄ y ⦃z⦄"
shows "⦃u⦄ (v ⋅ x + w ⋅ y) ⦃z⦄"
using assms by (fact phl_cond)
lemma ht_phl_export1:
assumes "x ⋅ y ≤ y ⋅ x ⋅ y"
and "⦃x ⋅ y⦄ z ⦃w⦄"
shows "⦃x⦄ y ⋅ z ⦃w⦄"
using assms by (fact phl_export1)
lemma ht_phl_export2:
assumes "z ⋅ w ≤ w ⋅ z ⋅ w"
and "⦃x⦄ y ⦃z⦄"
shows "⦃x⦄ y ⋅ w ⦃z ⋅ w⦄"
using assms by (fact phl_export2)
end
context it_pre_dioid begin
lemma ht_phl_while:
assumes "p ⋅ s ≤ s ⋅ p ⋅ s" and "p ⋅ w ≤ w ⋅ p ⋅ w"
and "⦃p ⋅ s⦄ x ⦃p⦄"
shows "⦃p⦄ it (s ⋅ x) ⋅ w ⦃p ⋅ w⦄"
using assms by (fact phl_while)
end
sublocale pre_conway < phl: it_pre_dioid where it = dagger
by standard (simp add: local.dagger_simr)
sublocale kleene_algebra < phl: it_pre_dioid where it = star ..
end
Theory PHL_DRA
section ‹Propositional Hoare Logic for Demonic Refinement Algebra›
text ‹In this section the generic iteration operator is instantiated to the strong iteration operator of
demonic refinement algebra that models possibly infinite iteration.›
theory PHL_DRA
imports DRA PHL_KA
begin
sublocale dra < total_phl: it_pre_dioid where it = strong_iteration
by standard (simp add: local.iteration_sim)
end
Theory Finite_Suprema
section ‹Finite Suprema›
theory Finite_Suprema
imports Dioid
begin
text ‹This file contains an adaptation of Isabelle's library for
finite sums to the case of (join) semilattices and dioids. In this
setting, addition is idempotent; finite sums are finite suprema.
We add some basic properties of finite suprema for (join) semilattices
and dioids.›
subsection ‹Auxiliary Lemmas›
lemma fun_im: "{f a |a. a ∈ A} = {b. b ∈ f ` A}"
by auto
lemma fset_to_im: "{f x |x. x ∈ X} = f ` X"
by auto
lemma cart_flip_aux: "{f (snd p) (fst p) |p. p ∈ (B × A)} = {f (fst p) (snd p) |p. p ∈ (A × B)}"
by auto
lemma cart_flip: "(λp. f (snd p) (fst p)) ` (B × A) = (λp. f (fst p) (snd p)) ` (A × B)"
by (metis cart_flip_aux fset_to_im)
lemma fprod_aux: "{x ⋅ y |x y. x ∈ (f ` A) ∧ y ∈ (g ` B)} = {f x ⋅ g y |x y. x ∈ A ∧ y ∈ B}"
by auto
subsection ‹Finite Suprema in Semilattices›
text ‹The first lemma shows that, in the context of semilattices,
finite sums satisfy the defining property of finite suprema.›
lemma sum_sup:
assumes "finite (A :: 'a::join_semilattice_zero set)"
shows "∑A ≤ z ⟷ (∀a ∈ A. a ≤ z)"
proof (induct rule: finite_induct[OF assms])
fix z ::'a
show "(∑{} ≤ z) = (∀a ∈ {}. a ≤ z)"
by simp
next
fix x z :: 'a and F :: "'a set"
assume finF: "finite F"
and xnF: "x ∉ F"
and indhyp: "(∑F ≤ z) = (∀a ∈ F. a ≤ z)"
show "(∑(insert x F) ≤ z) = (∀a ∈ insert x F. a ≤ z)"
proof -
have "∑(insert x F) ≤ z ⟷ (x + ∑F) ≤ z"
by (metis finF sum.insert xnF)
also have "... ⟷ x ≤ z ∧ ∑F ≤ z"
by simp
also have "... ⟷ x ≤ z ∧ (∀a ∈ F. a ≤ z)"
by (metis (lifting) indhyp)
also have "... ⟷ (∀a ∈ insert x F. a ≤ z)"
by (metis insert_iff)
ultimately show "(∑(insert x F) ≤ z) = (∀a ∈ insert x F. a ≤ z)"
by blast
qed
qed
text ‹This immediately implies some variants.›
lemma sum_less_eqI:
"(⋀x. x ∈ A ⟹ f x ≤ y) ⟹ sum f A ≤ (y::'a::join_semilattice_zero)"
apply (atomize (full))
apply (case_tac "finite A")
apply (erule finite_induct)
apply simp_all
done
lemma sum_less_eqE:
"⟦ sum f A ≤ y; x ∈ A; finite A ⟧ ⟹ f x ≤ (y::'a::join_semilattice_zero)"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule finite_induct)
apply auto
done
lemma sum_fun_image_sup:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
shows "∑(f ` A) ≤ z ⟷ (∀a ∈ A. f a ≤ z)"
by (simp add: assms sum_sup)
lemma sum_fun_sup:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A ::'a set)"
shows "∑{f a | a. a ∈ A} ≤ z ⟷ (∀a ∈ A. f a ≤ z)"
by (simp only: fset_to_im assms sum_fun_image_sup)
lemma sum_intro:
assumes "finite (A :: 'a::join_semilattice_zero set)" and "finite B"
shows "(∀a ∈ A. ∃b ∈ B. a ≤ b) ⟶ (∑A ≤ ∑B)"
by (metis assms order_refl order_trans sum_sup)
text ‹Next we prove an additivity property for suprema.›
lemma sum_union:
assumes "finite (A :: 'a::join_semilattice_zero set)"
and "finite (B :: 'a::join_semilattice_zero set)"
shows "∑(A ∪ B) = ∑A + ∑B"
proof -
have "∀z. ∑(A ∪ B) ≤ z ⟷ (∑A + ∑B ≤ z)"
by (auto simp add: assms sum_sup)
thus ?thesis
by (simp add: eq_iff)
qed
text ‹It follows that the sum (supremum) of a two-element set is the
join of its elements.›
lemma sum_bin[simp]: "∑{(x :: 'a::join_semilattice_zero),y} = x + y"
by (subst insert_is_Un, subst sum_union, auto)
text ‹Next we show that finite suprema are order preserving.›
lemma sum_iso:
assumes "finite (B :: 'a::join_semilattice_zero set)"
shows "A ⊆ B ⟶ ∑ A ≤ ∑ B"
by (metis assms finite_subset order_refl rev_subsetD sum_sup)
text ‹The following lemmas state unfold properties for suprema and
finite sets. They are subtly different from the non-idempotent case,
where additional side conditions are required.›
lemma sum_insert [simp]:
assumes "finite (A :: 'a::join_semilattice_zero set)"
shows "∑(insert x A) = x + ∑A"
proof -
have "∑(insert x A) = ∑{x} + ∑A"
by (metis insert_is_Un assms finite.emptyI finite.insertI sum_union)
thus ?thesis
by auto
qed
lemma sum_fun_insert:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
shows "∑(f ` (insert x A)) = f x + ∑(f ` A)"
by (simp add: assms)
text ‹Now we show that set comprehensions with nested suprema can
be flattened.›
lemma flatten1_im:
fixes f :: "'a ⇒ 'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
and "finite (B :: 'a set)"
shows "∑((λx. ∑(f x ` B)) ` A) = ∑((λp. f (fst p) (snd p)) ` (A × B))"
proof -
have "∀z. ∑((λx. ∑(f x ` B)) ` A) ≤ z ⟷ ∑((λp. f (fst p) (snd p)) ` (A × B)) ≤ z"
by (simp add: assms finite_cartesian_product sum_fun_image_sup)
thus ?thesis
by (simp add: eq_iff)
qed
lemma flatten2_im:
fixes f :: "'a ⇒ 'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A ::'a set)"
and "finite (B ::'a set)"
shows "∑((λy. ∑ ((λx. f x y) ` A)) ` B) = ∑((λp. f (fst p) (snd p)) ` (A × B))"
by (simp only: flatten1_im assms cart_flip)
lemma sum_fla