# Theory Signatures

(* Title:      Signatures for Kleene Algebra
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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)

(*
class residual_r_op =
fixes residual_r :: "'a ⇒ 'a ⇒ 'a" (infixr "→" 60)

class residual_l_op =
fixes residual_l :: "'a ⇒ 'a ⇒ 'a" (infixl "←" 60)
*)

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

(* Title:      From Semilattices to Dioids
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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)"

lemma add_left_idem [ac_simps]: "x + (x + y) = x + y"

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"
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
show "x ≤ y ⟹ y ≤ x ⟹ x = y"
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"
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 (* join_semilattice *)

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

sublocale join: bounded_semilattice_sup_bot "(+)" "(≤)" "(<)" 0

lemma no_trivial_inverse: "x ≠ 0 ⟹ ¬(∃y. x + y = 0)"

end (* join_semilattice_zero *)

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
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
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

semigroup reduct of a near dioid is a semilattice. Near dioids are
therefore ordered by the semilattice order.›

subclass join_semilattice

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"
hence "(x + y) ⋅ z = y ⋅ z"
by simp
thus "x ⋅ z ≤ y ⋅ z"
qed

lemma "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
(* nitpick [expect=genuine] -- "3-element counterexample" *)
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 (* near_dioid *)

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

lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
proof -
assume "x ≤ y"
hence "x + y = y"
also have "z ⋅ x + z ⋅ y ≤ z ⋅ (x + y)"
using subdistl_var by blast
moreover have "... = z ⋅ y"
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"

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

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

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 (* ab_near_semiring_one *)

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"

end (* ab_near_semiring_one_zerol *)

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 (* ab_pre_semiring_one_zerol *)

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}"

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 (*selective_near_semiring*)

class selective_semiring = selective_near_semiring + semiring_one_zero

begin

subclass dioid_one_zero ..

end (* selective_semiring *)

end


# Theory Dioid_Models

(* Title:      Models of Dioids
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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

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: ― ‹the complex product›
"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"
show "X ⋅ 1 = X"
qed

end (* instantiation *)

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)"
show "X + Y = Y + X"
show "(X + Y) ⋅ Z = X ⋅ Z + Y ⋅ Z"
by (auto simp add: plus_set_def c_prod_def)
show "1 ⋅ X = X"
show "X ⋅ 1 = X"
show "0 + X = X"
show "0 ⋅ X = 0"
show "X ⋅ 0 = 0"
show "X ⊆ Y ⟷ X + Y = Y"
show "X ⊂ Y ⟷ X ⊆ Y ∧ X ≠ Y"
by (fact psubset_eq)
show "X + X = X"
show "X ⋅ (Y + Z) = X ⋅ Y + X ⋅ Z"
by (auto simp add: plus_set_def c_prod_def)
qed

end (* instantiation *)

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)"
show "1 * xs = xs"
show "xs * 1 = xs"
qed

end  (* instantiation *)

text ‹Languages as sets of lists have already been formalised in
Isabelle in various places. We can now obtain much of their algebra

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"

lemma first_t_fusion [simp]: "last x = first y ⟹ first (t_fusion x y) = first x"

lemma last_t_fusion [simp]: "last x = first y ⟹ last (t_fusion x y) = last y"

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
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"
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 = {}"
show "x ⋅ {} = {}"
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"
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 (* instantiation *)

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
unit is minus infinity and the multiplicative unit is zero.›

datatype mreal = mreal real | MInfty  ― ‹minus infinity›

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 (* instantiation *)

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  ― ‹plus infinity›

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 (* instantiation *)

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  ― ‹plus infinity›

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 (* instantiation *)

end


# Theory Matrix

(* Title:      Matrix Model of Kleene Algebra
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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)"

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.›

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

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)"

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)"

"A + 0 = (A::('a::monoid_add,'m,'n) matrix)"
by (cases A, simp add: zero_matrix_def)

"0 + A = (A::('a::monoid_add,'m,'n) matrix)"
by (cases A, simp add: zero_matrix_def)

"(A::('a::ab_semigroup_add,'m,'n) matrix) + B = B + A"

"(A::('a::semigroup_add,'m,'n) matrix) + B + C = A + (B + C)"

"(A::('a::ab_semigroup_add,'m,'n) matrix) + (B + C) = B + (A + C)"

"A + 0 = (A::('a::monoid_add,'m) sqmatrix)"
by (cases A, simp add: zero_sqmatrix_def)

