# 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 ∈ X⋅Y ⟷ (∃u v. w = t_fusion u v ∧ u ∈ X ∧ v ∈ Y ∧ last u = first v)" by (unfold t_prod_def) auto lemma t_prod_intro [simp, intro]: "⟦ u ∈ X; v ∈ Y; last u = first v ⟧ ⟹ t_fusion u v ∈ X⋅Y" by (meson t_prod_iff) lemma t_prod_elim [elim]: "w ∈ X⋅Y ⟹ ∃u v. w = t_fusion u v ∧ u ∈ X ∧ v ∈ Y ∧ last u = first v" by (meson t_prod_iff) text ‹Finally we prove the interpretation statement that sets of traces under union and the complex product based on trace fusion together with the empty set of traces and the set of traces of length one forms a dioid.› interpretation trace_dioid: dioid_one_zero "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)" apply unfold_locales apply (auto simp add: t_prod_def t_one_def t_zero_def t_fusion_def) apply (metis last_append) apply (metis last_append append_assoc) done no_notation t_prod (infixl "⋅" 70) subsection ‹The Path Diod› text ‹The next model we consider are sets of paths in a graph. We consider two variants, one that contains the empty path and one that doesn't. The former leads to more difficult proofs and a more involved specification of the complex product. We start with paths that include the empty path. In this setting, a path is a list of nodes.› subsection ‹Path Models with the Empty Path› type_synonym 'a path = "'a list" text ‹Path fusion is defined similarly to trace fusion. Mathematically it should be a partial operation. The fusion of two empty paths yields the empty path; the fusion between a non-empty path and an empty one is undefined; the fusion of two non-empty paths appends the tail of the second path to the first one. We need to use a total alternative and make sure that undefined paths do not contribute to the complex product.› fun p_fusion :: "'a path ⇒ 'a path ⇒ 'a path" where "p_fusion [] _ = []" | "p_fusion _ [] = []" | "p_fusion ps (q # qs) = ps @ qs" lemma p_fusion_assoc: "p_fusion ps (p_fusion qs rs) = p_fusion (p_fusion ps qs) rs" proof (induct rs) case Nil show ?case by (metis p_fusion.elims p_fusion.simps(2)) case Cons show ?case proof (induct qs) case Nil show ?case by (metis neq_Nil_conv p_fusion.simps(1) p_fusion.simps(2)) case Cons show ?case proof - have "∀ps. ([] = ps ∨ hd ps # tl ps = ps) ∧ ((∀q qs. q # qs ≠ ps) ∨ [] ≠ ps)" using list.collapse by fastforce moreover hence "∀ps q qs. p_fusion ps (q # qs) = ps @ qs ∨ [] = ps" by (metis p_fusion.simps(3)) ultimately show ?thesis by (metis (no_types) Cons_eq_appendI append_eq_appendI p_fusion.simps(1) p_fusion.simps(3)) qed qed qed text ‹This lemma overapproximates the real situation, but it holds in all cases where path fusion should be defined.› lemma p_fusion_last: assumes "List.last ps = hd qs" and "ps ≠ []" and "qs ≠ []" shows "List.last (p_fusion ps qs) = List.last qs" by (metis (hide_lams, no_types) List.last.simps List.last_append append_Nil2 assms list.sel(1) neq_Nil_conv p_fusion.simps(3)) lemma p_fusion_hd: "⟦ps ≠ []; qs ≠ []⟧ ⟹ hd (p_fusion ps qs) = hd ps" by (metis list.exhaust p_fusion.simps(3) append_Cons list.sel(1)) lemma nonempty_p_fusion: "⟦ps ≠ []; qs ≠ []⟧ ⟹ p_fusion ps qs ≠ []" by (metis list.exhaust append_Cons p_fusion.simps(3) list.simps(2)) text ‹We now define a condition that filters out undefined paths in the complex product.› abbreviation p_filter :: "'a path ⇒ 'a path ⇒ bool" where "p_filter ps qs ≡ ((ps = [] ∧ qs = []) ∨ (ps ≠ [] ∧ qs ≠ [] ∧ (List.last ps) = hd qs))" no_notation times (infixl "⋅" 70) definition p_prod :: "'a path set ⇒ 'a path set ⇒ 'a path set" (infixl "⋅" 70) where "X ⋅ Y = {rs . ∃ps ∈ X. ∃qs ∈ Y. rs = p_fusion ps qs ∧ p_filter ps qs}" lemma p_prod_iff: "ps ∈ X ⋅ Y ⟷ (∃qs rs. ps = p_fusion qs rs ∧ qs ∈ X ∧ rs ∈ Y ∧ p_filter qs rs)" by (unfold p_prod_def) auto text ‹Due to the complexity of the filter condition, proving properties of complex products can be tedious.› lemma p_prod_assoc: "(X ⋅ Y) ⋅ Z = X ⋅ (Y ⋅ Z)" proof (rule set_eqI) fix ps show "ps ∈ (X ⋅ Y) ⋅ Z ⟷ ps ∈ X ⋅ (Y ⋅ Z)" proof (cases ps) case Nil thus ?thesis by auto (metis nonempty_p_fusion p_prod_iff)+ next case Cons thus ?thesis by (auto simp add: p_prod_iff) (metis (hide_lams, mono_tags) nonempty_p_fusion p_fusion_assoc p_fusion_hd p_fusion_last)+ qed qed text ‹We now define the multiplicative unit of the path dioid as the set of all paths of length one, including the empty path, and show the unit laws with respect to the path product.› definition p_one :: "'a path set" where "p_one ≡ {p . ∃q::'a. p = [q]} ∪ {[]}" lemma p_prod_onel [simp]: "p_one ⋅ X = X" proof (rule set_eqI) fix ps show "ps ∈ p_one ⋅ X ⟷ ps ∈ X" proof (cases ps) case Nil thus ?thesis by (auto simp add: p_one_def p_prod_def, metis nonempty_p_fusion not_Cons_self) next case Cons thus ?thesis by (auto simp add: p_one_def p_prod_def, metis append_Cons append_Nil list.sel(1) neq_Nil_conv p_fusion.simps(3), metis Cons_eq_appendI list.sel(1) last_ConsL list.simps(3) p_fusion.simps(3) self_append_conv2) qed qed lemma p_prod_oner [simp]: "X ⋅ p_one = X" proof (rule set_eqI) fix ps show "ps ∈ X ⋅ p_one ⟷ ps ∈ X" proof (cases ps) case Nil thus ?thesis by (auto simp add: p_one_def p_prod_def, metis nonempty_p_fusion not_Cons_self2, metis p_fusion.simps(1)) next case Cons thus ?thesis by (auto simp add: p_one_def p_prod_def, metis append_Nil2 neq_Nil_conv p_fusion.simps(3), metis list.sel(1) list.simps(2) p_fusion.simps(3) self_append_conv) qed qed text ‹Next we show distributivity laws at the powerset level.› lemma p_prod_distl: "X ⋅ (Y ∪ Z) = X ⋅ Y ∪ X ⋅ Z" proof (rule set_eqI) fix ps show "ps ∈ X ⋅ (Y ∪ Z) ⟷ ps ∈ X ⋅ Y ∪ X ⋅ Z" by (cases ps) (auto simp add: p_prod_iff) qed lemma p_prod_distr: "(X ∪ Y) ⋅ Z = X ⋅ Z ∪ Y ⋅ Z" proof (rule set_eqI) fix ps show "ps ∈ (X ∪ Y) ⋅ Z ⟷ ps ∈ X ⋅ Z ∪ Y ⋅ Z" by (cases ps) (auto simp add: p_prod_iff) qed text ‹Finally we show that sets of paths under union, the complex product, the unit set and the empty set form a dioid.› interpretation path_dioid: dioid_one_zero "(∪)" "(⋅)" p_one "{}" "(⊆)" "(⊂)" proof fix x y z :: "'a path set" show "x ∪ y ∪ z = x ∪ (y ∪ z)" by auto show "x ∪ y = y ∪ x" by auto show "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)" by (fact p_prod_assoc) show "(x ∪ y) ⋅ z = x ⋅ z ∪ y ⋅ z" by (fact p_prod_distr) show "p_one ⋅ x = x" by (fact p_prod_onel) show "x ⋅ p_one = x" by (fact p_prod_oner) show "{} ∪ x = x" by auto show "{} ⋅ x = {}" by (metis all_not_in_conv p_prod_iff) show "x ⋅ {} = {}" by (metis all_not_in_conv p_prod_iff) show "(x ⊆ y) = (x ∪ y = y)" by auto show "(x ⊂ y) = (x ⊆ y ∧ x ≠ y)" by auto show "x ∪ x = x" by auto show "x ⋅ (y ∪ z) = x ⋅ y ∪ x ⋅ z" by (fact p_prod_distl) qed no_notation p_prod (infixl "⋅" 70) subsection ‹Path Models without the Empty Path› text ‹We now build a model of paths that does not include the empty path and therefore leads to a simpler complex product.› datatype 'a ppath = Node 'a | Cons 'a "'a ppath" primrec pp_first :: "'a ppath ⇒ 'a" where "pp_first (Node x) = x" | "pp_first (Cons x _) = x" primrec pp_last :: "'a ppath ⇒ 'a" where "pp_last (Node x) = x" | "pp_last (Cons _ xs) = pp_last xs" text ‹The path fusion product (although we define it as a total funcion) should only be applied when the last element of the first argument is equal to the first element of the second argument.› primrec pp_fusion :: "'a ppath ⇒ 'a ppath ⇒ 'a ppath" where "pp_fusion (Node x) ys = ys" | "pp_fusion (Cons x xs) ys = Cons x (pp_fusion xs ys)" text ‹We now go through the same steps as for traces and paths before, showing that the first and last element of a trace a left or right unit for that trace and that the fusion product on traces is associative.› lemma pp_fusion_leftneutral [simp]: "pp_fusion (Node (pp_first x)) x = x" by simp lemma pp_fusion_rightneutral [simp]: "pp_fusion x (Node (pp_last x)) = x" by (induct x) simp_all lemma pp_first_pp_fusion [simp]: "pp_last x = pp_first y ⟹ pp_first (pp_fusion x y) = pp_first x" by (induct x) simp_all lemma pp_last_pp_fusion [simp]: "pp_last x = pp_first y ⟹ pp_last (pp_fusion x y) = pp_last y" by (induct x) simp_all lemma pp_fusion_assoc [simp]: "⟦ pp_last x = pp_first y; pp_last y = pp_first z ⟧ ⟹ pp_fusion x (pp_fusion y z) = pp_fusion (pp_fusion x y) z" by (induct x) simp_all text ‹We now lift the path fusion product to a complex product on sets of paths. This operation is total.› definition pp_prod :: "'a ppath set ⇒ 'a ppath set ⇒ 'a ppath set" (infixl "⋅" 70) where "X⋅Y = {pp_fusion u v| u v. u ∈ X ∧ v ∈ Y ∧ pp_last u = pp_first v}" text ‹Next we define the set of paths of length one as the multiplicative unit of the path dioid.› definition pp_one :: "'a ppath set" where "pp_one ≡ range Node" text ‹We again provide an elimination rule.› lemma pp_prod_iff: "w ∈ X⋅Y ⟷ (∃u v. w = pp_fusion u v ∧ u ∈ X ∧ v ∈ Y ∧ pp_last u = pp_first v)" by (unfold pp_prod_def) auto interpretation ppath_dioid: dioid_one_zero "(∪)" "(⋅)" pp_one "{}" "(⊆)" "(⊂)" proof fix x y z :: "'a ppath set" show "x ∪ y ∪ z = x ∪ (y ∪ z)" by auto show "x ∪ y = y ∪ x" by auto show "x ⋅ y ⋅ z = x ⋅ (y ⋅ z)" by (auto simp add: pp_prod_def, metis pp_first_pp_fusion pp_fusion_assoc, metis pp_last_pp_fusion) show "(x ∪ y) ⋅ z = x ⋅ z ∪ y ⋅ z" by (auto simp add: pp_prod_def) show "pp_one ⋅ x = x" by (auto simp add: pp_one_def pp_prod_def, metis pp_fusion.simps(1) pp_last.simps(1) rangeI) show "x ⋅ pp_one = x" by (auto simp add: pp_one_def pp_prod_def, metis pp_first.simps(1) pp_fusion_rightneutral rangeI) show "{} ∪ x = x" by auto show "{} ⋅ x = {}" by (simp add: pp_prod_def) show "x ⋅ {} = {}" by (simp add: pp_prod_def) show "x ⊆ y ⟷ x ∪ y = y" by auto show "x ⊂ y ⟷ x ⊆ y ∧ x ≠ y" by auto show "x ∪ x = x" by auto show "x ⋅ (y ∪ z) = x ⋅ y ∪ x ⋅ z" by (auto simp add: pp_prod_def) qed no_notation pp_prod (infixl "⋅" 70) subsection ‹The Distributive Lattice Dioid› text ‹A bounded distributive lattice is a distributive lattice with a least and a greatest element. Using Isabelle's lattice theory file we define a bounded distributive lattice as an axiomatic type class and show, using a sublocale statement, that every bounded distributive lattice is a dioid with one and zero.› class bounded_distributive_lattice = bounded_lattice + distrib_lattice sublocale bounded_distributive_lattice ⊆ dioid_one_zero sup inf top bot less_eq proof fix x y z show "sup (sup x y) z = sup x (sup y z)" by (fact sup_assoc) show "sup x y = sup y x" by (fact sup.commute) show "inf (inf x y) z = inf x (inf y z)" by (metis inf.commute inf.left_commute) show "inf (sup x y) z = sup (inf x z) (inf y z)" by (fact inf_sup_distrib2) show "inf top x = x" by simp show "inf x top = x" by simp show "sup bot x = x" by simp show "inf bot x = bot" by simp show "inf x bot = bot" by simp show "(x ≤ y) = (sup x y = y)" by (fact le_iff_sup) show "(x < y) = (x ≤ y ∧ x ≠ y)" by auto show "sup x x = x" by simp show "inf x (sup y z) = sup (inf x y) (inf x z)" by (fact inf_sup_distrib1) qed subsection ‹The Boolean Dioid› text ‹In this section we show that the booleans form a dioid, because the booleans form a bounded distributive lattice.› instantiation bool :: bounded_distributive_lattice begin instance .. end (* 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 ⟧ ⟹ (∑k∈S. f k * (if k = j then 1 else (0::'b::{semiring_0,monoid_mult}))) = 0" by (induct S rule: finite_induct, auto) lemma sum_delta_r_1 [simp]: "⟦ finite S; j ∈ S ⟧ ⟹ (∑k∈S. f k * (if k = j then 1 else (0::'b::{semiring_0,monoid_mult}))) = f j" by (induct S rule: finite_induct, auto) lemma matrix_mult_1_right [simp]: "(A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) *⇩_{M}1 = A" by (cases A, simp add: one_matrix_def) lemma sum_delta_l_0 [simp]: "⟦ finite S; i ∉ S ⟧ ⟹ (∑k∈S. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = 0" by (induct S rule: finite_induct, auto) lemma sum_delta_l_1 [simp]: "⟦ finite S; i ∈ S ⟧ ⟹ (∑k∈S. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = f i j" by (induct S rule: finite_induct, auto) lemma matrix_mult_1_left [simp]: "1 *⇩_{M}(A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) = A" by (cases A, simp add: one_matrix_def) lemma matrix_mult_assoc: "(A::('a::semiring_0,'m,'n) matrix) *⇩_{M}B *⇩_{M}C = A *⇩_{M}(B *⇩_{M}C)" apply (cases A) apply (cases B) apply (cases C) apply (simp add: sum_distrib_right sum_distrib_left mult.assoc) apply (subst sum.swap) apply (rule refl) done lemma matrix_mult_distrib_left: "(A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) *⇩_{M}(B + C) = A *⇩_{M}B + A *⇩_{M}C" by (cases A, cases B, cases C, simp add: distrib_left sum.distrib) lemma matrix_mult_distrib_right: "((A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) + B) *⇩_{M}C = A *⇩_{M}C + B *⇩_{M}C" by (cases A, cases B, cases C, simp add: distrib_right sum.distrib) lemma sqmatrix_mult_0_right [simp]: "(A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) * 0 = 0" by (cases A, simp add: zero_sqmatrix_def) lemma sqmatrix_mult_0_left [simp]: "0 * (A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) = 0" by (cases A, simp add: zero_sqmatrix_def) lemma sqmatrix_mult_1_right [simp]: "(A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) * 1 = A" by (cases A, simp add: one_sqmatrix_def) lemma sqmatrix_mult_1_left [simp]: "1 * (A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) = A" by (cases A, simp add: one_sqmatrix_def) lemma sqmatrix_mult_assoc: "(A::('a::{semiring_0,monoid_mult},'m) sqmatrix) * B * C = A * (B * C)" apply (cases A) apply (cases B) apply (cases C) apply (simp add: sum_distrib_right sum_distrib_left mult.assoc) apply (subst sum.swap) apply (rule refl) done lemma sqmatrix_mult_distrib_left: "(A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) * (B + C) = A * B + A * C" by (cases A, cases B, cases C, simp add: distrib_left sum.distrib) lemma sqmatrix_mult_distrib_right: "((A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) + B) * C = A * C + B * C" by (cases A, cases B, cases C, simp add: distrib_right sum.distrib) subsection ‹Square-Matrix Model of Dioids› text ‹The following subclass proofs are necessary to connect parts of our algebraic hierarchy to the hierarchy found in the Isabelle/HOL library.› subclass (in ab_near_semiring_one_zerol) comm_monoid_add proof fix a :: 'a show "0 + a = a" by (fact add_zerol) qed subclass (in semiring_one_zero) semiring_0 proof fix a :: 'a show "0 * a = 0" by (fact annil) show "a * 0 = 0" by (fact annir) qed subclass (in ab_near_semiring_one) monoid_mult .. instantiation sqmatrix :: (dioid_one_zero,len) dioid_one_zero begin instance proof fix A B C :: "('a, 'b) sqmatrix" show "A + B + C = A + (B + C)" by (fact sqmatrix_add_assoc) show "A + B = B + A" by (fact sqmatrix_add_commute) show "A * B * C = A * (B * C)" by (fact sqmatrix_mult_assoc) show "(A + B) * C = A * C + B * C" by (fact sqmatrix_mult_distrib_right) show "1 * A = A" by (fact sqmatrix_mult_1_left) show "A * 1 = A" by (fact sqmatrix_mult_1_right) show "0 + A = A" by (fact sqmatrix_add_0_left) show "0 * A = 0" by (fact sqmatrix_mult_0_left) show "A * 0 = 0" by (fact sqmatrix_mult_0_right) show "A + A = A" by (cases A, simp) show "A * (B + C) = A * B + A * C" by (fact sqmatrix_mult_distrib_left) qed end subsection ‹Kleene Star for Matrices› text ‹We currently do not implement the Kleene star of matrices, since this is complicated.› end

# Theory Conway

(* 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)) ` (A × B))" by (simp only: flatten1_im assms cart_flip) lemma sum_fla