summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Fri, 17 Jan 2014 10:02:50 +0100 | |

changeset 55027 | a74ea6d75571 |

parent 55026 | 258fa7b5a621 |

child 55028 | 00e849f5b397 |

folded 'Wellfounded_More_FP' into 'Wellfounded'

--- a/src/HOL/Cardinals/Order_Union.thy Fri Jan 17 10:02:49 2014 +0100 +++ b/src/HOL/Cardinals/Order_Union.thy Fri Jan 17 10:02:50 2014 +0100 @@ -7,7 +7,7 @@ header {* Order Union *} theory Order_Union -imports Wellfounded_More_FP +imports Order_Relation begin definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) where

--- a/src/HOL/Cardinals/README.txt Fri Jan 17 10:02:49 2014 +0100 +++ b/src/HOL/Cardinals/README.txt Fri Jan 17 10:02:50 2014 +0100 @@ -188,7 +188,7 @@ Should we define all constants from "wo_rel" in "rel" instead, so that their outside definition not be conditional in "wo_rel r"? -Theory Wellfounded_More (and Wellfounded_More_FP): +Theory Wellfounded_More: Recall the lemmas "wfrec" and "wf_induct". Theory Wellorder_Embedding (and Wellorder_Embedding_FP):

--- a/src/HOL/Cardinals/Wellfounded_More.thy Fri Jan 17 10:02:49 2014 +0100 +++ b/src/HOL/Cardinals/Wellfounded_More.thy Fri Jan 17 10:02:50 2014 +0100 @@ -8,7 +8,7 @@ header {* More on Well-Founded Relations *} theory Wellfounded_More -imports Wellfounded_More_FP Order_Relation_More +imports Wellfounded Order_Relation_More begin

--- a/src/HOL/Cardinals/Wellfounded_More_FP.thy Fri Jan 17 10:02:49 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,194 +0,0 @@ -(* Title: HOL/Cardinals/Wellfounded_More_FP.thy - Author: Andrei Popescu, TU Muenchen - Copyright 2012 - -More on well-founded relations (FP). -*) - -header {* More on Well-Founded Relations (FP) *} - -theory Wellfounded_More_FP -imports Wfrec Order_Relation -begin - - -text {* 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 \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> '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 "\<And> y. (y,x) : r \<Longrightarrow> (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 - - - -subsection {* 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 = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))" -proof- - obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> 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 *: "\<forall>a. wf(R a)" - have "wf r" - proof(unfold wf_def, clarify) - fix phi a - assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a" - obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast - with * have "wf (R a)" by auto - hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)" - unfolding wf_def by blast - moreover - have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b" - proof(auto simp add: chi_def R_def) - fix b - assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c" - hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c" - using assms trans_def[of r] by blast - thus "phi b" using ** by blast - qed - ultimately have "\<forall>b. chi b" by (rule mp) - with ** chi_def show "phi a" by blast - qed - } - ultimately show ?thesis using R_def by blast -qed - - -text {* 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 = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))" -proof- - let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)" - have "wf r = (\<forall>A. ?phi A)" - by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast) - (rule wfI_min, fast) - (* *) - also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)" - proof - assume "\<forall>A. ?phi A" - thus "\<forall>B \<le> Field r. ?phi B" by simp - next - assume *: "\<forall>B \<le> Field r. ?phi B" - show "\<forall>A. ?phi A" - proof(clarify) - fix A::"'a set" assume **: "A \<noteq> {}" - obtain B where B_def: "B = A Int (Field r)" by blast - show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r" - proof(cases "B = {}") - assume Case1: "B = {}" - obtain a where 1: "a \<in> A \<and> a \<notin> Field r" - using ** Case1 unfolding B_def by blast - hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast - thus ?thesis using 1 by blast - next - assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast - obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)" - using Case2 1 * by blast - have "\<forall>a' \<in> A. (a',a) \<notin> r" - proof(clarify) - fix a' assume "a' \<in> A" and **: "(a',a) \<in> r" - hence "a' \<in> B" unfolding B_def Field_def by blast - thus False using 2 ** by blast - qed - thus ?thesis using 2 unfolding B_def by blast - qed - qed - qed - finally show ?thesis by blast -qed - -subsection {* Characterizations of well-founded-ness *} - -text {* 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) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" -proof(cases "r \<le> Id") - assume Case1: "r \<le> Id" - hence temp: "r - Id = {}" by blast - hence "wf(r - Id)" by (simp add: temp) - moreover - {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}" - obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI - unfolding order_on_defs using Case1 Total_subset_Id by auto - hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast - hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast - } - ultimately show ?thesis by blast -next - assume Case2: "\<not> r \<le> Id" - hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI - unfolding order_on_defs by blast - show ?thesis - proof - assume *: "wf(r - Id)" - show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" - proof(clarify) - fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}" - hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" - using 1 * unfolding wf_eq_minimal2 by simp - moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)" - using Linear_order_in_diff_Id[of r] ** LI by blast - ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast - qed - next - assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" - show "wf(r - Id)" - proof(unfold wf_eq_minimal2, clarify) - fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}" - hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" - using 1 * by simp - moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)" - using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast - ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast - qed - qed -qed - -(*3*)corollary Linear_order_Well_order_iff: -assumes "Linear_order r" -shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" -using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast - -end

