(* 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 (