Theory Abstract_Rewriting
section ‹Abstract Rewrite Systems›
theory Abstract_Rewriting
imports
"HOL-Library.Infinite_Set"
"Regular-Sets.Regexp_Method"
Seq
begin
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)
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
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
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
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 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
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
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 (