"0 + A = (A::('a::monoid_add,'m) sqmatrix)"
by (cases A, simp add: zero_sqmatrix_def)

"(A::('a::ab_semigroup_add,'m) sqmatrix) + B = B + A"

"(A::('a::semigroup_add,'m) sqmatrix) + B + C = A + (B + C)"

"(A::('a::ab_semigroup_add,'m) sqmatrix) + (B + C) = B + (A + C)"

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)

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))"

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.›

proof
fix a :: 'a
show "0 + a = a"
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)"
show "A + B = B + A"
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"
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

(* Title:      Conway Algebra
Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

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⇧†"

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⇧†"
(*nitpick [expect=genuine]*)
oops

lemma "y ⋅ x⇧† = y + y ⋅ x ⋅ x⇧†"
(*nitpick [expect=genuine]*)
oops

lemma "(x + y)⇧† = x⇧† ⋅ (y ⋅ x⇧†)⇧†"
(*nitpick [expect=genuine]*)
oops

lemma "(x⇧†)⇧† = x⇧†"
(*nitpick [expect=genuine]*)
oops

lemma "(1 + x)⇧⋆ = x⇧⋆"
(*nitpick [expect = genuine]*)
oops

lemma "x⇧† ⋅ x = x ⋅ x⇧†"
(*nitpick [expect=genuine]*)
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
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
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"

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"
(*nitpick [expect=genuine]*)
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"
(*nitpick [expect=genuine]*)
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"
thus ?thesis
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⇧†"
(*nitpick [expect=genuine]*)
oops

lemma "(x⇧†)⇧† = x⇧†"
(*nitpick [expect=genuine]*)
oops

lemma dagger_denest_var [simp]: "(x + y)⇧† = (x⇧† ⋅ y⇧†)⇧†"
(* nitpick [expect=genuine]*)
oops

lemma star2 [simp]: "(1 + x)⇧† = x⇧†"
(*nitpick [expect=genuine]*)
oops

end

end


# Theory Kleene_Algebra

(* Title:      Kleene Algebra
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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.

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⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "x ⋅ x⇧⋆ = x⇧⋆"
(*nitpick [expect=genuine]*)
oops

text ‹Next we show that starred elements are transitive.›

lemma star_trans_eq [simp]: "x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"
proof (rule order.antisym) ― ‹this splits an equation into two inequalities›
have "x⇧⋆ + x ⋅ x⇧⋆ ≤ x⇧⋆"
by auto
thus "x⇧⋆ ⋅ x⇧⋆ ≤ x⇧⋆"
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"
qed

lemma star_inductl_var_equiv [simp]: "x⇧⋆ ⋅ y ≤ y ⟷ x ⋅ y ≤ y"
proof
assume "x ⋅ y ≤ y"
thus "x⇧⋆ ⋅ y ≤ y"
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"
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"
(*nitpick [expect=genuine]*)
oops

lemma "x⇧⋆ ⋅ z ≤ y ⟹ z + x ⋅ y ≤ y"
(*nitpick [expect=genuine]*)
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⇧⋆"

lemma star_inductl_eq:  "z + x ⋅ y = y ⟹ x⇧⋆ ⋅ z ≤ y"

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"
qed

lemma star_one [simp]: "1⇧⋆ = 1"

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⇧⋆"
have"(x⇧⋆)⇧⋆ ⋅ (x⇧⋆)⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (fact star_trans)
hence "x ⋅ (x⇧⋆)⇧⋆ ≤ (x⇧⋆)⇧⋆"
by (meson star_inductl_var_equiv)
thus "x⇧⋆ ≤ (x⇧⋆)⇧⋆"
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⇧⋆"
qed

lemma "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "x ≤ x⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "x⇧⋆ ⋅ x ≤ x⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "1 + x ⋅ x⇧⋆ = x⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "x ⋅ z ≤ z ⋅ y ⟹ x⇧⋆ ⋅ z ≤ z ⋅ y⇧⋆"
(*nitpick [expect=genuine]*)
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⇧⋆"
also have "x ⋅ y ≤ z⇧⋆ ⋅ y"
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"
(*nitpick [expect=genuine]*)
oops

end (* left_near_kleene_algebra *)

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⇧⋆"
(*nitpick [expect=genuine]*)
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⇧⋆"
also have "...  ≤ z ⋅ y⇧⋆"
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⇧⋆"
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)⇧⋆"

lemma "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma star_slide_var1: "x⇧⋆ ⋅ x ≤ x ⋅ x⇧⋆"

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⇧⋆"
qed

lemma "1 + x⇧⋆ ⋅ x = x⇧⋆"
(*nitpick [expect=genuine]*)
oops

text ‹Next we relate the star and the reflexive transitive closure
operation.›

lemma star_rtc1_eq [simp]: "1 + x + x⇧⋆ ⋅ x⇧⋆ = x⇧⋆"

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⇧⋆"
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"
qed

lemma star_rtc_least_eq: "1 + x + y ⋅ y = y ⟹ x⇧⋆ ≤ y"

lemma "1 + x + y ⋅ y ≤ y ⟷ x⇧⋆ ≤ y"
(*nitpick [expect=genuine]*)
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)⇧⋆"

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)⇧⋆"
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⇧⋆)⇧⋆"
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⇧⋆)⇧⋆"
hence "(y ⋅ x⇧⋆)⇧⋆ ≤ (x + y)⇧⋆"
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⇧⋆)⇧⋆"

lemma star_denest_var_5 [ac_simps]: "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = y⇧⋆ ⋅ (x ⋅ y⇧⋆)⇧⋆"

lemma "x⇧⋆ ⋅ (y ⋅ x⇧⋆)⇧⋆ = (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧⋆"
(*nitpick [expect=genuine]*)
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⇧⋆)⇧⋆"
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⇧⋆)⇧⋆"

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⇧⋆"
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⇧⋆"
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⇧⋆"

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⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "y ⋅ x ≤ x⇧⋆ ⋅ y⇧⋆ ⟹ (x + y)⇧⋆ ≤ x⇧⋆ ⋅ y⇧⋆"
(* nitpick [expect=genuine] *) 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⇧⋆"
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⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "(x ⋅ y)⇧⋆ ⋅ x = x ⋅ (y ⋅ x)⇧⋆"
(*nitpick [expect=genuine]*)
oops

lemma "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
(* nitpick [expect=genuine] *)
oops

end (* left_pre_kleene_algebra *)

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"
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"
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"
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)⇧⋆)"
finally show ?thesis
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
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⇧⋆"
thus ?thesis
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)⇧⋆"
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)⇧⋆"
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)⇧⋆"
show "(1 + x) ⋅ (x ⋅ x)⇧⋆ ≤ x⇧⋆"
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"
qed

lemma boffa: "x ⋅ x = x ⟹ x⇧⋆ = 1 + x"
by (auto intro: boffa_var)

(*
text {*
For the following two lemmas, Isabelle could neither find a
counterexample nor a proof automatically.
*}

lemma "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧⋆ ≤ y⇧⋆ ⋅ z"
-- "unfortunately, no counterexample found"
oops

lemma star_sim3: "z ⋅ x = y ⋅ z ⟹ z ⋅ x⇧⋆ = y⇧⋆ ⋅ z"
-- "we conjecture that this is not provable"
oops
*)

end (* left_kleene_algebra *)

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

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 (* left_kleene_algebra_zerol *)

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"
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"
qed

sublocale conway: pre_conway star

lemma star_inductr_var: "y ⋅ x ≤ y ⟹ y ⋅ x⇧⋆ ≤ y"

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

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"
show "0 ⊙ x = 0"
by (metis annir opp_mult_def)
show "x ⊙ 0 = 0"
by (metis annil opp_mult_def)
show "x + x = x"
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 (* kleene_algebra *)

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⇧⋆)"
also have "... = x ⋅ (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y ⋅ y⇧⋆)"
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⇧⋆"
also have "... ≤ (x ⋅ y)⇧⋆ ⋅ x⇧⋆ + (x ⋅ y)⇧⋆ ⋅ y⇧⋆"
using conway_c2_var join.sup_mono by blast
also have "... = (x ⋅ y)⇧⋆ ⋅ (x⇧⋆ + y⇧⋆)"
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⇧⋆)"
qed

end (* commutative_kleene_algebra *)

end


# Theory Kleene_Algebra_Models

(* Title:      Models of Kleene Algebra
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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 (* dioid_one_zero *)

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)"

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 (* instantiation *)

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

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)"
show "x + y = y + x"
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"
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"
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  (* instantiation *)

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)"

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)"

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›

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)"

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)"

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"
show "sup z (inf x y) ≤ y ⟹ inf (bdl_star x) z ≤ y"
show "sup z (inf y x) ≤ y ⟹ inf z (bdl_star x) ≤ y"
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"
show "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
show "x ⋅ y = y ⋅ x"
unfolding times_pnat_def by (cases x, cases y, simp_all)
qed