--- a/src/HOL/Cardinals/Wellorder_Relation_FP.thy Fri Jan 17 10:02:49 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Relation_FP.thy Fri Jan 17 10:02:50 2014 +0100 @@ -8,7 +8,7 @@ header {* Well-Order Relations (FP) *} theory Wellorder_Relation_FP -imports Wellfounded_More_FP +imports Order_Relation begin

--- a/src/HOL/Order_Relation.thy Fri Jan 17 10:02:49 2014 +0100 +++ b/src/HOL/Order_Relation.thy Fri Jan 17 10:02:50 2014 +0100 @@ -6,7 +6,7 @@ header {* Orders as Relations *} theory Order_Relation -imports Wellfounded +imports Wfrec begin subsection{* Orders on a set *} @@ -303,4 +303,183 @@ order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast qed + +subsection {* Variations on Well-Founded Relations *} + +text {* +This subsection contains some variations of the results from @{theory Wellfounded}: +\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} +*} + + +subsubsection {* Well-founded recursion via genuine fixpoints *} + +lemma wfrec_fixpoint: +fixes r :: "('a * 'a) set" and + H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> '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 "\<And> y. (y,x) : r \<Longrightarrow> (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 + + +subsubsection {* Characterizations of well-foundedness *} + +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. *} + +lemma trans_wf_iff: +assumes "trans r" +shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))" +proof- + obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> 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 *: "\<forall>a. wf(R a)" + have "wf r" + proof(unfold wf_def, clarify) + fix phi a + assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a" + obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast + with * have "wf (R a)" by auto + hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)" + unfolding wf_def by blast + moreover + have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b" + proof(auto simp add: chi_def R_def) + fix b + assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c" + hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c" + using assms trans_def[of r] by blast + thus "phi b" using ** by blast + qed + ultimately have "\<forall>b. chi b" by (rule mp) + with ** chi_def show "phi a" by blast + qed + } + ultimately show ?thesis using R_def by blast +qed + +text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded, +allowing one to assume the set included in the field. *} + +lemma wf_eq_minimal2: +"wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))" +proof- + let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)" + have "wf r = (\<forall>A. ?phi A)" + by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast) + (rule wfI_min, fast) + (* *) + also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)" + proof + assume "\<forall>A. ?phi A" + thus "\<forall>B \<le> Field r. ?phi B" by simp + next + assume *: "\<forall>B \<le> Field r. ?phi B" + show "\<forall>A. ?phi A" + proof(clarify) + fix A::"'a set" assume **: "A \<noteq> {}" + obtain B where B_def: "B = A Int (Field r)" by blast + show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r" + proof(cases "B = {}") + assume Case1: "B = {}" + obtain a where 1: "a \<in> A \<and> a \<notin> Field r" + using ** Case1 unfolding B_def by blast + hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast + thus ?thesis using 1 by blast + next + assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast + obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)" + using Case2 1 * by blast + have "\<forall>a' \<in> A. (a',a) \<notin> r" + proof(clarify) + fix a' assume "a' \<in> A" and **: "(a',a) \<in> r" + hence "a' \<in> B" unfolding B_def Field_def by blast + thus False using 2 ** by blast + qed + thus ?thesis using 2 unfolding B_def by blast + qed + qed + qed + finally show ?thesis by blast +qed + + +subsubsection {* Characterizations of well-foundedness *} + +text {* 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-foundedness of the strict version of the relation. *} + +lemma Linear_order_wf_diff_Id: +assumes LI: "Linear_order r" +shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" +proof(cases "r \<le> Id") + assume Case1: "r \<le> Id" + hence temp: "r - Id = {}" by blast + hence "wf(r - Id)" by (simp add: temp) + moreover + {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}" + obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI + unfolding order_on_defs using Case1 Total_subset_Id by auto + hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast + hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast + } + ultimately show ?thesis by blast +next + assume Case2: "\<not> r \<le> Id" + hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI + unfolding order_on_defs by blast + show ?thesis + proof + assume *: "wf(r - Id)" + show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" + proof(clarify) + fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}" + hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" + using 1 * unfolding wf_eq_minimal2 by simp + moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)" + using Linear_order_in_diff_Id[of r] ** LI by blast + ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast + qed + next + assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" + show "wf(r - Id)" + proof(unfold wf_eq_minimal2, clarify) + fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}" + hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" + using 1 * by simp + moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)" + using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast + ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast + qed + qed +qed + +corollary Linear_order_Well_order_iff: +assumes "Linear_order r" +shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" +using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast + end