Theory Z

(*
 * Title:      Z  
 * Author:     Bertram Felgenhauer (2016)
 * Author:     Julian Nagele (2016)
 * Author:     Vincent van Oostrom (2016)
 * Author:     Christian Sternagel (2016)
 * Maintainer: Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at>
 * Maintainer: Juilan Nagele <julian.nagele@uibk.ac.at>
 * Maintainer: Christian Sternagel <c.sternagel@gmail.com>
 * License:    BSD
 *)

section ‹The Z property›

theory Z
imports "Abstract-Rewriting.Abstract_Rewriting"
begin

locale z_property =
  fixes bullet :: "'a  'a" ("_" [1000] 1000)
  and R :: "'a rel"
  assumes Z: "(a, b)  R  (b, a)  R*  (a, b)  R*"
begin

lemma monotonicity:
  assumes "(a, b)  R*"
  shows "(a, b)  R*"
using assms
by (induct) (auto dest: Z)

lemma semi_confluence:
  shows "(R¯ O R*)  R"
proof (intro subrelI, elim relcompEpair, drule converseD)
  fix d a c
  assume "(a, c)  R*" and "(a, d)  R"
  then show "(d, c)  R"
  proof (cases)
    case (step b)
    then have "(a, b)  R*" by (auto simp: monotonicity)
    then have "(d, b)  R*" using (a, d)  R by (auto dest: Z)
    then show ?thesis using (b, c)  R by (auto dest: Z)
  qed auto
qed

lemma CR: "CR R"
by (intro semi_confluence_imp_CR semi_confluence)

definition "Rd = {(a, b). (a, b)  R*  (b, a)  R*}"

end

locale angle_property =
  fixes bullet :: "'a  'a" ("_" [1000] 1000)
  and R :: "'a rel"
  and Rd :: "'a rel"
  assumes intermediate: "R  Rd" "Rd  R*"
  and angle: "(a, b)  Rd  (b, a)  Rd"

sublocale angle_property  z_property
proof
  fix a b
  assume "(a, b)  R"
  with angle intermediate have "(b, a)  Rd" and "(a, b)  Rd" by auto
  then show "(b, a)  R*  (a, b)  R*" using intermediate by auto
qed

sublocale z_property  angle_property bullet R "z_property.Rd bullet R"
proof
  show "R  Rd" and "Rd  R*" unfolding Rd_def using Z by auto
  fix a b
  assume "(a, b)  Rd"
  then show "(b, a)  Rd" using monotonicity unfolding Rd_def by auto
qed

end