Theory Abstract-Rewriting.Abstract_Rewriting

(*  Title:       Abstract Rewriting
    Author:      Christian Sternagel <christian.sternagel@uibk.ac.at>
                 Rene Thiemann       <rene.tiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and Rene Thiemann
    License:     LGPL
*)

(*
Copyright 2010 Christian Sternagel and René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)

section ‹Abstract Rewrite Systems›

theory Abstract_Rewriting
imports
  "HOL-Library.Infinite_Set"
  "Regular-Sets.Regexp_Method"
  Seq
begin

(*FIXME: move*)
lemma trancl_mono_set:
  "r  s  r+  s+"
  by (blast intro: trancl_mono)

lemma relpow_mono:
  fixes r :: "'a rel"
  assumes "r  r'" shows "r ^^ n  r' ^^ n"
  using assms by (induct n) auto

lemma refl_inv_image:
  "refl R  refl (inv_image R f)"
  by (simp add: inv_image_def refl_on_def)

subsection ‹Definitions›

text ‹Two elements are \emph{joinable} (and then have in the joinability relation)
w.r.t.\ @{term "A"}, iff they have a common reduct.›
definition join :: "'a rel  'a rel"  ("(_)" [1000] 999) where
  "A = A* O (A¯)*"

text ‹Two elements are \emph{meetable} (and then have in the meetability relation)
w.r.t.\ @{term "A"}, iff they have a common ancestor.›
definition meet :: "'a rel  'a rel"  ("(_)" [1000] 999) where
  "A = (A¯)* O A*"

text ‹The \emph{symmetric closure} of a relation allows steps in both directions.›
abbreviation symcl :: "'a rel  'a rel"  ("(_)" [1000] 999) where
  "A  A  A¯"

text ‹A \emph{conversion} is a (possibly empty) sequence of steps in the symmetric closure.›
definition conversion :: "'a rel  'a rel"  ("(_*)" [1000] 999) where
  "A* = (A)*"

text ‹The set of \emph{normal forms} of an ARS constitutes all the elements that do
not have any successors.›
definition NF :: "'a rel  'a set" where
  "NF A = {a. A `` {a} = {}}"

definition normalizability :: "'a rel  'a rel"  ("(_!)" [1000] 999) where
  "A! = {(a, b). (a, b)  A*  b  NF A}"

notation (ASCII)
  symcl  ("(_^<->)" [1000] 999) and
  conversion  ("(_^<->*)" [1000] 999) and
  normalizability  ("(_^!)" [1000] 999)

lemma symcl_converse:
  "(A)¯ = A" by auto

lemma symcl_Un: "(A  B) = A  B" by auto

lemma no_step:
  assumes "A `` {a} = {}" shows "a  NF A"
  using assms by (auto simp: NF_def)

lemma joinI:
  "(a, c)  A*  (b, c)  A*  (a, b)  A"
  by (auto simp: join_def rtrancl_converse)

lemma joinI_left:
  "(a, b)  A*  (a, b)  A"
  by (auto simp: join_def)

lemma joinI_right: "(b, a)  A*  (a, b)  A"
  by (rule joinI) auto

lemma joinE:
  assumes "(a, b)  A"
  obtains c where "(a, c)  A*" and "(b, c)  A*"
  using assms by (auto simp: join_def rtrancl_converse)

lemma joinD:
  "(a, b)  A  c. (a, c)  A*  (b, c)  A*"
  by (blast elim: joinE)

lemma meetI:
  "(a, b)  A*  (a, c)  A*  (b, c)  A"
  by (auto simp: meet_def rtrancl_converse)

lemma meetE:
  assumes "(b, c)  A"
  obtains a where "(a, b)  A*" and "(a, c)  A*"
  using assms by (auto simp: meet_def rtrancl_converse)

lemma meetD: "(b, c)  A  a. (a, b)  A*  (a, c)  A*"
  by (blast elim: meetE)

lemma conversionI: "(a, b)  (A)*  (a, b)  A*"
  by (simp add: conversion_def)

lemma conversion_refl [simp]: "(a, a)  A*"
  by (simp add: conversion_def)

lemma conversionI':
  assumes "(a, b)  A*" shows "(a, b)  A*"
using assms
proof (induct)
  case base then show ?case by simp
next
  case (step b c)
  then have "(b, c)  A" by simp
  with (a, b)  A* show ?case unfolding conversion_def by (rule rtrancl.intros)
qed

lemma rtrancl_comp_trancl_conv:
  "r* O r = r+" by regexp

lemma trancl_o_refl_is_trancl:
  "r+ O r= = r+" by regexp

lemma conversionE:
  "(a, b)  A*  ((a, b)  (A)*  P)  P"
  by (simp add: conversion_def)

text ‹Later declarations are tried first for `proof' and `rule,' then have the ``main''
introduction\,/\, elimination rules for constants should be declared last.›
declare joinI_left [intro]
declare joinI_right [intro]
declare joinI [intro]
declare joinD [dest]
declare joinE [elim]

declare meetI [intro]
declare meetD [dest]
declare meetE [elim]

declare conversionI' [intro]
declare conversionI [intro]
declare conversionE [elim]

lemma conversion_trans:
  "trans (A*)"
  unfolding trans_def
