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