Theory Relation_Algebra_RTC

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

section ‹Reflexive Transitive Closure›

theory Relation_Algebra_RTC
  imports Relation_Algebra
begin

text ‹We impose the Kleene algebra axioms for the star on relation algebras.
This gives us a reflexive transitive closure operation.›

class relation_algebra_rtc = relation_algebra + star_op +
  assumes rtc_unfoldl: "1' +  x ; x⇧⋆ ≤ x⇧⋆"
    and rtc_inductl: "z + x ; y ≤ y ⟶ x⇧⋆ ; z ≤ y"
    and rtc_inductr: "z + y ; x ≤ y ⟶ z ; x⇧⋆ ≤ y"

sublocale relation_algebra_rtc ⊆ kleene_algebra "(+)" "(;)" "1'" 0 "(≤)" "(<)" star
apply (unfold_locales)
  apply (rule rtc_unfoldl)
 apply (simp add: local.rtc_inductl)
apply (simp add: rtc_inductr)
done

context relation_algebra_rtc
begin

text ‹First, we prove that the obvious interaction between the star and
converse is captured by the axioms.›

lemma star_conv: "(x⇧⋆)⇧⌣ = (x⇧⌣)⇧⋆"
proof (rule order.antisym)
  show "(x⇧⌣)⇧⋆ ≤ (x⇧⋆)⇧⌣"
    by (metis local.conv_add local.conv_contrav local.conv_e local.conv_iso local.star_rtc1 local.star_rtc_least)
  show "(x⇧⋆)⇧⌣ ≤ (x⇧⌣)⇧⋆"
    by (metis boffa_var conv_add conv_contrav conv_e conv_invol conv_iso star_denest star_ext star_iso star_plus_one sup.idem)
qed

text ‹Next we provide an example to show how facts from Kleene algebra are
picked up in relation algebra.›

lemma rel_church_rosser: "(x⇧⌣)⇧⋆ ; x⇧⋆ ≤ x⇧⋆ ; (x⇧⌣)⇧⋆ ⟹ (x + x⇧⌣)⇧⋆ = x⇧⋆ ; (x⇧⌣)⇧⋆"
by (fact church_rosser)

end (* relation_algebra_rtc *)

end