(* 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 ⟷ (∀a∈A. ∀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 ⟷ (∀a∈A. ∀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 ⟷ (∀a∈A. ∀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 ⟷ (∀a∈A. ∃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 "∀a∈A. (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 ⟶ (∃z∈Q. ∀y. (z, y) ∈ A ⟶ y ∉ Q)" proof (rule ccontr) assume "¬ (∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ A ⟶ y ∉ Q))" then obtain Q x where "x ∈ Q" and "∀z∈Q. ∃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 ⟶ (∃z∈Q. ∀y. (z, y) ∈ r ⟶ y ∉ Q)" proof (rule ccontr) assume "¬(∀Q. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ r ⟶ y ∉ Q))" then obtain Q where "x ∈ Q" and "∀z∈Q. ∃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 ⟶ (∃z∈Q. ∀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 "∀x∈A. 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 "∀a∈A. ∃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 ∧ (∀c∈Q. ∃b. (c, b) ∈ r ∧ b ∈ Q)" by (rule exI [of _ "?Q"]) then have "¬ (∀Q. a ∈ Q ⟶ (∃c∈Q. ∀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) ∈ (⋃r∈I. 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 ⟶ (∃z∈Q. ∀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. ∀i≥j. (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: "i≤f 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) ∈ (⋃i≤n. (S i)⇧^{↔}) ⟷ (t, s) ∈ (⋃i≤n. (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