Session Kleene_Algebra

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)"
  using local.add_assoc' local.add_comm by auto

lemma add_left_idem [ac_simps]: "x + (x + y) = x + y"
  unfolding add_assoc' [symmetric] by simp

text ‹The definition @{term "x  y  x + y = y"} of the order is
hidden in class @{class plus_ord}.

We show some simple order-based properties of semilattices. The
first one states that every semilattice is a partial order.›

subclass order
proof
  fix x y z :: 'a
  show "x < y  x  y  ¬ y  x"
    using local.add_comm local.less_def local.less_eq_def by force
  show "x  x"
    by (simp add: local.less_eq_def)
  show "x  y  y  z  x  z"
    by (metis add_assoc' less_eq_def)
  show "x  y  y  x  x = y"
    by (simp add: local.add_comm local.less_eq_def)
qed

text ‹Next we show that joins are least upper bounds.›

sublocale join: semilattice_sup "(+)"
  by (unfold_locales; simp add: ac_simps local.less_eq_def)

text ‹Next we prove that joins are isotone (order preserving).›

lemma add_iso: "x  y  x + z  y + z"
  using join.sup_mono by blast

text ‹
  The next lemma links the definition of order as @{term "x  y  x + y = y"}
  with a perhaps more conventional one known, e.g., from arithmetics.
›

lemma order_prop: "x  y  (z. x + z = y)"
proof
  assume "x  y"
  hence "x + y = y"
    by (simp add: less_eq_def)
  thus "z. x + z = y"
    by auto
next
  assume "z. x + z = y"
  then obtain c where "x + c = y"
    by auto
  hence "x + c  y"
    by simp
  thus "x  y"
    by simp
qed

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

subclass comm_monoid_add
  by (unfold_locales, simp_all add: add_assoc') (simp add: add_comm)

sublocale join: bounded_semilattice_sup_bot "(+)" "(≤)" "(<)" 0
  by unfold_locales (simp add: local.order_prop)
  
lemma no_trivial_inverse: "x  0  ¬(y. x + y = 0)"
  by (metis local.add_0_right local.join.sup_left_idem)

end (* 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
addition is idempotent. This generalises the notion of (additively)
idempotent semirings by dropping one distributivity law. Near dioids
are a starting point for process algebras.

By modelling variants of dioids as variants of semirings in which
addition is idempotent we follow the tradition of
Birkhoff~\cite{birkhoff67lattices}, but deviate from the definitions
in Gondran and Minoux's book~\cite{gondran10graphs}.›

class near_dioid = ab_near_semiring + plus_ord +
  assumes add_idem' [simp]: "x + x = x"

begin

text ‹Since addition is idempotent, the additive (commutative)
semigroup reduct of a near dioid is a semilattice. Near dioids are
therefore ordered by the semilattice order.›

subclass join_semilattice
  by unfold_locales (auto simp add: add.commute add.left_commute)

text ‹It follows that multiplication is right-isotone (but not
necessarily left-isotone).›

lemma mult_isor: "x  y  x  z  y  z"
proof -
  assume "x  y"
  hence "x + y = y"
    by (simp add: less_eq_def)
  hence "(x + y)  z = y  z"
    by simp
  thus "x  z  y  z"
    by (simp add: less_eq_def)
qed

lemma "x  y  z  x  z  y"
  (* 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
  by (simp add: local.join.sup_absorb2 local.subdistl)

lemma mult_isol: "x  y  z  x  z  y"
proof -
  assume "x  y"
  hence "x + y = y"
    by (simp add: less_eq_def)
  also have "z  x + z  y  z  (x + y)"
    using subdistl_var by blast
  moreover have "... = z  y"
    by (simp add: calculation)
  ultimately show "z  x  z  y"
    by auto
qed

lemma mult_isol_var: "u  x  v  y  u  v  x  y"
  by (meson local.dual_order.trans local.mult_isor mult_isol)

lemma mult_double_iso: "x  y  w  x  z  w  y  z"
  by (simp add: local.mult_isor mult_isol)

text ‹The following lemmas are relevant to propositional Hoare logic.›

lemma phl_cons2: "w  x  z  y  y  w  z  y  y  x"
  using local.order_trans mult_isol by blast

lemma phl_seq: 
assumes "p  x  x  r"
and "r  y  y  q" 
shows "p  (x  y)  x  y  q"
proof -
  have "p  x  y  x  r  y"
    using assms(1) mult_isor by blast
  thus ?thesis
    by (metis assms(2) order_prop order_trans subdistl mult_assoc)
qed

lemma phl_cond: 
assumes "u  v  v  u  v" and "u  w  w  u  w" 
and "x y. u  (x + y)  u  x + u  y"
and "u  v  x  x  z" and "u  w  y  y  z" 
shows "u  (v  x + w  y)  (v  x + w  y)  z"
proof -
  have a: "u  v  x  v  x  z" and b: "u  w  y  w  y  z"
    by (metis assms mult_assoc phl_seq)+
  have  "u  (v  x + w  y)  u  v  x + u  w  y"
    using assms(3) mult_assoc by auto
  also have "...  v  x  z + w  y  z"
    using a b join.sup_mono by blast
  finally show ?thesis
    by simp
qed

lemma phl_export1:
assumes "x  y  y  x  y"
and "(x  y)  z  z  w"
shows "x  (y  z)  (y  z)  w"
proof -
  have "x  y  z  y  x  y  z"
    by (simp add: assms(1) mult_isor)
  thus ?thesis
    using assms(1) assms(2) mult_assoc phl_seq by auto 
qed

lemma phl_export2: 
assumes "z  w  w  z  w"
and "x  y  y  z"
shows "x  (y  w)  y  w  (z  w)"
proof -
  have "x  y  w  y  z  w"
    using assms(2) mult_isor by blast
  thus ?thesis
    by (metis assms(1) dual_order.trans order_prop subdistl mult_assoc)
qed

end (* 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
  by unfold_locales (simp add: local.distrib_left)

subsection ‹Families of Nearsemirings with a Multiplicative Unit›

text ‹Multiplicative units are important, for instance, for defining
an operation of finite iteration or Kleene star on dioids. We do not
introduce left and right units separately since we have no application
for this.›

class ab_near_semiring_one = ab_near_semiring + one +
  assumes mult_onel [simp]: "1  x = x"
  and mult_oner [simp]: "x  1 = x"

begin

subclass monoid_mult
  by (unfold_locales, simp_all)

end (* 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"
  by (subst add_commute) simp

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}"
  by (simp add: local.select)

text ‹It follows immediately that every selective near semiring is a near dioid.›

subclass near_dioid
  by (unfold_locales, meson select)

text ‹Moreover, the order in a selective near semiring is obviously linear.›

subclass linorder
  by (unfold_locales, metis add.commute join.sup.orderI select)

end (*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
domain~\cite{desharnaismoellerstruth06kad}.

The advantage of formally linking these models with the abstract
axiomatisations of dioids is that all abstract theorems are
automatically available in all models. It therefore makes sense to
establish models for the strongest possible axiomatisations (whereas
theorems should be proved for the weakest ones).›


subsection ‹The Powerset Dioid over a Monoid›

text ‹We assume a multiplicative monoid and define the usual complex
product on sets of elements. We formalise the well known result that
this lifting induces a dioid.›

instantiation set :: (monoid_mult) monoid_mult
begin

  definition one_set_def:
    "1 = {1}"

  definition c_prod_def: ― ‹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"
      by (simp add: one_set_def c_prod_def)
    show "X  1 = X"
      by (simp add: one_set_def c_prod_def)
  qed

end (* instantiation *)

instantiation set :: (monoid_mult) dioid_one_zero
begin

  definition zero_set_def:
    "0 = {}"

  definition plus_set_def:
    "A + B = A  B"

  instance
  proof
    fix X Y Z :: "'a set"
    show "X + Y + Z = X + (Y + Z)"
      by (simp add: Un_assoc plus_set_def)
    show "X + Y = Y + X"
      by (simp add: Un_commute plus_set_def)
    show "(X + Y)  Z = X  Z + Y  Z"
      by (auto simp add: plus_set_def c_prod_def)
    show "1  X = X"
      by (simp add: one_set_def c_prod_def)
    show "X  1 = X"
      by (simp add: one_set_def c_prod_def)
    show "0 + X = X"
      by (simp add: plus_set_def zero_set_def)
    show "0  X = 0"
      by (simp add: c_prod_def zero_set_def)
    show "X  0 = 0"
      by (simp add: c_prod_def zero_set_def)
    show "X  Y  X + Y = Y"
      by (simp add: plus_set_def subset_Un_eq)
    show "X  Y  X  Y  X  Y"
      by (fact psubset_eq)
    show "X + X = X"
      by (simp add: Un_absorb plus_set_def)
    show "X  (Y + Z) = X  Y + X  Z"
      by (auto simp add: plus_set_def c_prod_def)
  qed

end (* 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)"
      by (simp add: times_list_def)
    show "1 * xs = xs"
      by (simp add: one_list_def times_list_def)
    show "xs * 1 = xs"
      by (simp add: one_list_def times_list_def)
  qed

end  (* instantiation *)

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

type_synonym 'a lan = "'a list set"

interpretation lan_dioid: dioid_one_zero "(+)" "(⋅)" "1::'a lan" "0" "(⊆)" "(⊂)" ..


subsection ‹Relation Dioids›

text ‹We now show that binary relations under union, relational
composition, the identity relation, the empty relation and set
inclusion form dioids. Due to the well developed relation library of
Isabelle this is entirely trivial.›

interpretation rel_dioid: dioid_one_zero "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)"
  by (unfold_locales, auto)

interpretation rel_monoid: monoid_mult Id "(O)" ..


subsection ‹Trace Dioids›

text ‹Traces have been considered, for instance, by
Kozen~\cite{kozen00hoare} in the context of Kleene algebras with
tests. Intuitively, a trace is an execution sequence of a labelled
transition system from some state to some other state, in which state
labels and action labels alternate, and which begin and end with a
state label.

Traces generalise words: words can be obtained from traces by
forgetting state labels. Similarly, sets of traces generalise
languages.

In this section we show that sets of traces under union, an
appropriately defined notion of complex product, the set of all traces
of length zero, the empty set of traces and set inclusion form a
dioid.

We first define the notion of trace and the product of traces, which
has been called \emph{fusion product} by Kozen.›

type_synonym ('p, 'a) trace = "'p × ('a × 'p) list"

definition first :: "('p, 'a) trace  'p" where
  "first = fst"

lemma first_conv [simp]: "first (p, xs) = p"
  by (unfold first_def, simp)

fun last :: "('p, 'a) trace  'p" where
  "last (p, []) = p"
| "last (_, xs) = snd (List.last xs)"

lemma last_append [simp]: "last (p, xs @ ys) = last (last (p, xs), ys)"
proof (cases xs)
  show "xs = []  last (p, xs @ ys) = last (last (p, xs), ys)"
    by simp
  show "a list. xs = a # list 
    last (p, xs @ ys) = last (last (p, xs), ys)"
  proof (cases ys)
    show "a list. xs = a # list; ys = []
       last (p, xs @ ys) = last (last (p, xs), ys)"
      by simp
    show "a list aa lista. xs = a # list; ys = aa # lista
       last (p, xs @ ys) = last (last (p, xs), ys)"
      by simp
  qed
qed

text ‹The fusion product is a partial operation. It is undefined if
the last element of the first trace and the first element of the
second trace are different. If these elements are the same, then the
fusion product removes the first element from the second trace and
appends the resulting object to the first trace.›

definition t_fusion :: "('p, 'a) trace  ('p, 'a) trace  ('p, 'a) trace" where
  "t_fusion x y  if last x = first y then (fst x, snd x @ snd y) else undefined"

text ‹We now show that the first element and the last element of a
trace are a left and right unit for that trace and prove some other
auxiliary lemmas.›

lemma t_fusion_leftneutral [simp]: "t_fusion (first x, []) x = x"
  by (cases x, simp add: t_fusion_def)

lemma fusion_rightneutral [simp]: "t_fusion x (last x, []) = x"
  by (simp add: t_fusion_def)

lemma first_t_fusion [simp]: "last x = first y  first (t_fusion x y) = first x"
  by (simp add: first_def t_fusion_def)

lemma last_t_fusion [simp]: "last x = first y  last (t_fusion x y) = last y"
  by (simp add: first_def t_fusion_def)

text ‹Next we show that fusion of traces is associative.›

lemma t_fusion_assoc [simp]:
  " last x = first y; last y = first z   t_fusion x (t_fusion y z) = t_fusion (t_fusion x y) z"
  by (cases x, cases y, cases z, simp add: t_fusion_def)


subsection ‹Sets of Traces›

text ‹We now lift the fusion product to a complex product on sets of
traces. This operation is total.›

no_notation
  times (infixl "" 70)

definition t_prod :: "('p, 'a) trace set  ('p, 'a) trace set  ('p, 'a) trace set" (infixl "" 70)
where "X  Y = {t_fusion u v| u v. u  X  v  Y  last u = first v}"

text ‹Next we define the empty set of traces and the set of traces
of length zero as the multiplicative unit of the trace dioid.›

definition t_zero :: "('p, 'a) trace set" where
  "t_zero  {}"

definition t_one :: "('p, 'a) trace set" where
  "t_one  p. {(p, [])}"

text ‹We now provide elimination rules for trace products.›

lemma t_prod_iff:
  "w  XY  (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  XY"
  by (meson t_prod_iff)

lemma t_prod_elim [elim]:
  "w  XY  u v. w = t_fusion u v  u  X  v  Y  last u = first v"
  by (meson t_prod_iff)

text ‹Finally we prove the interpretation statement that sets of traces
under union and the complex product based on trace fusion together
with the empty set of traces and the set of traces of length one forms
a dioid.›

interpretation trace_dioid: dioid_one_zero "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)"
apply unfold_locales
apply (auto simp add: t_prod_def t_one_def t_zero_def t_fusion_def)
apply (metis last_append)
apply (metis last_append append_assoc)
done

no_notation
  t_prod (infixl "" 70)


subsection ‹The Path Diod›

text ‹The next model we consider are sets of paths in a graph. We
consider two variants, one that contains the empty path and one that
doesn't. The former leads to more difficult proofs and a more involved
specification of the complex product. We start with paths that include
the empty path. In this setting, a path is a list of nodes.›

subsection ‹Path Models with the Empty Path›

type_synonym 'a path = "'a list"

text ‹Path fusion is defined similarly to trace
fusion. Mathematically it should be a partial operation. The fusion of
two empty paths yields the empty path; the fusion between a non-empty
path and an empty one is undefined; the fusion of two non-empty paths
appends the tail of the second path to the first one.

We need to use a total alternative and make sure that undefined paths
do not contribute to the complex product.›

fun p_fusion :: "'a path  'a path  'a path" where
  "p_fusion [] _ = []"
| "p_fusion _ [] = []"
| "p_fusion ps (q # qs) = ps @ qs"

lemma p_fusion_assoc:
  "p_fusion ps (p_fusion qs rs) = p_fusion (p_fusion ps qs) rs"
proof (induct rs)
  case Nil show ?case
    by (metis p_fusion.elims p_fusion.simps(2))
  case Cons show ?case
  proof (induct qs)
    case Nil show ?case
      by (metis neq_Nil_conv p_fusion.simps(1) p_fusion.simps(2))
    case Cons show ?case
      proof -
        have "ps. ([] = ps  hd ps # tl ps = ps)  ((q qs. q # qs  ps)  []  ps)"
          using list.collapse by fastforce
        moreover hence "ps q qs. p_fusion ps (q # qs) = ps @ qs  [] = ps"
          by (metis p_fusion.simps(3))
        ultimately show ?thesis
          by (metis (no_types) Cons_eq_appendI append_eq_appendI p_fusion.simps(1) p_fusion.simps(3))
      qed
  qed
qed

text ‹This lemma overapproximates the real situation, but it holds
in all cases where path fusion should be defined.›

lemma p_fusion_last:
  assumes "List.last ps = hd qs"
  and "ps  []"
  and "qs  []"
  shows "List.last (p_fusion ps qs) = List.last qs"
  by (metis (hide_lams, no_types) List.last.simps List.last_append append_Nil2 assms list.sel(1) neq_Nil_conv p_fusion.simps(3))

lemma p_fusion_hd: "ps  []; qs  []  hd (p_fusion ps qs) = hd ps"
  by (metis list.exhaust p_fusion.simps(3) append_Cons list.sel(1))

lemma nonempty_p_fusion: "ps  []; qs  []  p_fusion ps qs  []"
  by (metis list.exhaust append_Cons p_fusion.simps(3) list.simps(2))

text ‹We now define a condition that filters out undefined paths in
the complex product.›

abbreviation p_filter :: "'a path  'a path  bool" where
"p_filter ps qs  ((ps = []  qs = [])  (ps  []  qs  []  (List.last ps) = hd qs))"

no_notation
  times (infixl "" 70)

definition p_prod :: "'a path set  'a path set  'a path set" (infixl "" 70)
where "X  Y = {rs . ps  X. qs  Y. rs = p_fusion ps qs  p_filter ps qs}"

lemma p_prod_iff:
  "ps  X  Y  (qs rs. ps = p_fusion qs rs  qs  X  rs  Y  p_filter qs rs)"
  by (unfold p_prod_def) auto

text ‹Due to the complexity of the filter condition, proving
properties of complex products can be tedious.›

lemma p_prod_assoc: "(X  Y)  Z = X  (Y  Z)"
proof (rule set_eqI)
  fix ps
  show "ps  (X  Y)  Z  ps  X  (Y  Z)"
  proof (cases ps)
    case Nil thus ?thesis
      by auto (metis nonempty_p_fusion p_prod_iff)+
  next
    case Cons thus ?thesis
      by (auto simp add: p_prod_iff) (metis (hide_lams, mono_tags) nonempty_p_fusion p_fusion_assoc p_fusion_hd p_fusion_last)+
  qed
qed

text ‹We now define the multiplicative unit of the path dioid as the
set of all paths of length one, including the empty path, and show the
unit laws with respect to the path product.›

definition p_one :: "'a path set" where
  "p_one  {p . q::'a. p = [q]}  {[]}"

lemma p_prod_onel [simp]: "p_one  X = X"
proof (rule set_eqI)
    fix ps
    show "ps  p_one  X  ps  X"
    proof (cases ps)
      case Nil thus ?thesis
        by (auto simp add: p_one_def p_prod_def, metis nonempty_p_fusion not_Cons_self)
    next
      case Cons thus ?thesis
        by (auto simp add: p_one_def p_prod_def, metis append_Cons append_Nil list.sel(1) neq_Nil_conv p_fusion.simps(3), metis Cons_eq_appendI list.sel(1) last_ConsL list.simps(3) p_fusion.simps(3) self_append_conv2)
    qed
qed

lemma p_prod_oner [simp]: "X  p_one = X"
proof (rule set_eqI)
    fix ps
    show "ps  X  p_one  ps  X"
    proof (cases ps)
      case Nil thus ?thesis
        by (auto simp add: p_one_def p_prod_def, metis nonempty_p_fusion not_Cons_self2, metis p_fusion.simps(1))
    next
      case Cons thus ?thesis
        by (auto simp add: p_one_def p_prod_def, metis append_Nil2 neq_Nil_conv p_fusion.simps(3), metis list.sel(1) list.simps(2) p_fusion.simps(3) self_append_conv)
    qed
qed

text ‹Next we show distributivity laws at the powerset level.›

lemma p_prod_distl: "X  (Y  Z) = X  Y  X  Z"
proof (rule set_eqI)
  fix ps
  show "ps  X  (Y  Z)  ps  X  Y  X  Z"
  by (cases ps) (auto simp add: p_prod_iff)
qed


lemma p_prod_distr: "(X  Y)  Z = X  Z  Y  Z"
proof (rule set_eqI)
  fix ps
  show "ps  (X  Y)  Z  ps  X  Z  Y  Z"
    by (cases ps) (auto simp add: p_prod_iff)
qed

text ‹Finally we show that sets of paths under union, the complex
product, the unit set and the empty set form a dioid.›

interpretation path_dioid: dioid_one_zero "(∪)" "(⋅)" p_one "{}" "(⊆)" "(⊂)"
proof
  fix x y z :: "'a path set"
  show  "x  y  z = x  (y  z)"
    by auto
  show "x  y = y  x"
    by auto
  show "(x  y)  z = x  (y  z)"
    by (fact p_prod_assoc)
  show "(x  y)  z = x  z  y  z"
    by (fact p_prod_distr)
  show "p_one  x = x"
    by (fact p_prod_onel)
  show "x  p_one = x"
    by (fact p_prod_oner)
  show "{}  x = x"
    by auto
  show "{}  x = {}"
    by (metis all_not_in_conv p_prod_iff)
  show "x  {} = {}"
    by (metis all_not_in_conv p_prod_iff)
  show "(x  y) = (x  y = y)"
    by auto
  show "(x  y) = (x  y  x  y)"
    by auto
  show "x  x = x"
    by auto
  show "x  (y  z) = x  y  x  z"
    by (fact p_prod_distl)
qed

no_notation
  p_prod (infixl "" 70)


subsection ‹Path Models without the Empty Path›

text ‹We now build a model of paths that does not include the empty
path and therefore leads to a simpler complex product.›

datatype 'a ppath = Node 'a | Cons 'a "'a ppath"

primrec pp_first :: "'a ppath  'a" where
  "pp_first (Node x)   = x"
| "pp_first (Cons x _) = x"

primrec pp_last :: "'a ppath  'a" where
  "pp_last (Node x)    = x"
| "pp_last (Cons _ xs) = pp_last xs"

text ‹The path fusion product (although we define it as a total
funcion) should only be applied when the last element of the first
argument is equal to the first element of the second argument.›

primrec pp_fusion :: "'a ppath  'a ppath  'a ppath" where
  "pp_fusion (Node x) ys = ys"
| "pp_fusion (Cons x xs) ys = Cons x (pp_fusion xs ys)"

text ‹We now go through the same steps as for traces and paths
before, showing that the first and last element of a trace a left or
right unit for that trace and that the fusion product on traces is
associative.›

lemma pp_fusion_leftneutral [simp]: "pp_fusion (Node (pp_first x)) x = x"
  by simp

lemma pp_fusion_rightneutral [simp]: "pp_fusion x (Node (pp_last x)) = x"
  by (induct x) simp_all

lemma pp_first_pp_fusion [simp]:
  "pp_last x = pp_first y  pp_first (pp_fusion x y) = pp_first x"
  by (induct x) simp_all

lemma pp_last_pp_fusion [simp]:
  "pp_last x = pp_first y  pp_last (pp_fusion x y) = pp_last y"
  by (induct x) simp_all

lemma pp_fusion_assoc [simp]:
  " pp_last x = pp_first y; pp_last y = pp_first z   pp_fusion x (pp_fusion y z) = pp_fusion (pp_fusion x y) z"
  by (induct x) simp_all

text ‹We now lift the path fusion product to a complex product on
sets of paths. This operation is total.›

definition pp_prod :: "'a ppath set  'a ppath set  'a ppath set" (infixl "" 70)
  where "XY = {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  XY  (u v. w = pp_fusion u v  u  X  v  Y  pp_last u = pp_first v)"
  by (unfold pp_prod_def) auto

interpretation ppath_dioid: dioid_one_zero "(∪)" "(⋅)" pp_one "{}" "(⊆)" "(⊂)"
proof
  fix x y z :: "'a ppath set"
  show "x  y  z = x  (y  z)"
    by auto
  show "x  y = y  x"
    by auto
  show "x  y  z = x  (y  z)"
    by (auto simp add: pp_prod_def, metis pp_first_pp_fusion pp_fusion_assoc, metis pp_last_pp_fusion)
  show "(x  y)  z = x  z  y  z"
    by (auto simp add: pp_prod_def)
  show "pp_one  x = x"
    by (auto simp add: pp_one_def pp_prod_def, metis pp_fusion.simps(1) pp_last.simps(1) rangeI)
  show "x  pp_one = x"
    by (auto simp add: pp_one_def pp_prod_def, metis pp_first.simps(1) pp_fusion_rightneutral rangeI)
  show "{}  x = x"
    by auto
  show "{}  x = {}"
    by (simp add: pp_prod_def)
  show "x  {} = {}"
    by (simp add: pp_prod_def)
  show "x  y  x  y = y"
    by auto
   show "x  y  x  y  x  y"
     by auto
  show "x  x = x"
    by auto
  show "x  (y  z) = x  y  x  z"
    by (auto simp add: pp_prod_def)
qed

no_notation
  pp_prod (infixl "" 70)

subsection ‹The Distributive Lattice Dioid›

text ‹A bounded distributive lattice is a distributive lattice with
a least and a greatest element. Using Isabelle's lattice theory file
we define a bounded distributive lattice as an axiomatic type class
and show, using a sublocale statement, that every bounded distributive
lattice is a dioid with one and zero.›

class bounded_distributive_lattice = bounded_lattice + distrib_lattice

sublocale bounded_distributive_lattice  dioid_one_zero sup inf top bot less_eq
proof
  fix x y z
  show "sup (sup x y) z = sup x (sup y z)"
    by (fact sup_assoc)
  show "sup x y = sup y x"
    by (fact sup.commute)
  show "inf (inf x y) z = inf x (inf y z)"
    by (metis inf.commute inf.left_commute)
  show "inf (sup x y) z = sup (inf x z) (inf y z)"
    by (fact inf_sup_distrib2)
  show "inf top x = x"
    by simp
  show "inf x top = x"
    by simp
  show "sup bot x = x"
    by simp
  show "inf bot x = bot"
    by simp
  show "inf x bot = bot"
    by simp
  show "(x  y) = (sup x y = y)"
    by (fact le_iff_sup)
  show "(x < y) = (x  y  x  y)"
    by auto
  show "sup x x = x"
    by simp
  show "inf x (sup y z) = sup (inf x y) (inf x z)"
    by (fact inf_sup_distrib1)
qed


subsection ‹The Boolean Dioid›

text ‹In this section we show that the booleans form a dioid,
because the booleans form a bounded distributive lattice.›

instantiation bool :: bounded_distributive_lattice
begin

  instance ..

end (* 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
maximum, the operation of multiplication is addition, the additive
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)"
  by (simp add: UNIV_atMost)

text ‹Our matrix type is similar to \mbox{'a^'n^'m›} from
{\em HOL/Multivariate\_Analysis/Finite\_Cartesian\_Product.thy}, but
(i)~we explicitly define a type constructor for matrices and square
matrices, and (ii)~in the definition of operations, e.g., matrix
multiplication, we impose weaker sort requirements on the element
type.›

context notes [[typedef_overloaded]]
begin

datatype ('a,'m,'n) matrix = Matrix "'m atMost  'n atMost  'a"

datatype ('a,'m) sqmatrix = SqMatrix "'m atMost  'm atMost  'a"

end

fun sqmatrix_of_matrix where
  "sqmatrix_of_matrix (Matrix A) = SqMatrix A"

fun matrix_of_sqmatrix where
  "matrix_of_sqmatrix (SqMatrix A) = Matrix A"


subsection ‹0 and 1›

instantiation matrix :: (zero,type,type) zero
begin
  definition zero_matrix_def: "0  Matrix (λi j. 0)"
  instance ..
end

instantiation sqmatrix :: (zero,type) zero
begin
  definition zero_sqmatrix_def: "0  SqMatrix (λi j. 0)"
  instance ..
end

text ‹Tricky sort issues: compare @{term one_matrix} with @{term
one_sqmatrix} \dots›

instantiation matrix :: ("{zero,one}",len,len) one
begin
  definition one_matrix_def:
    "1  Matrix (λi j. if Rep_atMost i = Rep_atMost j then 1 else 0)"
  instance ..
end

instantiation sqmatrix :: ("{zero,one}",type) one
begin
  definition one_sqmatrix_def:
    "1  SqMatrix (λi j. if i = j then 1 else 0)"
  instance ..
end


subsection ‹Matrix Addition›

fun matrix_plus where
  "matrix_plus (Matrix A) (Matrix B) = Matrix (λi j. A i j + B i j)"

instantiation matrix :: (plus,type,type) plus
begin
  definition plus_matrix_def: "A + B  matrix_plus A B"
  instance ..
end

lemma plus_matrix_def' [simp]:
  "Matrix A + Matrix B = Matrix (λi j. A i j + B i j)"
  by (simp add: plus_matrix_def)

instantiation sqmatrix :: (plus,type) plus
begin
  definition plus_sqmatrix_def:
    "A + B  sqmatrix_of_matrix (matrix_of_sqmatrix A + matrix_of_sqmatrix B)"
  instance ..
end

lemma plus_sqmatrix_def' [simp]:
  "SqMatrix A + SqMatrix B = SqMatrix (λi j. A i j + B i j)"
  by (simp add: plus_sqmatrix_def)

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

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

lemma matrix_add_commute [simp]:
  "(A::('a::ab_semigroup_add,'m,'n) matrix) + B = B + A"
  by (cases A, cases B, simp add: add.commute)

lemma matrix_add_assoc:
  "(A::('a::semigroup_add,'m,'n) matrix) + B + C = A + (B + C)"
  by (cases A, cases B, cases C, simp add: add.assoc)

lemma matrix_add_left_commute [simp]:
  "(A::('a::ab_semigroup_add,'m,'n) matrix) + (B + C) = B + (A + C)"
  by (metis matrix_add_assoc matrix_add_commute)

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

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

lemma sqmatrix_add_commute [simp]:
  "(A::('a::ab_semigroup_add,'m) sqmatrix) + B = B + A"
  by (cases A, cases B, simp add: add.commute)

lemma sqmatrix_add_assoc:
  "(A::('a::semigroup_add,'m) sqmatrix) + B + C = A + (B + C)"
  by (cases A, cases B, cases C, simp add: add.assoc)

lemma sqmatrix_add_left_commute [simp]:
  "(A::('a::ab_semigroup_add,'m) sqmatrix) + (B + C) = B + (A + C)"
  by (metis sqmatrix_add_commute sqmatrix_add_assoc)


subsection ‹Order (via Addition)›

instantiation matrix :: (plus,type,type) plus_ord
begin
  definition less_eq_matrix_def:
    "(A::('a, 'b, 'c) matrix)  B  A + B = B"
  definition less_matrix_def:
    "(A::('a, 'b, 'c) matrix) < B  A  B  A  B"

  instance
  proof
    fix A B :: "('a, 'b, 'c) matrix"
    show "A  B  A + B = B"
      by (metis less_eq_matrix_def)
    show "A < B  A  B  A  B"
      by (metis less_matrix_def)
  qed
end

instantiation sqmatrix :: (plus,type) plus_ord
begin
  definition less_eq_sqmatrix_def:
    "(A::('a, 'b) sqmatrix)  B  A + B = B"
  definition less_sqmatrix_def:
    "(A::('a, 'b) sqmatrix) < B  A  B  A  B"

  instance
  proof
    fix A B :: "('a, 'b) sqmatrix"
    show "A  B  A + B = B"
      by (metis less_eq_sqmatrix_def)
    show "A < B  A  B  A  B"
      by (metis less_sqmatrix_def)
  qed
end


subsection ‹Matrix Multiplication›

fun matrix_times :: "('a::{comm_monoid_add,times},'m,'k) matrix  ('a,'k,'n) matrix  ('a,'m,'n) matrix" where
  "matrix_times (Matrix A) (Matrix B) = Matrix (λi j. sum (λk. A i k * B k j) (UNIV::'k atMost set))"

notation matrix_times (infixl "*M" 70)

instantiation sqmatrix :: ("{comm_monoid_add,times}",type) times
begin
  definition times_sqmatrix_def:
    "A * B = sqmatrix_of_matrix (matrix_of_sqmatrix A *M matrix_of_sqmatrix B)"
  instance ..
end

lemma times_sqmatrix_def' [simp]:
  "SqMatrix A * SqMatrix B = SqMatrix (λi j. sum (λk. A i k * B k j) (UNIV::'k atMost set))"
  by (simp add: times_sqmatrix_def)

lemma matrix_mult_0_right [simp]:
  "(A::('a::{comm_monoid_add,mult_zero},'m,'n) matrix) *M 0 = 0"
  by (cases A, simp add: zero_matrix_def)

lemma matrix_mult_0_left [simp]:
  "0 *M (A::('a::{comm_monoid_add,mult_zero},'m,'n) matrix) = 0"
  by (cases A, simp add: zero_matrix_def)

lemma sum_delta_r_0 [simp]:
  " finite S; j  S   (kS. 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   (kS. 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   (kS. (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   (kS. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = f i j"
  by (induct S rule: finite_induct, auto)

lemma matrix_mult_1_left [simp]:
  "1 *M (A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) = A"
  by (cases A, simp add: one_matrix_def)

lemma matrix_mult_assoc:
  "(A::('a::semiring_0,'m,'n) matrix) *M B *M C = A *M (B *M C)"
 apply (cases A)
 apply (cases B)
 apply (cases C)
 apply (simp add: sum_distrib_right sum_distrib_left mult.assoc)
 apply (subst sum.swap)
 apply (rule refl)
done

lemma matrix_mult_distrib_left:
  "(A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) *M (B + C) = A *M B + A *M C"
  by (cases A, cases B, cases C, simp add: distrib_left sum.distrib)

lemma matrix_mult_distrib_right:
  "((A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) + B) *M C = A *M C + B *M C"
  by (cases A, cases B, cases C, simp add: distrib_right sum.distrib)

lemma sqmatrix_mult_0_right [simp]:
  "(A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) * 0 = 0"
  by (cases A, simp add: zero_sqmatrix_def)

lemma sqmatrix_mult_0_left [simp]:
  "0 * (A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) = 0"
  by (cases A, simp add: zero_sqmatrix_def)

lemma sqmatrix_mult_1_right [simp]:
  "(A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) * 1 = A"
  by (cases A, simp add: one_sqmatrix_def)

lemma sqmatrix_mult_1_left [simp]:
  "1 * (A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) = A"
  by (cases A, simp add: one_sqmatrix_def)

lemma sqmatrix_mult_assoc:
  "(A::('a::{semiring_0,monoid_mult},'m) sqmatrix) * B * C = A * (B * C)"
 apply (cases A)
 apply (cases B)
 apply (cases C)
 apply (simp add: sum_distrib_right sum_distrib_left mult.assoc)
 apply (subst sum.swap)
 apply (rule refl)
done

lemma sqmatrix_mult_distrib_left:
  "(A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) * (B + C) = A * B + A * C"
  by (cases A, cases B, cases C, simp add: distrib_left sum.distrib)

lemma sqmatrix_mult_distrib_right:
  "((A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) + B) * C = A * C + B * C"
  by (cases A, cases B, cases C, simp add: distrib_right sum.distrib)


subsection ‹Square-Matrix Model of Dioids›

text ‹The following subclass proofs are necessary to connect parts
of our algebraic hierarchy to the hierarchy found in the Isabelle/HOL
library.›

subclass (in ab_near_semiring_one_zerol) comm_monoid_add
proof
  fix a :: 'a
  show "0 + a = a"
    by (fact add_zerol)
qed

subclass (in semiring_one_zero) semiring_0
proof
  fix a :: 'a
  show "0 * a = 0"
    by (fact annil)
  show "a * 0 = 0"
    by (fact annir)
qed

subclass (in ab_near_semiring_one) monoid_mult ..

instantiation sqmatrix :: (dioid_one_zero,len) dioid_one_zero
begin
  instance
  proof
    fix A B C :: "('a, 'b) sqmatrix"
    show "A + B + C = A + (B + C)"
      by (fact sqmatrix_add_assoc)
    show "A + B = B + A"
      by (fact sqmatrix_add_commute)
    show "A * B * C = A * (B * C)"
      by (fact sqmatrix_mult_assoc)
    show "(A + B) * C = A * C + B * C"
      by (fact sqmatrix_mult_distrib_right)
    show "1 * A = A"
      by (fact sqmatrix_mult_1_left)
    show "A * 1 = A"
      by (fact sqmatrix_mult_1_right)
    show "0 + A = A"
      by (fact sqmatrix_add_0_left)
    show "0 * A = 0"
      by (fact sqmatrix_mult_0_left)
    show "A * 0 = 0"
      by (fact sqmatrix_mult_0_right)
    show "A + A = A"
      by (cases A, simp)
    show "A * (B + C) = A * B + A * C"
      by (fact sqmatrix_mult_distrib_left)
  qed
end

subsection ‹Kleene Star for Matrices›

text ‹We currently do not implement the Kleene star of matrices,
since this is complicated.›

end

Theory Conway

(* 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"
  by (simp add: dagger_refl local.join.sup_absorb2)

lemma star_1l: "x  x  x"
  using dagger_unfoldl local.join.sup.bounded_iff by blast

lemma star_1r: "x  x  x"
  using dagger_unfoldr local.join.sup.bounded_iff by blast

lemma dagger_ext: "x  x"
  by (metis dagger_unfoldl_distr local.join.sup.boundedE star_1r)

lemma dagger_trans_eq [simp]: "x  x = x"
  by (metis dagger_unfoldr_eq local.dagger_denest local.join.sup.idem mult_assoc)

lemma dagger_subdist:  "x  (x + y)"
  by (metis dagger_unfoldr_distr local.dagger_denest local.order_prop)

lemma dagger_subdist_var:  "x + y  (x + y)"
  using dagger_subdist local.join.sup_commute by fastforce

lemma dagger_iso [intro]: "x  y  x  y"
  by (metis less_eq_def dagger_subdist)

lemma star_square: "(x  x)  x"
  by (metis dagger_plus_one dagger_subdist dagger_trans_eq dagger_unfoldr_distr dagger_denest
    distrib_right' order.eq_iff join.sup_commute less_eq_def mult_onel mult_assoc)

lemma dagger_rtc1_eq [simp]: "1 + x + x  x = x"
  by (simp add: local.dagger_ext local.dagger_refl local.join.sup_absorb2)

text ‹Nitpick refutes the next lemmas.›

lemma " y + y  x  x = y  x"
(*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
   by (metis add_commute local.distrib_left mult_assoc)
qed

lemma dagger_slide_var1: "x  x  x  x"
  by (metis local.dagger_unfoldl_distr local.dagger_unfoldr_eq local.distrib_left order.eq_iff local.mult_1_right mult_assoc)

lemma dagger_slide_var1_eq: "x  x = x  x"
  by (metis local.dagger_unfoldl_distr local.dagger_unfoldr_eq local.distrib_left local.mult_1_right mult_assoc)

lemma dagger_slide_eq: "(x  y)  x = x  (y  x)"
proof -
  have "(x  y)  x = x + x  (y  x)  y  x"
    by (metis local.dagger_prod_unfold local.distrib_right' local.mult_onel)
  also have "... = x  (1 + (y  x)  y  x)"
    using local.distrib_left local.mult_1_right mult_assoc by presburger
  finally show ?thesis
    by (simp add: mult_assoc)
qed

end

subsection ‹Conway Algebras with  Zero›

class near_conway_base_zerol = near_conway_base + near_dioid_one_zerol

begin

lemma dagger_annil [simp]: "1 + x  0 = (x  0)"
  by (metis annil dagger_unfoldl_eq mult.assoc)

lemma zero_dagger [simp]: "0 = 1"
  by (metis add_0_right annil dagger_annil)

end

class pre_conway_base_zerol = near_conway_base_zerol + pre_dioid

class conway_base_zerol = pre_conway_base_zerol + dioid

subclass (in pre_conway_base_zerol) pre_conway_base ..

subclass (in conway_base_zerol) conway_base ..

context conway_base_zerol
begin

lemma "z  x  y  z  z  x  y  z"
(*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"
    by (simp add: local.join.le_supI1)
  thus ?thesis
    by (simp add: local.dagger_simr)
qed

end

class near_conway_zerol = near_conway + near_dioid_one_zerol

class pre_conway = near_conway + pre_dioid_one

begin

subclass pre_conway_base ..

lemma dagger_slide: "x  (y  x) = (x  y)  x"
  by (metis add.commute dagger_prod_unfold join.sup_least mult_1_right mult.assoc subdistl dagger_slide_var dagger_unfoldl_distr order.antisym)

lemma dagger_denest2: "(x + y) = x  (y  x)"
  by (metis dagger_denest dagger_slide)

lemma preservation2: "y  x  y  (x  y)  x  x  y"
  by (metis dagger_slide local.dagger_iso local.mult_isol)

lemma preservation1_eq: "x  y  x  y  x  y  x  y  (x  y)  x = x  y"
  by (simp add: local.dagger_simr order.eq_iff preservation2)

end

class pre_conway_zerol = near_conway_zerol + pre_dioid_one_zerol

begin

subclass pre_conway ..

end

class conway = pre_conway + dioid_one

class conway_zerol = pre_conway + dioid_one_zerol

begin

subclass conway_base ..

text ‹Nitpick refutes the next lemmas.›

lemma "1 = 1"
(*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.

We start with near dioids, then consider pre-dioids and finally
dioids. It turns out that many of the known laws of Kleene algebras
hold already in these more general settings. In fact, all our
equational theorems have been proved within left Kleene algebras, as
expected.

Although most of the proofs in this file could be fully automated by
Sledgehammer and Metis, we display step-wise proofs as they would
appear in a text book. First, this file may then be useful as a
reference manual on Kleene algebra. Second, it is better protected
against changes in the underlying theories and supports easy
translation of proofs into other settings.›

class left_near_kleene_algebra = near_dioid_one + star_op +
  assumes star_unfoldl: "1 + x  x  x"
  and star_inductl: "z + x  y  y  x  z  y"

begin

text ‹First we prove two immediate consequences of the unfold
axiom. The first one states that starred elements are reflexive.›

lemma star_ref [simp]: "1  x"
  using star_unfoldl by auto
 
text ‹Reflexivity of starred elements implies, by definition of the
order, that~$1$ is an additive unit for starred elements.›

lemma star_plus_one [simp]: "1 + x = x"
  using less_eq_def star_ref by blast

lemma star_1l [simp]: "x  x  x"
  using star_unfoldl by auto

lemma "x  x  x"
(*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"
    by (simp add: star_inductl)
  next show "x  x  x"
    using mult_isor star_ref by fastforce
qed

lemma star_trans: "x  x  x"
  by simp
  
text ‹We now derive variants of the star induction axiom.›

lemma star_inductl_var: "x  y  y  x  y  y"
proof -
  assume "x  y  y"
  hence "y + x  y  y"
    by simp
  thus "x  y  y"
    by (simp add: star_inductl)
qed

lemma star_inductl_var_equiv [simp]: "x  y  y  x  y  y"
proof
  assume "x  y  y"
  thus "x  y  y"
    by (simp add: star_inductl_var)
next
  assume "x  y  y"
  hence  "x  y = y"
    by (metis order.eq_iff mult_1_left mult_isor star_ref)
  moreover hence "x  y = x  x  y"
    by (simp add: mult.assoc)
  moreover have "...  x  y"
    by (metis mult_isor star_1l)
  ultimately show "x  y  y" 
    by auto
qed

lemma star_inductl_var_eq:  "x  y = y  x  y  y"
  by (metis order.eq_iff star_inductl_var)

lemma star_inductl_var_eq2: "y = x  y  y = x  y"
proof -
  assume hyp: "y = x  y"
  hence "y  x  y"
    using mult_isor star_ref by fastforce
  thus "y = x  y"
    using hyp order.eq_iff by auto
qed

lemma "y = x  y  y = x  y"
(*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"
  by (simp add: star_inductl_one)

lemma star_inductl_eq:  "z + x  y = y  x  z  y"
  by (simp add: star_inductl)

text ‹We now prove two facts related to~$1$.›

lemma star_subid: "x  1  x = 1"
proof -
  assume "x  1"
  hence "1 + x  1  1"
    by simp
  hence "x  1"
    by (metis mult_oner star_inductl)
  thus "x = 1"
    by (simp add: order.antisym)
qed

lemma star_one [simp]: "1 = 1"
  by (simp add: star_subid)

text ‹We now prove a subdistributivity property for the star (which
is equivalent to isotonicity of star).›

lemma star_subdist:  "x  (x + y)"
proof -
  have "x  (x + y)  (x + y)  (x + y)"
    by simp
  also have "...   (x + y)"
    by (metis star_1l)
  thus ?thesis
    using calculation order_trans star_inductl_star by blast
qed

lemma star_subdist_var:  "x + y  (x + y)"
  using join.sup_commute star_subdist by force

lemma star_iso [intro]: "x  y  x  y"
  by (metis less_eq_def star_subdist)

text ‹We now prove some more simple properties.›

lemma star_invol [simp]: "(x) = x"
proof (rule order.antisym)
  have "x  x = x"
    by (fact star_trans_eq)
  thus "(x)  x"
    by (simp add: star_inductl_star)
  have"(x)  (x)  (x)"
    by (fact star_trans)
  hence "x  (x)  (x)"
    by (meson star_inductl_var_equiv)
  thus "x  (x)"
    by (simp add: star_inductl_star)
qed

lemma star2 [simp]: "(1 + x) = x"
proof (rule order.antisym)
  show "x  (1 + x)"
    by auto
  have "x + x  x  x"
    by simp
  thus "(1 + x)  x"
    by (simp add: star_inductl_star)
qed

lemma "1 + x  x  x"
(*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"
    by (simp add: star_inductl)
  also have "x  y  z  y"
    by (simp add: assm mult_isor)
  thus "x  y  z"
    using calculation order.trans by blast
qed

lemma star_star_closure: "x  z  (x)  z"
  by (metis star_invol)

lemma star_closed_unfold: "x = x  x = 1 + x  x"
  by (metis star_plus_one star_trans_eq)

lemma "x = x  x = 1 + x  x"
(*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"
    by (simp add: mult_isor)
  also have "...   z  y"
    by (simp add: mult_isol mult_assoc)
  finally have "x  z  y  z  y"
    by simp
  hence "z + x  z  y  z  y"
    by (metis join.sup_least mult_isol mult_oner star_ref)
  thus "x  z  z  y"
    by (simp add: star_inductl mult_assoc)
qed

text ‹The next lemma is used in omega algebras to prove, for
instance, Bachmair and Dershowitz's separation of termination
theorem~\cite{bachmair86commutation}. The property at the left-hand
side of the equivalence is known as \emph{quasicommutation}.›

lemma quasicomm_var: "y  x  x  (x + y)  y  x  x  (x + y)"
proof
  assume "y  x  x  (x + y)"
  thus "y  x  x  (x + y)"
    using star_sim1 by force
next
  assume "y  x  x  (x + y)"
  thus "y  x  x  (x + y)"
    by (meson mult_isor order_trans star_ext)
qed

lemma star_slide1: "(x  y)  x  x  (y  x)"
  by (simp add: mult_assoc star_sim1)

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

lemma star_slide_var1: "x  x  x  x" 
  by (simp add: star_sim1)

text ‹We now show that the (left) star unfold axiom can be strengthened to an equality.›

lemma star_unfoldl_eq [simp]: "1 + x  x = x"
proof (rule order.antisym)
  show "1 + x  x  x"
    by (fact star_unfoldl)
  have "1 + x  (1 + x  x)  1 + x  x"
    by (meson join.sup_mono eq_refl mult_isol star_unfoldl)
  thus "x  1 + x  x"
    by (simp add: star_inductl_one)
qed

lemma "1 + x  x = x"
(*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"
  by (simp add: join.sup.absorb2)

lemma star_rtc1: "1 + x + x  x  x"
  by simp

lemma star_rtc2: "1 + x  x  x  x = x"
proof
  assume "1 + x  x  x"
  thus "x = x"
    by (simp add: order.eq_iff local.star_inductl_one)
next
  assume "x = x"
  thus "1 + x  x  x"
    using local.star_closed_unfold by auto
qed

lemma star_rtc3: "1 + x  x = x  x = x"
  by (metis order_refl star_plus_one star_rtc2 star_trans_eq)

lemma star_rtc_least: "1 + x + y  y  y  x  y"
proof -
  assume "1 + x + y  y  y"
  hence "1 + x  y  y"
    by (metis join.le_sup_iff mult_isol_var star_trans_eq star_rtc2)
  thus "x  y"
    by (simp add: star_inductl_one)
qed

lemma star_rtc_least_eq: "1 + x + y  y = y  x  y"
  by (simp add: star_rtc_least)

lemma "1 + x + y  y  y  x  y"
(*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)"
  by (simp add: prod_star_closure star_iso)

text ‹We now prove variants of sum-elimination laws under a star.
These are also known a denesting laws or as sum-star laws.›

lemma star_denest [simp]: "(x + y) = (x  y)"
proof (rule order.antisym)
  have "x + y  x  y"
    by (metis join.sup.bounded_iff mult_1_right mult_isol_var mult_onel star_ref star_ext)
  thus "(x + y)  (x  y)"
    by (fact star_iso)
  have "x  y  (x + y)"
    by (fact star_subdist_var_3)
  thus "(x  y)  (x + y)"
    by (simp add: prod_star_closure star_inductl_star)
qed

lemma star_sum_var [simp]: "(x + y) = (x + y)"
  by simp

lemma star_denest_var [simp]: "x  (y  x) = (x + y)"
proof (rule order.antisym)
  have "1  x  (y  x)"
    by (metis mult_isol_var mult_oner star_ref)
  moreover have "x  x  (y  x)  x  (y  x)"
    by (simp add: mult_isor)
  moreover have "y  x  (y  x)  x  (y  x)"
    by (metis mult_isol_var mult_onel star_1l star_ref)
  ultimately have "1 + (x + y)  x  (y  x)  x  (y  x)"
    by auto
  thus "(x + y)  x  (y  x)"
    by (metis mult.assoc mult_oner star_inductl)
  have "(y  x)  (y  x)"
    by (simp add: mult_isol_var star_iso)
  hence "(y  x)  (x + y)"
    by (metis add.commute star_denest)
  moreover have "x  (x + y)"
    by (fact star_subdist)
  ultimately show "x  (y  x)  (x + y)"
    using prod_star_closure by blast
qed

lemma star_denest_var_2 [simp]: "x  (y  x) = (x  y)"
  by simp

lemma star_denest_var_3 [simp]: "x  (y  x) = (x  y)"
  by simp

lemma star_denest_var_4 [ac_simps]: "(y  x) = (x  y)"
  by (metis add_comm star_denest)

lemma star_denest_var_5 [ac_simps]: "x  (y  x) = y  (x  y)"
  by (simp add: star_denest_var_4)

lemma "x  (y  x) = (x  y)  x"
(*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)"
    by (simp add: mult_assoc)
  thus "(x + y)  x  y  (x + y)"
    by simp
  have "1  (x + y)  x  y"
    by (metis dual_order.trans mult_1_left mult_isor star_ref)
  moreover have "(x + y)  (x + y)  x  y  (x + y)  x  y"
    using mult_isor star_1l by presburger
  ultimately have "1 + (x + y)  (x + y)  x  y  (x + y)  x  y"
    by simp
  thus "(x + y)  (x + y)  x  y"
    by (metis mult.assoc star_inductl_one)
qed

lemma star_denest_var_8 [simp]: "x  y  (x  y) = (x  y)"
  by (simp add: mult_assoc)

lemma star_denest_var_9 [simp]: "(x  y)  x  y = (x  y)"
  using star_denest_var_7 by simp

text ‹The following statements are well known from term
rewriting. They are all variants of the Church-Rosser theorem in
Kleene algebra~\cite{struth06churchrosser}. But first we prove a law
relating two confluence properties.›

lemma confluence_var [iff]: "y  x  x  y  y  x  x  y"
proof
  assume "y  x  x  y"
  thus "y  x  x  y"
    using star_sim1 by fastforce
next
  assume "y  x  x  y"
  thus "y  x  x  y"
    by (meson mult_isor order_trans star_ext)
qed

lemma church_rosser [intro]: "y  x  x  y  (x + y) = x  y"
proof (rule order.antisym)
  assume "y  x  x  y"
  hence "x  y  (x  y)  x  x  y  y"
    by (metis mult_isol mult_isor mult.assoc)
  hence "x  y  (x  y)  x  y"
    by (simp add: mult_assoc)
  moreover have "1  x  y"
    by (metis dual_order.trans mult_1_right mult_isol star_ref)
  ultimately have "1 + x  y  (x  y)  x  y"
    by simp
  hence "(x  y)  x  y"
    by (simp add: star_inductl_one)
  thus "(x + y)  x  y"
    by simp
  thus "x  y  (x + y)"
    by simp 
qed

lemma church_rosser_var: "y  x  x  y  (x + y) = x  y"
  by fastforce

lemma church_rosser_to_confluence: "(x + y)  x  y  y  x  x  y"
  by (metis add_comm order.eq_iff star_subdist_var_3)

lemma church_rosser_equiv: "y  x  x  y  (x + y) = x  y"
  using church_rosser_to_confluence order.eq_iff by blast

lemma confluence_to_local_confluence: "y  x  x  y  y  x  x  y"
  by (meson mult_isol_var order_trans star_ext)


lemma "y  x  x  y  y  x  x  y"
(*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"
    by (simp add: order.eq_iff)
qed

lemma sup_id_star2: "1  x  x  x = x"
  by (metis order.antisym mult_isol mult_oner star_1r)

lemma "1 + x  x = x"
(*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"
    by (simp add: star_inductl_one)
qed

text ‹The following more complex unfold law has been used as an
axiom, called prodstar, by Conway~\cite{conway71regular}.›

lemma star_prod_unfold [simp]: "1 + x  (y  x)  y = (x  y)"
proof (rule order.antisym)
  have "(x  y) = 1 + (x  y)  x  y"
    by (simp add: mult_assoc)
  thus "(x  y)  1 + x  (y  x)  y"
    by (metis join.sup_mono mult_isor order_refl star_slide1)
  have "1 + x  (y  x)  y  1 + x  y   (x  y)"
    by (metis join.sup_mono eq_refl mult.assoc mult_isol star_slide1)
  thus "1 + x  (y  x)  y  (x  y)"
    by simp
qed

text ‹The slide laws, which have previously been inequalities, now
become equations.›

lemma star_slide [ac_simps]: "(x  y)  x = x  (y  x)"
proof -
  have "x  (y  x) = x  (1 + y  (x  y)  x)"
    by simp
  also have "... = (1 + x  y  (x  y))  x"
    by (simp add: distrib_left mult_assoc)
  finally show ?thesis
    by simp
qed

lemma star_slide_var [ac_simps]: "x  x = x  x"
  by (metis mult_onel mult_oner star_slide)

lemma star_sum_unfold_var [simp]: "1 + x  (x + y)  y = (x + y)"
  by (metis star_denest star_denest_var_3 star_denest_var_4 star_plus_one star_slide)

text ‹The following law shows how starred sums can be unfolded.›

lemma star_sum_unfold [simp]: "x + x  y  (x + y) = (x + y)"
proof -
  have "(x + y) = x  (y  x )"
    by simp
  also have "... = x  (1 + y  x  (y  x ))"
    by simp
  also have "... = x  (1 + y  (x + y))"
    by (simp add: mult.assoc)
  finally show ?thesis
    by (simp add: distrib_left mult_assoc)
qed

text ‹The following property appears in process algebra.›

lemma troeger: "(x + y)  z = x  (y  (x + y)  z + z)"
proof -
  have "(x + y)  z = x  z + x  y  (x + y)  z"
    by (metis (full_types) distrib_right star_sum_unfold)
  thus ?thesis
    by (simp add: add_commute distrib_left mult_assoc)
qed

text ‹The following properties are related to a property from
propositional dynamic logic which has been attributed to Albert
Meyer~\cite{harelkozentiuryn00dynamic}. Here we prove it as a theorem
of Kleene algebra.›

lemma star_square: "(x  x)  x"
proof -
  have "x  x  x  x"
    by (simp add: prod_star_closure)
  thus ?thesis
    by (simp add: star_inductl_star)  
qed

lemma meyer_1 [simp]: "(1 + x)  (x  x) = x"
proof (rule order.antisym)
  have "x   (1 + x)  (x  x) = x  (x  x) + x  x  (x  x)"
    by (simp add: distrib_left)
  also have "...  x  (x  x) + (x  x)"
    using join.sup_mono star_1l by blast
  finally have "x   (1 + x)  (x  x)  (1 + x)  (x  x)"
    by (simp add: join.sup_commute)
  moreover have "1  (1 + x)  (x  x)"
    using join.sup.coboundedI1 by auto
  ultimately have "1 + x  (1 + x)  (x  x)  (1 + x)  (x  x)"
    by auto
  thus "x  (1 + x)  (x  x)"
    by (simp add: star_inductl_one mult_assoc)
  show "(1 + x)  (x  x)  x"
    by (simp add: prod_star_closure star_square)
qed

text ‹The following lemma says that transitive elements are equal to
their transitive closure.›

lemma tc: "x  x  x  x  x = x"
proof -
  assume "x  x  x"
  hence "x + x  x  x"
    by simp
  hence "x  x  x"
    by (fact star_inductl)
  thus  "x  x = x"
    by (metis mult_isol mult_oner star_ref star_slide_var order.eq_iff)
qed

lemma tc_eq: "x  x = x  x  x = x"
  by (auto intro: tc)


text ‹The next fact has been used by Boffa~\cite{boffa90remarque} to
axiomatise the equational theory of regular expressions.›

lemma boffa_var: "x  x  x  x = 1 + x"
proof -
  assume "x  x  x"
  moreover have "x = 1 + x  x"
    by simp
  ultimately show "x = 1 + x"
    by (simp add: tc)
qed

lemma boffa: "x  x = x  x = 1 + x"
  by (auto intro: boffa_var)

(*
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
  by standard (simp_all add: local.star_slide)

lemma star_zero [simp]: "0 = 1"
  by (rule local.conway.zero_dagger)

text ‹
In principle,~$1$ could therefore be defined from~$0$ in this setting.
›

end (* 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"
    by (simp add: mult_isor)
  finally have "y  z  x  y  z"
    by simp
  moreover have "z  y  z"
    using mult_isor star_ref by fastforce
  ultimately have "z + y  z  x  y  z"
    by simp
  thus "z  x  y  z"
    by (simp add: star_inductr)
qed

sublocale conway: pre_conway star
  by standard (simp add: star_sim2)

lemma star_inductr_var: "y  x  y  y  x  y"
  by (simp add: star_inductr)

lemma star_inductr_var_equiv: "y  x  y  y  x  y"
  by (meson order_trans mult_isol star_ext star_inductr_var)

lemma star_sim3: "z  x = y  z  z  x = y  z"
  by (simp add: order.eq_iff star_sim1 star_sim2)

lemma star_sim4: "x  y   y  x  x  y  y  x"
  by (auto intro: star_sim1 star_sim2)

lemma star_inductr_eq: "z + y  x = y  z  x  y"
  by (auto intro: star_inductr)

lemma star_inductr_var_eq: "y  x = y  y  x  y"
  by (auto intro: star_inductr_var)

lemma star_inductr_var_eq2: "y  x = y  y  x = y"
  by (metis mult_onel star_one star_sim3)

lemma bubble_sort: "y  x  x  y  (x + y) = x  y"
  by (fastforce intro: star_sim4)

lemma independence1: "x  y = 0  x  y = y"
proof -
  assume "x  y = 0"
  moreover have "x  y = y + x  x  y"
    by (metis distrib_right mult_onel star_unfoldr_eq)
  ultimately show "x  y = y"
    by (metis add_0_left add.commute join.sup_ge1 order.eq_iff star_inductl_eq)
qed

lemma independence2: "x  y = 0  x  y = x"
  by (metis annil mult_onel star_sim3 star_zero)

lemma lazycomm_var: "y  x  x  (x + y) + y  y  x  x  (x + y) + y"
proof
  let ?t = "x  (x + y)"
  assume hyp: "y  x  ?t + y"
  have "(?t + y)  x = ?t  x + y  x"
    by (fact distrib_right)
  also have "...  ?t  x + ?t + y"
    using hyp join.sup.coboundedI2 join.sup_assoc by auto
  also have "...  ?t + y"
    using eq_refl join.sup_least join.sup_mono mult_isol prod_star_closure star_subdist_var_1 mult_assoc by presburger
  finally have "y + (?t + y)  x  ?t + y"
    by simp
  thus "y  x  x  (x + y) + y"
    by (fact star_inductr)
next
  assume "y  x  x  (x + y) + y"
  thus "y  x  x  (x + y) + y"
    using dual_order.trans mult_isol star_ext by blast
qed

lemma arden_var: "(y v. y  x  y + v  y  x  v)  z = x  z + w  z = x  w"
  by (auto simp: add_comm order.eq_iff star_inductl_eq)

lemma "(x y. y  x  y  y = 0)  y  x  y + z  y  x  z"
  by (metis eq_refl mult_onel)

end

text ‹Finally, here come the Kleene algebras \`a~la
Kozen~\cite{kozen94complete}. We only prove quasi-identities in this
section. Since left Kleene algebras are complete with respect to the
equational theory of regular expressions and regular languages, all
identities hold already without the right star induction axiom.›

class kleene_algebra = left_kleene_algebra_zero +
  assumes star_inductr': "z + y  x  y  z  x  y"
begin

subclass kleene_algebra_zerol 
  by standard (simp add: star_inductr')

sublocale conway_zerol: conway star ..

text ‹
The next lemma shows that opposites of Kleene algebras (i.e., Kleene
algebras with the order of multiplication swapped) are again Kleene
algebras.
›

lemma dual_kleene_algebra:
  "class.kleene_algebra (+) (⊙) 1 0 (≤) (<) star"
proof
  fix x y z :: 'a
  show "(x  y)  z = x  (y  z)"
    by (metis mult.assoc opp_mult_def)
  show "(x + y)  z = x  z + y  z"
    by (metis opp_mult_def distrib_left)
  show "1  x = x"
    by (metis mult_oner opp_mult_def)
  show "x  1 = x"
    by (metis mult_onel opp_mult_def)
  show "0 + x = x"
    by (fact add_zerol)
  show "0  x = 0"
    by (metis annir opp_mult_def)
   show "x  0 = 0"
    by (metis annil opp_mult_def)
  show "x + x = x"
    by (fact add_idem)
  show "x  (y + z) = x  y + x  z"
    by (metis distrib_right opp_mult_def)
  show "z  x  z  (x + y)"
    by (metis mult_isor opp_mult_def order_prop)
  show "1 + x  x  x"
    by (metis opp_mult_def order_refl star_slide_var star_unfoldl_eq)
  show "z + x  y  y  x  z  y"
    by (metis opp_mult_def star_inductr)
  show "z + y  x  y  z  x  y"
    by (metis opp_mult_def star_inductl)
qed

end (* 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)"
    by (simp add: add_assoc)
  also have "... = x  (x  y)  (x + y  y)"
    by (simp add: add_commute)
  also have "... = (x  y)  (x  x) + (x  y)  x  y  y"
    using distrib_left mult_comm mult_assoc by force
  also have "...  (x  y)  x + (x  y)  x  y  y"
    using add_iso mult_isol by force
  also have "...  (x  y)  x + (x  y)  y"
    using conway_c2_var join.sup_mono by blast
  also have "... = (x  y)  (x + y)"
    by (simp add: distrib_left)
  finally have "x  (x  y)  (x + y)  (x  y)  (x + y)" .
  moreover have "y  (x  y)  (x + y)"
    by (metis dual_order.trans join.sup_ge2 mult_1_left mult_isor star_ref)
  ultimately have "y + x  (x  y)  (x + y)  (x  y)  (x + y)"
    by simp
  thus "x  y  (x  y)  (x + y)"
    by (simp add: mult.assoc star_inductl)
qed

end (* 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)"
  by (simp add: star_def)

  lemma star_contl: "X  Y = (n. X  Y ^ n)"
  by (auto simp add: star_elim c_prod_def)

  lemma star_contr: "X  Y = (n. X ^ n  Y)"
  by (auto simp add: star_elim c_prod_def)

  instance
  proof
    fix X Y Z :: "'a set"
    show "1 + X  X  X"
    proof -
      have "1 + X  X = (X ^ 0)  (n. X ^ (Suc n))"
        by (auto simp add: star_def c_prod_def plus_set_def one_set_def)
      also have "... = (n. X ^ n)"
        by (metis Un_0_Suc)
      also have "... = X"
        by (simp only: star_def)
      finally show ?thesis
        by (metis subset_refl)
    qed
  next
    fix X Y Z :: "'a set"
    assume hyp: "Z + X  Y  Y"
    show  "X  Z  Y"
      by (simp add: star_contr SUP_le_iff) (meson hyp dioid_one_zero_class.power_inductl)
  next
    fix X Y Z :: "'a set"
    assume hyp: "Z + Y  X  Y"
    show  "Z  X  Y"
      by (simp add: star_contl SUP_le_iff) (meson dioid_one_zero_class.power_inductr hyp) 
  qed

end (* 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
adapted from there.›

fun lang :: "'a rexp  'a lan" where
  "lang Zero = 0"  ― ‹{}›
| "lang One = 1"  ― ‹{[]}›
| "lang (Atom a) = {[a]}"
| "lang (Plus x y) = lang x + lang y"
| "lang (Times x y) = lang x  lang y"
| "lang (Star x) = (lang x)"

typedef 'a reg_lan = "range lang :: 'a lan set"
  by auto

setup_lifting type_definition_reg_lan

instantiation reg_lan :: (type) kleene_algebra
begin

  lift_definition star_reg_lan :: "'a reg_lan  'a reg_lan"
    is star
    by (metis (hide_lams, no_types) image_iff lang.simps(6) rangeI)

  lift_definition zero_reg_lan :: "'a reg_lan"
    is 0
    by (metis lang.simps(1) rangeI)

  lift_definition one_reg_lan :: "'a reg_lan"
    is 1
    by (metis lang.simps(2) rangeI)

  lift_definition less_eq_reg_lan :: "'a reg_lan  'a reg_lan  bool"
    is less_eq .

  lift_definition less_reg_lan :: "'a reg_lan  'a reg_lan  bool"
    is less .

  lift_definition plus_reg_lan :: "'a reg_lan  'a reg_lan  'a reg_lan"
    is plus
    by (metis (hide_lams, no_types) image_iff lang.simps(4) rangeI)

  lift_definition times_reg_lan :: "'a reg_lan  'a reg_lan  'a reg_lan"
    is times
    by (metis (hide_lams, no_types) image_iff lang.simps(5) rangeI)

  instance
  proof
    fix x y z :: "'a reg_lan"
    show "x + y + z = x + (y + z)"
      by transfer (metis join_semilattice_class.add_assoc')
    show "x + y = y + x"
      by transfer (metis join_semilattice_class.add_comm)
    show "x  y  z = x  (y  z)"
      by transfer (metis semigroup_mult_class.mult.assoc)
    show "(x + y)  z = x  z + y  z"
      by transfer (metis semiring_class.distrib_right)
    show "1  x = x"
      by transfer (metis monoid_mult_class.mult_1_left)
    show "x  1 = x"
      by transfer (metis monoid_mult_class.mult_1_right)
    show "0 + x = x"
      by transfer (metis join_semilattice_zero_class.add_zero_l)
    show "0  x = 0"
      by transfer (metis ab_near_semiring_one_zerol_class.annil)
    show "x  0 = 0"
      by transfer (metis ab_near_semiring_one_zero_class.annir)
    show "x  y  x + y = y"
      by transfer (metis plus_ord_class.less_eq_def)
    show "x < y  x  y  x  y"
      by transfer (metis plus_ord_class.less_def)
    show "x + x = x"
      by transfer (metis join_semilattice_class.add_idem)
    show "x  (y + z) = x  y + x  z"
      by transfer (metis semiring_class.distrib_left)
    show "z  x  z  (x + y)"
      by transfer (metis pre_dioid_class.subdistl)
    show "1 + x  x  x"
      by transfer (metis star_unfoldl)
    show "z + x  y  y  x  z  y"
      by transfer (metis star_inductl)
    show "z + y  x  y  z  x  y"
      by transfer (metis star_inductr)
  qed

end  (* 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)"
  by (simp add: power_is_relpow rtrancl_is_UN_relpow)

lemma rel_star_contl: "X O Y^* = (n. X O rel_dioid.power Y n)"
by (metis rel_star_def relcomp_UNION_distrib)

lemma rel_star_contr: "X^* O Y = (n. (rel_dioid.power X n) O Y)"
by (metis rel_star_def relcomp_UNION_distrib2)

interpretation rel_kleene_algebra: kleene_algebra "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl
proof
  fix x y z :: "'a rel"
  show "Id  x O x*  x*"
    by (metis order_refl r_comp_rtrancl_eq rtrancl_unfold)
next
  fix x y z :: "'a rel"
  assume "z  x O y  y"
  thus "x* O z  y"
    by (simp only: rel_star_contr, metis (lifting) SUP_le_iff rel_dioid.power_inductl)
next
  fix x y z :: "'a rel"
  assume "z  y O x  y"
  thus "z O x*  y"
    by (simp only: rel_star_contl, metis (lifting) SUP_le_iff rel_dioid.power_inductr)
qed

subsection ‹Trace Kleene Algebras›

text ‹Again, the proof that sets of traces form Kleene algebras
follows the same schema.›

definition t_star :: "('p, 'a) trace set  ('p, 'a) trace set" where
  "t_star X  n. trace_dioid.power X n"

lemma t_star_elim: "x  t_star X  (n. x  trace_dioid.power X n)"
  by (simp add: t_star_def)

lemma t_star_contl: "t_prod X (t_star Y) = (n. t_prod X (trace_dioid.power Y n))"
  by (auto simp add: t_star_elim t_prod_def)

lemma t_star_contr: "t_prod (t_star X) Y = (n. t_prod (trace_dioid.power X n) Y)"
  by (auto simp add: t_star_elim t_prod_def)

interpretation trace_kleene_algebra: kleene_algebra "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)" t_star
proof
  fix X Y Z :: "('a, 'b) trace set"
  show "t_one  t_prod X (t_star X)  t_star X"
    proof -
      have "t_one  t_prod X (t_star X) = (trace_dioid.power X 0)  (n. trace_dioid.power X (Suc n))"
        by (auto simp add: t_star_def t_prod_def)
      also have "... = (n. trace_dioid.power X n)"
        by (metis Un_0_Suc)
      also have "... = t_star X"
        by (metis t_star_def)
      finally show ?thesis
        by (metis subset_refl)
    qed
  show "Z  t_prod X Y  Y  t_prod (t_star X) Z  Y"
    by (simp only: ball_UNIV t_star_contr SUP_le_iff) (metis trace_dioid.power_inductl)
  show "Z  t_prod Y X  Y  t_prod Z (t_star X)  Y"
    by (simp only: ball_UNIV t_star_contl SUP_le_iff) (metis trace_dioid.power_inductr)
qed


subsection ‹Path Kleene Algebras›

text ‹We start with paths that include the empty path.›

definition p_star :: "'a path set  'a path set" where
  "p_star X  n. path_dioid.power X n"

lemma p_star_elim: "x  p_star X  (n. x  path_dioid.power X n)"
by (simp add: p_star_def)

lemma p_star_contl: "p_prod X (p_star Y) = (n. p_prod X (path_dioid.power Y n))"
apply (auto simp add: p_prod_def p_star_elim)
   apply (metis p_fusion.simps(1))
  apply metis
 apply (metis p_fusion.simps(1) p_star_elim)
apply (metis p_star_elim)
done

lemma p_star_contr: "p_prod (p_star X) Y = (n. p_prod (path_dioid.power X n) Y)"
apply (auto simp add: p_prod_def p_star_elim)
   apply (metis p_fusion.simps(1))
  apply metis
 apply (metis p_fusion.simps(1) p_star_elim)
apply (metis p_star_elim)
done

interpretation path_kleene_algebra: kleene_algebra "(∪)" p_prod p_one "{}" "(⊆)" "(⊂)" p_star
proof
  fix X Y Z :: "'a path set"
  show "p_one  p_prod X (p_star X)  p_star X"
    proof -
      have "p_one  p_prod X (p_star X) = (path_dioid.power X 0)  (n. path_dioid.power X (Suc n))"
        by (auto simp add: p_star_def p_prod_def)
      also have "... = (n. path_dioid.power X n)"
        by (metis Un_0_Suc)
      also have "... = p_star X"
        by (metis p_star_def)
      finally show ?thesis
        by (metis subset_refl)
    qed
  show "Z  p_prod X Y  Y  p_prod (p_star X) Z  Y"
    by (simp only: ball_UNIV p_star_contr SUP_le_iff) (metis path_dioid.power_inductl)
  show "Z  p_prod Y X  Y  p_prod Z (p_star X)  Y"
    by (simp only: ball_UNIV p_star_contl SUP_le_iff) (metis path_dioid.power_inductr)
qed

text ‹We now consider a notion of paths that does not include the
empty path.›

definition pp_star :: "'a ppath set  'a ppath set" where
  "pp_star X  n. ppath_dioid.power X n"

lemma pp_star_elim: "x  pp_star X  (n. x  ppath_dioid.power X n)"
by (simp add: pp_star_def)

lemma pp_star_contl: "pp_prod X (pp_star Y) = (n. pp_prod X (ppath_dioid.power Y n))"
by (auto simp add: pp_prod_def pp_star_elim)

lemma pp_star_contr: "pp_prod (pp_star X) Y = (n. pp_prod (ppath_dioid.power X n) Y)"
by (auto simp add: pp_prod_def pp_star_elim)

interpretation ppath_kleene_algebra: kleene_algebra "(∪)" pp_prod pp_one "{}" "(⊆)" "(⊂)" pp_star
proof
  fix X Y Z :: "'a ppath set"
  show "pp_one  pp_prod X (pp_star X)  pp_star X"
    proof -
      have "pp_one  pp_prod X (pp_star X) = (ppath_dioid.power X 0)  (n. ppath_dioid.power X (Suc n))"
        by (auto simp add: pp_star_def pp_prod_def)
      also have "... = (n. ppath_dioid.power X n)"
        by (metis Un_0_Suc)
      also have "... = pp_star X"
        by (metis pp_star_def)
      finally show ?thesis
        by (metis subset_refl)
    qed
  show "Z  pp_prod X Y  Y  pp_prod (pp_star X) Z  Y"
    by (simp only: ball_UNIV pp_star_contr SUP_le_iff) (metis ppath_dioid.power_inductl)
  show "Z  pp_prod Y X  Y  pp_prod Z (pp_star X)  Y"
    by (simp only: ball_UNIV pp_star_contl SUP_le_iff) (metis ppath_dioid.power_inductr)
qed


subsection ‹The Distributive Lattice Kleene Algebra›

text ‹In the case of bounded distributive lattices, the star maps
all elements to to the maximal element.›

definition (in bounded_distributive_lattice) bdl_star :: "'a  'a" where
  "bdl_star x = top"

sublocale bounded_distributive_lattice  kleene_algebra sup inf top bot less_eq less bdl_star
proof
  fix x y z :: 'a
  show "sup top (inf x (bdl_star x))  bdl_star x"
    by (simp add: bdl_star_def)
  show "sup z (inf x y)  y  inf (bdl_star x) z  y"
    by (simp add: bdl_star_def)
  show "sup z (inf y x)  y  inf z (bdl_star x)  y"
    by (simp add: bdl_star_def)
qed


subsection ‹The Min-Plus Kleene Algebra›

text ‹One cannot define a Kleene star for max-plus and min-plus
algebras that range over the real numbers. Here we define the star for
a min-plus algebra restricted to natural numbers and~$+\infty$. The
resulting Kleene algebra is commutative. Similar variants can be
obtained for max-plus algebras and other algebras ranging over the
positive or negative integers.›

instantiation pnat :: commutative_kleene_algebra
begin

  definition star_pnat where
    "x  (1::pnat)"

  instance
  proof
    fix x y z :: pnat
    show "1 + x  x  x"
      by (metis star_pnat_def zero_pnat_top)
    show "z + x  y  y  x  z  y"
      by (simp add: star_pnat_def)
    show "z + y  x  y  z  x  y"
      by (simp add: star_pnat_def)
    show "x  y = y  x"
      unfolding times_pnat_def by (cases x, cases y, simp_all)
  qed

end (* 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ω"
  by (metis add.commute add_zero_l annir omega_coinduct)

lemma omega_coinduct_eq: "y = z + x  y  y  xω + x  z"
  by (simp add: local.omega_coinduct)

lemma omega_coinduct_eq_var1: "y = 1 + x  y  y  xω + x"
  by (simp add: omega_coinduct_var1)

lemma  omega_coinduct_eq_var2: "y = x  y  y  xω"
  by (simp add: omega_coinduct_var2)

lemma "y = x  y + z  y = x  z + xω"
  (* 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ω"
    by (simp add: mult_assoc omega_coinduct_var2)
  show  "xω  x  xω"
    by (fact omega_unfold)
qed

lemma omega_unfold_var: "z + x  xω  xω + x  z"
  by (simp add: local.omega_coinduct)

lemma "z + x  xω = xω + x  z"
  (* 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)ω"
  by (simp add: omega_iso)

lemma zero_omega [simp]: "0ω = 0"
  by (metis annil omega_unfold_eq)

text ‹The next lemma is another variant of omega unfold›

lemma star_omega_1 [simp]: "x  xω = xω"
proof (rule order.antisym)
  have "x  xω  xω"
    by simp
  thus "x  xω  xω"
    by simp
  show "xω  x  xω"
    using local.star_inductl_var_eq2 by auto
qed

text ‹The next lemma says that~@{term "1ω"} is the maximal element
of omega algebra. We therefore baptise it~$\top$.›

lemma max_element: "x  1ω"
  by (simp add: omega_coinduct_eq_var2)

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

lemma star_omega_3 [simp]: "(x)ω = "
proof -
  have "1  x"
    by (fact star_ref)
  hence "  (x)ω"
    by (simp add: omega_iso top_def)
  thus ?thesis
    by (simp add: local.order.antisym max_element top_def)
qed

text ‹The following lemma is strange since it is counterintuitive
that one should be able to append something after an infinite
iteration.›

lemma omega_1: "xω  y  xω"
proof -
  have "xω  y  x  xω  y"
    by simp
  thus ?thesis
    by (metis mult.assoc omega_coinduct_var2)
qed

lemma "xω  y = xω"
  (*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ω"
    by (simp add: mult_assoc)
  also have "...  y  z  xω"
    by (simp add: hyp local.mult_isor)
  finally show "z  xω  yω"
    by (simp add: mult_assoc omega_coinduct_var2)
qed

lemma "z  x  y  z  z  xω  yω  z"
  (* 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)ω"
    by (simp add: local.star_slide_var mult_assoc)
  also have "... = x  x  x  (x  x)ω"
    by (simp add: mult_assoc)
  also have "... = x  (x  x)ω"
    by (simp add: mult_assoc)
  thus "(x  x)ω  xω"
    using calculation omega_coinduct_eq_var2 by auto
   show "xω  (x  x)ω"
    by (simp add: mult_assoc omega_coinduct_eq_var2)
qed

lemma wagner_2_var: "x  (y  x)ω  (x  y)ω"
proof -
  have "x  y  x  x  y  x"
    by auto
  thus "x  (y  x)ω  (x  y)ω"
    by (simp add: mult_assoc omega_simulation)
qed

lemma wagner_2 [simp]: "x  (y  x)ω = (x  y)ω"
proof (rule order.antisym)
  show "x  (y  x)ω  (x  y)ω"
    by (rule wagner_2_var)
  have "(x  y)ω = x  y  (x  y)ω"
    by simp
  thus "(x  y)ω  x  (y  x)ω"
    by (metis mult.assoc mult_isol wagner_2_var)
qed

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

lemma wagner_3:
assumes "x  (x + y)ω + z = (x + y)ω"
shows "(x + y)ω = xω + x  z"
proof (rule order.antisym)
  show  "(x + y)ω  xω + x  z"
    using assms local.join.sup_commute omega_coinduct_eq by auto
  have "x  z  (x + y)ω"
    using assms local.join.sup_commute local.star_inductl_eq by auto
  thus "xω + x  z  (x + y)ω"
    by (simp add: omega_subdist)
qed

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

lemma wagner_1_var [simp]: "(x  x)ω = xω"
  by (simp add: local.star_slide_var)

lemma star_omega_4 [simp]: "(xω) = 1 + xω"
proof (rule order.antisym)
  have "(xω) = 1 + xω  (xω)"
    by simp
  also have "...  1 + xω  "
    by (simp add: omega_sup_id)
  finally show "(xω)  1 + xω"
    by simp
  show "1 + xω  (xω)"
    by simp
qed

lemma star_omega_5 [simp]: "xω  (xω) = xω"
proof (rule order.antisym)
  show "xω  (xω)  xω"
    by (rule omega_1)
  show "xω  xω  (xω)"
    by (simp add: omega_sup_id)
qed

text ‹The next law shows how omegas below a sum can be unfolded.›

lemma omega_sum_unfold: "xω + x  y  (x + y)ω = (x + y)ω"
proof -
  have "(x + y)ω = x  (x + y)ω + y  (x+y)ω"
    by (metis distrib_right omega_unfold_eq)
  thus ?thesis
    by (metis mult.assoc wagner_3)
qed

text ‹
The next two lemmas apply induction and coinduction to this law.
›

lemma omega_sum_unfold_coind: "(x + y)ω  (x  y)ω + (x  y)  xω"
  by (simp add: omega_coinduct_eq omega_sum_unfold)

lemma omega_sum_unfold_ind: "(x  y)  xω  (x + y)ω"
  by (simp add: local.star_inductl_eq omega_sum_unfold)

lemma wagner_1_gen: "(x  y)ω  (x + y)ω"
proof -
  have "(x  y)ω  ((x + y)  (x + y))ω"
    using local.join.le_sup_iff local.join.sup.cobounded1 local.mult_isol_var local.star_subdist_var omega_iso by presburger
  thus ?thesis
    by (metis wagner_1)
qed

lemma wagner_1_var_gen: "(x  y)ω  (x + y)ω"
proof -
  have "(x  y)ω = x  (y  x)ω"
    by simp
  also have "...  x  (x + y)ω"
    by (metis add.commute mult_isol wagner_1_gen)
  also have "...  (x + y)  (x + y)ω"
    using local.mult_isor local.star_subdist by auto
  thus ?thesis
    by (metis calculation order_trans star_omega_1)
qed

text ‹The next lemma is a variant of the denest law for the star at
the level of omega.›

lemma omega_denest [simp]: "(x + y)ω = (x  y)ω + (x  y)  xω"
proof (rule order.antisym)
  show "(x + y)ω  (x  y)ω + (x  y)  xω"
    by (rule omega_sum_unfold_coind)
  have "(x  y)ω   (x + y)ω"
    by (rule wagner_1_var_gen)
  hence "(x  y)  xω  (x + y)ω"
    by (simp add: omega_sum_unfold_ind)
  thus "(x  y)ω + (x  y)  xω  (x + y)ω"
    by (simp add: wagner_1_var_gen)
qed

text ‹The next lemma yields a separation theorem for infinite
iteration in the presence of a quasicommutation property. A
nondeterministic loop over~@{term x} and~@{term y} can be refined into
separate infinite loops over~@{term x} and~@{term y}.›

lemma omega_sum_refine:
  assumes "y  x  x  (x + y)"
  shows "(x + y)ω = xω + x  yω"
proof (rule order.antisym)
  have a: "y  x  x  (x + y)"
    using assms local.quasicomm_var by blast
  have "(x + y)ω = yω + y  x  (x + y)ω"
    by (metis add.commute omega_sum_unfold)
  also have "...  yω + x  (x + y)  (x + y)ω"
    using a local.join.sup_mono local.mult_isol_var by blast
  also have "...  x  (x + y)ω + yω"
    using local.eq_refl local.join.sup_commute mult_assoc star_omega_1 by presburger
  finally show "(x + y)ω  xω + x  yω"
    by (metis add_commute local.omega_coinduct)
  have "xω + x  yω  (x + y)ω + (x + y)  (x + y)ω"
    using local.join.sup.cobounded2 local.join.sup.mono local.mult_isol_var local.star_subdist omega_iso omega_subdist by presburger
  thus "xω + x  yω  (x + y)ω"
    by (metis local.join.sup_idem star_omega_1)
qed

text ‹The following theorem by Bachmair and
Dershowitz~\cite{bachmair86commutation} is a corollary.›

lemma bachmair_dershowitz:
  assumes "y  x  x  (x + y)"
  shows "(x + y)ω = 0  xω + yω = 0"
  by (metis add_commute assms local.annir local.join.le_bot local.no_trivial_inverse omega_subdist omega_sum_refine)

text ‹
The next lemmas consider an abstract variant of the empty word
property from language theory and match it with the absence of
infinite iteration~\cite{struth12regeq}.
›

definition (in dioid_one_zero) ewp
where "ewp x  ¬(y. y  x  y  y = 0)"

lemma ewp_super_id1: "0  1  1  x  ewp x"
  by (metis ewp_def mult_oner)

lemma "0  1  1  x  ewp x"
  (* 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"
    by (simp add: assms(2) local.omega_coinduct_eq)
  hence "y  x  z"
    by (simp add: assms(1))
  thus "x  z = y"
    by (simp add: assms(2) order.eq_iff local.star_inductl_eq)
qed

lemma ardens_lemma: "¬ ewp x  z + x  y = y  x  z = y"
  by (simp add: ardens_lemma_var ewp_neg_and_omega)

lemma ardens_lemma_equiv:
  assumes "¬ ewp x"
  shows "z + x  y = y  x  z = y"
  by (metis ardens_lemma_var assms ewp_neg_and_omega local.conway.dagger_unfoldl_distr mult_assoc)

lemma ardens_lemma_var_equiv: "xω = 0  (z + x  y = y  x  z = y)"
  by (simp add: ardens_lemma_equiv ewp_neg_and_omega)

lemma arden_conv1: "(y z. z + x  y = y  x  z = y)  ¬ ewp x"
  by (metis add_zero_l annir ewp_neg_and_omega omega_unfold_eq)

lemma arden_conv2: "(y z. z + x  y = y  x  z = y)  xω = 0"
  using arden_conv1 ewp_neg_and_omega by blast

lemma arden_var3: "(y z. z + x  y = y  x  z = y)  xω = 0"
  using arden_conv2 ardens_lemma_var by blast

end

subsection ‹Omega Algebras›

class omega_algebra = kleene_algebra + left_omega_algebra

end

Theory Omega_Algebra_Models

(* 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 = "
  by (simp add: local.join.sup.absorb1 top_ref)

lemma top_elim: "x  y  x  "
  by (simp add: local.mult_isol top_ref)

lemma iteration_unfoldl_distl [simp]: " y + y  x  x = y  x"
  by (metis distrib_left mult.assoc mult_oner iteration_unfoldl)

lemma iteration_unfoldl_distr [simp]: " y + x  x  y = x  y"
  by (metis distrib_right' mult_1_left iteration_unfoldl)

lemma iteration_unfoldl' [simp]: "z  y + z  x  x  y = z  x  y"
  by (metis iteration_unfoldl_distl local.distrib_right)

lemma iteration_idem [simp]: "x  x = x"
proof (rule order.antisym)
  have "x  x  1 + x  x  x"
    by (metis add_assoc iteration_unfoldl_distr local.eq_refl local.iteration_unfoldl local.subdistl_eq mult_assoc)
  thus "x  x  x"
    using local.coinduction mult_assoc by fastforce
  show "x   x  x"
    using local.coinduction by auto
qed

lemma iteration_induct: "x  x  x  x"
proof -
  have "x + x  (x  x) = x  x"
    by (metis (no_types) local.distrib_left local.iteration_unfoldl local.mult_oner)
  thus ?thesis
    by (simp add: local.coinduction)
qed

lemma iteration_ref_star: "x  x"
  by (simp add: local.star_inductl_one)

lemma iteration_subdist: "x  (x + y)"
  by (metis add_assoc' distrib_right' mult_oner coinduction join.sup_ge1 iteration_unfoldl)

lemma iteration_iso: "x  y  x  y"
  using iteration_subdist local.order_prop by auto
 
lemma iteration_unfoldr [simp]: "1 + x  x = x"
  by (metis add_0_left annil eq_refl isolation mult.assoc iteration_idem iteration_unfoldl iteration_unfoldl_distr star_denest star_one star_prod_unfold star_slide tc)

lemma iteration_unfoldr_distl [simp]: " y + y  x  x = y  x"
  by (metis distrib_left mult.assoc mult_oner iteration_unfoldr)

lemma iteration_unfoldr_distr [simp]: " y + x  x  y = x  y"
  by (metis iteration_unfoldl_distr iteration_unfoldr_distl)

lemma iteration_unfold_eq: "x  x = x  x"
  by (metis iteration_unfoldl_distr iteration_unfoldr_distl)
  
lemma iteration_unfoldr' [simp]: "z  y + z  x  x  y = z  x  y"
  by (metis distrib_left mult.assoc iteration_unfoldr_distr)

lemma iteration_double [simp]: "(x) = "
  by (simp add: iteration_iso iteration_refl order.eq_iff top_ref)

lemma star_iteration [simp]: "(x) = "
  by (simp add: iteration_iso order.eq_iff top_ref)

lemma iteration_star [simp]: "(x) = x"
  by (metis (no_types) iteration_idem iteration_refl local.star_inductr_var_eq2 local.sup_id_star1)

lemma iteration_star2 [simp]: "x  x = x"
proof -
  have f1: "(x)  x = x"
    by (metis (no_types) it_ext iteration_induct iteration_star local.bubble_sort local.join.sup.absorb1)
  have "x = x  x"
    by simp
  hence "x  x = x  (x)  (x  (x))"
    using f1 by (metis (no_types) iteration_star local.star_denest_var_4 mult_assoc)
  thus ?thesis
    using f1 by (metis (no_types) iteration_star local.star_denest_var_4 local.star_denest_var_8)
qed

lemma iteration_zero [simp]: "0 = 1"
  by (metis add_zeror annil iteration_unfoldl)

lemma iteration_annil [simp]: "(x  0) = 1 + x  0"
  by (metis annil iteration_unfoldl mult.assoc)

lemma iteration_subdenest: "x  y  (x + y)"
  by (metis add_commute iteration_idem iteration_subdist local.mult_isol_var)
  
lemma sup_id_top: "1  y  y   = "
  using order.eq_iff local.mult_isol_var top_ref by fastforce

lemma iteration_top [simp]: "x   = "
  by (simp add: iteration_refl sup_id_top)

text ‹Next, we prove some simulation laws for data refinement.›

lemma iteration_sim: "z  y  x  z  z  y  x  z"
proof -
  assume assms: "z  y  x  z"
  have "z  y = z + z  y  y"
    by simp
  also have "...  z + x  z  y"
    by (metis assms add.commute add_iso mult_isor)
  finally show "z  y  x  z"
    by (simp add: local.coinduction mult_assoc)
qed

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

lemma "y  z  z  x  y  z  z  x"
(*nitpick [expect=genuine]*)
oops
  
text ‹Next, we prove some sliding laws.›

lemma iteration_slide_var: "x  (y  x)  (x  y)  x"
  by (simp add: iteration_sim mult_assoc)

lemma iteration_prod_unfold [simp]: "1 + y  (x  y)  x = (y  x)"
proof (rule order.antisym)
  have "1 + y  (x  y)  x  1 + (y  x)  y  x"
    using iteration_slide_var local.join.sup_mono local.mult_isor by blast
  thus "1 + y  (x  y)  x   (y  x)"
    by (simp add: mult_assoc)
  have "(y  x) = 1 + y  x  (y  x)"
    by simp
  thus "(y  x)  1 + y  (x  y)  x"
    by (metis iteration_sim local.eq_refl local.join.sup.mono local.mult_isol mult_assoc)
qed

lemma iteration_slide: "x  (y  x) = (x  y)  x"
  by (metis iteration_prod_unfold iteration_unfoldl_distr distrib_left mult_1_right mult.assoc)

lemma star_iteration_slide [simp]: " y  (x  y) = (x  y)"
  by (metis iteration_star2 local.conway.dagger_unfoldl_distr local.join.sup.orderE local.mult_isor local.star_invol local.star_subdist local.star_trans_eq)

text ‹The following laws are called denesting laws.›

lemma iteration_sub_denest: "(x + y)  x  (y  x)"
proof -
  have "(x + y) = x  (x + y) + y  (x + y) + 1"
    by (metis add.commute distrib_right' iteration_unfoldl)
  hence "(x + y)  x  (y  (x + y) + 1)"
    by (metis add_assoc' join.sup_least join.sup_ge1 join.sup_ge2 coinduction)
  moreover hence "x  (y  (x + y) + 1)  x  (y  x)"
    by (metis add_iso mult.assoc mult_isol add.commute coinduction mult_oner mult_isol)
  ultimately show ?thesis
    using local.order_trans by blast
qed

lemma iteration_denest: "(x + y) = x  (y  x)"
proof -
  have "x  (y  x)  x  x  (y  x) + y  x  (y  x) + 1"
    by (metis add.commute iteration_unfoldl_distr add_assoc' add.commute iteration_unfoldl order_refl)
  thus ?thesis
    by (metis add.commute iteration_sub_denest order.antisym coinduction distrib_right' iteration_sub_denest mult.assoc mult_oner order.antisym)
qed
(*
end

sublocale dra ⊆ conway_zerol strong_iteration 
  apply (unfold_locales)
  apply (simp add: iteration_denest iteration_slide)
  apply simp
  by (simp add: iteration_sim)


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"
    by (metis add.assoc distrib_left mult_1_right add_0_left mult_1_right)
  finally show ?thesis
    by (metis add.commute iteration_denest iteration_slide mult.assoc)
qed

lemma iteration_denest3: "(y  x)  y = (x + y)"
proof (rule order.antisym)
  have  "(y  x)  y  (y  x)  y"
    by (simp add: iteration_iso iteration_ref_star local.mult_isor)
  thus  "(y  x)  y  (x + y)"
    by (metis iteration_denest iteration_slide local.join.sup_commute)
  have "(x + y) = y + y  x  (x + y)"
    by (metis iteration_denest2 local.join.sup_commute)
  thus "(x + y)  (y  x)  y"
    by (simp add: local.coinduction) 
qed

text ‹Now we prove separation laws for reasoning about distributed systems in the context of action systems.›

lemma iteration_sep: "y  x  x  y  (x + y) = x  y"
proof -
  assume "y  x  x  y"
  hence "y  x  x(x + y)"
    by (metis star_sim1 add.commute mult_isol order_trans star_subdist)
  hence "y  x  (x + y) + y  x  (x + y) + y"
    by (metis mult_isor mult.assoc iteration_star2 join.sup.mono eq_refl)
  thus ?thesis
    by (metis iteration_denest2 add.commute coinduction add.commute less_eq_def iteration_subdenest)
qed

lemma iteration_sim2: "y  x  x  y  y  x  x  y"
  by (metis add.commute iteration_sep iteration_subdenest)

lemma iteration_sep2: "y  x  x  y  (x + y) = x  y"
proof - 
  assume "y  x  x  y"
  hence "y  (y  x)  y  x  y  y"
    by (metis mult.assoc mult_isor iteration_sim star_denest_var_2 star_sim1 star_slide_var star_trans_eq tc_eq)
  moreover have "x  y  y  x  y"
    by (metis eq_refl mult.assoc iteration_star2)
  moreover have "(y  x)  y  y  (y  x)  y"
    by (metis mult_isor mult_onel star_ref)
  ultimately show ?thesis
    by (metis order.antisym iteration_denest3 iteration_subdenest order_trans)
qed

lemma iteration_sep3: "y  x  x  (x + y)  (x + y) = x  y"
proof -
  assume "y  x  x  (x + y)"
  hence "y  x  x  (x + y)"
    by (metis star_sim1)
  hence "y  x  (x + y) + y  x  (x + y)  (x + y) + y"
    by (metis add_iso mult_isor)
  hence "(x + y)  x  y"
    by (metis mult.assoc iteration_denest2 iteration_star2 add.commute coinduction)
  thus ?thesis
    by (metis add.commute less_eq_def iteration_subdenest)
qed

lemma iteration_sep4: "y  0 = 0  z  x = 0  y  x  (x + z)  y  (x + y + z) = x  (y + z)"
proof -
  assume assms: "y  0 = 0" "z  x = 0" "y  x  (x + z)  y"
  have "y  y  z  y  z  y"
    by (metis mult_isor star_1l mult_oner order_trans star_plus_one subdistl)
  have "y  z  x  x  y  z"
    by (metis join.bot_least assms(1) assms(2) independence1 mult.assoc)
  have "y  (x + y  z)  (x + z)  y + y  y  z"
    by (metis assms(3) distrib_left mult.assoc add_iso)
  also have "...  (x + y  z)  y + y  y  z" 
    by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor)
  also have "...  (x + y  z)  y + y  z   y" using y  y  z  y  z  y
    by (metis add.commute add_iso)
  finally have "y  (x + y  z)  (x + y  z)  y"
    by (metis add.commute add_idem' add.left_commute distrib_right)
  moreover have "(x + y + z)  (x + y + y  z)"
    by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor iteration_iso)  
  moreover have "... = (x + y  z)  y"
    by (metis add_commute calculation(1) iteration_sep2 local.add_left_comm)
  moreover have "... = x  (y  z)  y" using y  z  x  x  y  z
    by (metis iteration_sep mult.assoc)
  ultimately have "(x + y + z)  x  (y + z)"
    by (metis add.commute mult.assoc iteration_denest3)
  thus ?thesis
    by (metis add.commute add.left_commute less_eq_def iteration_subdenest)
qed

text ‹Finally, we prove some blocking laws.›

text ‹Nitpick refutes the next lemma.›

lemma "x  y = 0  x  y = y"
(*nitpick*)
oops

lemma iteration_idep: "x  y = 0  x  y = x"
  by (metis add_zeror annil iteration_unfoldl_distl)

text ‹Nitpick refutes the next lemma.›

lemma "y  w  x  y + z  y  w  x  z"
(*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"
    by (simp add: it_simr mult.assoc)
  thus ?thesis
    using assms(2) phl_export2 by blast
qed

end

text ‹Next we define a Hoare triple to make the format of the rules more explicit.›

context pre_dioid_one
begin

abbreviation (in near_dioid) ht :: "'a  'a  'a  bool" ("___") where
  "x y z  x  y  y  z" 

lemma ht_phl_skip: "x 1 x"
  by simp
  
lemma ht_phl_cons1: "x  w  w y z  x y z"
  by (fact phl_cons1)

lemma ht_phl_cons2: "w  x  z y w  z y x"
  by (fact phl_cons2)

lemma ht_phl_seq: "p x r  r y q  p x  y q"
  by (fact phl_seq)

lemma ht_phl_cond: 
assumes "u  v  v  u  v" and "u  w  w  u  w" 
and "x y. u  (x + y)  u  x + u  y"
and "u  v x z" and "u  w y z" 
shows "u (v  x + w  y) z"
  using assms by (fact phl_cond)

lemma  ht_phl_export1: 
assumes "x  y  y  x  y"
and "x  y z w"
shows "x y  z w"
  using assms by (fact phl_export1)

lemma ht_phl_export2: 
assumes "z  w  w  z  w"
and "x y z"
shows "x y  w z  w"
  using assms by (fact phl_export2)

end

context it_pre_dioid begin

lemma ht_phl_while:  
assumes "p  s  s  p  s" and "p  w  w  p  w"
and  "p  s x p"
shows "p it (s  x)  w p  w"
  using assms by (fact phl_while)

end

sublocale pre_conway < phl: it_pre_dioid where it = dagger
  by standard (simp add: local.dagger_simr)

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

end

Theory PHL_DRA

(* 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 
  by standard (simp add: local.iteration_sim)
  
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)"
  by (simp add: assms sum_sup)

lemma sum_fun_sup:
  fixes f :: "'a  'b::join_semilattice_zero"
  assumes "finite (A ::'a set)"
  shows "{f a | a. a  A}  z  (a  A. f a  z)"
  by (simp only: fset_to_im assms sum_fun_image_sup)

lemma sum_intro:
  assumes "finite (A :: 'a::join_semilattice_zero set)" and "finite B"
  shows "(a  A. b  B. a  b)  (A  B)"
  by (metis assms order_refl order_trans sum_sup)

text ‹Next we prove an additivity property for suprema.›

lemma sum_union:
  assumes "finite (A :: 'a::join_semilattice_zero set)"
  and "finite (B :: 'a::join_semilattice_zero set)"
  shows "(A  B) = A + B"
proof -
    have "z. (A  B)  z  (A + B  z)"
      by (auto simp add: assms sum_sup)
  thus ?thesis
    by (simp add: eq_iff)
qed

text ‹It follows that the sum (supremum) of a two-element set is the
join of its elements.›

lemma sum_bin[simp]: "{(x :: 'a::join_semilattice_zero),y} = x + y"
  by (subst insert_is_Un, subst sum_union, auto)

text ‹Next we show that finite suprema are order preserving.›

lemma sum_iso:
  assumes "finite (B :: 'a::join_semilattice_zero set)"
  shows "A  B   A   B"
  by (metis assms finite_subset order_refl rev_subsetD sum_sup)

text ‹The following lemmas state unfold properties for suprema and
finite sets. They are subtly different from the non-idempotent case,
where additional side conditions are required.›

lemma sum_insert [simp]:
  assumes "finite (A :: 'a::join_semilattice_zero set)"
  shows "(insert x A) = x + A"
proof -
  have "(insert x A) = {x} + A"
    by (metis insert_is_Un assms finite.emptyI finite.insertI sum_union)
  thus ?thesis
    by auto
qed

lemma sum_fun_insert:
  fixes f :: "'a  'b::join_semilattice_zero"
  assumes "finite (A :: 'a set)"
  shows "(f ` (insert x A)) = f x + (f ` A)"
  by (simp add: assms)

text ‹Now we show that set comprehensions with nested suprema can
be flattened.›

lemma flatten1_im:
  fixes f :: "'a  'a  'b::join_semilattice_zero"
  assumes "finite (A :: 'a set)"
  and "finite (B :: 'a set)"
  shows "((λx. (f x ` B)) ` A) = ((λp. f (fst p) (snd p)) ` (A × B))"
proof -
  have "z. ((λx. (f x ` B)) ` A)  z  ((λp. f (fst p) (snd p)) ` (A × B))  z"
    by (simp add: assms finite_cartesian_product sum_fun_image_sup)
  thus ?thesis
    by (simp add: eq_iff)
qed

lemma flatten2_im:
  fixes f :: "'a  'a  'b::join_semilattice_zero"
  assumes "finite (A ::'a set)"
  and "finite (B ::'a set)"
  shows "((λy.  ((λx. f x y) ` A)) ` B) = ((λp. f (fst p) (snd p)