end (* instantiation *)

end


# Theory Omega_Algebra

(* Title:      Omega Algebra
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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⇧ω"

lemma omega_coinduct_eq: "y = z + x ⋅ y ⟹ y ≤ x⇧ω + x⇧⋆ ⋅ z"

lemma omega_coinduct_eq_var1: "y = 1 + x ⋅ y ⟹ y ≤ x⇧ω + x⇧⋆"

lemma  omega_coinduct_eq_var2: "y = x ⋅ y ⟹ y ≤ x⇧ω"

lemma "y = x ⋅ y + z ⟹ y = x⇧⋆ ⋅ z + x⇧ω"
(* nitpick [expect=genuine] -- "2-element counterexample" *)
oops

lemma "y = 1 + x ⋅ y ⟹ y = x⇧ω + x⇧⋆"
(* nitpick [expect=genuine] -- "3-element counterexample" *)
oops

lemma "y = x ⋅ y ⟹ y = x⇧ω"
(* nitpick [expect=genuine] -- "2-element counterexample" *)
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⇧ω"
show  "x⇧ω ≤ x ⋅ x⇧ω"
by (fact omega_unfold)
qed

lemma omega_unfold_var: "z + x ⋅ x⇧ω ≤ x⇧ω + x⇧⋆ ⋅ z"

lemma "z + x ⋅ x⇧ω = x⇧ω + x⇧⋆ ⋅ z"
(* nitpick [expect=genuine] -- "4-element counterexample" *)
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)⇧ω"

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⇧ω"

definition top ("⊤")
where "⊤ = 1⇧ω"

lemma star_omega_3 [simp]: "(x⇧⋆)⇧ω = ⊤"
proof -
have "1 ≤ x⇧⋆"
by (fact star_ref)
hence "⊤ ≤ (x⇧⋆)⇧ω"
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⇧ω"
(*nitpick [expect=genuine] -- "2-element counterexample"*)
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"
(* nitpick [expect=genuine] -- "4-element counterexample" *)
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⇧ω"
also have "... ≤ y ⋅ z ⋅ x⇧ω"
finally show "z ⋅ x⇧ω ≤ y⇧ω"
qed

lemma "z ⋅ x ≤ y ⋅ z ⟹ z ⋅ x⇧ω ≤ y⇧ω ⋅ z"
(* nitpick [expect=genuine] -- "4-element counterexample" *)
oops

lemma "y ⋅ z  ≤ z ⋅ x ⟹ y⇧ω ≤ z ⋅ x⇧ω"
(* nitpick [expect=genuine] -- "2-element counterexample" *)
oops

lemma "y ⋅ z  ≤ z ⋅ x ⟹ y⇧ω ⋅ z ≤ x⇧ω"
(* nitpick [expect=genuine] -- "4-element counterexample" *)
oops

text ‹Next we prove transitivity of omega elements.›

lemma omega_omega: "(x⇧ω)⇧ω ≤ x⇧ω"
by (metis omega_1 omega_unfold_eq)

(*
lemma "x⇧ω ⋅ x⇧ω = x⇧ω"
nitpick -- "no proof, no counterexample"

lemma "(x⇧ω)⇧ω = x⇧ω"
nitpick -- "no proof, no counterexample"
*)

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⇧⋆)⇧ω"
also have "... = x ⋅ x ⋅ x⇧⋆ ⋅ (x ⋅ x⇧⋆)⇧ω"
also have "... = x ⋅ (x ⋅ x⇧⋆)⇧ω"
thus "(x ⋅ x⇧⋆)⇧ω ≤ x⇧ω"
using calculation omega_coinduct_eq_var2 by auto
show "x⇧ω ≤ (x ⋅ x⇧⋆)⇧ω"
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)⇧ω"
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)⇧ω"
qed

text ‹
This identity is called~(R4) in Wagner's paper.
›

lemma wagner_1_var [simp]: "(x⇧⋆ ⋅ x)⇧ω = x⇧ω"

