# Theory Wellfounded2

Up to index of Isabelle/HOL/Free-Groups

theory Wellfounded2
imports Order_Relation2 Wfrec
header {* More on well-founded relations *}(* author: Andrei Popescu *)theory Wellfounded2imports Wellfounded Order_Relation2 "~~/src/HOL/Library/Wfrec"begintext {* This section contains some variations of results in the theory @{text "Wellfounded.thy"}:\begin{itemize} \item means for slightly more direct definitions by well-founded recursion;\item variations of well-founded induction; \item means for proving a linear order to be a well-order. \end{itemize} *}subsection {* Well-founded recursion via genuine fixpoints *}(*2*)lemma wfrec_fixpoint:fixes r :: "('a * 'a) set" and       H :: "('a => 'b) => 'a => 'b" assumes WF: "wf r" and ADM: "adm_wf r H"shows "wfrec r H = H (wfrec r H)"proof(rule ext)  fix x  have "wfrec r H x = H (cut (wfrec r H) r x) x"   using wfrec[of r H] WF by simp  also   {have "!! y. (y,x) : r ==> (cut (wfrec r H) r x) y = (wfrec r H) y"   by (auto simp add: cut_apply)   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"   using ADM adm_wf_def[of r H] by auto  }  finally show "wfrec r H x = H (wfrec r H) x" .qed (*2*)lemma adm_wf_unique_fixpoint:fixes r :: "('a * 'a) set" and       H :: "('a => 'b) => 'a => 'b" and       f :: "'a => 'b" and g :: "'a => 'b"assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g"shows "f = g"proof-  {fix x    have "f x = g x"   proof(rule wf_induct[of r "(λx. f x = g x)"],          auto simp add: WF)     fix x assume "∀y. (y, x) ∈ r --> f y = g y"     hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto     thus "f x = g x" using fFP and gFP by simp   qed  }  thus ?thesis by (simp add: ext)qed(*2*)lemma wfrec_unique_fixpoint:fixes r :: "('a * 'a) set" and       H :: "('a => 'b) => 'a => 'b" and       f :: "'a => 'b"assumes WF: "wf r" and ADM: "adm_wf r H" and         fp: "f = H f"shows "f = wfrec r H"proof-  have "H (wfrec r H) = wfrec r H"   using assms wfrec_fixpoint[of r H] by simp   thus ?thesis   using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simpqedsubsection {* Characterizations of well-founded-ness *}text {* A transitive relation is well-founded iff it is locally" well-founded, i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}(*3*)lemma trans_wf_iff:assumes "trans r" shows "wf r = (∀a. wf(r Int (r^-1{a} × r^-1{a})))"proof-  obtain R where R_def: "R = (λ a. r Int (r^-1{a} × r^-1{a}))" by blast  {assume *: "wf r"   {fix a     have "wf(R a)"     using * R_def wf_subset[of r "R a"] by auto   }  }  (*  *)  moreover   {assume *: "∀a. wf(R a)"   have "wf r"    proof(unfold wf_def, clarify)     fix phi a      assume **: "∀a. (∀b. (b,a) ∈ r --> phi b) --> phi a"     obtain chi where chi_def: "chi = (λb. (b,a) ∈ r --> phi b)" by blast     with * have "wf (R a)" by auto     hence "(∀b. (∀c. (c,b) ∈ R a --> chi c) --> chi b) --> (∀b. chi b)"     unfolding wf_def by blast     moreover      have "∀b. (∀c. (c,b) ∈ R a --> chi c) --> chi b"      proof(auto simp add: chi_def R_def)       fix b        assume 1: "(b,a) ∈ r" and 2: "∀c. (c, b) ∈ r ∧ (c, a) ∈ r --> phi c"       hence "∀c. (c, b) ∈ r --> phi c"       using assms trans_def[of r] by blast        thus "phi b" using ** by blast     qed     ultimately have  "∀b. chi b" by (rule mp)         with ** chi_def show "phi a" by blast   qed  }  ultimately show ?thesis using R_def by blastqedtext {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded, allowing one to assume the set included in the field.  *}(*2*)lemma wf_eq_minimal2: "wf r = (∀A. A <= Field r ∧ A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. ¬ (a',a) ∈ r))"proof-  let ?phi = "λ A. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. ¬ (a',a) ∈ r)"  have "wf r = (∀A. ?phi A)"  proof(unfold wf_eq_minimal, auto)    fix A c assume *: "∀A. (∃c. c ∈ A) --> (∃a∈A. ∀a'. (a', a) ∈ r --> a' ∉ A)" and                   **: "∀a∈A. ∃a'∈A. (a', a) ∈ r" and                  ***: "c ∈ A"    obtain a where "a ∈ A ∧ (∀a'. (a', a) ∈ r --> a' ∉ A)"     using * *** by auto    with ** show False by blast  next    fix A::"'a set" and c     assume *: "∀A. A ≠ {} --> (∃a∈A. ∀a'∈A. (a', a) ∉ r)" and            **: "c ∈ A"    obtain a where "a ∈ A ∧ (∀a'∈A. (a', a) ∉ r)" using * ** by blast    thus "∃a∈A. ∀a'. (a', a) ∈ r --> a' ∉ A" by blast  qed  (* Why did this not go directly by blast?  *)  (*  *)     also have "(∀A. ?phi A) = (∀B ≤ Field r. ?phi B)"  proof    assume "∀A. ?phi A"     thus "∀B ≤ Field r. ?phi B" by simp  next    assume *: "∀B ≤ Field r. ?phi B"    show "∀A. ?phi A"    proof(clarify)      fix A::"'a set" assume **: "A ≠ {}"        obtain B where B_def: "B = A Int (Field r)" by blast      show "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r"       proof(cases "B = {}")        assume Case1: "B = {}"        obtain a where 1: "a ∈ A ∧ a ∉ Field r" using ** Case1 B_def by auto        hence "∀a' ∈ A. (a',a) ∉ r" using 1 unfolding Field_def by blast        thus ?thesis using 1 by auto       next        assume Case2: "B ≠ {}" have 1: "B ≤ Field r" using B_def by auto        obtain a where 2: "a ∈ B ∧ (∀a' ∈ B. (a',a) ∉ r)"         using Case2 1 * by blast        have "∀a' ∈ A. (a',a) ∉ r"        proof(clarify)          fix a' assume "a' ∈ A" and **: "(a',a) ∈ r"          hence "a' ∈ B" using B_def Field_def by fastforce           thus False using 2 ** by auto        qed        thus ?thesis using 2 B_def by auto      qed    qed  qed  finally show ?thesis by blastqedtext {* The next lemma and its corollary enable one to prove that a linear order is a well-order in a way which is more standard than via well-founded-ness of the strict version of the relation.  *}(*3*)lemma Linear_order_wf_diff_Id: assumes LI: "Linear_order r"shows "wf(r - Id) = (∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r))"proof(cases "r ≤ Id")  assume Case1: "r ≤ Id"   hence temp: "r - Id = {}" by blast   hence "wf(r - Id)" by (auto simp add: temp)   (* did not work with "using temp"!  *)  moreover   {fix A assume *: "A ≤ Field r" and **: "A ≠ {}"   obtain a where 1: "r = {} ∨ r = {(a,a)}" using LI    unfolding order_on_defs using Case1 rel.Total_subset_Id by blast   hence "A = {a} ∧ r = {(a,a)}" using * ** unfolding Field_def by blast   hence "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r" using 1 by auto  }  ultimately show ?thesis by blastnext  assume Case2: "¬ r ≤ Id"  hence 1: "Field r = Field(r - Id)" using rel.Total_Id_Field LI   unfolding order_on_defs by blast    show ?thesis   proof    assume *: "wf(r - Id)"    show "∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r)"     proof(clarify)      fix A assume **: "A ≤ Field r" and ***: "A ≠ {}"      hence "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id"       using 1 * unfolding wf_eq_minimal2 by auto      moreover have "∀a ∈ A. ∀a' ∈ A. ((a,a') ∈ r) = ((a',a) ∉ r - Id)"         using rel.Linear_order_in_diff_Id[of r] ** LI by blast      ultimately show "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r" by blast    qed  next     assume *: "∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r)"    show "wf(r - Id)"    proof(unfold wf_eq_minimal2, clarify)      fix A assume **: "A ≤ Field(r - Id)" and ***: "A ≠ {}"      hence "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r"       using 1 * by auto      moreover have "∀a ∈ A. ∀a' ∈ A. ((a,a') ∈ r) = ((a',a) ∉ r - Id)"         using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast      ultimately show "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id" by blast    qed  qed qed(*3*)corollary Linear_order_Well_order_iff: assumes LI: "Linear_order r"shows "Well_order r = (∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r))"using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by autoend