proof (intro allI impI)
  fix a b c assume "(a, b)  A*" and "(b, c)  A*"
  then show "(a, c)  A*" unfolding conversion_def
  proof (induct)
    case base then show ?case by simp
  next
    case (step b c')
    from (b, c')  A and (c', c)  (A)*
      have "(b, c)  (A)*" by (rule converse_rtrancl_into_rtrancl)
    with step show ?case by simp
  qed
qed

lemma conversion_sym:
  "sym (A*)"
  unfolding sym_def
proof (intro allI impI)
  fix a b assume "(a, b)  A*" then show "(b, a)  A*" unfolding conversion_def
  proof (induct)
    case base then show ?case by simp
  next
    case (step b c)
    then have "(c, b)  A" by blast
    from (c, b)  A and (b, a)  (A)*
      show ?case by (rule converse_rtrancl_into_rtrancl)
  qed
qed

lemma conversion_inv:
  "(x, y)  R*  (y, x)  R*"
  by (auto simp: conversion_def)
     (metis (full_types) rtrancl_converseD symcl_converse)+


lemma conversion_converse [simp]:
  "(A*)¯ = A*"
  by (metis conversion_sym sym_conv_converse_eq)

lemma conversion_rtrancl [simp]:
  "(A*)* = A*"
  by (metis conversion_def rtrancl_idemp)

lemma rtrancl_join_join:
  assumes "(a, b)  A*" and "(b, c)  A" shows "(a, c)  A"
proof -
  from (b, c)  A obtain b' where "(b, b')  A*" and "(b', c)  (A¯)*"
    unfolding join_def by blast
  with (a, b)  A* have "(a, b')  A*" by simp
  with (b', c)  (A¯)* show ?thesis unfolding join_def by blast
qed

lemma join_rtrancl_join:
  assumes "(a, b)  A" and "(c, b)  A*" shows "(a, c)  A"
proof -
  from (c, b)  A* have "(b, c)  (A¯)*" unfolding rtrancl_converse by simp
  from (a, b)  A obtain a' where "(a, a')  A*" and "(a', b)  (A¯)*"
    unfolding join_def by best
  with (b, c)  (A¯)* have "(a', c)  (A¯)*" by simp
  with (a, a')  A* show ?thesis unfolding join_def by blast
qed

lemma NF_I: "(b. (a, b)  A)  a  NF A" by (auto intro: no_step)

lemma NF_E: "a  NF A  ((a, b)  A  P)  P" by (auto simp: NF_def)

declare NF_I [intro]
declare NF_E [elim]

lemma NF_no_step: "a  NF A  b. (a, b)  A" by auto

lemma NF_anti_mono:
  assumes "A  B" shows "NF B  NF A"
  using assms by auto

lemma NF_iff_no_step: "a  NF A = (b. (a, b)  A)" by auto

lemma NF_no_trancl_step:
  assumes "a  NF A" shows "b. (a, b)  A+"
proof -
  from assms have "b. (a, b)  A" by auto
  show ?thesis
  proof (intro allI notI)
    fix b assume "(a, b)  A+"
    then show False by (induct) (auto simp: b. (a, b)  A)
   qed
qed

lemma NF_Id_on_fst_image [simp]: "NF (Id_on (fst ` A)) = NF A" by force

lemma fst_image_NF_Id_on [simp]: "fst ` R = Q  NF (Id_on Q) = NF R" by force

lemma NF_empty [simp]: "NF {} = UNIV" by auto

lemma normalizability_I: "(a, b)  A*  b  NF A  (a, b)  A!"
by (simp add: normalizability_def)

lemma normalizability_I': "(a, b)  A*  (b, c)  A!  (a, c)  A!"
by (auto simp add: normalizability_def)

lemma normalizability_E: "(a, b)  A!  ((a, b)  A*  b  NF A  P)  P"
by (simp add: normalizability_def)

declare normalizability_I' [intro]
declare normalizability_I [intro]
declare normalizability_E [elim]


subsection ‹Properties of ARSs›

text ‹The following properties on (elements of) ARSs are defined: completeness,
Church-Rosser property, semi-completeness, strong normalization, unique normal
forms, Weak Church-Rosser property, and weak normalization.›

definition CR_on :: "'a rel  'a set  bool" where
  "CR_on r A  (aA. b c. (a, b)  r*  (a, c)  r*  (b, c)  join r)"

abbreviation CR :: "'a rel  bool" where
  "CR r  CR_on r UNIV"

definition SN_on :: "'a rel  'a set  bool" where
  "SN_on r A  ¬ (f. f 0  A  chain r f)"

abbreviation SN :: "'a rel  bool" where
  "SN r  SN_on r UNIV"

text ‹Alternative definition of @{term "SN"}.›
lemma SN_def: "SN r = (x. SN_on r {x})"
  unfolding SN_on_def by blast

definition UNF_on :: "'a rel  'a set  bool" where
  "UNF_on r A  (aA. b c. (a, b)  r!  (a, c)  r!  b = c)"

abbreviation UNF :: "'a rel  bool" where "UNF r  UNF_on r UNIV"

definition WCR_on :: "'a rel  'a set  bool" where
  "WCR_on r A  (aA. b c. (a, b)  r  (a, c)  r  (b, c)  join r)"

abbreviation WCR :: "'a rel  bool" where "WCR r  WCR_on r UNIV"

definition WN_on :: "'a rel  'a set  bool" where
  "WN_on r A  (aA. b. (a, b)  r!)"

abbreviation WN :: "'a rel  bool" where
  "WN r  WN_on r UNIV"

lemmas CR_defs = CR_on_def
lemmas SN_defs = SN_on_def
lemmas UNF_defs = UNF_on_def
lemmas WCR_defs = WCR_on_def
lemmas WN_defs = WN_on_def

definition complete_on :: "'a rel  'a set  bool" where
  "complete_on r A  SN_on r A  CR_on r A"

abbreviation complete :: "'a rel  bool" where
  "complete r  complete_on r UNIV"

definition semi_complete_on :: "'a rel  'a set  bool" where
  "semi_complete_on r A   WN_on r A  CR_on r A"

abbreviation semi_complete :: "'a rel  bool" where
  "semi_complete r  semi_complete_on r UNIV"

lemmas complete_defs = complete_on_def
lemmas semi_complete_defs = semi_complete_on_def

text ‹Unique normal forms with respect to conversion.›
definition UNC :: "'a rel  bool" where
  "UNC A  (a b. a  NF A  b  NF A  (a, b)  A*  a = b)"

lemma complete_onI:
  "SN_on r A  CR_on r A  complete_on r A"
  by (simp add: complete_defs)

lemma complete_onE:
  "complete_on r A  (SN_on r A  CR_on r A  P)  P"
  by (simp add: complete_defs)

lemma CR_onI:
  "(a b c. a  A  (a, b)  r*  (a, c)  r*  (b, c)  join r)  CR_on r A"
  by (simp add: CR_defs)

lemma CR_on_singletonI:
  "(b c. (a, b)  r*  (a, c)  r*  (b, c)  join r)  CR_on r {a}"
  by (simp add: CR_defs)

lemma CR_onE:
  "CR_on r A  a  A  ((b, c)  join r  P)  ((a, b)  r*  P)  ((a, c)  r*  P)  P"
  unfolding CR_defs by blast

lemma CR_onD:
  "CR_on r A  a  A  (a, b)  r*  (a, c)  r*  (b, c)  join r"
  by (blast elim: CR_onE)

lemma semi_complete_onI: "WN_on r A  CR_on r A  semi_complete_on r A"
  by (simp add: semi_complete_defs)

lemma semi_complete_onE:
  "semi_complete_on r A  (WN_on r A  CR_on r A  P)  P"
  by (simp add: semi_complete_defs)

declare semi_complete_onI [intro]
declare semi_complete_onE [elim]

declare complete_onI [intro]
declare complete_onE [elim]

declare CR_onI [intro]
declare CR_on_singletonI [intro]

declare CR_onD [dest]
declare CR_onE [elim]

lemma UNC_I:
  "(a b. a  NF A  b  NF A  (a, b)  A*  a = b)  UNC A"
  by (simp add: UNC_def)

lemma UNC_E:
  "UNC A; a = b  P; a  NF A  P; b  NF A  P; (a, b)  A*  P  P"
  unfolding UNC_def by blast

lemma UNF_onI: "(a b c. a  A  (a, b)  r!  (a, c)  r!  b = c)  UNF_on r A"
  by (simp add: UNF_defs)

lemma UNF_onE:
  "UNF_on r A  a  A  (b = c  P)  ((a, b)  r!  P)  ((a, c)  r!  P)  P"
  unfolding UNF_on_def by blast

lemma UNF_onD:
  "UNF_on r A  a  A  (a, b)  r!  (a, c)  r!  b = c"
  by (blast elim: UNF_onE)

declare UNF_onI [intro]
declare UNF_onD [dest]
declare UNF_onE [elim]

lemma SN_onI:
  assumes "f. f 0  A; chain r f  False"
  shows "SN_on r A"
  using assms unfolding SN_defs by blast

lemma SN_I: "(a. SN_on A {a})  SN A"
  unfolding SN_on_def by blast

lemma SN_on_trancl_imp_SN_on:
  assumes "SN_on (R+) T" shows "SN_on R T"
proof (rule ccontr)
  assume "¬ SN_on R T"
  then obtain s where "s 0  T" and "chain R s" unfolding SN_defs by auto
  then have "chain (R+) s" by auto
  with s 0  T have "¬ SN_on (R+) T" unfolding SN_defs by auto
  with assms show False by simp
qed

lemma SN_onE:
  assumes "SN_on r A"
    and "¬ (f. f 0  A  chain r f)  P"
  shows "P"
  using assms unfolding SN_defs by simp

lemma not_SN_onE:
  assumes "¬ SN_on r A"
    and "f. f 0  A; chain r f  P"
  shows "P"
  using assms unfolding SN_defs by blast

declare SN_onI [intro]
declare SN_onE [elim]
declare not_SN_onE [Pure.elim, elim]

lemma refl_not_SN: "(x, x)  R  ¬ SN R"
  unfolding SN_defs by force

lemma SN_on_irrefl:
  assumes "SN_on r A"
  shows "aA. (a, a)  r"
proof (intro ballI notI)
  fix a assume "a  A" and "(a, a)  r"
  with assms show False unfolding SN_defs by auto
qed

lemma WCR_onI: "(a b c. a  A  (a, b)  r  (a, c)  r  (b, c)  join r)  WCR_on r A"
  by (simp add: WCR_defs)

lemma WCR_onE:
  "WCR_on r A  a  A  ((b, c)  join r  P)  ((a, b)  r  P)  ((a, c)  r  P)  P"
  unfolding WCR_on_def by blast

lemma SN_nat_bounded: "SN {(x, y :: nat). x < y  y  b}" (is "SN ?R")
proof 
  fix f
  assume "chain ?R f"
  then have steps: "i. (f i, f (Suc i))  ?R" ..
  {
    fix i
    have inc: "f 0 + i  f i"
    proof (induct i)
      case 0 then show ?case by auto
    next
      case (Suc i)
      have "f 0 + Suc i  f i + Suc 0" using Suc by simp
      also have "...  f (Suc i)" using steps [of i]
        by auto
      finally show ?case by simp
    qed
  }
  from this [of "Suc b"] steps [of b]
  show False by simp
qed

lemma WCR_onD:
  "WCR_on r A  a  A  (a, b)  r  (a, c)  r  (b, c)  join r"
  by (blast elim: WCR_onE)

lemma WN_onI: "(a. a  A  b. (a, b)  r!)  WN_on r A"
  by (auto simp: WN_defs)

lemma WN_onE: "WN_on r A  a  A  (b. (a, b)  r!  P)  P"
 unfolding WN_defs by blast

lemma WN_onD: "WN_on r A  a  A  b. (a, b)  r!"
  by (blast elim: WN_onE)

declare WCR_onI [intro]
declare WCR_onD [dest]
declare WCR_onE [elim]

declare WN_onI [intro]
declare WN_onD [dest]
declare WN_onE [elim]

text ‹Restricting a relation @{term r} to those elements that are strongly
normalizing with respect to a relation @{term s}.›
definition restrict_SN :: "'a rel  'a rel  'a rel" where
  "restrict_SN r s = {(a, b) | a b. (a, b)  r  SN_on s {a}}"

lemma SN_restrict_SN_idemp [simp]: "SN (restrict_SN A A)"
  by (auto simp: restrict_SN_def SN_defs)

lemma SN_on_Image:
  assumes "SN_on r A"
  shows "SN_on r (r `` A)"
proof
  fix f
  assume "f 0  r `` A" and chain: "chain r f"
  then obtain a where "a  A" and 1: "(a, f 0)  r" by auto
  let ?g = "case_nat a f"
  from cons_chain [OF 1 chain] have "chain r ?g" .
  moreover have "?g 0  A" by (simp add: a  A)
  ultimately have "¬ SN_on r A" unfolding SN_defs by best
  with assms show False by simp
qed

lemma SN_on_subset2:
  assumes "A  B" and "SN_on r B"
  shows "SN_on r A"
  using assms unfolding SN_on_def by blast

lemma step_preserves_SN_on:
  assumes 1: "(a, b)  r"
    and 2: "SN_on r {a}"
  shows "SN_on r {b}"
  using 1 and SN_on_Image [OF 2] and SN_on_subset2 [of "{b}" "r `` {a}"] by auto

lemma steps_preserve_SN_on: "(a, b)  A*  SN_on A {a}  SN_on A {b}"
  by (induct rule: rtrancl.induct) (auto simp: step_preserves_SN_on)

(*FIXME: move*)
lemma relpow_seq:
  assumes "(x, y)  r^^n"
  shows "f. f 0 = x  f n = y  (i<n. (f i, f (Suc i))  r)"
using assms
proof (induct n arbitrary: y)
  case 0 then show ?case by auto
next
  case (Suc n)
  then obtain z where "(x, z)  r^^n" and "(z, y)  r" by auto
  from Suc(1)[OF (x, z)  r^^n]
    obtain f where "f 0 = x" and "f n = z" and seq: "i<n. (f i, f (Suc i))  r" by auto
  let ?n = "Suc n"
  let ?f = "λi. if i = ?n then y else f i"
  have "?f ?n = y" by simp
  from f 0 = x have "?f 0 = x" by simp
  from seq have seq': "i<n. (?f i, ?f (Suc i))  r" by auto
  with f n = z and (z, y)  r have "i<?n. (?f i, ?f (Suc i))  r" by auto
  with ?f 0 = x and ?f ?n = y show ?case by best
qed

lemma rtrancl_imp_seq:
  assumes "(x, y)  r*"
  shows "f n. f 0 = x  f n = y  (i<n. (f i, f (Suc i))  r)"
  using assms [unfolded rtrancl_power] and relpow_seq [of x y _ r] by blast

lemma SN_on_Image_rtrancl:
  assumes "SN_on r A"
  shows "SN_on r (r* `` A)"
proof
  fix f
  assume f0: "f 0  r* `` A" and chain: "chain r f"
  then obtain a where a: "a  A" and "(a, f 0)  r*" by auto
  then obtain n where "(a, f 0)  r^^n" unfolding rtrancl_power by auto
  show False
  proof (cases n)
    case 0
    with (a, f 0)  r^^n have "f 0 = a" by simp
    then have "f 0  A" by (simp add: a)
    with chain have "¬ SN_on r A" by auto
    with assms show False by simp
  next
    case (Suc m)
    from relpow_seq [OF (a, f 0)  r^^n]
      obtain g where g0: "g 0 = a" and "g n = f 0"
      and gseq: "i<n. (g i, g (Suc i))  r" by auto
    let ?f = "λi. if i < n then g i else f (i - n)"
    have "chain r ?f"
    proof
      fix i
      {
        assume "Suc i < n"
        then have "(?f i, ?f (Suc i))  r" by (simp add: gseq)
      }
      moreover
      {
        assume "Suc i > n"
        then have eq: "Suc (i - n) = Suc i - n" by arith
        from chain have "(f (i - n), f (Suc (i - n)))  r" by simp
        then have "(f (i - n), f (Suc i - n))  r" by (simp add: eq)
        with Suc i > n have "(?f i, ?f (Suc i))  r" by simp
      }
      moreover
      {
        assume "Suc i = n"
        then have eq: "f (Suc i - n) = g n" by (simp add: g n = f 0)
        from Suc i = n have eq': "i = n - 1" by arith
        from gseq have "(g i, f (Suc i - n))  r" unfolding eq by (simp add: Suc eq')
        then have "(?f i, ?f (Suc i))  r" using Suc i = n by simp
      }
      ultimately show "(?f i, ?f (Suc i))  r" by simp
    qed
    moreover have "?f 0  A"
    proof (cases n)
      case 0
      with (a, f 0)  r^^n have eq: "a = f 0" by simp
      from a show ?thesis by (simp add: eq 0)
    next
      case (Suc m)
      then show ?thesis by (simp add: a g0)
    qed
    ultimately have "¬ SN_on r A" unfolding SN_defs by best
    with assms show False by simp
  qed
qed

(* FIXME: move somewhere else *)
declare subrelI [Pure.intro]

lemma restrict_SN_trancl_simp [simp]: "(restrict_SN A A)+ = restrict_SN (A+) A" (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
  proof
    fix a b assume "(a, b)  ?lhs" then show "(a, b)  ?rhs"
      unfolding restrict_SN_def by (induct rule: trancl.induct) auto
  qed
next
  show "?rhs  ?lhs"
  proof
    fix a b assume "(a, b)  ?rhs"
    then have "(a, b)  A+" and "SN_on A {a}" unfolding restrict_SN_def by auto
    then show "(a, b)  ?lhs"
    proof (induct rule: trancl.induct)
      case (r_into_trancl x y) then show ?case unfolding restrict_SN_def by auto
    next
      case (trancl_into_trancl a b c)
      then have IH: "(a, b)  ?lhs" by auto
      from trancl_into_trancl have "(a, b)  A*" by auto
      from this and SN_on A {a} have "SN_on A {b}" by (rule steps_preserve_SN_on)
      with (b, c)  A have "(b, c)  ?lhs" unfolding restrict_SN_def by auto
      with IH show ?case by simp
    qed
  qed
qed

lemma SN_imp_WN:
  assumes "SN A" shows "WN A"
proof -
  from SN A have "wf (A¯)" by (simp add: SN_defs wf_iff_no_infinite_down_chain)
  show "WN A"
  proof
    fix a
    show "b. (a, b)  A!" unfolding normalizability_def NF_def Image_def
      by (rule wfE_min [OF wf (A¯), of a "A* `` {a}", simplified])
         (auto intro: rtrancl_into_rtrancl)
  qed
qed

lemma UNC_imp_UNF:
 assumes "UNC r" shows "UNF r"
proof - {
  fix x y z assume "(x, y)  r!" and "(x, z)  r!"
  then have "(x, y)  r*" and "(x, z)  r*" and "y  NF r" and "z  NF r" by auto
  then have "(x, y)  r*" and "(x, z)  r*" by auto
  then have "(z, x)  r*" using conversion_sym unfolding sym_def by best
  with (x, y)  r* have "(z, y)  r*" using conversion_trans unfolding trans_def by best
  from assms and this and z  NF r and y  NF r have "z = y" unfolding UNC_def by auto
} then show ?thesis by auto
qed

lemma join_NF_imp_eq:
 assumes "(x, y)  r" and "x  NF r" and "y  NF r"
 shows "x = y"
proof -
  from (x, y)  r obtain z where "(x, z)r*" and "(z, y)(r¯)*" unfolding join_def by auto
  then have "(y, z)  r*" unfolding rtrancl_converse by simp
  from x  NF r have "(x, z)  r+" using NF_no_trancl_step by best
  then have "x = z" using rtranclD [OF (x, z)  r*] by auto
  from y  NF r have "(y, z)  r+" using NF_no_trancl_step by best
  then have "y = z" using rtranclD [OF (y, z)  r*] by auto
  with x = z show ?thesis by simp
qed

lemma rtrancl_Restr:
  assumes "(x, y)  (Restr r A)*"
  shows "(x, y)  r*"
  using assms by induct auto

lemma join_mono:
  assumes "r  s"
  shows "r  s"
  using rtrancl_mono [OF assms] by (auto simp: join_def rtrancl_converse)


lemma CR_iff_meet_subset_join: "CR r = (r  r)"
proof
 assume "CR r" show "r  r"
 proof (rule subrelI)
  fix x y assume "(x, y)  r"
  then obtain z where "(z, x)  r*" and "(z, y)  r*" using meetD by best
  with CR r show "(x, y)  r" by (auto simp: CR_defs)
 qed
next
 assume "r  r" {
  fix x y z assume "(x, y)  r*" and "(x, z)  r*"
  then have "(y, z)  r" unfolding meet_def rtrancl_converse by auto
  with r  r have "(y, z)  r" by auto
 } then show "CR r" by (auto simp: CR_defs)
qed

lemma CR_divergence_imp_join:
  assumes "CR r" and "(x, y)  r*" and "(x, z)  r*"
  shows "(y, z)  r"
using assms by auto

lemma join_imp_conversion: "r  r*"
proof
  fix x z assume "(x, z)  r"
  then obtain y where "(x, y)  r*" and "(z, y)  r*" by auto
  then have "(x, y)  r*" and "(z, y)  r*" by auto
  from (z, y)  r* have "(y, z)  r*" using conversion_sym unfolding sym_def by best
  with (x, y)  r* show "(x, z)  r*" using conversion_trans unfolding trans_def by best
qed

lemma meet_imp_conversion: "r  r*"
proof (rule subrelI)
  fix y z assume "(y, z)  r"
  then obtain x where "(x, y)  r*" and "(x, z)  r*" by auto
  then have "(x, y)  r*" and "(x, z)  r*" by auto
  from (x, y)  r* have "(y, x)  r*" using conversion_sym unfolding sym_def by best
  with (x, z)  r* show "(y, z)  r*" using conversion_trans unfolding trans_def by best
qed

lemma CR_imp_UNF:
  assumes "CR r" shows "UNF r"
proof - {
fix x y z assume "(x, y)  r!" and "(x, z)  r!"
  then have "(x, y)  r*" and "y  NF r" and "(x, z)  r*" and "z  NF r"
    unfolding normalizability_def by auto
  from assms and (x, y)  r* and (x, z)  r* have "(y, z)  r"
    by (rule CR_divergence_imp_join)
  from this and y  NF r and z  NF r have "y = z" by (rule join_NF_imp_eq)
} then show ?thesis by auto
qed

lemma CR_iff_conversion_imp_join: "CR r = (r*  r)"
proof (intro iffI subrelI)
  fix x y assume "CR r" and "(x, y)  r*"
  then obtain n where "(x, y)  (r)^^n" unfolding conversion_def rtrancl_is_UN_relpow by auto
  then show "(x, y)  r"
  proof (induct n arbitrary: x)
    case 0
    assume "(x, y)  r ^^ 0" then have "x = y" by simp
    show ?case unfolding x = y by auto
  next
    case (Suc n)
    from (x, y)  r ^^ Suc n obtain  z where "(x, z)  r" and "(z, y)  r ^^ n"
      using relpow_Suc_D2 by best
    with Suc have "(z, y)  r" by simp
    from (x, z)  r show ?case
    proof
      assume "(x, z)  r" with (z, y)  r show ?thesis by (auto intro: rtrancl_join_join)
    next
      assume "(x, z)  r¯"
      then have "(z, x)  r*" by simp
      from (z, y)  r obtain z' where "(z, z')  r*" and "(y, z')  r*" by auto
      from CR r and (z, x)  r* and (z, z')  r* have "(x, z')  r"
        by (rule CR_divergence_imp_join)
      then obtain x' where "(x, x')  r*" and "(z', x')  r*" by auto
      with (y, z')  r* show ?thesis by auto
    qed
  qed
next
  assume "r*  r" then show "CR r" unfolding CR_iff_meet_subset_join
    using meet_imp_conversion by auto
qed

lemma CR_imp_conversionIff_join:
  assumes "CR r" shows "r* = r"
proof
  show "r*  r" using CR_iff_conversion_imp_join assms by auto
next
  show "r  r*" by (rule join_imp_conversion)
qed

lemma sym_join: "sym (join r)" by (auto simp: sym_def)

lemma join_sym: "(s, t)  A  (t, s)  A" by auto

lemma CR_join_left_I:
  assumes "CR r" and "(x, y)  r*" and "(x, z)  r" shows "(y, z)  r"
proof -
  from (x, z)  r obtain x' where "(x, x')  r*" and "(z, x')  r" by auto
  from CR r and (x, x')  r* and (x, y)  r* have "(x, y)  r" by auto
  then have "(y, x)  r" using join_sym by best
  from CR r have "r* = r" by (rule CR_imp_conversionIff_join)
  from (y, x)  r and (x, z)  r show ?thesis using conversion_trans
    unfolding trans_def r* = r [symmetric] by best
qed

lemma CR_join_right_I:
 assumes "CR r" and "(x, y)  r" and "(y, z)  r*" shows "(x, z)  r"
proof -
  have "r* = r" by (rule CR_imp_conversionIff_join [OF CR r])
  from (y, z)  r* have "(y, z)  r*" by auto
  with (x, y)  r show ?thesis unfolding r* = r [symmetric] using conversion_trans
    unfolding trans_def by fast
qed

lemma NF_not_suc:
  assumes "(x, y)  r*" and "x  NF r" shows "x = y"
proof -
  from x  NF r have "y. (x, y)  r" using NF_no_step by auto
  then have "x  Domain r" unfolding Domain_unfold by simp
  from (x, y)  r* show ?thesis unfolding Not_Domain_rtrancl [OF x  Domain r] by simp
qed

lemma semi_complete_imp_conversionIff_same_NF:
  assumes "semi_complete r"
  shows "((x, y)  r*) = (u v. (x, u)  r!  (y, v)  r!  u = v)"
proof -
  from assms have "WN r" and "CR r" unfolding semi_complete_defs by auto
  then have "r* = r" using CR_imp_conversionIff_join by auto
  show ?thesis
  proof
    assume "(x, y)  r*"
    from (x, y)  r* have "(x, y)  r" unfolding r* = r .
    show "u v. (x, u)  r!  (y, v)  r!  u = v"
    proof (intro allI impI, elim conjE)
      fix u v assume "(x, u)  r!" and "(y, v)  r!"
      then have "(x, u)  r*" and "(y, v)  r*" and "u  NF r" and "v  NF r" by auto
      from CR r and (x, u)  r* and (x, y)  r have "(u, y)  r"
        by (auto intro: CR_join_left_I)
      then have "(y, u)  r" using join_sym by best
      with (x, y)  r have "(x, u)  r" unfolding r* = r [symmetric]
        using conversion_trans unfolding trans_def by best
      from CR r and (x, y)  r and (y, v)  r* have "(x, v)  r"
        by (auto intro: CR_join_right_I)
      then have "(v, x)  r" using join_sym unfolding sym_def by best
      with (x, u)  r have "(v, u)  r" unfolding r* = r [symmetric]
        using conversion_trans unfolding trans_def by best
      then obtain v' where "(v, v')  r*" and "(u, v')  r*" by auto
      from (u, v')  r* and u  NF r have "u = v'" by (rule NF_not_suc)
      from (v, v')  r* and v  NF r have "v = v'" by (rule NF_not_suc)
      then show "u = v" unfolding u = v' by simp
    qed
  next
    assume equal_NF:"u v. (x, u)  r!  (y, v)  r!  u = v"
    from WN r obtain u where "(x, u)  r!" by auto
    from WN r obtain v where "(y, v)  r!" by auto
    from (x, u)  r! and (y, v)  r! have "u = v" using equal_NF by simp
    from (x, u)  r! and (y, v)  r! have "(x, v)  r*" and "(y, v)  r*"
      unfolding u = v by auto
    then have "(x, v)  r*" and "(y, v)  r*" by auto
    from (y, v)  r* have "(v, y)  r*" using conversion_sym unfolding sym_def by best
    with (x, v)  r* show "(x, y)  r*" using conversion_trans unfolding trans_def by best
  qed
qed

lemma CR_imp_UNC:
  assumes "CR r" shows "UNC r"
proof - {
  fix x y assume "x  NF r" and "y  NF r" and "(x, y)  r*"
  have "r* = r" by (rule CR_imp_conversionIff_join [OF assms])
  from (x, y)  r* have "(x, y)  r" unfolding r* = r by simp
  then obtain x' where "(x, x')  r*" and "(y, x')  r*" by best
  from (x, x')  r* and x  NF r have "x = x'" by (rule NF_not_suc)
  from (y, x')  r* and y  NF r have "y = x'" by (rule NF_not_suc)
  then have "x = y" unfolding x = x' by simp
} then show ?thesis by (auto simp: UNC_def)
qed

lemma WN_UNF_imp_CR:
  assumes "WN r" and "UNF r" shows "CR r"
proof - {
  fix x y z assume "(x, y)  r*" and "(x, z)  r*"
  from assms obtain y' where "(y, y')  r!" unfolding WN_defs by best
  with (x, y)  r* have "(x, y')  r!" by auto
  from assms obtain z' where "(z, z')  r!" unfolding WN_defs by best
  with (x, z)  r* have "(x, z')  r!" by auto
  with (x, y')  r! have "y' = z'" using UNF r unfolding UNF_defs by auto
  from (y, y')  r! and (z, z')  r! have "(y, z)  r" unfolding y' = z' by auto
} then show ?thesis by auto
qed

definition diamond :: "'a rel  bool" ("") where
  " r  (r¯ O r)  (r O r¯)"

lemma diamond_I [intro]: "(r¯ O r)  (r O r¯)   r" unfolding diamond_def by simp

lemma diamond_E [elim]: " r  ((r¯ O r)  (r O r¯)  P)  P"
  unfolding diamond_def by simp

lemma diamond_imp_semi_confluence:
  assumes " r" shows "(r¯ O r*)  r"
proof (rule subrelI)
  fix y z assume "(y, z)   r¯ O r*"
  then obtain x where "(x, y)  r" and "(x, z)  r*" by best
  then obtain n where "(x, z)  r^^n" using rtrancl_imp_UN_relpow by best
  with (x, y)  r show "(y, z)  r"
  proof (induct n arbitrary: x z y)
    case 0 then show ?case by auto
  next
    case (Suc n)
    from (x, z)  r^^Suc n obtain x' where "(x, x')  r" and "(x', z)  r^^n"
      using relpow_Suc_D2 by best
    with (x, y)  r have "(y, x')  (r¯ O r)" by auto
    with  r have "(y, x')  (r O r¯)" by auto
    then obtain y' where "(x', y')  r" and "(y, y')  r" by best
    with Suc and (x', z)  r^^n have "(y', z)  r" by auto
    with (y, y')  r show ?case by (auto intro: rtrancl_join_join)
  qed
qed

lemma semi_confluence_imp_CR:
  assumes "(r¯ O r*)  r" shows "CR r"
proof - {
  fix x y z assume "(x, y)  r*" and "(x, z)  r*"
  then obtain n where "(x, z)  r^^n" using rtrancl_imp_UN_relpow by best
  with (x, y)  r* have "(y, z)  r"
  proof (induct n arbitrary: x y z)
    case 0 then show ?case by auto
  next
    case (Suc n)
    from (x, z)  r^^Suc n obtain x' where "(x, x')  r" and "(x', z)  r^^n"
      using relpow_Suc_D2 by best
    from (x, x')  r and (x, y)  r* have "(x', y)  (r¯ O r* )" by auto
    with assms have "(x', y)  r" by auto
    then obtain y' where "(x', y')  r*" and "(y, y')  r*" by best
    with Suc and (x', z)  r^^n have "(y', z)  r" by simp
    then obtain u where "(z, u)  r*" and "(y', u)  r*" by best
    from (y, y')  r* and (y', u)  r* have "(y, u)  r*" by auto
    with (z, u)  r* show ?case by best
  qed
} then show ?thesis by auto
qed
 
lemma diamond_imp_CR:
  assumes " r" shows "CR r"
  using assms by (rule diamond_imp_semi_confluence [THEN semi_confluence_imp_CR])

lemma diamond_imp_CR':
  assumes " s" and "r  s" and "s  r*" shows "CR r"
  unfolding CR_iff_meet_subset_join
proof -
  from  s have "CR s" by (rule diamond_imp_CR)
  then have "s  s" unfolding CR_iff_meet_subset_join by simp
  from r  s have "r*  s*" by (rule rtrancl_mono)
  from s  r* have "s*  (r*)*" by (rule rtrancl_mono)
  then have "s*  r*" by simp
  with r*  s* have "r* = s*" by simp
  show "r  r" unfolding meet_def join_def rtrancl_converse r* = s*
    unfolding rtrancl_converse [symmetric] meet_def [symmetric]
      join_def [symmetric] by (rule s  s)
qed

lemma SN_imp_minimal:
  assumes "SN A"
  shows "Q x. x  Q  (zQ. y. (z, y)  A  y  Q)"
proof (rule ccontr)
  assume "¬ (Q x. x  Q  (zQ. y. (z, y)  A  y  Q))"
  then obtain Q x where "x  Q" and "zQ. y. (z, y)  A  y  Q" by auto
  then have "z. y. z  Q  (z, y)  A  y  Q" by auto
  then have "f. x. x  Q  (x, f x)  A  f x  Q" by (rule choice)
  then obtain f where a:"x. x  Q  (x, f x)  A  f x  Q" (is "x. ?P x") by best
  let ?S = "λi. (f ^^ i) x"
  have "?S 0 = x" by simp
  have "i. (?S i, ?S (Suc i))  A  ?S (Suc i)  Q"
  proof
    fix i show "(?S i, ?S (Suc i))  A  ?S (Suc i)  Q"
      by (induct i) (auto simp: x  Q a)
  qed
  with ?S 0 = x have "S. S 0 = x  chain A S" by fast
  with assms show False by auto
qed

lemma SN_on_imp_on_minimal:
  assumes "SN_on r {x}"
  shows "Q. x  Q  (zQ. y. (z, y)  r  y  Q)"
proof (rule ccontr)
  assume "¬(Q. x  Q  (zQ. y. (z, y)  r  y  Q))"
  then obtain Q where "x  Q" and "zQ. y. (z, y)  r  y  Q" by auto
  then have "z. y. z  Q  (z, y)  r  y  Q" by auto
  then have "f. x. x  Q  (x, f x)  r  f x  Q" by (rule choice)
  then obtain f where a: "x. x  Q  (x, f x)  r  f x  Q" (is "x. ?P x") by best
  let ?S = "λi. (f ^^ i) x"
  have "?S 0 = x" by simp
  have "i. (?S i,?S(Suc i))  r  ?S(Suc i)  Q"
  proof
    fix i show "(?S i,?S(Suc i))  r  ?S(Suc i)  Q" by (induct i) (auto simp:x  Q a)
  qed
  with ?S 0 = x have "S. S 0 = x  chain r S" by fast
  with assms show False by auto
qed

lemma minimal_imp_wf:
  assumes "Q x. x  Q  (zQ. y. (z, y)  r  y  Q)"
  shows "wf(r¯)"
proof (rule ccontr)
  assume "¬ wf(r¯)"
  then have "P. (x. (y. (x, y)  r  P y)  P x)  (x. ¬ P x)" unfolding wf_def by simp
  then obtain P x where suc:"x. (y. (x, y)  r  P y)  P x" and "¬ P x" by auto
  let ?Q = "{x. ¬ P x}"
  from ¬ P x have "x  ?Q" by simp
  from assms have "x. x  ?Q  (z?Q. y. (z, y)  r  y  ?Q)" by (rule allE [where x = ?Q])
  with x  ?Q obtain z where "z  ?Q" and min:" y. (z, y)  r  y  ?Q" by best
  from z  ?Q have "¬ P z" by simp
  with suc obtain y where "(z, y)  r" and "¬ P y" by best
  then have "y  ?Q" by simp
  with (z, y)  r and min show False by simp
qed

lemmas SN_imp_wf = SN_imp_minimal [THEN minimal_imp_wf]

lemma wf_imp_SN:
  assumes "wf (A¯)" shows "SN A"
proof - {
  fix a
  let ?P = "λa. ¬(S. S 0 = a  chain A S)"
  from wf (A¯) have "?P a"
  proof induct
    case (less a)
    then have IH: "b. (a, b)  A  ?P b" by auto
    show "?P a"
    proof (rule ccontr)
      assume "¬ ?P a"
      then obtain S where "S 0 = a" and "chain A S" by auto
      then have "(S 0, S 1)  A" by auto
      with IH have "?P (S 1)" unfolding S 0 = a by auto
      with chain A S show False by auto
    qed
  qed
  then have "SN_on A {a}" unfolding SN_defs by auto
} then show ?thesis by fast
qed

lemma SN_nat_gt: "SN {(a, b :: nat) . a > b}"
proof -
  from wf_less have "wf ({(x, y) . (x :: nat) > y}¯)" unfolding converse_unfold by auto
  from wf_imp_SN [OF this] show ?thesis .
qed


lemma SN_iff_wf: "SN A = wf (A¯)" by (auto simp: SN_imp_wf wf_imp_SN)

lemma SN_imp_acyclic: "SN R  acyclic R"
  using wf_acyclic [of "R¯", unfolded SN_iff_wf [symmetric]] by auto

lemma SN_induct:
  assumes sn: "SN r" and step: "a. (b. (a, b)  r  P b)  P a"
  shows "P a"
using sn unfolding SN_iff_wf proof induct
  case (less a)
  with step show ?case by best
qed

(* The same as well-founded induction, but in the 'correct' direction. *)
lemmas SN_induct_rule = SN_induct [consumes 1, case_names IH, induct pred: SN]

lemma SN_on_induct [consumes 2, case_names IH, induct pred: SN_on]:
  assumes SN: "SN_on R A"
    and "s  A"
    and imp: "t. (u. (t, u)  R  P u)  P t"
  shows "P s"
proof -
  let ?R = "restrict_SN R R"
  let ?P = "λt. SN_on R {t}  P t"
  have "SN_on R {s}  P s"
  proof (rule SN_induct [OF SN_restrict_SN_idemp [of R], of ?P])
    fix a
    assume ind: "b. (a, b)  ?R  SN_on R {b}  P b"
    show "SN_on R {a}  P a"
    proof
      assume SN: "SN_on R {a}"
      show "P a"
      proof (rule imp)
        fix b
        assume "(a, b)  R"
        with SN step_preserves_SN_on [OF this SN]
        show "P b" using ind [of b] unfolding restrict_SN_def by auto
      qed
    qed
  qed
  with SN show "P s" using s  A unfolding SN_on_def by blast
qed

(* link SN_on to acc / accp *)
lemma accp_imp_SN_on:
  assumes "x. x  A  Wellfounded.accp g x"
  shows "SN_on {(y, z). g z y} A"
proof - {
  fix x assume "x  A"
  from assms [OF this]
  have "SN_on {(y, z). g z y} {x}"
  proof (induct rule: accp.induct)
    case (accI x)
    show ?case
    proof
      fix f
      assume x: "f 0  {x}" and steps: " i. (f i, f (Suc i))  {a. (λ(y, z). g z y) a}"
      then have "g (f 1) x" by auto
      from accI(2)[OF this] steps x show False unfolding SN_on_def by auto
    qed
  qed
  }
  then show ?thesis unfolding SN_on_def by blast
qed

lemma SN_on_imp_accp:
  assumes "SN_on {(y, z). g z y} A"
  shows "xA. Wellfounded.accp g x"
proof
  fix x assume "x  A"
  with assms show "Wellfounded.accp g x"
  proof (induct rule: SN_on_induct)
    case (IH x)
    show ?case
    proof
      fix y
      assume "g y x"
      with IH show "Wellfounded.accp g y" by simp
    qed
  qed
qed

lemma SN_on_conv_accp:
  "SN_on {(y, z). g z y} {x} = Wellfounded.accp g x"
  using SN_on_imp_accp [of g "{x}"]
        accp_imp_SN_on [of "{x}" g]
  by auto

lemma SN_on_conv_acc: "SN_on {(y, z). (z, y)  r} {x}  x  Wellfounded.acc r"
  unfolding SN_on_conv_accp accp_acc_eq ..

lemma acc_imp_SN_on:
  assumes "x  Wellfounded.acc r" shows "SN_on {(y, z). (z, y)  r} {x}"
  using assms unfolding SN_on_conv_acc by simp

lemma SN_on_imp_acc:
  assumes "SN_on {(y, z). (z, y)  r} {x}" shows "x  Wellfounded.acc r"
  using assms unfolding SN_on_conv_acc by simp


subsection ‹Newman's Lemma›

lemma rtrancl_len_E [elim]:
  assumes "(x, y)  r*" obtains n where "(x, y)  r^^n"
  using rtrancl_imp_UN_relpow [OF assms] by best

lemma relpow_Suc_E2' [elim]:
  assumes "(x, z)  A^^Suc n" obtains y where "(x, y)  A" and "(y, z)  A*"
proof -
  assume assm: "y. (x, y)  A  (y, z)  A*  thesis"
  from relpow_Suc_E2 [OF assms] obtain y where "(x, y)  A" and "(y, z)  A^^n" by auto
  then have "(y, z)  A*" using (*FIXME*) relpow_imp_rtrancl by auto
  from assm [OF (x, y)  A this] show thesis .
qed

lemmas SN_on_induct' [consumes 1, case_names IH] = SN_on_induct [OF _ singletonI]

lemma Newman_local:
  assumes "SN_on r X" and WCR: "WCR_on r {x. SN_on r {x}}"
  shows "CR_on r X"
proof - {
  fix x
  assume "x  X"
  with assms have "SN_on r {x}" unfolding SN_on_def by auto
  with this  have "CR_on r {x}"
  proof (induct rule: SN_on_induct')
    case (IH x) show ?case
    proof
      fix y z assume "(x, y)  r*" and "(x, z)  r*"
      from (x, y)  r* obtain m where "(x, y)  r^^m" ..
      from (x, z)  r* obtain n where "(x, z)  r^^n" ..
      show "(y, z)  r"
      proof (cases n)
        case 0
        from (x, z)  r^^n have eq: "x = z" by (simp add: 0)
        from (x, y)  r* show ?thesis unfolding eq ..
      next
        case (Suc n')
        from (x, z)  r^^n [unfolded Suc] obtain t where "(x, t)  r" and "(t, z)  r*" ..
        show ?thesis
        proof (cases m)
          case 0
          from (x, y)  r^^m have eq: "x = y" by (simp add: 0)
          from (x, z)  r* show ?thesis unfolding eq ..
        next
          case (Suc m')
          from (x, y)  r^^m [unfolded Suc] obtain s where "(x, s)  r" and "(s, y)  r*" ..          
          from WCR IH(2) have "WCR_on r {x}" unfolding WCR_on_def by auto
          with (x, s)  r and (x, t)  r have "(s, t)  r" by auto
          then obtain u where "(s, u)  r*" and "(t, u)  r*" ..
          from (x, s)  r IH(2) have "SN_on r {s}" by (rule step_preserves_SN_on)
          from IH(1)[OF (x, s)  r this] have "CR_on r {s}" .
          from this and (s, u)  r* and (s, y)  r* have "(u, y)  r" by auto
          then obtain v where "(u, v)  r*" and "(y, v)  r*" ..
          from (x, t)  r IH(2) have "SN_on r {t}" by (rule step_preserves_SN_on)
          from IH(1)[OF (x, t)  r this] have "CR_on r {t}" .
          moreover from (t, u)  r* and (u, v)  r* have "(t, v)  r*" by auto
          ultimately have "(z, v)  r" using (t, z)  r* by auto
          then obtain w where "(z, w)  r*" and "(v, w)  r*" ..
          from (y, v)  r* and (v, w)  r* have "(y, w)  r*" by auto
          with (z, w)  r* show ?thesis by auto
        qed
      qed
    qed
  qed
  }
  then show ?thesis unfolding CR_on_def by blast
qed

lemma Newman: "SN r  WCR r  CR r"
  using Newman_local [of r UNIV]
  unfolding WCR_on_def by auto
  
lemma Image_SN_on:
  assumes "SN_on r (r `` A)"
  shows "SN_on r A"
proof
  fix f
  assume "f 0  A" and chain: "chain r f"
  then have "f (Suc 0)  r `` A" by auto
  with assms have "SN_on r {f (Suc 0)}" by (auto simp add: f 0  A SN_defs)
  moreover have "¬ SN_on r {f (Suc 0)}"
  proof -
    have "f (Suc 0)  {f (Suc 0)}" by simp
    moreover from chain have "chain r (f  Suc)" by auto
    ultimately show ?thesis by auto
  qed
  ultimately show False by simp
qed

lemma SN_on_Image_conv: "SN_on r (r `` A) = SN_on r A"
  using SN_on_Image and Image_SN_on by blast

text ‹If all successors are terminating, then the current element is also terminating.›
lemma step_reflects_SN_on:
  assumes "(b. (a, b)  r  SN_on r {b})"
  shows "SN_on r {a}"
  using assms and Image_SN_on [of r "{a}"] by (auto simp: SN_defs)

lemma SN_on_all_reducts_SN_on_conv:
  "SN_on r {a} = (b. (a, b)  r  SN_on r {b})"
  using SN_on_Image_conv [of r "{a}"] by (auto simp: SN_defs)

lemma SN_imp_SN_trancl: "SN R  SN (R+)"
  unfolding SN_iff_wf by (rule wf_converse_trancl)

lemma SN_trancl_imp_SN:
  assumes "SN (R+)" shows "SN R"
  using assms by (rule SN_on_trancl_imp_SN_on)

lemma SN_trancl_SN_conv: "SN (R+) = SN R"
  using SN_trancl_imp_SN [of R] SN_imp_SN_trancl [of R] by blast

lemma SN_inv_image: "SN R  SN (inv_image R f)" unfolding SN_iff_wf by simp

lemma SN_subset: "SN R  R'  R  SN R'" unfolding SN_defs by blast
 
lemma SN_pow_imp_SN:
  assumes "SN (A^^Suc n)" shows "SN A"
proof (rule ccontr)
  assume "¬ SN A"
  then obtain S where "chain A S" unfolding SN_defs by auto
  from chain_imp_relpow [OF this]
    have step: "i. (S i, S (i + (Suc n)))  A^^Suc n" .
  let ?T = "λi. S (i * (Suc n))"
  have "chain (A^^Suc n) ?T"
  proof
    fix i show "(?T i, ?T (Suc i))  A^^Suc n" unfolding mult_Suc
      using step [of "i * Suc n"] by (simp only: add.commute)
  qed
  then have "¬ SN (A^^Suc n)" unfolding SN_defs by fast
  with assms show False by simp
qed

(* TODO: move to Isabelle Library? *)
lemma pow_Suc_subset_trancl: "R^^(Suc n)  R+"
  using trancl_power [of _ R] by blast

lemma SN_imp_SN_pow:
  assumes "SN R" shows "SN (R^^Suc n)"
  using SN_subset [where R="R+", OF SN_imp_SN_trancl [OF assms] pow_Suc_subset_trancl] by simp
  
(*FIXME: needed in HOL/Wellfounded.thy*)
lemma SN_pow: "SN R  SN (R ^^ Suc n)"
  by (rule iffI, rule SN_imp_SN_pow, assumption, rule SN_pow_imp_SN, assumption)

lemma SN_on_trancl:
  assumes "SN_on r A" shows "SN_on (r+) A"
using assms
proof (rule contrapos_pp)
  let ?r = "restrict_SN r r"
  assume "¬ SN_on (r+) A"
  then obtain f where "f 0  A" and chain: "chain (r+) f" by auto
  have "SN ?r" by (rule SN_restrict_SN_idemp)
  then have "SN (?r+)" by (rule SN_imp_SN_trancl)
  have "i. (f 0, f i)  r*"
  proof
    fix i show "(f 0, f i)  r*"
    proof (induct i)
      case 0 show ?case ..
    next
      case (Suc i)
      from chain have "(f i, f (Suc i))  r+" ..
      with Suc show ?case by auto
    qed
  qed
  with assms have "i. SN_on r {f i}"
    using steps_preserve_SN_on [of "f 0" _ r]
    and f 0  A
    and SN_on_subset2 [of "{f 0}" "A"] by auto
  with chain have "chain (?r+) f"
    unfolding restrict_SN_trancl_simp
    unfolding restrict_SN_def by auto
  then have "¬ SN_on (?r+) {f 0}" by auto
  with SN (?r+) have False by (simp add: SN_defs)
  then show "¬ SN_on r A" by simp
qed

lemma SN_on_trancl_SN_on_conv: "SN_on (R+) T = SN_on R T"
  using SN_on_trancl_imp_SN_on [of R] SN_on_trancl [of R] by blast


text ‹Restrict an ARS to elements of a given set.›
definition "restrict" :: "'a rel  'a set  'a rel" where
  "restrict r S = {(x, y). x  S  y  S  (x, y)  r}"

lemma SN_on_restrict:
  assumes "SN_on r A"
  shows "SN_on (restrict r S) A" (is "SN_on ?r A")
proof (rule ccontr)
  assume "¬ SN_on ?r A"
  then have "f. f 0  A  chain ?r f" by auto
  then have "f. f 0  A  chain r f" unfolding restrict_def by auto
  with SN_on r A show False by auto
qed

lemma restrict_rtrancl: "(restrict r S)*  r*" (is "?r*  r*")
proof - {
  fix x y assume "(x, y)  ?r*" then have "(x, y)  r*" unfolding restrict_def by induct auto
} then show ?thesis by auto
qed

lemma rtrancl_Image_step:
  assumes "a  r* `` A"
    and "(a, b)  r*"
  shows "b  r* `` A"
proof -
  from assms(1) obtain c where "c  A" and "(c, a)  r*" by auto
  with assms have "(c, b)  r*" by auto
  with c  A show ?thesis by auto
qed

lemma WCR_SN_on_imp_CR_on:
  assumes "WCR r" and "SN_on r A" shows "CR_on r A"
proof -
  let ?S = "r* `` A"
  let ?r = "restrict r ?S"
  have "x. SN_on ?r {x}"
  proof
    fix y have "y  ?S  y  ?S" by simp
    then show "SN_on ?r {y}"
    proof
      assume "y  ?S" then show ?thesis unfolding restrict_def by auto
    next
      assume "y  ?S"
      then have "y  r* `` A" by simp
      with SN_on_Image_rtrancl [OF SN_on r A]
        have "SN_on r {y}" using SN_on_subset2 [of "{y}" "r* `` A"] by blast
      then show ?thesis by (rule SN_on_restrict)
    qed
  qed
  then have "SN ?r" unfolding SN_defs by auto
  {
    fix x y assume "(x, y)  r*" and "x  ?S" and "y  ?S"
    then obtain n where "(x, y)  r^^n" and "x  ?S" and "y  ?S"
      using rtrancl_imp_UN_relpow by best
    then have "(x, y)  ?r*"
    proof (induct n arbitrary: x y)
      case 0 then show ?case by simp
    next
      case (Suc n)
      from (x, y)  r^^Suc n obtain x' where "(x, x')  r" and "(x', y)  r^^n"
        using relpow_Suc_D2 by best
      then have "(x, x')  r*" by simp
      with x  ?S have "x'  ?S" by (rule rtrancl_Image_step)
      with Suc and (x', y)  r^^n have "(x', y)  ?r*" by simp
      from (x, x')  r and x  ?S and x'  ?S have "(x, x')  ?r"
        unfolding restrict_def by simp
      with (x', y)  ?r* show ?case by simp
    qed
  }
  then have a:"x y. (x, y)  r*  x  ?S  y  ?S  (x, y)  ?r*" by simp
  {
    fix x' y z assume "(x', y)  ?r" and "(x', z)  ?r"
    then have "x'  ?S" and "y  ?S" and "z  ?S" and "(x', y)  r" and "(x', z)  r"
      unfolding restrict_def by auto
    with WCR r have "(y, z)  r" by auto
    then obtain u where "(y, u)  r*" and "(z, u)  r*" by auto
    from x'  ?S obtain x where "x  A" and "(x, x')  r*" by auto
    from (x', y)  r have "(x', y)  r*" by auto
    with (y, u)  r* have "(x', u)  r*" by auto
    with (x, x')  r* have "(x, u)  r*" by simp
    then have "u  ?S" using x  A by auto
    from y  ?S and u  ?S and (y, u)  r* have "(y, u)  ?r*" using a by auto
    from z  ?S and u  ?S and (z, u)  r* have "(z, u)  ?r*" using a by auto
    with (y, u)  ?r* have "(y, z)  ?r" by auto
  }
  then have "WCR ?r" by auto
  have "CR ?r" using Newman [OF SN ?r WCR ?r] by simp
  {
    fix x y z assume "x  A" and "(x, y)  r*" and "(x, z)  r*"
    then have "y  ?S" and "z  ?S" by auto
    have "x  ?S" using x  A by auto
    from a and (x, y)  r* and x  ?S and y  ?S have "(x, y)  ?r*" by simp
    from a and (x, z)  r* and x  ?S and z  ?S have "(x, z)  ?r*" by simp
    with CR ?r and (x, y)  ?r* have "(y, z)  ?r" by auto
    then obtain u where "(y, u)  ?r*" and "(z, u)  ?r*" by best
    then have "(y, u)  r*" and "(z, u)  r*" using restrict_rtrancl by auto
    then have "(y, z)  r" by auto
  }
  then show ?thesis by auto
qed

lemma SN_on_Image_normalizable:
  assumes "SN_on r A"
  shows "aA. b. b  r! `` A"
proof
  fix a assume a: "a  A"
  show "b. b  r! `` A"
  proof (rule ccontr)
    assume "¬ (b. b  r! `` A)"
    then have A: "b. (a, b)  r*  b  NF r" using a by auto
    then have "a  NF r" by auto
    let ?Q = "{c. (a, c)  r*  c  NF r}"
    have "a  ?Q" using a  NF r by simp
    have "c?Q. b. (c, b)  r  b  ?Q"
    proof
      fix c
      assume "c  ?Q"
      then have "(a, c)  r*" and "c  NF r" by auto
      then obtain d where "(c, d)  r" by auto
      with (a, c)  r* have "(a, d)  r*" by simp
      with A have "d  NF r" by simp
      with (c, d)  r and (a, c)  r*
        show "b. (c, b)  r  b  ?Q" by auto
    qed
    with a  ?Q have "a  ?Q  (c?Q. b. (c, b)  r  b  ?Q)" by auto
    then have "Q. a  Q  (cQ. b. (c, b)  r  b  Q)" by (rule exI [of _ "?Q"])
    then have "¬ (Q. a  Q  (cQ. b. (c, b)  r  b  Q))" by simp
    with SN_on_imp_on_minimal [of r a] have "¬ SN_on r {a}" by blast
    with assms and a  A and SN_on_subset2 [of "{a}" A r] show False by simp
  qed
qed

lemma SN_on_imp_normalizability:
  assumes "SN_on r {a}" shows "b. (a, b)  r!"
  using SN_on_Image_normalizable [OF assms] by auto


subsection ‹Commutation›

definition commute :: "'a rel  'a rel  bool" where
  "commute r s  ((r¯)* O s*)  (s* O (r¯)*)"

lemma CR_iff_self_commute: "CR r = commute r r"
  unfolding commute_def CR_iff_meet_subset_join meet_def join_def
  by simp

(* FIXME: move somewhere else *)
lemma rtrancl_imp_rtrancl_UN: 
  assumes "(x, y)  r*" and "r  I"
  shows "(x, y)  (rI. r)*" (is "(x, y)  ?r*")
using assms proof induct
  case base then show ?case by simp
next
  case (step y z)
  then have "(x, y)  ?r*" by simp
  from (y, z)  r and r  I have "(y, z)  ?r*" by auto
  with (x, y)  ?r* show ?case by auto
qed

definition quasi_commute :: "'a rel  'a rel  bool" where
  "quasi_commute r s  (s O r)  r O (r  s)*"

lemma rtrancl_union_subset_rtrancl_union_trancl: "(r  s+)* = (r  s)*"
proof
  show "(r  s+)*  (r  s)*"
  proof (rule subrelI)
    fix x y assume "(x, y)  (r  s+)*"
    then show "(x, y)  (r  s)*"
    proof (induct)
      case base then show ?case by auto
    next
      case (step y z)
      then have "(y, z)  r  (y, z)  s+" by auto
      then have "(y, z)  (r  s)*"
      proof
        assume "(y, z)  r" then show ?thesis by auto
      next
        assume "(y, z)  s+"
        then have "(y, z)  s*" by auto
        then have "(y, z)  r*  s*" by auto
        then show ?thesis using rtrancl_Un_subset by auto
      qed
      with (x, y)  (r  s)* show ?case by simp
    qed
  qed
next
  show "(r  s)*  (r  s+)*"
  proof (rule subrelI)
    fix x y assume "(x, y)  (r  s)*"
    then show "(x, y)  (r  s+)*"
    proof (induct)
      case base then show ?case by auto
    next
      case (step y z)
      then have "(y, z)  (r  s+)*" by auto
      with (x, y)  (r  s+)* show ?case by auto
    qed
  qed
qed

lemma qc_imp_qc_trancl:
  assumes "quasi_commute r s" shows "quasi_commute r (s+)"
unfolding quasi_commute_def
proof (rule subrelI)
  fix x z assume "(x, z)  s+ O r"
  then obtain y where "(x, y)  s+" and "(y, z)  r" by best
  then show "(x, z)  r O (r  s+)*"
  proof (induct arbitrary: z)
    case (base y)
    then have "(x, z)  (s O r)" by auto
    with assms have "(x, z)  r O (r  s)*" unfolding quasi_commute_def by auto
    then show ?case using rtrancl_union_subset_rtrancl_union_trancl by auto
  next
    case (step a b)
    then have "(a, z)  (s O r)" by auto
    with assms have "(a, z)  r O (r  s)*" unfolding quasi_commute_def by auto
    then obtain u where "(a, u)  r" and "(u, z)  (r  s)*" by best
    then have "(u, z)  (r  s+)*" using rtrancl_union_subset_rtrancl_union_trancl by auto
    from (a, u)  r and step have "(x, u)  r O (r  s+)*" by auto
    then obtain v where "(x, v)  r" and "(v, u)  (r  s+)*" by best
    with (u, z)  (r  s+)* have "(v, z)  (r  s+)*" by auto
    with (x, v)  r show ?case by auto
  qed
qed

lemma steps_reflect_SN_on:
  assumes "¬ SN_on r {b}" and "(a, b)  r*"
  shows "¬ SN_on r {a}"
  using SN_on_Image_rtrancl [of r "{a}"]
  and assms and SN_on_subset2 [of "{b}" "r* `` {a}" r] by blast

lemma chain_imp_not_SN_on:
   assumes "chain r f"
   shows "¬ SN_on r {f i}"
proof -
  let ?f = "λj. f (i + j)"
  have "?f 0  {f i}" by simp
  moreover have "chain r ?f" using assms by auto
  ultimately have "?f 0  {f i}  chain r ?f" by blast
  then have "g. g 0  {f i}  chain r g" by (rule exI [of _ "?f"])
  then show ?thesis unfolding SN_defs by auto
qed

lemma quasi_commute_imp_SN:
  assumes "SN r" and "SN s" and "quasi_commute r s"
  shows "SN (r  s)"
proof -
  have "quasi_commute r (s+)" by (rule qc_imp_qc_trancl [OF quasi_commute r s])
  let ?B = "{a. ¬ SN_on (r  s) {a}}"
  {
    assume "¬ SN(r  s)"
    then obtain a where "a  ?B" unfolding SN_defs by fast
    from SN r have "Q x. x  Q  (zQ. y. (z, y)  r  y  Q)"
      by (rule SN_imp_minimal)
    then have "x. x  ?B  (z?B. y. (z, y)  r  y  ?B)" by (rule spec [where x = ?B])
    with a  ?B obtain b where "b  ?B" and min: "y. (b, y)  r  y  ?B" by auto
    from b  ?B obtain S where "S 0 = b" and
      chain: "chain (r  s) S" unfolding SN_on_def by auto
    let ?S = "λi. S(Suc i)"
    have "?S 0 = S 1" by simp
    from chain have "chain (r  s) ?S" by auto
    with ?S 0 = S 1 have "¬ SN_on (r  s) {S 1}" unfolding SN_on_def by auto
    from S 0 = b and chain have "(b, S 1)  r  s" by auto
    with min and ¬ SN_on (r  s) {S 1} have "(b, S 1)  s" by auto
    let ?i = "LEAST i. (S i, S(Suc i))  s"
    {
      assume "chain s S"
      with S 0 = b have "¬ SN_on s {b}" unfolding SN_on_def by auto
      with SN s have False unfolding SN_defs by auto
    }
    then have ex: "i. (S i, S(Suc i))  s" by auto
    then have "(S ?i, S(Suc ?i))  s" by (rule LeastI_ex)
    with chain have "(S ?i, S(Suc ?i))  r" by auto
    have ini: "i<?i. (S i, S(Suc i))  s" using not_less_Least by auto
    {
      fix i assume "i < ?i" then have "(b, S(Suc i))  s+"
      proof (induct i)
        case 0 then show ?case using (b, S 1)  s and S 0 = b by auto
      next
        case (Suc k)
      then have "(b, S(Suc k))  s+" and "Suc k < ?i" by auto
      with i<?i. (S i, S(Suc i))  s have "(S(Suc k), S(Suc(Suc k)))  s" by fast
      with (b, S(Suc k))  s+ show ?case by auto
    qed
    }
    then have pref: "i<?i. (b, S(Suc i))  s+" by auto
    from (b, S 1)  s and S 0 = b have "(S 0, S(Suc 0))  s" by auto
    {
      assume "?i = 0"
      from ex have "(S ?i, S(Suc ?i))  s" by (rule LeastI_ex)
      with (S 0, S(Suc 0))  s have False unfolding ?i = 0 by simp
    }
    then have "0 < ?i" by auto
    then obtain j where "?i =  Suc j" unfolding gr0_conv_Suc by best
    with ini have "(S(?i-Suc 0), S(Suc(?i-Suc 0)))  s" by auto
    with pref have "(b, S(Suc j))  s+" unfolding ?i = Suc j by auto
    then have "(b, S ?i)  s+" unfolding ?i = Suc j by auto
    with (S ?i, S(Suc ?i))  r have "(b, S(Suc ?i))  (s+ O r)" by auto
    with quasi_commute r (s+) have "(b, S(Suc ?i))  r O (r  s+)*"
      unfolding quasi_commute_def by auto
    then obtain c where "(b, c)  r" and "(c, S(Suc ?i))  (r  s+)*" by best
    from (b, c)  r have "(b, c)  (r  s)*" by auto
    from chain_imp_not_SN_on [of S "r  s"]
      and chain have "¬ SN_on (r  s) {S (Suc ?i)}" by auto
    from (c, S(Suc ?i))  (r  s+)* have "(c, S(Suc ?i))  (r  s)*"
      unfolding rtrancl_union_subset_rtrancl_union_trancl by auto
    with steps_reflect_SN_on [of "r  s"]
      and ¬ SN_on (r  s) {S(Suc ?i)} have "¬ SN_on (r  s) {c}" by auto
    then have "c  ?B" by simp
    with (b, c)  r and min have False by auto
  }
  then show ?thesis by auto
qed


subsection ‹Strong Normalization›

lemma non_strict_into_strict:
  assumes compat: "NS O S  S"
    and steps: "(s, t)  (NS*) O S"
  shows "(s, t)  S"
using steps proof
  fix x u z
  assume "(s, t) = (x, z)" and "(x, u)  NS*" and "(u, z)  S"
  then have "(s, u)  NS*" and "(u, t)  S" by auto
  then show ?thesis
  proof (induct rule:rtrancl.induct)
    case (rtrancl_refl x) then show ?case .
  next
    case (rtrancl_into_rtrancl a b c)
    with compat show ?case by auto
  qed
qed

lemma comp_trancl:
  assumes "R O S  S" shows "R O S+  S+"
proof (rule subrelI)
  fix w z assume "(w, z)  R O S+"
  then obtain x where R_step: "(w, x)  R" and S_seq: "(x, z)  S+" by best
  from tranclD [OF S_seq] obtain y where S_step: "(x, y)  S" and S_seq': "(y, z)  S*" by auto
  from R_step and S_step have "(w, y)  R O S" by auto
  with assms have "(w, y)  S" by auto
  with S_seq' show "(w, z)  S+" by simp
qed

lemma comp_rtrancl_trancl:
  assumes comp: "R O S  S"
    and seq: "(s, t)  (R  S)* O S"
  shows "(s, t)  S+"
using seq proof
  fix x u z
  assume "(s, t) = (x, z)" and "(x, u)  (R  S)*" and "(u, z)  S"
  then have "(s, u)  (R  S)*" and "(u, t)  S+" by auto
  then show ?thesis
  proof (induct rule: rtrancl.induct)
    case (rtrancl_refl x) then show ?case .
  next
    case (rtrancl_into_rtrancl a b c)
    then have "(b, c)  R  S" by simp
    then show ?case
    proof
      assume "(b, c)  S"
      with rtrancl_into_rtrancl
      have "(b, t)  S+" by simp
      with rtrancl_into_rtrancl show ?thesis by simp
    next
      assume "(b, c)  R"
      with comp_trancl [OF comp] rtrancl_into_rtrancl
      show ?thesis by auto
    qed
  qed
qed

lemma trancl_union_right: "r+  (s  r)+"
proof (rule subrelI)
  fix x y assume "(x, y)  r+" then show "(x, y)  (s  r)+"
  proof (induct)
    case base then show ?case by auto
  next
    case (step a b)
    then have "(a, b)  (s  r)+" by auto
    with (x, a)  (s  r)+ show ?case by auto
  qed
qed

lemma restrict_SN_subset: "restrict_SN R S  R"
proof (rule subrelI)
  fix a b assume "(a, b)  restrict_SN R S" then show "(a, b)  R" unfolding restrict_SN_def by simp
qed

lemma chain_Un_SN_on_imp_first_step:
  assumes "chain (R  S) t" and "SN_on S {t 0}"
  shows "i. (t i, t (Suc i))  R  (j<i. (t j, t (Suc j))  S  (t j, t (Suc j))  R)"
proof -
  from SN_on S {t 0} obtain i where "(t i, t (Suc i))  S" by blast
  with assms have "(t i, t (Suc i))  R" (is "?P i") by auto
  let ?i = "Least ?P"
  from ?P i have "?P ?i" by (rule LeastI)
  have "j<?i. (t j, t (Suc j))  R" using not_less_Least by auto
  moreover with assms have "j<?i. (t j, t (Suc j))  S" by best
  ultimately have "j<?i. (t j, t (Suc j))  S  (t j, t (Suc j))  R" by best
  with ?P ?i show ?thesis by best
qed

lemma first_step:
  assumes C: "C = A  B" and steps: "(x, y)  C*" and Bstep: "(y, z)  B"
  shows "y. (x, y)  A* O B"
  using steps
proof (induct rule: converse_rtrancl_induct)
  case base
  show ?case using Bstep by auto
next 
  case (step u x)
  from step(1)[unfolded C] 
  show ?case
  proof
    assume "(u, x)  B"
    then show ?thesis by auto
  next
    assume ux: "(u, x)  A"
    from step(3) obtain y where "(x, y)  A* O B" by auto
    then obtain z where "(x, z)  A*" and step: "(z, y)  B" by auto
    with ux have "(u, z)  A*" by auto
    with step have "(u, y)  A* O B" by auto
    then show ?thesis by auto
  qed
qed

lemma first_step_O:
  assumes C: "C = A  B" and steps: "(x, y)  C* O B"
  shows " y. (x, y)  A* O B"
proof -
  from steps obtain z where "(x, z)  C*" and "(z, y)  B" by auto
  from first_step [OF C this] show ?thesis .
qed

lemma firstStep:
  assumes LSR: "L = S  R" and xyL: "(x, y)  L*"
  shows "(x, y)  R*  (x, y)  R* O S O L*"
proof (cases "(x, y)  R*")
  case True
  then show ?thesis by simp
next
  case False 
  let ?SR = "S  R"
  from xyL and LSR have "(x, y)  ?SR*" by simp
  from this and False have "(x, y)  R* O S O ?SR*" 
  proof (induct rule: rtrancl_induct)
    case base then show ?case by simp
  next
    case (step y z)
    then show ?case
    proof (cases "(x, y)  R*")
      case False with step have "(x, y)  R* O S O ?SR*" by simp
      from this obtain u where xu: "(x, u)  R* O S" and uy: "(u, y)  ?SR*" by force
      from (y, z)  ?SR have "(y, z)  ?SR*" by auto
      with uy have "(u, z)  ?SR*" by (rule rtrancl_trans)
      with xu show ?thesis by auto
    next
      case True 
      have "(y, z)  S" 
      proof (rule ccontr)
        assume "(y, z)  S" with (y, z)  ?SR have "(y, z)  R" by auto
        with True  have "(x, z)  R*"  by auto
        with (x, z)  R* show False ..
      qed
      with True show ?thesis by auto
    qed
  qed
  with LSR show ?thesis by simp
qed


lemma non_strict_ending:
  assumes chain: "chain (R  S) t"
    and comp: "R O S  S"
    and SN: "SN_on S {t 0}"
  shows "j. ij. (t i, t (Suc i))  R - S"
proof (rule ccontr)
  assume "¬ ?thesis"
  with chain have "i. j. j  i  (t j, t (Suc j))  S" by blast
  from choice [OF this] obtain f where S_steps: "i. i  f i  (t (f i), t (Suc (f i)))  S" ..
  let ?t = "λi. t (((Suc  f) ^^ i) 0)"
  have S_chain: "i. (t i, t (Suc (f i)))  S+"
  proof
    fix i
    from S_steps have leq: "if i" and step: "(t(f i), t(Suc(f i)))  S" by auto
    from chain_imp_rtrancl [OF chain leq] have "(t i, t(f i))  (R  S)*" .
    with step have "(t i, t(Suc(f i)))  (R  S)* O S" by auto
    from comp_rtrancl_trancl [OF comp this] show "(t i, t(Suc(f i)))  S+" .
  qed
  then have "chain (S+) ?t"by simp
  moreover have "SN_on (S+) {?t 0}" using SN_on_trancl [OF SN] by simp
  ultimately show False unfolding SN_defs by best
qed

lemma SN_on_subset1:
  assumes "SN_on r A" and "s  r"
  shows "SN_on s A"
  using assms unfolding SN_defs by blast

lemmas SN_on_mono = SN_on_subset1

lemma rtrancl_fun_conv:
  "((s, t)  R*) = ( f n. f 0 = s  f n = t  ( i < n. (f i, f (Suc i))  R))"
  unfolding rtrancl_is_UN_relpow using relpow_fun_conv [where R = R]
  by auto

lemma compat_tr_compat:
  assumes "NS O S  S" shows "NS* O S  S"
  using non_strict_into_strict [where S = S and NS = NS] assms by blast

lemma right_comp_S [simp]:
  assumes "(x, y)  S O (S O S* O NS*  NS*)"
  shows "(x, y)  (S O S* O NS*)"
proof-
  from assms have "(x, y)  (S O S O S* O NS*)  (S O NS*)" by auto
  then have  xy:"(x, y)  (S O (S O S*) O NS*)  (S O NS*)" by auto
  have "S O S*  S*" by auto
  with xy have "(x, y)  (S O S* O NS*)  (S O NS*)" by auto
  then show "(x, y)  (S O S* O NS*)" by auto
qed

lemma compatible_SN:
  assumes SN: "SN S"
  and compat: "NS O S  S" 
  shows "SN (S O S* O NS*)" (is "SN ?A")
proof
  fix F assume chain: "chain ?A F"
  from compat compat_tr_compat have tr_compat: "NS* O S  S" by blast
  have "i. (y z. (F i, y)  S  (y, z)   S*  (z, F (Suc i))  NS*)"
  proof
    fix i
    from chain have "(F i, F (Suc i))  (S O S* O NS*)" by auto
    then show " y z. (F i, y)   S  (y, z)   S*  (z, F (Suc i))  NS*"
      unfolding relcomp_def (*FIXME:relcomp_unfold*) using mem_Collect_eq by auto
  qed
  then have " f. ( i. ( z. (F i, f i)   S  ((f i, z)   S*) (z, F (Suc i))  NS*))"
    by (rule choice)
  then obtain f
    where " i. ( z. (F i, f i)   S  ((f i, z)   S*) (z, F (Suc i))  NS*)" ..
  then have " g.  i. (F i, f i)   S  (f i, g i)   S*  (g i, F (Suc i))  NS*"
    by (rule choice)
  then obtain g where " i. (F i, f i)   S  (f i, g i)   S*  (g i, F (Suc i))  NS*" ..
  then have " i. (f i, g i)   S*  (g i, F (Suc i))  NS*  (F (Suc i), f (Suc i))   S"
    by auto
  then have " i. (f i, g i)   S*  (g i, f (Suc i))   S" unfolding relcomp_def (*FIXME*)
    using tr_compat by auto
  then have all:" i. (f i, g i)   S*  (g i, f (Suc i))   S+" by auto
  have " i. (f i, f (Suc i))   S+"
  proof
    fix i
    from all have "(f i, g i)   S*  (g i, f (Suc i))   S+" ..
    then show "(f i, f (Suc i))   S+" using transitive_closure_trans by auto
  qed
  then have "x. f 0 = x  chain (S+) f"by auto
  then obtain x where "f 0 = x  chain (S+) f" by auto
  then have "f. f 0 = x  chain (S+) f" by auto
  then have "¬ SN_on (S+) {x}" by auto
  then have "¬ SN (S+)" unfolding SN_defs by auto
  then have wfSconv:"¬ wf ((S+)¯)" using SN_iff_wf by auto
  from SN have "wf (S¯)" using SN_imp_wf [where?r=S] by simp
  with wf_converse_trancl wfSconv show False by auto
qed

lemma compatible_rtrancl_split:
  assumes compat: "NS O S  S"
   and steps: "(x, y)  (NS  S)*"
  shows "(x, y)  S O S* O NS*  NS*"
proof-
  from steps have " n. (x, y)  (NS  S)^^n" using rtrancl_imp_relpow [where ?R="NS  S"] by auto
  then obtain n where "(x, y)  (NS  S)^^n" by auto
  then show "(x, y)   S O S* O NS*  NS*"
  proof (induct n arbitrary: x, simp)
    case (Suc m)
    assume "(x, y)  (NS  S)^^(Suc m)"
    then have " z. (x, z)  (NS  S)  (z, y)  (NS  S)^^m"
      using relpow_Suc_D2 [where ?R="NS  S"] by auto
    then obtain z where xz:"(x, z)  (NS  S)" and zy:"(z, y)  (NS  S)^^m" by auto
    with Suc have zy:"(z, y)   S O S* O NS*  NS*" by auto
    then show "(x, y)   S O S* O NS*  NS*"
    proof (cases "(x, z)  NS")
      case True
      from compat compat_tr_compat have trCompat: "NS* O S  S" by blast
      from zy True have "(x, y)  (NS O S O S* O NS*)  (NS O NS*)" by auto
      then have "(x, y)  ((NS O S) O S* O NS*)  (NS O NS*)" by auto
      then have "(x, y)  ((NS* O S) O S* O NS*)  (NS O NS*)" by auto
      with trCompat have xy:"(x, y)  (S O S* O NS*)  (NS O NS*)" by auto
      have "NS O NS*  NS*" by auto
      with xy show "(x, y)  (S O S* O NS*)  NS*" by auto
    next
      case False
      with xz have xz:"(x, z)  S" by auto
      with zy have "(x, y)  S O (S O S* O NS*  NS*)" by auto
      then show "(x, y)  (S O S* O NS*)  NS*" using right_comp_S by simp
    qed
  qed
qed

lemma compatible_conv:
  assumes compat: "NS O S  S" 
  shows "(NS  S)* O S O (NS  S)* = S O S* O NS*" 
proof -
  let ?NSuS = "NS  S"
  let ?NSS = "S O S* O NS*"
  let ?midS = "?NSuS* O S O ?NSuS*"
  have one: "?NSS  ?midS" by regexp 
  have "?NSuS* O S  (?NSS  NS*) O S"
    using compatible_rtrancl_split [where S = S and NS = NS] compat by blast
  also have "  ?NSS O S  NS* O S" by auto
  also have "  ?NSS O S  S" using compat compat_tr_compat [where S = S and NS = NS] by auto
  also have "  S O ?NSuS*" by regexp
  finally have "?midS  S O ?NSuS* O ?NSuS*" by blast
  also have "  S O ?NSuS*" by regexp
  also have "  S O (?NSS  NS*)"
    using compatible_rtrancl_split [where S = S and NS = NS] compat by blast
  also have "  ?NSS" by regexp
  finally have two: "?midS  ?NSS" . 
  from one two show ?thesis by auto 
qed

lemma compatible_SN': 
  assumes compat: "NS O S  S" and SN: "SN S"
  shows "SN((NS  S)* O S O (NS  S)*)"
using compatible_conv [where S = S and NS = NS] 
  compatible_SN [where S = S and NS = NS] assms by force

lemma rtrancl_diff_decomp:
  assumes "(x, y)  A* - B*"
  shows "(x, y)  A* O (A - B) O A*"
proof-
  from assms have A: "(x, y)  A*" and B:"(x, y)  B*" by auto
  from A have " k. (x, y)  A^^k" by (rule rtrancl_imp_relpow)
  then obtain k where Ak:"(x, y)  A^^k" by auto
  from Ak B show "(x, y)  A* O (A - B) O A*"
  proof (induct k arbitrary: x)
    case 0
    with (x, y)  B* 0 show ?case using ccontr by auto
  next
    case (Suc i)
    then have B:"(x, y)  B*" and ASk:"(x, y)  A ^^ Suc i" by auto
    from ASk have "z. (x, z)  A  (z, y)  A ^^ i" using relpow_Suc_D2 [where ?R=A] by auto
    then obtain z where xz:"(x, z)  A" and "(z, y)  A ^^ i" by auto
    then have zy:"(z, y)  A*" using relpow_imp_rtrancl by auto
    from xz show "(x, y)  A* O (A - B) O A*"
    proof (cases "(x, z)  B")
      case False
      with xz zy show "(x, y)  A* O (A - B) O A*" by auto
    next
      case True
      then have "(x, z)  B*" by auto
      have "(x, z)  B*; (z, y)  B*  (x, y)  B*" using rtrancl_trans [of x z B] by auto
      with  (x, z)  B* (x, y)  B* have "(z, y)  B*" by auto
      with Suc (z, y)  A ^^ i have "(z, y)  A* O (A - B) O A*" by auto
      with xz have xy:"(x, y)  A O A* O (A - B) O A*" by auto
      have "A O A* O (A - B) O A*  A* O (A - B) O A*" by regexp
      from this xy show "(x, y)  A* O (A - B) O A*"
        using subsetD [where ?A="A O A* O (A - B) O A*"] by auto
    qed
  qed
qed

lemma SN_empty [simp]: "SN {}" by auto

lemma SN_on_weakening:
  assumes "SN_on R1 A"
  shows "SN_on (R1  R2) A"
proof -
  {
    assume "S. S 0  A  chain (R1  R2) S"
    then obtain S where
      S0: "S 0  A" and
      SN: "chain (R1  R2) S"
      by auto
    from SN have SN': "chain R1 S" by simp
    with S0 and assms have "False" by auto
  }
  then show ?thesis by force
qed

(* an explicit version of infinite reduction *)
definition ideriv :: "'a rel  'a rel  (nat  'a)  bool" where
  "ideriv R S as  (i. (as i, as (Suc i))  R  S)  (INFM i. (as i, as (Suc i))  R)"

lemma ideriv_mono: "R  R'  S  S'  ideriv R S as  ideriv R' S' as"
  unfolding ideriv_def INFM_nat by blast

fun
  shift :: "(nat  'a)  nat  nat  'a"
where
  "shift f j = (λ i. f (i+j))"

lemma ideriv_split:
  assumes ideriv: "ideriv R S as"
    and nideriv: "¬ ideriv (D  (R  S)) (R  S - D) as"
  shows " i. ideriv (R - D) (S - D) (shift as i)"
proof -
  have RS: "R - D  (S - D) = R  S - D" by auto
  from ideriv [unfolded ideriv_def]
  have as: " i. (as i, as (Suc i))  R  S"
    and inf: "INFM i. (as i, as (Suc i))  R" by auto
  show ?thesis
  proof (cases "INFM i. (as i, as (Suc i))  D  (R  S)")
    case True
    have "ideriv (D  (R  S)) (R  S - D) as"
      unfolding ideriv_def
      using as True  by auto
    with nideriv show ?thesis ..
  next
    case False
    from False [unfolded INFM_nat]
    obtain i where Dn: " j. i < j  (as j, as (Suc j))  D  (R  S)"
      by auto
    from Dn as have as: " j. i < j  (as j, as (Suc j))  R  S - D" by auto
    show ?thesis
    proof (rule exI [of _ "Suc i"], unfold ideriv_def RS, insert as, intro conjI, simp, unfold INFM_nat, intro allI)
      fix m
      from inf [unfolded INFM_nat] obtain j where j: "j > Suc i + m"
        and R: "(as j, as (Suc j))  R" by auto
      with as [of j] have RD: "(as j, as (Suc j))  R - D" by auto      
      show " j > m. (shift as (Suc i) j, shift as (Suc i) (Suc j))  R - D"
        by (rule exI [of _ "j - Suc i"], insert j RD, auto)
    qed
  qed
qed

lemma ideriv_SN:
  assumes SN: "SN S"
    and compat: "NS O S  S"
    and R: "R  NS  S"
  shows "¬ ideriv (S  R) (R - S) as"
proof
  assume "ideriv (S  R) (R - S) as"
  with R have steps: " i. (as i, as (Suc i))  NS  S"
    and inf: "INFM i. (as i, as (Suc i))  S  R" unfolding ideriv_def by auto
  from non_strict_ending [OF steps compat] SN
  obtain i where i: " j. j  i  (as j, as (Suc j))  NS - S" by fast
  from inf [unfolded INFM_nat] obtain j where "j > i" and "(as j, as (Suc j))  S" by auto
  with i [of j] show False by auto
qed

lemma Infm_shift: "(INFM i. P (shift f n i)) = (INFM i. P (f i))" (is "?S = ?O")
proof 
  assume ?S
  show ?O
    unfolding INFM_nat_le 
  proof
    fix m
    from ?S [unfolded INFM_nat_le]
    obtain k where k: "k  m" and p: "P (shift f n k)" by auto
    show " k  m. P (f k)"
      by (rule exI [of _ "k + n"], insert k p, auto)
  qed
next
  assume ?O
  show ?S
    unfolding INFM_nat_le 
  proof
    fix m
    from ?O [unfolded INFM_nat_le]
    obtain k where k: "k  m + n" and p: "P (f k)" by auto
    show " k  m. P (shift f n k)"
      by (rule exI [of _ "k - n"], insert k p, auto)
  qed
qed

lemma rtrancl_list_conv:
  "(s, t)  R*  
    ( ts. last (s # ts) = t  (i<length ts. ((s # ts) ! i, (s # ts) ! Suc i)  R))" (is "?l = ?r")
proof 
  assume ?r
  then obtain ts where "last (s # ts) = t  (i<length ts. ((s # ts) ! i, (s # ts) ! Suc i)  R)" ..
  then show ?l
  proof (induct ts arbitrary: s, simp)
    case (Cons u ll)
    then have "last (u # ll) = t  (i<length ll. ((u # ll) ! i, (u # ll) ! Suc i)  R)" by auto
    from Cons(1)[OF this] have rec: "(u, t)  R*" .
    from Cons have "(s, u)  R" by auto
    with rec show ?case by auto
  qed
next
  assume ?l
  from rtrancl_imp_seq [OF this]
  obtain S n where s: "S 0 = s" and t: "S n = t" and steps: " i<n. (S i, S (Suc i))  R" by auto
  let ?ts = "map (λ i. S (Suc i)) [0 ..< n]"
  show ?r
  proof (rule exI [of _ ?ts], intro conjI, 
      cases n, simp add: s [symmetric] t [symmetric], simp add: t [symmetric]) 
    show " i < length ?ts. ((s # ?ts) ! i, (s # ?ts) ! Suc i)  R" 
    proof (intro allI impI)
      fix i
      assume i: "i < length ?ts"
      then show "((s # ?ts) ! i, (s # ?ts) ! Suc i)  R"
      proof (cases i, simp add: s [symmetric] steps)
        case (Suc j)
        with i steps show ?thesis by simp
      qed
    qed
  qed
qed

lemma SN_reaches_NF:
  assumes "SN_on r {x}"
  shows "y. (x, y)  r*  y  NF r"
using assms
proof (induct rule: SN_on_induct')
  case (IH x)
  show ?case
  proof (cases "x  NF r")
    case True
    then show ?thesis by auto
  next
    case False
    then obtain y where step: "(x, y)  r" by auto
    from IH [OF this] obtain z where steps: "(y, z)  r*" and NF: "z  NF r" by auto
    show ?thesis
      by (intro exI, rule conjI [OF _ NF], insert step steps, auto)
  qed
qed

lemma SN_WCR_reaches_NF:
  assumes SN: "SN_on r {x}" 
    and WCR: "WCR_on r {x. SN_on r {x}}"
  shows "∃! y. (x, y)  r*  y  NF r"
proof -
  from SN_reaches_NF [OF SN] obtain y where steps: "(x, y)  r*" and NF: "y  NF r" by auto
  show ?thesis
  proof(rule, rule conjI [OF steps NF])
    fix z
    assume steps': "(x, z)  r*  z  NF r"
    from Newman_local [OF SN WCR] have "CR_on r {x}" by auto
    from CR_onD [OF this _ steps] steps' have "(y, z)  r" by simp
    from join_NF_imp_eq [OF this NF] steps' show "z = y" by simp
  qed
qed

definition some_NF :: "'a rel  'a  'a" where
  "some_NF r x = (SOME y. (x, y)  r*  y  NF r)"

lemma some_NF:
  assumes SN: "SN_on r {x}" 
  shows "(x, some_NF r x)  r*  some_NF r x  NF r"
  using someI_ex [OF SN_reaches_NF [OF SN]]
  unfolding some_NF_def .

lemma some_NF_WCR:
  assumes SN: "SN_on r {x}"
    and WCR: "WCR_on r {x. SN_on r {x}}"
    and steps: "(x, y)  r*"
    and NF: "y  NF r"
  shows "y = some_NF r x"
proof -
  let ?p = "λ y. (x, y)  r*  y  NF r"
  from SN_WCR_reaches_NF [OF SN WCR]
  have one: "∃! y. ?p y" .
  from steps NF have y: "?p y" ..
  from some_NF [OF SN] have some: "?p (some_NF r x)" .
  from one some y show ?thesis by auto
qed

lemma some_NF_UNF:
  assumes UNF: "UNF r"
    and steps: "(x, y)  r*"
    and NF: "y  NF r"
  shows "y = some_NF r x"
proof -
  let ?p = "λ y. (x, y)  r*  y  NF r"
  from steps NF have py: "?p y" by simp
  then have pNF: "?p (some_NF r x)" unfolding some_NF_def 
    by (rule someI)
  from py have y: "(x, y)  r!" by auto
  from pNF have nf: "(x, some_NF r x)  r!" by auto
  from UNF [unfolded UNF_on_def] y nf show ?thesis by auto
qed

definition "the_NF A a = (THE b. (a, b)  A!)"

context
  fixes A
  assumes SN: "SN A" and CR: "CR A"
begin
lemma the_NF: "(a, the_NF A a)  A!"
proof -
  obtain b where ab: "(a, b)  A!" using SN by (meson SN_imp_WN UNIV_I WN_onE)
  moreover have "(a, c)  A!  c = b" for c
    using CR and ab by (meson CR_divergence_imp_join join_NF_imp_eq normalizability_E)
  ultimately have "∃!b. (a, b)  A!" by blast
  then show ?thesis unfolding the_NF_def by (rule theI')
qed

lemma the_NF_NF: "the_NF A a  NF A"
  using the_NF by (auto simp: normalizability_def)

lemma the_NF_step:
  assumes "(a, b)  A"
  shows "the_NF A a = the_NF A b"
  using the_NF and assms
  by (meson CR SN SN_imp_WN conversionI' r_into_rtrancl semi_complete_imp_conversionIff_same_NF semi_complete_onI)

lemma the_NF_steps:
  assumes "(a, b)  A*"
  shows "the_NF A a = the_NF A b"
  using assms by (induct) (auto dest: the_NF_step)

lemma the_NF_conv:
  assumes "(a, b)  A*"
  shows "the_NF A a = the_NF A b"
  using assms
  by (meson CR WN_on_def the_NF semi_complete_imp_conversionIff_same_NF semi_complete_onI)

end


definition weak_diamond :: "'a rel  bool" ("w◇") where
  "w◇ r  (r¯ O r) - Id  (r O r¯)"

lemma weak_diamond_imp_CR:
  assumes wd: "w◇ r"
  shows "CR r"
proof (rule semi_confluence_imp_CR, rule)
  fix x y
  assume "(x, y)  r¯ O r*"
  then obtain z where step: "(z, x)  r" and steps: "(z, y)  r*" by auto
  from steps
  have " u. (x, u)  r*  (y, u)  r=" 
  proof (induct) 
    case base
    show ?case
      by (rule exI [of _ x], insert step, auto)
  next
    case (step y' y)
    from step(3) obtain u where xu: "(x, u)  r*" and y'u: "(y', u)  r=" by auto
    from y'u have "(y', u)  r  y' = u" by auto
    then show ?case
    proof
      assume y'u: "y' = u"
      with xu step(2) have xy: "(x, y)  r*" by auto
      show ?thesis 
        by (intro exI conjI, rule xy, simp)
    next
      assume "(y', u)  r"
      with step(2) have uy: "(u, y)  r¯ O r" by auto
      show ?thesis
      proof (cases "u = y")
        case True
        show ?thesis
          by (intro exI conjI, rule xu, unfold True, simp)
      next
        case False
        with uy
          wd [unfolded weak_diamond_def] obtain u' where uu': "(u, u')  r"
          and yu': "(y, u')  r" by auto
        from xu uu' have xu: "(x, u')  r*" by auto
        show ?thesis
          by (intro exI conjI, rule xu, insert yu', auto)
      qed
    qed
  qed        
  then show "(x, y)  r" by auto
qed

lemma steps_imp_not_SN_on:
  fixes t :: "'a  'b"
    and R :: "'b rel"
  assumes steps: " x. (t x, t (f x))  R"
  shows "¬ SN_on R {t x}"
proof  
  let ?U = "range t"
  assume "SN_on R {t x}"
  from SN_on_imp_on_minimal [OF this, rule_format, of ?U]
  obtain tz where tz: "tz  range t" and min: " y. (tz, y)  R  y  range t" by auto
  from tz obtain z where tz: "tz = t z" by auto
  from steps [of z] min [of "t (f z)"] show False unfolding tz by auto
qed

lemma steps_imp_not_SN:
  fixes t :: "'a  'b"
    and R :: "'b rel"
  assumes steps: " x. (t x, t (f x))  R"
  shows "¬ SN R"
proof -
  from steps_imp_not_SN_on [of t f R, OF steps]
  show ?thesis unfolding SN_def by blast
qed

lemma steps_map:
  assumes fg: "t u R . P t  Q R  (t, u)  R  P u  (f t, f u)  g R"
  and t: "P t"
  and R: "Q R"
  and S: "Q S"
  shows "((t, u)  R*  (f t, f u)  (g R)*)
     ((t, u)  R* O S O R*  (f t, f u)  (g R)* O (g S) O (g R)*)"
proof -
  {
    fix t u
    assume "(t, u)  R*" and "P t"
    then have "P u  (f t, f u)  (g R)*"
    proof (induct)
      case (step u v)
      from step(3)[OF step(4)] have Pu: "P u" and steps: "(f t, f u)  (g R)*" by auto
      from fg [OF Pu R step(2)] have Pv: "P v" and step: "(f u, f v)  g R" by auto
      with steps have "(f t, f v)  (g R)*" by auto
      with Pv show ?case by simp
    qed simp
  } note main = this
  note maint = main [OF _ t]
  from maint [of u] have one: "(t, u)  R*  (f t, f u)  (g R)*" by simp
  show ?thesis
  proof (rule conjI [OF one impI])
    assume "(t, u)  R* O S O R*"
    then obtain s v where ts: "(t, s)  R*" and sv: "(s, v)  S" and vu: "(v, u)  R*" by auto
    from maint [OF ts] have Ps: "P s" and ts: "(f t, f s)  (g R)*" by auto
    from fg [OF Ps S sv] have Pv: "P v" and sv: "(f s, f v)  g S" by auto
    from main [OF vu Pv] have vu: "(f v, f u)  (g R)*" by auto
    from ts sv vu show "(f t, f u)  (g R)* O g S O (g R)*" by auto
  qed
qed


subsection ‹Terminating part of a relation›

inductive_set
  SN_part :: "'a rel  'a set"
  for r :: "'a rel"
where
  SN_partI: "(y. (x, y)  r  y  SN_part r)  x  SN_part r"

text ‹The accessible part of a relation is the same as the terminating part
(just two names for the same definition -- modulo argument order). See
@{thm accI}.›

text ‹Characterization of @{const SN_on} via terminating part.›
lemma SN_on_SN_part_conv:
  "SN_on r A  A  SN_part r"
proof -
  {
    fix x assume "SN_on r A" and "x  A"
    then have "x  SN_part r" by (induct) (auto intro: SN_partI)
  } moreover {
    fix x assume "x  A" and "A  SN_part r"
    then have "x  SN_part r" by auto
    then have "SN_on r {x}" by (induct) (auto intro: step_reflects_SN_on)
  } ultimately show ?thesis by (force simp: SN_defs)
qed

text ‹Special case for ``full'' termination.›
lemma SN_SN_part_UNIV_conv:
  "SN r  SN_part r = UNIV"
  using SN_on_SN_part_conv [of r UNIV] by auto

lemma closed_imp_rtrancl_closed: assumes L: "L  A"
  and R: "R `` A  A"
  shows "{t | s. s  L  (s,t)  R^*}  A"
proof -
  {
    fix s t
    assume "(s,t)  R^*" and "s  L" 
    hence "t  A"
      by (induct, insert L R, auto)
  }
  thus ?thesis by auto
qed

lemma trancl_steps_relpow: assumes "a  b^+"
  shows "(x,y)  a^^n   m. m  n  (x,y)  b^^m"
proof (induct n arbitrary: y)
  case 0 thus ?case by (intro exI[of _ 0], auto)
next
  case (Suc n z)
  from Suc(2) obtain y where xy: "(x,y)  a ^^ n" and yz: "(y,z)  a" by auto
  from Suc(1)[OF xy] obtain m where m: "m  n" and xy: "(x,y)  b ^^ m" by auto
  from yz assms have "(y,z)  b^+" by auto
  from this[unfolded trancl_power] obtain k where k: "k > 0" and yz: "(y,z)  b ^^ k" by auto
  from xy yz have "(x,z)  b ^^ (m + k)" unfolding relpow_add by auto
  with k m show ?case by (intro exI[of _ "m + k"], auto)
qed

lemma relpow_image: assumes f: " s t. (s,t)  r  (f s, f t)  r'"
  shows "(s,t)  r ^^ n  (f s, f t)  r' ^^ n"
proof (induct n arbitrary: t)
  case (Suc n u)
  from Suc(2) obtain t where st: "(s,t)  r ^^ n" and tu: "(t,u)  r" by auto
  from Suc(1)[OF st] f[OF tu] show ?case by auto
qed auto

lemma relpow_refl_mono:
 assumes refl:" x. (x,x)  Rel"
 shows "m  n (a,b)  Rel ^^ m  (a,b)  Rel ^^ n"
proof (induct rule:dec_induct)
  case (step i)
  hence abi:"(a, b)  Rel ^^ i" by auto
  from refl[of b] abi relpowp_Suc_I[of i "λ x y. (x,y)  Rel"] show "(a, b)  Rel ^^ Suc i" by auto
qed

lemma SN_on_induct_acc_style [consumes 1, case_names IH]:
  assumes sn: "SN_on R {a}"
    and IH: "x. SN_on R {x}  y. (x, y)  R  P y   P x"
  shows "P a"
proof -
  from sn SN_on_conv_acc [of "R¯" a] have a: "a  termi R" by auto
  show ?thesis
  proof (rule Wellfounded.acc.induct [OF a, of P], rule IH)
    fix x
    assume "y. (y, x)  R¯  y  termi R"
    from this [folded SN_on_conv_acc]
      show "SN_on R {x}" by simp fast
  qed auto
qed

(* Lemma 2.3 in Huet: Confluent Reductions *)
lemma partially_localize_CR:
  "CR r  ( x y z. (x, y)  r  (x, z)  r*  (y, z)  join r)" 
proof
  assume "CR r"
  thus " x y z. (x, y)  r  (x, z)  r*  (y, z)  join r" by auto
next
  assume 1:" x y z. (x, y)  r  (x, z)  r*  (y, z)  join r" 
  show "CR r"
  proof
    fix a b c
    assume 2: "a  UNIV" and 3: "(a, b)  r*" and 4: "(a, c)  r*"
    then obtain n  where "(a,c)  r^^n" using rtrancl_is_UN_relpow by fast
    with 2 3 show "(b,c)  join r" 
    proof (induct n arbitrary: a b c)
      case 0 thus ?case by auto
    next
      case (Suc m)
      from Suc(4) obtain d where ad: "(a, d)  r^^m" and dc: "(d, c)  r" by auto
      from Suc(1) [OF Suc(2) Suc(3) ad] have "(b, d)  join r" .
      with 1 dc joinE joinI [of b _ r c] join_rtrancl_join show ?case by metis
    qed
  qed
qed

definition strongly_confluent_on :: "'a rel  'a set  bool"
where 
  "strongly_confluent_on r A 
    (x  A.  y z. (x, y)  r  (x, z)  r  (u. (y, u)  r*  (z, u)  r=))"

abbreviation strongly_confluent :: "'a rel  bool"
where
  "strongly_confluent r  strongly_confluent_on r UNIV"

lemma strongly_confluent_on_E11:
  "strongly_confluent_on r A  x  A  (x, y)  r  (x, z)  r 
    u. (y, u)  r*  (z, u)  r="
unfolding strongly_confluent_on_def by blast

lemma strongly_confluentI [intro]:
  "x y z. (x, y)  r  (x, z)  r  u. (y, u)  r*  (z, u)  r=  strongly_confluent r" 
unfolding strongly_confluent_on_def by auto

lemma strongly_confluent_E1n:
  assumes scr: "strongly_confluent r"
  shows "(x, y)  r=  (x, z)  r ^^ n  u. (y, u)  r*  (z, u)  r="
proof (induct n arbitrary: x y z)
  case (Suc m)
  from Suc(3) obtain w where xw: "(x, w)  r^^m" and wz: "(w, z)  r" by auto
  from Suc(1) [OF Suc(2) xw] obtain u where yu: "(y, u)  r*" and wu: "(w, u)  r=" by auto
  from strongly_confluent_on_E11 [OF scr, of w] wz yu wu show ?case 
    by (metis UnE converse_rtrancl_into_rtrancl iso_tuple_UNIV_I pair_in_Id_conv rtrancl_trans)
qed auto

(* Lemma 2.5 in Huet: Confluent Reductions *)
lemma strong_confluence_imp_CR: 
  assumes "strongly_confluent r"
  shows "CR r"
proof -
  { fix x y z
    have "(x, y)  r  (x, z)  r*  (y, z)  join r" 
      by (cases "x = y", insert strongly_confluent_E1n [OF assms], blast+) }
  then show "CR r" using partially_localize_CR by blast
qed

lemma WCR_alt_def: "WCR A  A¯ O A  A" by (auto simp: WCR_defs)

lemma NF_imp_SN_on: "a  NF R  SN_on R {a}" unfolding SN_on_def NF_def by blast

lemma Union_sym: "(s, t)  (in. (S i))  (t, s)  (in. (S i))" by auto

lemma peak_iff: "(x, y)  A¯ O B  (u. (u, x)  A  (u, y)  B)" by auto

lemma CR_NF_conv:
  assumes "CR r" and "t  NF r" and "(u, t)  r*"
  shows "(u, t)  r!"
using assms
unfolding CR_imp_conversionIff_join [OF CR r]
by (auto simp: NF_iff_no_step normalizability_def)
   (metis (mono_tags) converse_rtranclE joinE)

lemma NF_join_imp_reach:
  assumes "y  NF A" and "(x, y)  A"
  shows "(x, y)  A*"
using assms by (auto simp: join_def) (metis NF_not_suc rtrancl_converseD)

lemma conversion_O_conversion [simp]:
  "A* O A* = A*"
  by (force simp: converse_def)

lemma trans_O_iff: "trans A  A O A  A" unfolding trans_def by auto
lemma refl_O_iff: "refl A  Id  A" unfolding refl_on_def by auto

lemma relpow_Suc: "r ^^ Suc n = r O r ^^ n"
  using relpow_add[of 1 n r] by auto

lemma converse_power: fixes r :: "'a rel" shows "(r¯)^^n = (r^^n)¯"
proof (induct n)
  case (Suc n)
  show ?case unfolding relpow.simps(2)[of _ "r¯"] relpow_Suc[of _ r]
    by (simp add: Suc converse_relcomp)
qed simp

lemma conversion_mono: "A  B  A*  B*"
by (auto simp: conversion_def intro!: rtrancl_mono)

lemma conversion_conversion_idemp [simp]: "(A*)* = A*"
  by auto

lemma lower_set_imp_not_SN_on:
  assumes "s  X" "t  X. u  X. (t,u)  R" shows "¬ SN_on R {s}"
  by (meson SN_on_imp_on_minimal assms)


lemma SN_on_Image_rtrancl_iff[simp]: "SN_on R (R* `` X)  SN_on R X" (is "?l = ?r")
proof(intro iffI)
  assume "?l" show "?r" by (rule SN_on_subset2[OF _ ?l], auto)
qed (fact SN_on_Image_rtrancl)

lemma O_mono1: "R  R'  S O R  S O R'" by auto
lemma O_mono2: "R  R'  R O T  R' O T" by auto

lemma rtrancl_O_shift: "(S O R)* O S = S O (R O S)*"
  (* regexp does not work, since R is of type 'a x 'b set, not 'a rel *)
proof(intro equalityI subrelI)
  fix x y
  assume "(x,y)  (S O R)* O S"
  then obtain n where "(x,y)  (S O R)^^n O S" by blast
  then show "(x,y)  S O (R O S)*"
  proof(induct n arbitrary: y)
    case IH: (Suc n)
    then obtain z where xz: "(x,z)  (S O R)^^n O S" and zy: "(z,y)  R O S" by auto
    from IH.hyps[OF xz] zy have "(x,y)  S O (R O S)* O R O S" by auto
    then show ?case by(fold trancl_unfold_right, auto)
  qed auto
next
  fix x y
  assume "(x,y)  S O (R O S)*"
  then obtain n where "(x,y)  S O (R O S)^^n" by blast
  then show "(x,y)  (S O R)* O S"
  proof(induct n arbitrary: y)
    case IH: (Suc n)
    then obtain z where xz: "(x,z)  S O (R O S)^^n" and zy: "(z,y)  R O S" by auto
    from IH.hyps[OF xz] zy have "(x,y)  ((S O R)* O S O R) O S" by auto
    from this[folded trancl_unfold_right]
    show ?case by (rule rev_subsetD[OF _ O_mono2], auto simp: O_assoc)
  qed auto
qed

lemma O_rtrancl_O_O: "R O (S O R)* O S = (R O S)+"
  by (unfold rtrancl_O_shift trancl_unfold_left, auto)

lemma SN_on_subset_SN_terms:
  assumes SN: "SN_on R X" shows "X  {x. SN_on R {x}}"
proof(intro subsetI, unfold mem_Collect_eq)
  fix x assume x: "x  X"
  show "SN_on R {x}" by (rule SN_on_subset2[OF _ SN], insert x, auto)
qed

lemma SN_on_Un2:
  assumes "SN_on R X" and "SN_on R Y" shows "SN_on R (X  Y)"
  using assms by fast

lemma SN_on_UN:
  assumes "x. SN_on R (X x)" shows "SN_on R (x. X x)"
  using assms by fast

lemma Image_subsetI: "R  R'  R `` X  R' `` X" by auto

lemma SN_on_O_comm:
  assumes SN: "SN_on ((R :: ('a×'b) set) O (S :: ('b×'a) set)) (S `` X)"
  shows "SN_on (S O R) X"
proof
  fix seq :: "nat  'b" assume seq0: "seq 0  X" and chain: "chain (S O R) seq"
  from SN have SN: "SN_on (R O S) ((R O S)* `` S `` X)" by simp
  { fix i a
    assume ia: "(seq i,a)  S" and aSi: "(a,seq (Suc i))  R"
    have "seq i  (S O R)* `` X"
    proof (induct i)
      case 0 from seq0 show ?case by auto
    next
      case (Suc i) with chain have "seq (Suc i)  ((S O R)* O S O R) `` X" by blast
      also have "...  (S O R)* `` X" by (fold trancl_unfold_right, auto)
      finally show ?case.
    qed
    with ia have "a  ((S O R)* O S) `` X" by auto
    then have a: "a  ((R O S)*) `` S `` X" by (auto simp: rtrancl_O_shift)
    with ia aSi have False
    proof(induct "a" arbitrary: i rule: SN_on_induct[OF SN])
      case 1 show ?case by (fact a)
    next
      case IH: (2 a)
      from chain obtain b
      where *: "(seq (Suc i), b)  S" "(b, seq (Suc (Suc i)))  R" by auto
      with IH have ab: "(a,b)  R O S" by auto
      with a  (R O S)* `` S `` X have "b  ((R O S)* O R O S) `` S `` X" by auto
      then have "b  (R O S)* `` S `` X"
        by (rule rev_subsetD, intro Image_subsetI, fold trancl_unfold_right, auto)
      from IH.hyps[OF ab * this] IH.prems ab show False by auto
    qed
  }
  with chain show False by auto
qed

lemma SN_O_comm: "SN (R O S)  SN (S O R)"
  by (intro iffI; rule SN_on_O_comm[OF SN_on_subset2], auto)

lemma chain_mono: assumes "R'  R" "chain R' seq" shows "chain R seq"
  using assms by auto

context
  fixes S R
  assumes push: "S O R  R O S*"
begin

lemma rtrancl_O_push: "S* O R  R O S*"
proof-
  { fix n
    have "s t. (s,t)  S ^^ n O R  (s,t)  R O S*"
    proof(induct n)
      case (Suc n)
        then obtain u where "(s,u)  S" "(u,t)  R O S*" unfolding relpow_Suc by blast
        then have "(s,t)  S O R O S*" by auto
        also have "...  R O S* O S*" using push by blast
        also have "...  R O S*" by auto
        finally show ?case.
    qed auto
  }
  thus ?thesis by blast
qed

lemma rtrancl_U_push: "(S  R)* = R* O S*"
proof(intro equalityI subrelI)
  fix x y
  assume "(x,y)  (S  R)*"
  also have "...  (S* O R)* O S*" by regexp
  finally obtain z where xz: "(x,z)  (S* O R)*" and zy: "(z,y)  S*" by auto
  from xz have "(x,z)  R* O S*"
  proof (induct rule: rtrancl_induct)
    case (step z w)
      then have "(x,w)  R* O S* O S* O R" by auto
      also have "...  R* O S* O R" by regexp
      also have "...  R* O R O S*" using rtrancl_O_push by auto
      also have "...  R* O S*" by regexp
      finally show ?case.
  qed auto
  with zy show "(x,y)  R* O S*" by auto
qed regexp

lemma SN_on_O_push:
  assumes SN: "SN_on R X" shows "SN_on (R O S*) X"
proof
  fix seq
  have SN: "SN_on R (R* `` X)" using SN_on_Image_rtrancl[OF SN].
  moreover assume "seq (0::nat)  X"
    then have "seq 0  R* `` X" by auto
  ultimately show "chain (R O S*) seq  False"
  proof(induct "seq 0" arbitrary: seq rule: SN_on_induct)
    case IH
    then have 01: "(seq 0, seq 1)  R O S*"
          and 12: "(seq 1, seq 2)  R O S*"
          and 23: "(seq 2, seq 3)  R O S*" by (auto simp: eval_nat_numeral)
    then obtain s t
    where s: "(seq 0, s)  R" and s1: "(s, seq 1)  S*"
      and t: "(seq 1, t)  R" and t2: "(t, seq 2)  S*" by auto
    from s1 t have "(s,t)  S* O R" by auto
    with rtrancl_O_push have st: "(s,t)  R O S*" by auto
    from t2 23 have "(t, seq 3)  S* O R O S*" by auto
    also from rtrancl_O_push have "...  R O S* O S*" by blast
    finally have t3: "(t, seq 3)  R O S*" by regexp
    let ?seq = "λi. case i of 0  s | Suc 0  t | i  seq (Suc i)"
    show ?case
    proof(rule IH)
      from s show "(seq 0, ?seq 0)  R" by auto
      show "chain (R O S*) ?seq"
      proof (intro allI)
        fix i show "(?seq i, ?seq (Suc i))  R O S*"
        proof (cases i)
          case 0 with st show ?thesis by auto
        next
          case (Suc i) with t3 IH show ?thesis by (cases i, auto simp: eval_nat_numeral)
        qed
      qed
    qed
  qed
qed

lemma SN_on_Image_push:
  assumes SN: "SN_on R X" shows "SN_on R (S* `` X)"
proof-
  { fix n
    have "SN_on R ((S^^n) `` X)"
    proof(induct n)
      case 0 from SN show ?case by auto
      case (Suc n)
        from SN_on_O_push[OF this] have "SN_on (R O S*) ((S ^^ n) `` X)".
        from SN_on_Image[OF this]
        have "SN_on (R O S*) ((R O S*) `` (S ^^ n) `` X)".
        then have "SN_on R ((R O S*) `` (S ^^ n) `` X)" by (rule SN_on_mono, auto)
        from SN_on_subset2[OF Image_mono[OF push subset_refl] this]
        have "SN_on R (R `` (S ^^ Suc n) `` X)" by (auto simp: relcomp_Image)
        then show ?case by fast
    qed
  }
  then show ?thesis by fast
qed

end

lemma not_SN_onI[intro]: "f 0  X  chain R f  ¬ SN_on R X"
  by (unfold SN_on_def not_not, intro exI conjI)
lemma shift_comp[simp]: "shift (f  seq) n = f  (shift seq n)" by auto

lemma Id_on_union: "Id_on (A  B) = Id_on A  Id_on B" unfolding Id_on_def by auto

lemma relpow_union_cases: "(a,d)  (A  B)^^n  (a,d)  B^^n  ( b c k m. (a,b)  B^^k  (b,c)  A  (c,d)  (A  B)^^m  n = Suc (k + m))"
proof (induct n arbitrary: a d)
  case (Suc n a e)
  let ?AB = "A  B"
  from Suc(2) obtain b where ab: "(a,b)  ?AB" and be: "(b,e)  ?AB^^n" by (rule relpow_Suc_E2)
  from ab
  show ?case
  proof
    assume "(a,b)  A"
    show ?thesis
    proof (rule disjI2, intro exI conjI)
      show "Suc n = Suc (0 + n)" by simp
      show "(a,b)  A" by fact
    qed (insert be, auto)
  next
    assume ab: "(a,b)  B"
    from Suc(1)[OF be]
    show ?thesis
    proof
      assume "(b,e)  B ^^ n"
      with ab show ?thesis
        by (intro disjI1 relpow_Suc_I2)
    next
      assume " c d k m. (b, c)  B ^^ k  (c, d)  A  (d, e)  ?AB ^^ m  n = Suc (k + m)"
      then obtain c d k m where "(b, c)  B ^^ k" and *: "(c, d)  A" "(d, e)  ?AB ^^ m" "n = Suc (k + m)" by blast
      with ab have ac: "(a,c)  B ^^ (Suc k)" by (intro relpow_Suc_I2)
      show ?thesis
        by (intro disjI2 exI conjI, rule ac, (rule *)+, simp add: *)
    qed
  qed
qed simp

lemma trans_refl_imp_rtrancl_id:
  assumes "trans r" "refl r"
  shows "r* = r"
proof
  show "r*  r"
  proof
    fix x y
    assume "(x,y)  r*"
    thus "(x,y)  r"
      by (induct, insert assms, unfold refl_on_def trans_def, blast+)
  qed
qed regexp

lemma trans_refl_imp_O_id:
  assumes "trans r" "refl r"
  shows "r O r = r"
proof(intro equalityI)
  show "r O r  r" by(fact trans_O_subset[OF assms(1)])
  have "r  r O Id" by auto
  moreover have "Id  r" by(fact assms(2)[unfolded refl_O_iff])
  ultimately show "r  r O r" by auto
qed

lemma relcomp3_I:
  assumes "(t, u)  A" and "(s, t)  B" and "(u, v)  B"
  shows "(s, v)  B O A O B"
  using assms by blast

lemma relcomp3_transI:
  assumes "trans B" and "(t, u)  B O A O B" and "(s, t)  B" and "(u, v)  B"
  shows "(s, v)  B O A O B"
using assms by (auto simp: trans_def intro: relcomp3_I)

lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp
  converse_converse converse_Id

lemma qc_SN_relto_iff:
  assumes "r O s  s O (s  r)*"
  shows "SN (r* O s O r*) = SN s"
proof -
  from converse_mono [THEN iffD2 , OF assms]
  have *: "s¯ O r¯  (s¯  r¯)* O s¯" unfolding converse_inward .
  have "(r* O s O r*)¯ = (r¯)* O s¯ O (r¯)*"
    by (simp only: converse_relcomp O_assoc rtrancl_converse)
  with qc_wf_relto_iff [OF *]
  show ?thesis by (simp add: SN_iff_wf)
qed

lemma conversion_empty [simp]: "conversion {} = Id"
  by (auto simp: conversion_def)

lemma symcl_idemp [simp]: "(r) = r" by auto

end