lemma star_omega_4 [simp]: "(x⇧ω)⇧⋆ = 1 + x⇧ω"
proof (rule order.antisym)
have "(x⇧ω)⇧⋆ = 1 + x⇧ω ⋅ (x⇧ω)⇧⋆"
by simp
also have "... ≤ 1 + x⇧ω ⋅ ⊤"
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⇧ω)⇧⋆"
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⇧ω"

lemma omega_sum_unfold_ind: "(x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω ≤ (x + y)⇧ω"

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)⇧ω"
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)⇧ω"
thus "(x⇧⋆ ⋅ y)⇧ω + (x⇧⋆ ⋅ y)⇧⋆ ⋅ x⇧ω ≤ (x + y)⇧ω"
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)⇧ω"
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⇧ω"
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"
(* nitpick [expect=genuine] -- "3-element counterexample" *)
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"
hence "y ≤ x⇧⋆ ⋅ z"
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"

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)"

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

(* Title:      Kleene Algebra
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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"

(* FIXME: The equivalent, but perhaps more elegant point-free version
"x ∈ R O omega R ⟹ x ∈ omega R"
fails due to missing monotonicity lemmas. *)

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

(* Title:      Demonic refinement algebra
Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

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⇧∞"
(*nitpick [expect=genuine]*)
oops

lemma top_mult_annil [simp]: "⊤ ⋅ x = ⊤"
by (simp add: local.coinduction local.order.antisym top_ref)

lemma top_add_annil [simp]: "⊤ + x = ⊤"

lemma top_elim: "x ⋅ y ≤ x ⋅ ⊤"

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
qed

lemma iteration_ref_star: "x⇧⋆ ≤ x⇧∞"

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"

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⇧∞ ⋅ ⊤ = ⊤"

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⇧∞"
finally show "z ⋅ y⇧∞ ≤ x⇧∞ ⋅ z"
qed

text ‹Nitpick gives a counterexample to the dual simulation law.›

lemma "y ⋅ z ≤ z ⋅ x ⟹ y⇧∞ ⋅ z ≤ z ⋅ x⇧∞"
(*nitpick [expect=genuine]*)
oops

text ‹Next, we prove some sliding laws.›

lemma iteration_slide_var: "x ⋅ (y ⋅ x)⇧∞ ≤ (x ⋅ y)⇧∞ ⋅ x"

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)⇧∞"
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"
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⇧∞)⇧∞"
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"
thus ?thesis
by (metis add.commute iteration_sub_denest order.antisym coinduction distrib_right' iteration_sub_denest mult.assoc mult_oner order.antisym)
qed
(*
end

sublocale dra ⊆ conway_zerol strong_iteration
apply (unfold_locales)
apply simp

context dra
begin
*)
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⇧∞"
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⇧∞"
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
qed

lemma iteration_sim2: "y ⋅ x ≤ x ⋅ y ⟹ y⇧∞ ⋅ x⇧∞ ≤ x⇧∞ ⋅ y⇧∞"

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⇧∞"
hence "(x + y)⇧∞ ≤ x⇧∞ ⋅ y⇧∞"
by (metis mult.assoc iteration_denest2 iteration_star2 add.commute coinduction)
thus ?thesis
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⇧⋆›
finally have "y ⋅ (x + y⇧⋆ ⋅ z) ≤ (x + y⇧⋆ ⋅ z) ⋅ y⇧⋆"
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⇧∞"
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)⇧∞"
thus ?thesis
qed

text ‹Finally, we prove some blocking laws.›

text ‹Nitpick refutes the next lemma.›

lemma "x ⋅ y = 0 ⟹ x⇧∞ ⋅ y = y"
(*nitpick*)
oops

lemma iteration_idep: "x ⋅ y = 0 ⟹ x ⋅ y⇧∞ = x"

text ‹Nitpick refutes the next lemma.›

lemma "y ⋅ w ≤ x ⋅ y + z ⟹ y ⋅ w⇧∞ ≤ x⇧∞ ⋅ z"
(*nitpick [expect=genuine]*)
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

(* Title:      Generalised Hoare Logic for Kleene Algebra
Author:     Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

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

sublocale kleene_algebra < phl: it_pre_dioid where it = star ..

end


# Theory PHL_DRA

(* Title:      General Hoare Logic for Demonic Refinement Algebra
Author:     Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

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

end


# Theory Finite_Suprema

(* Title:      Finite Suprema
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹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)"

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
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)"

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
shows "∑((λy. ∑ ((λx. f x y)  A))  B) = ∑((λp. f (fst p) (snd p)`