(*
 * 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^\<bullet>) ∈ R^* ∧ (a^\<bullet>, b^\<bullet>) ∈ R^*"
begin

lemma monotonicity:
  assumes "(a, b) ∈ R^*"
  shows "(a^\<bullet>, b^\<bullet>) ∈ R^*"
using assms
by (induct) (auto dest: Z)

lemma semi_confluence:
  shows "(R^-1 O R^*) ⊆ R^\<down>"
proof (intro subrelI, elim relcompEpair, drule converseD)
  fix d a c
  assume "(a, c) ∈ R^*" and "(a, d) ∈ R"
  then show "(d, c) ∈ R^\<down>"
  proof (cases)
    case (step b)
    then have "(a^\<bullet>, b^\<bullet>) ∈ R^*" by (auto simp: monotonicity)
    then have "(d, b^\<bullet>) ∈ 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^\<bullet>) ∈ 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^\<bullet>) ∈ R_d"

sublocale angle_property ⊆ z_property
proof
  fix a b
  assume "(a, b) ∈ R"
  with angle intermediate have "(b, a^\<bullet>) ∈ R_d" and "(a^\<bullet>, b^\<bullet>) ∈ R_d" by auto
  then show "(b, a^\<bullet>) ∈ R^* ∧ (a^\<bullet>, b^\<bullet>) ∈ 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^\<bullet>) ∈ R_d" using monotonicity unfolding R_{d_def} by auto
qed

end