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 "R⇩d = {(a, b). (a, b) ∈ R⇧* ∧ (b, a⇧∙) ∈ R⇧*}"

end

locale angle_property =
  fixes bullet :: "'a ⇒ 'a" (‹_⇧∙› [1000] 1000)
  and R :: "'a rel"
  and R⇩d :: "'a rel"
  assumes intermediate: "R ⊆ R⇩d" "R⇩d ⊆ R⇧*"
  and angle: "(a, b) ∈ R⇩d ⟹ (b, a⇧∙) ∈ R⇩d"

sublocale angle_property ⊆ z_property
proof
  fix a b
  assume "(a, b) ∈ R"
  with angle intermediate have "(b, a⇧∙) ∈ R⇩d" and "(a⇧∙, b⇧∙) ∈ R⇩d" by auto
  then show "(b, a⇧∙) ∈ R⇧* ∧ (a⇧∙, b⇧∙) ∈ R⇧*" using intermediate by auto
qed

sublocale z_property ⊆ angle_property bullet R "z_property.R⇩d bullet R"
proof
  show "R ⊆ R⇩d" and "R⇩d ⊆ R⇧*" unfolding R⇩d_def using Z by auto
  fix a b
  assume "(a, b) ∈ R⇩d"
  then show "(b, a⇧∙) ∈ R⇩d" using monotonicity unfolding R⇩d_def by auto
qed

end