# HG changeset patch # User wenzelm # Date 1469998578 -7200 # Node ID c0cbfd2b5a45f68a1183f6ce3bdcd63e89c897a7 # Parent aee0d92995b69f307d1b7b6087b3ac639f1f6955 misc tuning and modernization; diff -r aee0d92995b6 -r c0cbfd2b5a45 src/HOL/Order_Relation.thy --- a/src/HOL/Order_Relation.thy Sun Jul 31 19:09:21 2016 +0200 +++ b/src/HOL/Order_Relation.thy Sun Jul 31 22:56:18 2016 +0200 @@ -9,7 +9,7 @@ imports Wfrec begin -subsection\Orders on a set\ +subsection \Orders on a set\ definition "preorder_on A r \ refl_on A r \ trans r" @@ -27,51 +27,48 @@ lemma preorder_on_empty[simp]: "preorder_on {} {}" -by(simp add:preorder_on_def trans_def) + by (simp add: preorder_on_def trans_def) lemma partial_order_on_empty[simp]: "partial_order_on {} {}" -by(simp add:partial_order_on_def) + by (simp add: partial_order_on_def) lemma lnear_order_on_empty[simp]: "linear_order_on {} {}" -by(simp add:linear_order_on_def) + by (simp add: linear_order_on_def) lemma well_order_on_empty[simp]: "well_order_on {} {}" -by(simp add:well_order_on_def) + by (simp add: well_order_on_def) -lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r" -by (simp add:preorder_on_def) +lemma preorder_on_converse[simp]: "preorder_on A (r\) = preorder_on A r" + by (simp add: preorder_on_def) -lemma partial_order_on_converse[simp]: - "partial_order_on A (r^-1) = partial_order_on A r" -by (simp add: partial_order_on_def) +lemma partial_order_on_converse[simp]: "partial_order_on A (r\) = partial_order_on A r" + by (simp add: partial_order_on_def) -lemma linear_order_on_converse[simp]: - "linear_order_on A (r^-1) = linear_order_on A r" -by (simp add: linear_order_on_def) +lemma linear_order_on_converse[simp]: "linear_order_on A (r\) = linear_order_on A r" + by (simp add: linear_order_on_def) -lemma strict_linear_order_on_diff_Id: - "linear_order_on A r \ strict_linear_order_on A (r-Id)" -by(simp add: order_on_defs trans_diff_Id) +lemma strict_linear_order_on_diff_Id: "linear_order_on A r \ strict_linear_order_on A (r - Id)" + by (simp add: order_on_defs trans_diff_Id) lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}" -unfolding order_on_defs by simp + by (simp add: order_on_defs) lemma linear_order_on_acyclic: assumes "linear_order_on A r" shows "acyclic (r - Id)" -using strict_linear_order_on_diff_Id[OF assms] -by(auto simp add: acyclic_irrefl strict_linear_order_on_def) + using strict_linear_order_on_diff_Id[OF assms] + by (auto simp add: acyclic_irrefl strict_linear_order_on_def) lemma linear_order_on_well_order_on: assumes "finite r" shows "linear_order_on A r \ well_order_on A r" -unfolding well_order_on_def -using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast + unfolding well_order_on_def + using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast -subsection\Orders on the field\ +subsection \Orders on the field\ abbreviation "Refl r \ refl_on (Field r) r" @@ -87,50 +84,57 @@ lemma subset_Image_Image_iff: - "\ Preorder r; A \ Field r; B \ Field r\ \ - r `` A \ r `` B \ (\a\A.\b\B. (b,a):r)" -unfolding preorder_on_def refl_on_def Image_def -apply (simp add: subset_eq) -unfolding trans_def by fast + "Preorder r \ A \ Field r \ B \ Field r \ + r `` A \ r `` B \ (\a\A.\b\B. (b, a) \ r)" + apply (simp add: preorder_on_def refl_on_def Image_def subset_eq) + apply (simp only: trans_def) + apply fast + done lemma subset_Image1_Image1_iff: - "\ Preorder r; a : Field r; b : Field r\ \ r `` {a} \ r `` {b} \ (b,a):r" -by(simp add:subset_Image_Image_iff) + "Preorder r \ a \ Field r \ b \ Field r \ r `` {a} \ r `` {b} \ (b, a) \ r" + by (simp add: subset_Image_Image_iff) lemma Refl_antisym_eq_Image1_Image1_iff: - assumes r: "Refl r" and as: "antisym r" and abf: "a \ Field r" "b \ Field r" + assumes "Refl r" + and as: "antisym r" + and abf: "a \ Field r" "b \ Field r" shows "r `` {a} = r `` {b} \ a = b" + (is "?lhs \ ?rhs") proof - assume "r `` {a} = r `` {b}" - hence e: "\x. (a, x) \ r \ (b, x) \ r" by (simp add: set_eq_iff) - have "(a, a) \ r" "(b, b) \ r" using r abf by (simp_all add: refl_on_def) - hence "(a, b) \ r" "(b, a) \ r" using e[of a] e[of b] by simp_all - thus "a = b" using as[unfolded antisym_def] by blast -qed fast + assume ?lhs + then have *: "\x. (a, x) \ r \ (b, x) \ r" + by (simp add: set_eq_iff) + have "(a, a) \ r" "(b, b) \ r" using \Refl r\ abf by (simp_all add: refl_on_def) + then have "(a, b) \ r" "(b, a) \ r" using *[of a] *[of b] by simp_all + then show ?rhs + using \antisym r\[unfolded antisym_def] by blast +next + assume ?rhs + then show ?lhs by fast +qed lemma Partial_order_eq_Image1_Image1_iff: - "\Partial_order r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" -by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff) + "Partial_order r \ a \ Field r \ b \ Field r \ r `` {a} = r `` {b} \ a = b" + by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff) lemma Total_Id_Field: -assumes TOT: "Total r" and NID: "\ (r <= Id)" -shows "Field r = Field(r - Id)" -using mono_Field[of "r - Id" r] Diff_subset[of r Id] -proof(auto) - have "r \ {}" using NID by fast - then obtain b and c where "b \ c \ (b,c) \ r" using NID by auto - hence 1: "b \ c \ {b,c} \ Field r" by (auto simp: Field_def) - + assumes "Total r" + and not_Id: "\ r \ Id" + shows "Field r = Field (r - Id)" + using mono_Field[of "r - Id" r] Diff_subset[of r Id] +proof auto fix a assume *: "a \ Field r" - obtain d where 2: "d \ Field r" and 3: "d \ a" - using * 1 by auto - hence "(a,d) \ r \ (d,a) \ r" using * TOT - by (simp add: total_on_def) - thus "a \ Field(r - Id)" using 3 unfolding Field_def by blast + from not_Id have "r \ {}" by fast + with not_Id obtain b and c where "b \ c \ (b,c) \ r" by auto + then have "b \ c \ {b, c} \ Field r" by (auto simp: Field_def) + with * obtain d where "d \ Field r" "d \ a" by auto + with * \Total r\ have "(a, d) \ r \ (d, a) \ r" by (simp add: total_on_def) + with \d \ a\ show "a \ Field (r - Id)" unfolding Field_def by blast qed -subsection\Orders on a type\ +subsection \Orders on a type\ abbreviation "strict_linear_order \ strict_linear_order_on UNIV" @@ -141,297 +145,303 @@ subsection \Order-like relations\ -text\In this subsection, we develop basic concepts and results pertaining -to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or -total relations. We also further define upper and lower bounds operators.\ +text \ + In this subsection, we develop basic concepts and results pertaining + to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or + total relations. We also further define upper and lower bounds operators. +\ subsubsection \Auxiliaries\ -lemma refl_on_domain: -"\refl_on A r; (a,b) : r\ \ a \ A \ b \ A" -by(auto simp add: refl_on_def) +lemma refl_on_domain: "refl_on A r \ (a, b) \ r \ a \ A \ b \ A" + by (auto simp add: refl_on_def) -corollary well_order_on_domain: -"\well_order_on A r; (a,b) \ r\ \ a \ A \ b \ A" -by (auto simp add: refl_on_domain order_on_defs) +corollary well_order_on_domain: "well_order_on A r \ (a, b) \ r \ a \ A \ b \ A" + by (auto simp add: refl_on_domain order_on_defs) -lemma well_order_on_Field: -"well_order_on A r \ A = Field r" -by(auto simp add: refl_on_def Field_def order_on_defs) +lemma well_order_on_Field: "well_order_on A r \ A = Field r" + by (auto simp add: refl_on_def Field_def order_on_defs) -lemma well_order_on_Well_order: -"well_order_on A r \ A = Field r \ Well_order r" -using well_order_on_Field by auto +lemma well_order_on_Well_order: "well_order_on A r \ A = Field r \ Well_order r" + using well_order_on_Field [of A] by auto lemma Total_subset_Id: -assumes TOT: "Total r" and SUB: "r \ Id" -shows "r = {} \ (\a. r = {(a,a)})" -proof- - {assume "r \ {}" - then obtain a b where 1: "(a,b) \ r" by fast - hence "a = b" using SUB by blast - hence 2: "(a,a) \ r" using 1 by simp - {fix c d assume "(c,d) \ r" - hence "{a,c,d} \ Field r" using 1 unfolding Field_def by blast - hence "((a,c) \ r \ (c,a) \ r \ a = c) \ - ((a,d) \ r \ (d,a) \ r \ a = d)" - using TOT unfolding total_on_def by blast - hence "a = c \ a = d" using SUB by blast - } - hence "r \ {(a,a)}" by auto - with 2 have "\a. r = {(a,a)}" by blast - } - thus ?thesis by blast + assumes "Total r" + and "r \ Id" + shows "r = {} \ (\a. r = {(a, a)})" +proof - + have "\a. r = {(a, a)}" if "r \ {}" + proof - + from that obtain a b where ab: "(a, b) \ r" by fast + with \r \ Id\ have "a = b" by blast + with ab have aa: "(a, a) \ r" by simp + have "a = c \ a = d" if "(c, d) \ r" for c d + proof - + from that have "{a, c, d} \ Field r" + using ab unfolding Field_def by blast + then have "((a, c) \ r \ (c, a) \ r \ a = c) \ ((a, d) \ r \ (d, a) \ r \ a = d)" + using \Total r\ unfolding total_on_def by blast + with \r \ Id\ show ?thesis by blast + qed + then have "r \ {(a, a)}" by auto + with aa show ?thesis by blast + qed + then show ?thesis by blast qed lemma Linear_order_in_diff_Id: -assumes LI: "Linear_order r" and - IN1: "a \ Field r" and IN2: "b \ Field r" -shows "((a,b) \ r) = ((b,a) \ r - Id)" -using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force + assumes "Linear_order r" + and "a \ Field r" + and "b \ Field r" + shows "(a, b) \ r \ (b, a) \ r - Id" + using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force subsubsection \The upper and lower bounds operators\ -text\Here we define upper (``above") and lower (``below") bounds operators. -We think of \r\ as a {\em non-strict} relation. The suffix ``S" -at the names of some operators indicates that the bounds are strict -- e.g., -\underS a\ is the set of all strict lower bounds of \a\ (w.r.t. \r\). -Capitalization of the first letter in the name reminds that the operator acts on sets, rather -than on individual elements.\ +text \ + Here we define upper (``above") and lower (``below") bounds operators. We + think of \r\ as a \<^emph>\non-strict\ relation. The suffix \S\ at the names of + some operators indicates that the bounds are strict -- e.g., \underS a\ is + the set of all strict lower bounds of \a\ (w.r.t. \r\). Capitalization of + the first letter in the name reminds that the operator acts on sets, rather + than on individual elements. +\ -definition under::"'a rel \ 'a \ 'a set" -where "under r a \ {b. (b,a) \ r}" +definition under :: "'a rel \ 'a \ 'a set" + where "under r a \ {b. (b, a) \ r}" -definition underS::"'a rel \ 'a \ 'a set" -where "underS r a \ {b. b \ a \ (b,a) \ r}" +definition underS :: "'a rel \ 'a \ 'a set" + where "underS r a \ {b. b \ a \ (b, a) \ r}" -definition Under::"'a rel \ 'a set \ 'a set" -where "Under r A \ {b \ Field r. \a \ A. (b,a) \ r}" +definition Under :: "'a rel \ 'a set \ 'a set" + where "Under r A \ {b \ Field r. \a \ A. (b, a) \ r}" -definition UnderS::"'a rel \ 'a set \ 'a set" -where "UnderS r A \ {b \ Field r. \a \ A. b \ a \ (b,a) \ r}" +definition UnderS :: "'a rel \ 'a set \ 'a set" + where "UnderS r A \ {b \ Field r. \a \ A. b \ a \ (b, a) \ r}" -definition above::"'a rel \ 'a \ 'a set" -where "above r a \ {b. (a,b) \ r}" +definition above :: "'a rel \ 'a \ 'a set" + where "above r a \ {b. (a, b) \ r}" -definition aboveS::"'a rel \ 'a \ 'a set" -where "aboveS r a \ {b. b \ a \ (a,b) \ r}" +definition aboveS :: "'a rel \ 'a \ 'a set" + where "aboveS r a \ {b. b \ a \ (a, b) \ r}" -definition Above::"'a rel \ 'a set \ 'a set" -where "Above r A \ {b \ Field r. \a \ A. (a,b) \ r}" +definition Above :: "'a rel \ 'a set \ 'a set" + where "Above r A \ {b \ Field r. \a \ A. (a, b) \ r}" -definition AboveS::"'a rel \ 'a set \ 'a set" -where "AboveS r A \ {b \ Field r. \a \ A. b \ a \ (a,b) \ r}" +definition AboveS :: "'a rel \ 'a set \ 'a set" + where "AboveS r A \ {b \ Field r. \a \ A. b \ a \ (a, b) \ r}" definition ofilter :: "'a rel \ 'a set \ bool" -where "ofilter r A \ (A \ Field r) \ (\a \ A. under r a \ A)" + where "ofilter r A \ A \ Field r \ (\a \ A. under r a \ A)" -text\Note: In the definitions of \Above[S]\ and \Under[S]\, - we bounded comprehension by \Field r\ in order to properly cover - the case of \A\ being empty.\ +text \ + Note: In the definitions of \Above[S]\ and \Under[S]\, we bounded + comprehension by \Field r\ in order to properly cover the case of \A\ being + empty. +\ -lemma underS_subset_under: "underS r a \ under r a" -by(auto simp add: underS_def under_def) +lemma underS_subset_under: "underS r a \ under r a" + by (auto simp add: underS_def under_def) lemma underS_notIn: "a \ underS r a" -by(simp add: underS_def) + by (simp add: underS_def) -lemma Refl_under_in: "\Refl r; a \ Field r\ \ a \ under r a" -by(simp add: refl_on_def under_def) +lemma Refl_under_in: "Refl r \ a \ Field r \ a \ under r a" + by (simp add: refl_on_def under_def) -lemma AboveS_disjoint: "A Int (AboveS r A) = {}" -by(auto simp add: AboveS_def) +lemma AboveS_disjoint: "A \ (AboveS r A) = {}" + by (auto simp add: AboveS_def) lemma in_AboveS_underS: "a \ Field r \ a \ AboveS r (underS r a)" -by(auto simp add: AboveS_def underS_def) + by (auto simp add: AboveS_def underS_def) -lemma Refl_under_underS: - assumes "Refl r" "a \ Field r" - shows "under r a = underS r a \ {a}" -unfolding under_def underS_def -using assms refl_on_def[of _ r] by fastforce +lemma Refl_under_underS: "Refl r \ a \ Field r \ under r a = underS r a \ {a}" + unfolding under_def underS_def + using refl_on_def[of _ r] by fastforce lemma underS_empty: "a \ Field r \ underS r a = {}" -by (auto simp: Field_def underS_def) + by (auto simp: Field_def underS_def) -lemma under_Field: "under r a \ Field r" -by(unfold under_def Field_def, auto) +lemma under_Field: "under r a \ Field r" + by (auto simp: under_def Field_def) -lemma underS_Field: "underS r a \ Field r" -by(unfold underS_def Field_def, auto) +lemma underS_Field: "underS r a \ Field r" + by (auto simp: underS_def Field_def) -lemma underS_Field2: -"a \ Field r \ underS r a < Field r" -using underS_notIn underS_Field by fast +lemma underS_Field2: "a \ Field r \ underS r a \ Field r" + using underS_notIn underS_Field by fast -lemma underS_Field3: -"Field r \ {} \ underS r a < Field r" -by(cases "a \ Field r", simp add: underS_Field2, auto simp add: underS_empty) +lemma underS_Field3: "Field r \ {} \ underS r a \ Field r" + by (cases "a \ Field r") (auto simp: underS_Field2 underS_empty) -lemma AboveS_Field: "AboveS r A \ Field r" -by(unfold AboveS_def Field_def, auto) +lemma AboveS_Field: "AboveS r A \ Field r" + by (auto simp: AboveS_def Field_def) lemma under_incr: - assumes TRANS: "trans r" and REL: "(a,b) \ r" - shows "under r a \ under r b" -proof(unfold under_def, auto) - fix x assume "(x,a) \ r" - with REL TRANS trans_def[of r] - show "(x,b) \ r" by blast + assumes "trans r" + and "(a, b) \ r" + shows "under r a \ under r b" + unfolding under_def +proof auto + fix x assume "(x, a) \ r" + with assms trans_def[of r] show "(x, b) \ r" by blast qed lemma underS_incr: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - REL: "(a,b) \ r" -shows "underS r a \ underS r b" -proof(unfold underS_def, auto) - assume *: "b \ a" and **: "(b,a) \ r" - with ANTISYM antisym_def[of r] REL - show False by blast + assumes "trans r" + and "antisym r" + and ab: "(a, b) \ r" + shows "underS r a \ underS r b" + unfolding underS_def +proof auto + assume *: "b \ a" and **: "(b, a) \ r" + with \antisym r\ antisym_def[of r] ab show False + by blast next - fix x assume "x \ a" "(x,a) \ r" - with REL TRANS trans_def[of r] - show "(x,b) \ r" by blast + fix x assume "x \ a" "(x, a) \ r" + with ab \trans r\ trans_def[of r] show "(x, b) \ r" + by blast qed lemma underS_incl_iff: -assumes LO: "Linear_order r" and - INa: "a \ Field r" and INb: "b \ Field r" -shows "(underS r a \ underS r b) = ((a,b) \ r)" + assumes LO: "Linear_order r" + and INa: "a \ Field r" + and INb: "b \ Field r" + shows "underS r a \ underS r b \ (a, b) \ r" + (is "?lhs \ ?rhs") proof - assume "(a,b) \ r" - thus "underS r a \ underS r b" using LO - by (simp add: order_on_defs underS_incr) + assume ?rhs + with \Linear_order r\ show ?lhs + by (simp add: order_on_defs underS_incr) next - assume *: "underS r a \ underS r b" - {assume "a = b" - hence "(a,b) \ r" using assms - by (simp add: order_on_defs refl_on_def) - } - moreover - {assume "a \ b \ (b,a) \ r" - hence "b \ underS r a" unfolding underS_def by blast - hence "b \ underS r b" using * by blast - hence False by (simp add: underS_notIn) - } - ultimately - show "(a,b) \ r" using assms - order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast + assume *: ?lhs + have "(a, b) \ r" if "a = b" + using assms that by (simp add: order_on_defs refl_on_def) + moreover have False if "a \ b" "(b, a) \ r" + proof - + from that have "b \ underS r a" unfolding underS_def by blast + with * have "b \ underS r b" by blast + then show ?thesis by (simp add: underS_notIn) + qed + ultimately show "(a,b) \ r" + using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast qed lemma finite_Linear_order_induct[consumes 3, case_names step]: assumes "Linear_order r" - and "x \ Field r" - and "finite r" - and step: "\x. \x \ Field r; \y. y \ aboveS r x \ P y\ \ P x" + and "x \ Field r" + and "finite r" + and step: "\x. x \ Field r \ (\y. y \ aboveS r x \ P y) \ P x" shows "P x" -using assms(2) -proof(induct rule: wf_induct[of "r\ - Id"]) + using assms(2) +proof (induct rule: wf_induct[of "r\ - Id"]) + case 1 from assms(1,3) show "wf (r\ - Id)" using linear_order_on_well_order_on linear_order_on_converse unfolding well_order_on_def by blast next - case (2 x) then show ?case - by - (rule step; auto simp: aboveS_def intro: FieldI2) + case prems: (2 x) + show ?case + by (rule step) (use prems in \auto simp: aboveS_def intro: FieldI2\) 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} + This subsection contains some variations of the results from @{theory Wellfounded}: + \<^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. \ 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.\ +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 = (\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 - } - } - (* *) + assumes "trans r" + shows "wf r \ (\a. wf (r \ (r\``{a} \ r\``{a})))" +proof - + define R where "R a = r \ (r\``{a} \ r\``{a})" for a + have "wf (R a)" if "wf r" for a + using that 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 blast + have "wf r" if *: "\a. wf(R a)" + unfolding wf_def + proof clarify + fix phi a + assume **: "\a. (\b. (b, a) \ r \ phi b) \ phi a" + define chi where "chi b \ (b, a) \ r \ phi b" for b + with * have "wf (R a)" by auto + then have "(\b. (\c. (c, b) \ R a \ chi c) \ chi b) \ (\b. chi b)" + unfolding wf_def by blast + also have "\b. (\c. (c, b) \ R a \ chi c) \ chi b" + proof (auto simp add: chi_def R_def) + fix b + assume "(b, a) \ r" and "\c. (c, b) \ r \ (c, a) \ r \ phi c" + then have "\c. (c, b) \ r \ phi c" + using assms trans_def[of r] by blast + with ** show "phi b" by blast + qed + finally have "\b. chi b" . + with ** chi_def show "phi a" by blast + qed + ultimately show ?thesis unfolding R_def by blast qed text \The next lemma is a variation of \wf_eq_minimal\ from Wellfounded, -allowing one to assume the set included in the field.\ + allowing one to assume the set included in the field.\ -lemma wf_eq_minimal2: -"wf r = (\A. A <= Field r \ A \ {} \ (\a \ A. \a' \ A. \ (a',a) \ r))" +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)" - by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast) - (rule wfI_min, fast) - (* *) - also have "(\A. ?phi A) = (\B \ Field r. ?phi B)" + let ?phi = "\A. A \ {} \ (\a \ A. \a' \ A. (a',a) \ r)" + have "wf r \ (\A. ?phi A)" + apply (auto simp: ex_in_conv [THEN sym]) + apply (erule wfE_min) + apply assumption + apply blast + apply (rule wfI_min) + apply fast + done + also have "(\A. ?phi A) \ (\B \ Field r. ?phi B)" proof assume "\A. ?phi A" - thus "\B \ Field r. ?phi B" by simp + then show "\B \ Field r. ?phi B" by simp next - assume *: "\B \ Field r. ?phi B" + 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 unfolding B_def by blast - hence "\a' \ A. (a',a) \ r" using 1 unfolding Field_def by blast - thus ?thesis using 1 by blast + proof clarify + fix A :: "'a set" + assume **: "A \ {}" + define B where "B = A \ Field r" + show "\a \ A. \a' \ A. (a', a) \ r" + proof (cases "B = {}") + case True + with ** obtain a where a: "a \ A" "a \ Field r" + unfolding B_def by blast + with a have "\a' \ A. (a',a) \ r" + unfolding Field_def by blast + with a show ?thesis by blast next - assume Case2: "B \ {}" have 1: "B \ Field r" unfolding B_def by blast - 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" unfolding B_def Field_def by blast - thus False using 2 ** by blast + case False + have "B \ Field r" unfolding B_def by blast + with False * obtain a where a: "a \ B" "\a' \ B. (a', a) \ r" + by blast + have "(a', a) \ r" if "a' \ A" for a' + proof + assume a'a: "(a', a) \ r" + with that have "a' \ B" unfolding B_def Field_def by blast + with a a'a show False by blast qed - thus ?thesis using 2 unfolding B_def by blast + with a show ?thesis unfolding B_def by blast qed qed qed @@ -441,58 +451,67 @@ 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.\ +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) = (\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 (simp add: 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 Total_subset_Id by auto - hence "A = {a} \ r = {(a,a)}" using * ** unfolding Field_def by blast - hence "\a \ A. \a' \ A. (a,a') \ r" using 1 by blast - } + assumes "Linear_order r" + shows "wf (r - Id) \ (\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r))" +proof (cases "r \ Id") + case True + then have *: "r - Id = {}" by blast + have "wf (r - Id)" by (simp add: *) + moreover have "\a \ A. \a' \ A. (a, a') \ r" + if *: "A \ Field r" and **: "A \ {}" for A + proof - + from \Linear_order r\ True + obtain a where a: "r = {} \ r = {(a, a)}" + unfolding order_on_defs using Total_subset_Id [of r] by blast + with * ** have "A = {a} \ r = {(a, a)}" + unfolding Field_def by blast + with a show ?thesis by blast + qed ultimately show ?thesis by blast next - assume Case2: "\ r \ Id" - hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI - unfolding order_on_defs by blast + case False + with \Linear_order r\ have Field: "Field r = Field (r - Id)" + unfolding order_on_defs using Total_Id_Field [of r] 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 simp - moreover have "\a \ A. \a' \ A. ((a,a') \ r) = ((a',a) \ r - Id)" - using Linear_order_in_diff_Id[of r] ** LI by blast - ultimately show "\a \ A. \a' \ A. (a,a') \ r" by blast + 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 \ {}" + then have "\a \ A. \a' \ A. (a',a) \ r - Id" + using Field * unfolding wf_eq_minimal2 by simp + moreover have "\a \ A. \a' \ A. (a, a') \ r \ (a', a) \ r - Id" + using Linear_order_in_diff_Id [OF \Linear_order r\] ** 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 simp - moreover have "\a \ A. \a' \ A. ((a,a') \ r) = ((a',a) \ r - Id)" - using 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 + assume *: "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r)" + show "wf (r - Id)" + unfolding wf_eq_minimal2 + proof clarify + fix A + assume **: "A \ Field(r - Id)" and ***: "A \ {}" + then have "\a \ A. \a' \ A. (a,a') \ r" + using Field * by simp + moreover have "\a \ A. \a' \ A. (a, a') \ r \ (a', a) \ r - Id" + using Linear_order_in_diff_Id [OF \Linear_order r\] ** mono_Field[of "r - Id" r] by blast + ultimately show "\a \ A. \a' \ A. (a',a) \ r - Id" + by blast qed qed qed corollary Linear_order_Well_order_iff: -assumes "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 blast + "Linear_order r \ + Well_order r \ (\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r))" + unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast end diff -r aee0d92995b6 -r c0cbfd2b5a45 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Sun Jul 31 19:09:21 2016 +0200 +++ b/src/HOL/Wellfounded.thy Sun Jul 31 22:56:18 2016 +0200 @@ -9,7 +9,7 @@ section \Well-founded Recursion\ theory Wellfounded -imports Transitive_Closure + imports Transitive_Closure begin subsection \Basic Definitions\ @@ -59,12 +59,14 @@ lemma wf_not_refl [simp]: "wf r \ (a, a) \ r" by (blast elim: wf_asym) -lemma wf_irrefl: assumes "wf r" obtains "(a, a) \ r" +lemma wf_irrefl: + assumes "wf r" + obtains "(a, a) \ r" by (drule wf_not_refl[OF assms]) lemma wf_wellorderI: assumes wf: "wf {(x::'a::ord, y). x < y}" - assumes lin: "OFCLASS('a::ord, linorder_class)" + and lin: "OFCLASS('a::ord, linorder_class)" shows "OFCLASS('a::ord, wellorder_class)" using lin apply (rule wellorder_class.intro) @@ -83,7 +85,7 @@ lemma wfE_pf: assumes wf: "wf R" - assumes a: "A \ R `` A" + and a: "A \ R `` A" shows "A = {}" proof - from wf have "x \ A" for x @@ -130,10 +132,13 @@ qed lemma wf_eq_minimal: "wf r \ (\Q x. x \ Q \ (\z\Q. \y. (y, z) \ r \ y \ Q))" -apply auto -apply (erule wfE_min, assumption, blast) -apply (rule wfI_min, auto) -done + apply auto + apply (erule wfE_min) + apply assumption + apply blast + apply (rule wfI_min) + apply auto + done lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] @@ -200,18 +205,13 @@ then show ?thesis by (simp add: bot_fun_def) qed -lemma wf_Int1: "wf r \ wf (r Int r')" - apply (erule wf_subset) - apply (rule Int_lower1) - done +lemma wf_Int1: "wf r \ wf (r \ r')" + by (erule wf_subset) (rule Int_lower1) -lemma wf_Int2: "wf r \ wf (r' Int r)" - apply (erule wf_subset) - apply (rule Int_lower2) - done +lemma wf_Int2: "wf r \ wf (r' \ r)" + by (erule wf_subset) (rule Int_lower2) -text \Exponentiation\ - +text \Exponentiation.\ lemma wf_exp: assumes "wf (R ^^ n)" shows "wf R" @@ -222,38 +222,43 @@ show "A = {}" by (rule wfE_pf) qed -text \Well-foundedness of insert\ - +text \Well-foundedness of \insert\.\ lemma wf_insert [iff]: "wf (insert (y, x) r) \ wf r \ (x, y) \ r\<^sup>*" -apply (rule iffI) - apply (blast elim: wf_trancl [THEN wf_irrefl] - intro: rtrancl_into_trancl1 wf_subset - rtrancl_mono [THEN [2] rev_subsetD]) -apply (simp add: wf_eq_minimal, safe) -apply (rule allE, assumption, erule impE, blast) -apply (erule bexE) -apply (rename_tac "a", case_tac "a = x") - prefer 2 -apply blast -apply (case_tac "y \ Q") - prefer 2 apply blast -apply (rule_tac x = "{z. z \ Q \ (z,y) \ r\<^sup>*}" in allE) - apply assumption -apply (erule_tac V = "\Q. (\x. x \ Q) \ P Q" for P in thin_rl) + apply (rule iffI) + apply (blast elim: wf_trancl [THEN wf_irrefl] + intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN [2] rev_subsetD]) + apply (simp add: wf_eq_minimal) + apply safe + apply (rule allE) + apply assumption + apply (erule impE) + apply blast + apply (erule bexE) + apply (rename_tac a, case_tac "a = x") + prefer 2 + apply blast + apply (case_tac "y \ Q") + prefer 2 + apply blast + apply (rule_tac x = "{z. z \ Q \ (z,y) \ r\<^sup>*}" in allE) + apply assumption + apply (erule_tac V = "\Q. (\x. x \ Q) \ P Q" for P in thin_rl) (*essential for speed*) -(*blast with new substOccur fails*) -apply (fast intro: converse_rtrancl_into_rtrancl) -done + (*blast with new substOccur fails*) + apply (fast intro: converse_rtrancl_into_rtrancl) + done subsubsection \Well-foundedness of image\ lemma wf_map_prod_image: "wf r \ inj f \ wf (map_prod f f ` r)" -apply (simp only: wf_eq_minimal, clarify) -apply (case_tac "\p. f p \ Q") -apply (erule_tac x = "{p. f p \ Q}" in allE) -apply (fast dest: inj_onD, blast) -done + apply (simp only: wf_eq_minimal) + apply clarify + apply (case_tac "\p. f p \ Q") + apply (erule_tac x = "{p. f p \ Q}" in allE) + apply (fast dest: inj_onD) +apply blast + done subsection \Well-Foundedness Results for Unions\ @@ -270,24 +275,21 @@ by (rule wfE_min [OF \wf R\ \x \ Q\]) blast with \wf S\ obtain z where "z \ ?Q'" and zmin: "\y. (y, z) \ S \ y \ ?Q'" by (erule wfE_min) - { - fix y assume "(y, z) \ S" - then have "y \ ?Q'" by (rule zmin) - have "y \ Q" - proof - assume "y \ Q" - with \y \ ?Q'\ obtain w where "(w, y) \ R" and "w \ Q" by auto - from \(w, y) \ R\ \(y, z) \ S\ have "(w, z) \ R O S" by (rule relcompI) - with \R O S \ R\ have "(w, z) \ R" .. - with \z \ ?Q'\ have "w \ Q" by blast - with \w \ Q\ show False by contradiction - qed - } + have "y \ Q" if "(y, z) \ S" for y + proof + from that have "y \ ?Q'" by (rule zmin) + assume "y \ Q" + with \y \ ?Q'\ obtain w where "(w, y) \ R" and "w \ Q" by auto + from \(w, y) \ R\ \(y, z) \ S\ have "(w, z) \ R O S" by (rule relcompI) + with \R O S \ R\ have "(w, z) \ R" .. + with \z \ ?Q'\ have "w \ Q" by blast + with \w \ Q\ show False by contradiction + qed with \z \ ?Q'\ show "\z\Q. \y. (y, z) \ R \ S \ y \ Q" by blast qed -text \Well-foundedness of indexed union with disjoint domains and ranges\ +text \Well-foundedness of indexed union with disjoint domains and ranges.\ lemma wf_UN: assumes "\i\I. wf (r i)" @@ -306,10 +308,9 @@ done lemma wfP_SUP: - "\i. wfP (r i) \ \i j. r i \ r j \ inf (DomainP (r i)) (RangeP (r j)) = bot \ wfP (SUPREMUM UNIV r)" - apply (rule wf_UN[to_pred]) - apply simp_all - done + "\i. wfP (r i) \ \i j. r i \ r j \ inf (DomainP (r i)) (RangeP (r j)) = bot \ + wfP (SUPREMUM UNIV r)" + by (rule wf_UN[to_pred]) simp_all lemma wf_Union: assumes "\r\R. wf r" @@ -458,9 +459,7 @@ subsection \Acyclic relations\ lemma wf_acyclic: "wf r \ acyclic r" -apply (simp add: acyclic_def) -apply (blast elim: wf_trancl [THEN wf_irrefl]) -done + by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl]) lemmas wfP_acyclicP = wf_acyclic [to_pred] @@ -468,15 +467,15 @@ subsubsection \Wellfoundedness of finite acyclic relations\ lemma finite_acyclic_wf [rule_format]: "finite r \ acyclic r \ wf r" -apply (erule finite_induct, blast) -apply (simp only: split_tupled_all) -apply simp -done + apply (erule finite_induct) + apply blast + apply (simp add: split_tupled_all) + done lemma finite_acyclic_wf_converse: "finite r \ acyclic r \ wf (r\)" -apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) -apply (erule acyclic_converse [THEN iffD2]) -done + apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) + apply (erule acyclic_converse [THEN iffD2]) + done text \ Observe that the converse of an irreflexive, transitive, @@ -488,12 +487,14 @@ shows "wf (r\)" proof - have "acyclic r" - using \irrefl r\ and \trans r\ by (simp add: irrefl_def acyclic_irrefl) - with \finite r\ show ?thesis by (rule finite_acyclic_wf_converse) + using \irrefl r\ and \trans r\ + by (simp add: irrefl_def acyclic_irrefl) + with \finite r\ show ?thesis + by (rule finite_acyclic_wf_converse) qed lemma wf_iff_acyclic_if_finite: "finite r \ wf r = acyclic r" -by (blast intro: finite_acyclic_wf wf_acyclic) + by (blast intro: finite_acyclic_wf wf_acyclic) subsection \@{typ nat} is well-founded\ @@ -528,8 +529,10 @@ unfolding less_eq rtrancl_eq_or_trancl by auto lemma wf_pred_nat: "wf pred_nat" - apply (unfold wf_def pred_nat_def, clarify) - apply (induct_tac x, blast+) + apply (unfold wf_def pred_nat_def) + apply clarify + apply (induct_tac x) + apply blast+ done lemma wf_less_than [iff]: "wf less_than" @@ -583,15 +586,13 @@ lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] theorem accp_downward: "accp r b \ r a b \ accp r a" - apply (erule accp.cases) - apply fast - done + by (cases rule: accp.cases) lemma not_accp_down: assumes na: "\ accp R x" obtains z where "R z x" and "\ accp R z" proof - - assume a: "\z. \R z x; \ accp R z\ \ thesis" + assume a: "\z. R z x \ \ accp R z \ thesis" show thesis proof (cases "\z. R z x \ accp R z") case True @@ -612,12 +613,11 @@ done theorem accp_downwards: "accp r a \ r\<^sup>*\<^sup>* b a \ accp r b" - apply (blast dest: accp_downwards_aux) - done + by (blast dest: accp_downwards_aux) theorem accp_wfPI: "\x. accp r x \ wfP r" apply (rule wfPUNIVI) - apply (rule_tac P=P in accp_induct) + apply (rule_tac P = P in accp_induct) apply blast apply blast done @@ -629,22 +629,22 @@ done theorem wfP_accp_iff: "wfP r = (\x. accp r x)" - apply (blast intro: accp_wfPI dest: accp_wfPD) - done + by (blast intro: accp_wfPI dest: accp_wfPD) text \Smaller relations have bigger accessible parts:\ lemma accp_subset: - assumes sub: "R1 \ R2" + assumes "R1 \ R2" shows "accp R2 \ accp R1" proof (rule predicate1I) - fix x assume "accp R2 x" + fix x + assume "accp R2 x" then show "accp R1 x" proof (induct x) fix x - assume ih: "\y. R2 y x \ accp R1 y" - with sub show "accp R1 x" + assume "\y. R2 y x \ accp R1 y" + with assms show "accp R1 x" by (blast intro: accp.accI) qed qed @@ -655,9 +655,9 @@ lemma accp_subset_induct: assumes subset: "D \ accp R" - and dcl: "\x z. \D x; R z x\ \ D z" + and dcl: "\x z. D x \ R z x \ D z" and "D x" - and istep: "\x. \D x; (\z. R z x \ P z)\ \ P x" + and istep: "\x. D x \ (\z. R z x \ P z) \ P x" shows "P x" proof - from subset and \D x\ @@ -665,8 +665,7 @@ then show "P x" using \D x\ proof (induct x) fix x - assume "D x" - and "\y. R y x \ D y \ P y" + assume "D x" and "\y. R y x \ D y \ P y" with dcl and istep show "P x" by blast qed qed @@ -691,15 +690,17 @@ text \Inverse Image\ -lemma wf_inv_image [simp,intro!]: "wf r \ wf (inv_image r f)" for f :: "'a \ 'b" -apply (simp add: inv_image_def wf_eq_minimal) -apply clarify -apply (subgoal_tac "\w::'b. w \ {w. \x::'a. x \ Q \ f x = w}") -prefer 2 apply (blast del: allE) -apply (erule allE) -apply (erule (1) notE impE) -apply blast -done +lemma wf_inv_image [simp,intro!]: "wf r \ wf (inv_image r f)" + for f :: "'a \ 'b" + apply (simp add: inv_image_def wf_eq_minimal) + apply clarify + apply (subgoal_tac "\w::'b. w \ {w. \x::'a. x \ Q \ f x = w}") + prefer 2 + apply (blast del: allE) + apply (erule allE) + apply (erule (1) notE impE) + apply blast + done text \Measure functions into @{typ nat}\ @@ -710,17 +711,15 @@ by (simp add:measure_def) lemma wf_measure [iff]: "wf (measure f)" -apply (unfold measure_def) -apply (rule wf_less_than [THEN wf_inv_image]) -done + unfolding measure_def by (rule wf_less_than [THEN wf_inv_image]) lemma wf_if_measure: "(\x. P x \ f(g x) < f x) \ wf {(y,x). P x \ y = g x}" for f :: "'a \ nat" -apply(insert wf_measure[of f]) -apply(simp only: measure_def inv_image_def less_than_def less_eq) -apply(erule wf_subset) -apply auto -done + apply (insert wf_measure[of f]) + apply (simp only: measure_def inv_image_def less_than_def less_eq) + apply (erule wf_subset) + apply auto + done subsubsection \Lexicographic combinations\ @@ -730,13 +729,18 @@ where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \ ra \ a = a' \ (b, b') \ rb}" lemma wf_lex_prod [intro!]: "wf ra \ wf rb \ wf (ra <*lex*> rb)" -apply (unfold wf_def lex_prod_def) -apply (rule allI, rule impI) -apply (simp only: split_paired_All) -apply (drule spec, erule mp) -apply (rule allI, rule impI) -apply (drule spec, erule mp, blast) -done + apply (unfold wf_def lex_prod_def) + apply (rule allI) + apply (rule impI) + apply (simp only: split_paired_All) + apply (drule spec) + apply (erule mp) + apply (rule allI) + apply (rule impI) + apply (drule spec) + apply (erule mp) + apply blast + done lemma in_lex_prod[simp]: "((a, b), (a', b')) \ r <*lex*> s \ (a, a') \ r \ a = a' \ (b, b') \ s" by (auto simp:lex_prod_def) @@ -752,19 +756,17 @@ where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\x. (f x, x))" lemma wf_mlex: "wf R \ wf (f <*mlex*> R)" - unfolding mlex_prod_def - by auto + by (auto simp: mlex_prod_def) lemma mlex_less: "f x < f y \ (x, y) \ f <*mlex*> R" - unfolding mlex_prod_def by simp + by (simp add: mlex_prod_def) lemma mlex_leq: "f x \ f y \ (x, y) \ R \ (x, y) \ f <*mlex*> R" - unfolding mlex_prod_def by auto + by (auto simp: mlex_prod_def) -text \proper subset relation on finite sets\ - +text \Proper subset relation on finite sets.\ definition finite_psubset :: "('a set \ 'a set) set" - where "finite_psubset = {(A,B). A < B \ finite B}" + where "finite_psubset = {(A, B). A \ B \ finite B}" lemma wf_finite_psubset[simp]: "wf finite_psubset" apply (unfold finite_psubset_def) @@ -776,15 +778,15 @@ lemma trans_finite_psubset: "trans finite_psubset" by (auto simp add: finite_psubset_def less_le trans_def) -lemma in_finite_psubset[simp]: "(A, B) \ finite_psubset \ A < B \ finite B" +lemma in_finite_psubset[simp]: "(A, B) \ finite_psubset \ A \ B \ finite B" unfolding finite_psubset_def by auto text \max- and min-extension of order to finite sets\ inductive_set max_ext :: "('a \ 'a) set \ ('a set \ 'a set) set" for R :: "('a \ 'a) set" -where - max_extI[intro]: "finite X \ finite Y \ Y \ {} \ (\x. x \ X \ \y\Y. (x, y) \ R) \ (X, Y) \ max_ext R" + where max_extI[intro]: + "finite X \ finite Y \ Y \ {} \ (\x. x \ X \ \y\Y. (x, y) \ R) \ (X, Y) \ max_ext R" lemma max_ext_wf: assumes wf: "wf r" @@ -792,23 +794,24 @@ proof (rule acc_wfI, intro allI) fix M show "M \ acc (max_ext r)" (is "_ \ ?W") - proof cases - assume "finite M" + proof (cases "finite M") + case True then show ?thesis proof (induct M) - show "{} \ ?W" + case empty + show ?case by (rule accI) (auto elim: max_ext.cases) next - fix M a assume "M \ ?W" "finite M" - with wf show "insert a M \ ?W" + case (insert a M) + from wf \M \ ?W\ \finite M\ show "insert a M \ ?W" proof (induct arbitrary: M) fix M a - assume "M \ ?W" and [intro]: "finite M" + assume "M \ ?W" + assume [intro]: "finite M" assume hyp: "\b M. (b, a) \ r \ M \ ?W \ finite M \ insert b M \ ?W" - have add_less: "\M \ ?W ; (\y. y \ N \ (y, a) \ r)\ \ N \ M \ ?W" + have add_less: "M \ ?W \ (\y. y \ N \ (y, a) \ r) \ N \ M \ ?W" if "finite N" "finite M" for N M :: "'a set" using that by (induct N arbitrary: M) (auto simp: hyp) - show "insert a M \ ?W" proof (rule accI) fix N @@ -823,14 +826,13 @@ then have finites: "finite ?N1" "finite ?N2" by auto have "?N2 \ ?W" - proof cases - assume [simp]: "M = {}" + proof (cases "M = {}") + case [simp]: True have Mw: "{} \ ?W" by (rule accI) (auto elim: max_ext.cases) - from * have "?N2 = {}" by auto with Mw show "?N2 \ ?W" by (simp only:) next - assume "M \ {}" + case False from * finites have N2: "(?N2, M) \ max_ext r" by (rule_tac max_extI[OF _ _ \M \ {}\]) auto with \M \ ?W\ show "?N2 \ ?W" by (rule acc_downward) @@ -842,15 +844,13 @@ qed qed next - assume [simp]: "\ finite M" + case [simp]: False show ?thesis by (rule accI) (auto elim: max_ext.cases) qed qed -lemma max_ext_additive: - "(A, B) \ max_ext R \ (C, D) \ max_ext R \ - (A \ C, B \ D) \ max_ext R" +lemma max_ext_additive: "(A, B) \ max_ext R \ (C, D) \ max_ext R \ (A \ C, B \ D) \ max_ext R" by (force elim!: max_ext.cases) @@ -874,13 +874,13 @@ obtain z where z: "z \ \Q" "\y. (y, z) \ r \ y \ \Q" by (erule wfE_min) from z obtain m where "m \ Q" "z \ m" by auto - from \m \ Q\ - show ?thesis - proof (rule, intro bexI allI impI) + from \m \ Q\ show ?thesis + proof (intro rev_bexI allI impI) fix n assume smaller: "(n, m) \ min_ext r" - with \z \ m\ obtain y where y: "y \ n" "(y, z) \ r" by (auto simp: min_ext_def) - then show "n \ Q" using z(2) by auto + with \z \ m\ obtain y where "y \ n" "(y, z) \ r" + by (auto simp: min_ext_def) + with z(2) show "n \ Q" by auto qed qed qed @@ -893,32 +893,33 @@ and f :: "'a \ nat" assumes "\a b. (b, a) \ r \ ub b \ ub a \ ub a \ f b \ f b > f a" shows "wf r" - apply (rule wf_subset[OF wf_measure[of "\a. ub a - f a"]]) - apply (auto dest: assms) - done + by (rule wf_subset[OF wf_measure[of "\a. ub a - f a"]]) (auto dest: assms) lemma wf_bounded_set: fixes ub :: "'a \ 'b set" and f :: "'a \ 'b set" assumes "\a b. (b,a) \ r \ finite (ub a) \ ub b \ ub a \ ub a \ f b \ f b \ f a" shows "wf r" - apply(rule wf_bounded_measure[of r "\a. card(ub a)" "\a. card(f a)"]) - apply(drule assms) + apply (rule wf_bounded_measure[of r "\a. card (ub a)" "\a. card (f a)"]) + apply (drule assms) apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) done lemma finite_subset_wf: assumes "finite A" - shows "wf {(X,Y). X \ Y \ Y \ A}" + shows "wf {(X,Y). X \ Y \ Y \ A}" proof (intro finite_acyclic_wf) - have "{(X,Y). X \ Y \ Y \ A} \ Pow A \ Pow A" by blast + have "{(X,Y). X \ Y \ Y \ A} \ Pow A \ Pow A" + by blast then show "finite {(X,Y). X \ Y \ Y \ A}" by (rule finite_subset) (auto simp: assms finite_cartesian_product) next have "{(X, Y). X \ Y \ Y \ A}\<^sup>+ = {(X, Y). X \ Y \ Y \ A}" by (intro trancl_id transI) blast - also have " \x. (x, x) \ \" by blast - finally show "acyclic {(X,Y). X \ Y \ Y \ A}" by (rule acyclicI) + also have " \x. (x, x) \ \" + by blast + finally show "acyclic {(X,Y). X \ Y \ Y \ A}" + by (rule acyclicI) qed hide_const (open) acc accp diff -r aee0d92995b6 -r c0cbfd2b5a45 src/HOL/Wfrec.thy --- a/src/HOL/Wfrec.thy Sun Jul 31 19:09:21 2016 +0200 +++ b/src/HOL/Wfrec.thy Sun Jul 31 22:56:18 2016 +0200 @@ -7,20 +7,20 @@ section \Well-Founded Recursion Combinator\ theory Wfrec -imports Wellfounded + imports Wellfounded begin -inductive wfrec_rel :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ 'a \ 'b \ bool" for R F where - wfrecI: "(\z. (z, x) \ R \ wfrec_rel R F z (g z)) \ wfrec_rel R F x (F g x)" +inductive wfrec_rel :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ 'a \ 'b \ bool" for R F + where wfrecI: "(\z. (z, x) \ R \ wfrec_rel R F z (g z)) \ wfrec_rel R F x (F g x)" -definition cut :: "('a \ 'b) \ ('a \ 'a) set \ 'a \ 'a \ 'b" where - "cut f R x = (\y. if (y, x) \ R then f y else undefined)" +definition cut :: "('a \ 'b) \ ('a \ 'a) set \ 'a \ 'a \ 'b" + where "cut f R x = (\y. if (y, x) \ R then f y else undefined)" -definition adm_wf :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ bool" where - "adm_wf R F \ (\f g x. (\z. (z, x) \ R \ f z = g z) \ F f x = F g x)" +definition adm_wf :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ bool" + where "adm_wf R F \ (\f g x. (\z. (z, x) \ R \ f z = g z) \ F f x = F g x)" -definition wfrec :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ ('a \ 'b)" where - "wfrec R F = (\x. THE y. wfrec_rel R (\f x. F (cut f R x) x) x y)" +definition wfrec :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ ('a \ 'b)" + where "wfrec R F = (\x. THE y. wfrec_rel R (\f x. F (cut f R x) x) x y)" lemma cuts_eq: "(cut f R x = cut g R x) \ (\y. (y, x) \ R \ f y = g y)" by (simp add: fun_eq_iff cut_def) @@ -28,13 +28,17 @@ lemma cut_apply: "(x, a) \ R \ cut f R a x = f x" by (simp add: cut_def) -text\Inductive characterization of wfrec combinator; for details see: -John Harrison, "Inductive definitions: automation and application"\ +text \ + Inductive characterization of \wfrec\ combinator; for details see: + John Harrison, "Inductive definitions: automation and application". +\ lemma theI_unique: "\!x. P x \ P x \ x = The P" by (auto intro: the_equality[symmetric] theI) -lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\!y. wfrec_rel R F x y" +lemma wfrec_unique: + assumes "adm_wf R F" "wf R" + shows "\!y. wfrec_rel R F x y" using \wf R\ proof induct define f where "f y = (THE z. wfrec_rel R F y z)" for y @@ -46,44 +50,46 @@ qed lemma adm_lemma: "adm_wf R (\f x. F (cut f R x) x)" - by (auto simp add: adm_wf_def - intro!: arg_cong[where f="\x. F x y" for y] cuts_eq[THEN iffD2]) + by (auto simp: adm_wf_def intro!: arg_cong[where f="\x. F x y" for y] cuts_eq[THEN iffD2]) lemma wfrec: "wf R \ wfrec R F a = F (cut (wfrec R F) R a) a" -apply (simp add: wfrec_def) -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) -apply (rule wfrec_rel.wfrecI) -apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) -done + apply (simp add: wfrec_def) + apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality]) + apply assumption + apply (rule wfrec_rel.wfrecI) + apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) + done -text\* This form avoids giant explosions in proofs. NOTE USE OF ==\ +text \This form avoids giant explosions in proofs. NOTE USE OF \\\.\ lemma def_wfrec: "f \ wfrec R F \ wf R \ f a = F (cut f R a) a" - by (auto intro: wfrec) + by (auto intro: wfrec) subsubsection \Well-founded recursion via genuine fixpoints\ lemma wfrec_fixpoint: - assumes WF: "wf R" and ADM: "adm_wf R F" + assumes wf: "wf R" + and adm: "adm_wf R F" shows "wfrec R F = F (wfrec R F)" proof (rule ext) fix x have "wfrec R F x = F (cut (wfrec R F) R x) x" - using wfrec[of R F] WF by simp + using wfrec[of R F] wf by simp also - { have "\ y. (y,x) \ R \ (cut (wfrec R F) R x) y = (wfrec R F) y" - by (auto simp add: cut_apply) - hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x" - using ADM adm_wf_def[of R F] by auto } + have "\y. (y, x) \ R \ cut (wfrec R F) R x y = wfrec R F y" + by (auto simp add: cut_apply) + then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x" + using adm adm_wf_def[of R F] by auto finally show "wfrec R F x = F (wfrec R F) x" . qed + subsection \Wellfoundedness of \same_fst\\ -definition same_fst :: "('a \ bool) \ ('a \ ('b \ 'b) set) \ (('a \ 'b) \ ('a \ 'b)) set" where - "same_fst P R = {((x', y'), (x, y)) . x' = x \ P x \ (y',y) \ R x}" - \\For @{const wfrec} declarations where the first n parameters +definition same_fst :: "('a \ bool) \ ('a \ ('b \ 'b) set) \ (('a \ 'b) \ ('a \ 'b)) set" + where "same_fst P R = {((x', y'), (x, y)) . x' = x \ P x \ (y',y) \ R x}" + \ \For @{const wfrec} declarations where the first n parameters stay unchanged in the recursive call.\ lemma same_fstI [intro!]: "P x \ (y', y) \ R x \ ((x, y'), (x, y)) \ same_fst P R" @@ -92,12 +98,13 @@ lemma wf_same_fst: assumes prem: "\x. P x \ wf (R x)" shows "wf (same_fst P R)" -apply (simp cong del: imp_cong add: wf_def same_fst_def) -apply (intro strip) -apply (rename_tac a b) -apply (case_tac "wf (R a)") - apply (erule_tac a = b in wf_induct, blast) -apply (blast intro: prem) -done + apply (simp cong del: imp_cong add: wf_def same_fst_def) + apply (intro strip) + apply (rename_tac a b) + apply (case_tac "wf (R a)") + apply (erule_tac a = b in wf_induct) + apply blast + apply (blast intro: prem) + done end diff -r aee0d92995b6 -r c0cbfd2b5a45 src/HOL/Zorn.thy --- a/src/HOL/Zorn.thy Sun Jul 31 19:09:21 2016 +0200 +++ b/src/HOL/Zorn.thy Sun Jul 31 22:56:18 2016 +0200 @@ -1,7 +1,7 @@ -(* Title: HOL/Zorn.thy - Author: Jacques D. Fleuriot - Author: Tobias Nipkow, TUM - Author: Christian Sternagel, JAIST +(* Title: HOL/Zorn.thy + Author: Jacques D. Fleuriot + Author: Tobias Nipkow, TUM + Author: Christian Sternagel, JAIST Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF). The well-ordering theorem. @@ -10,7 +10,7 @@ section \Zorn's Lemma\ theory Zorn -imports Order_Relation Hilbert_Choice + imports Order_Relation Hilbert_Choice begin subsection \Zorn's Lemma for the Subset Relation\ @@ -20,36 +20,38 @@ text \Let \P\ be a binary predicate on the set \A\.\ locale pred_on = fixes A :: "'a set" - and P :: "'a \ 'a \ bool" (infix "\" 50) + and P :: "'a \ 'a \ bool" (infix "\" 50) begin -abbreviation Peq :: "'a \ 'a \ bool" (infix "\" 50) where - "x \ y \ P\<^sup>=\<^sup>= x y" +abbreviation Peq :: "'a \ 'a \ bool" (infix "\" 50) + where "x \ y \ P\<^sup>=\<^sup>= x y" + +text \A chain is a totally ordered subset of \A\.\ +definition chain :: "'a set \ bool" + where "chain C \ C \ A \ (\x\C. \y\C. x \ y \ y \ x)" -text \A chain is a totally ordered subset of @{term A}.\ -definition chain :: "'a set \ bool" where - "chain C \ C \ A \ (\x\C. \y\C. x \ y \ y \ x)" - -text \We call a chain that is a proper superset of some set @{term X}, -but not necessarily a chain itself, a superchain of @{term X}.\ -abbreviation superchain :: "'a set \ 'a set \ bool" (infix " chain C \ X \ C" +text \ + We call a chain that is a proper superset of some set \X\, + but not necessarily a chain itself, a superchain of \X\. +\ +abbreviation superchain :: "'a set \ 'a set \ bool" (infix " chain C \ X \ C" text \A maximal chain is a chain that does not have a superchain.\ -definition maxchain :: "'a set \ bool" where - "maxchain C \ chain C \ \ (\S. C bool" + where "maxchain C \ chain C \ (\S. C We define the successor of a set to be an arbitrary -superchain, if such exists, or the set itself, otherwise.\ -definition suc :: "'a set \ 'a set" where - "suc C = (if \ chain C \ maxchain C then C else (SOME D. C + We define the successor of a set to be an arbitrary + superchain, if such exists, or the set itself, otherwise. +\ +definition suc :: "'a set \ 'a set" + where "suc C = (if \ chain C \ maxchain C then C else (SOME D. C C \ A; \x y. \x \ C; y \ C\ \ x \ y \ y \ x\ \ chain C" +lemma chainI [Pure.intro?]: "C \ A \ (\x y. x \ C \ y \ C \ x \ y \ y \ x) \ chain C" unfolding chain_def by blast -lemma chain_total: - "chain C \ x \ C \ y \ C \ x \ y \ y \ x" +lemma chain_total: "chain C \ x \ C \ y \ C \ x \ y \ y \ x" by (simp add: chain_def) lemma not_chain_suc [simp]: "\ chain X \ suc X = X" @@ -64,62 +66,67 @@ lemma chain_empty [simp]: "chain {}" by (auto simp: chain_def) -lemma not_maxchain_Some: - "chain C \ \ maxchain C \ C \ maxchain C \ C \ maxchain C \ suc C \ C" +lemma suc_not_equals: "chain C \ \ maxchain C \ suc C \ C" using not_maxchain_Some by (auto simp: suc_def) lemma subset_suc: - assumes "X \ Y" shows "X \ suc Y" + assumes "X \ Y" + shows "X \ suc Y" using assms by (rule subset_trans) (rule suc_subset) -text \We build a set @{term \} that is closed under applications -of @{term suc} and contains the union of all its subsets.\ -inductive_set suc_Union_closed ("\") where - suc: "X \ \ \ suc X \ \" | - Union [unfolded Pow_iff]: "X \ Pow \ \ \X \ \" - -text \Since the empty set as well as the set itself is a subset of -every set, @{term \} contains at least @{term "{} \ \"} and -@{term "\\ \ \"}.\ -lemma - suc_Union_closed_empty: "{} \ \" and - suc_Union_closed_Union: "\\ \ \" - using Union [of "{}"] and Union [of "\"] by simp+ -text \Thus closure under @{term suc} will hit a maximal chain -eventually, as is shown below.\ +text \ + We build a set @{term \} that is closed under applications + of @{term suc} and contains the union of all its subsets. +\ +inductive_set suc_Union_closed ("\") + where + suc: "X \ \ \ suc X \ \" + | Union [unfolded Pow_iff]: "X \ Pow \ \ \X \ \" -lemma suc_Union_closed_induct [consumes 1, case_names suc Union, - induct pred: suc_Union_closed]: - assumes "X \ \" - and "\X. \X \ \; Q X\ \ Q (suc X)" - and "\X. \X \ \; \x\X. Q x\ \ Q (\X)" - shows "Q X" - using assms by (induct) blast+ +text \ + Since the empty set as well as the set itself is a subset of + every set, @{term \} contains at least @{term "{} \ \"} and + @{term "\\ \ \"}. +\ +lemma suc_Union_closed_empty: "{} \ \" + and suc_Union_closed_Union: "\\ \ \" + using Union [of "{}"] and Union [of "\"] by simp_all + +text \Thus closure under @{term suc} will hit a maximal chain + eventually, as is shown below.\ -lemma suc_Union_closed_cases [consumes 1, case_names suc Union, - cases pred: suc_Union_closed]: +lemma suc_Union_closed_induct [consumes 1, case_names suc Union, induct pred: suc_Union_closed]: assumes "X \ \" - and "\Y. \X = suc Y; Y \ \\ \ Q" - and "\Y. \X = \Y; Y \ \\ \ Q" + and "\X. X \ \ \ Q X \ Q (suc X)" + and "\X. X \ \ \ \x\X. Q x \ Q (\X)" + shows "Q X" + using assms by induct blast+ + +lemma suc_Union_closed_cases [consumes 1, case_names suc Union, cases pred: suc_Union_closed]: + assumes "X \ \" + and "\Y. X = suc Y \ Y \ \ \ Q" + and "\Y. X = \Y \ Y \ \ \ Q" shows "Q" - using assms by (cases) simp+ + using assms by cases simp_all text \On chains, @{term suc} yields a chain.\ lemma chain_suc: - assumes "chain X" shows "chain (suc X)" + assumes "chain X" + shows "chain (suc X)" using assms - by (cases "\ chain X \ maxchain X") - (force simp: suc_def dest: not_maxchain_Some)+ + by (cases "\ chain X \ maxchain X") (force simp: suc_def dest: not_maxchain_Some)+ lemma chain_sucD: - assumes "chain X" shows "suc X \ A \ chain (suc X)" + assumes "chain X" + shows "suc X \ A \ chain (suc X)" proof - - from \chain X\ have *: "chain (suc X)" by (rule chain_suc) - then have "suc X \ A" unfolding chain_def by blast + from \chain X\ have *: "chain (suc X)" + by (rule chain_suc) + then have "suc X \ A" + unfolding chain_def by blast with * show ?thesis by blast qed @@ -128,27 +135,31 @@ and *: "\Z. Z \ \ \ Z \ Y \ Z = Y \ suc Z \ Y" shows "X \ Y \ suc Y \ X" using \X \ \\ -proof (induct) +proof induct case (suc X) with * show ?case by (blast del: subsetI intro: subset_suc) -qed blast +next + case Union + then show ?case by blast +qed lemma suc_Union_closed_subsetD: assumes "Y \ X" and "X \ \" and "Y \ \" shows "X = Y \ suc Y \ X" - using assms(2-, 1) + using assms(2,3,1) proof (induct arbitrary: Y) case (suc X) - note * = \\Y. \Y \ \; Y \ X\ \ X = Y \ suc Y \ X\ + note * = \\Y. Y \ \ \ Y \ X \ X = Y \ suc Y \ X\ with suc_Union_closed_total' [OF \Y \ \\ \X \ \\] - have "Y \ X \ suc X \ Y" by blast + have "Y \ X \ suc X \ Y" by blast then show ?case proof assume "Y \ X" with * and \Y \ \\ have "X = Y \ suc Y \ X" by blast then show ?thesis proof - assume "X = Y" then show ?thesis by simp + assume "X = Y" + then show ?thesis by simp next assume "suc Y \ X" then have "suc Y \ suc X" by (rule subset_suc) @@ -164,21 +175,22 @@ proof (rule ccontr) assume "\ ?thesis" with \Y \ \X\ obtain x y z - where "\ suc Y \ \X" - and "x \ X" and "y \ x" and "y \ Y" - and "z \ suc Y" and "\x\X. z \ x" by blast + where "\ suc Y \ \X" + and "x \ X" and "y \ x" and "y \ Y" + and "z \ suc Y" and "\x\X. z \ x" by blast with \X \ \\ have "x \ \" by blast - from Union and \x \ X\ - have *: "\y. \y \ \; y \ x\ \ x = y \ suc y \ x" by blast - with suc_Union_closed_total' [OF \Y \ \\ \x \ \\] - have "Y \ x \ suc x \ Y" by blast + from Union and \x \ X\ have *: "\y. y \ \ \ y \ x \ x = y \ suc y \ x" + by blast + with suc_Union_closed_total' [OF \Y \ \\ \x \ \\] have "Y \ x \ suc x \ Y" + by blast then show False proof assume "Y \ x" with * [OF \Y \ \\] have "x = Y \ suc Y \ x" by blast then show False proof - assume "x = Y" with \y \ x\ and \y \ Y\ show False by blast + assume "x = Y" + with \y \ x\ and \y \ Y\ show False by blast next assume "suc Y \ x" with \x \ X\ have "suc Y \ \X" by blast @@ -199,75 +211,87 @@ proof (cases "\Z\\. Z \ Y \ Z = Y \ suc Z \ Y") case True with suc_Union_closed_total' [OF assms] - have "X \ Y \ suc Y \ X" by blast - then show ?thesis using suc_subset [of Y] by blast + have "X \ Y \ suc Y \ X" by blast + with suc_subset [of Y] show ?thesis by blast next case False - then obtain Z - where "Z \ \" and "Z \ Y" and "Z \ Y" and "\ suc Z \ Y" by blast - with suc_Union_closed_subsetD and \Y \ \\ show ?thesis by blast + then obtain Z where "Z \ \" and "Z \ Y" and "Z \ Y" and "\ suc Z \ Y" + by blast + with suc_Union_closed_subsetD and \Y \ \\ show ?thesis + by blast qed text \Once we hit a fixed point w.r.t. @{term suc}, all other elements -of @{term \} are subsets of this fixed point.\ + of @{term \} are subsets of this fixed point.\ lemma suc_Union_closed_suc: assumes "X \ \" and "Y \ \" and "suc Y = Y" shows "X \ Y" -using \X \ \\ -proof (induct) + using \X \ \\ +proof induct case (suc X) - with \Y \ \\ and suc_Union_closed_subsetD - have "X = Y \ suc X \ Y" by blast - then show ?case by (auto simp: \suc Y = Y\) -qed blast + with \Y \ \\ and suc_Union_closed_subsetD have "X = Y \ suc X \ Y" + by blast + then show ?case + by (auto simp: \suc Y = Y\) +next + case Union + then show ?case by blast +qed lemma eq_suc_Union: assumes "X \ \" shows "suc X = X \ X = \\" + (is "?lhs \ ?rhs") proof - assume "suc X = X" - with suc_Union_closed_suc [OF suc_Union_closed_Union \X \ \\] - have "\\ \ X" . - with \X \ \\ show "X = \\" by blast + assume ?lhs + then have "\\ \ X" + by (rule suc_Union_closed_suc [OF suc_Union_closed_Union \X \ \\]) + with \X \ \\ show ?rhs + by blast next from \X \ \\ have "suc X \ \" by (rule suc) then have "suc X \ \\" by blast - moreover assume "X = \\" + moreover assume ?rhs ultimately have "suc X \ X" by simp moreover have "X \ suc X" by (rule suc_subset) - ultimately show "suc X = X" .. + ultimately show ?lhs .. qed lemma suc_in_carrier: assumes "X \ A" shows "suc X \ A" using assms - by (cases "\ chain X \ maxchain X") - (auto dest: chain_sucD) + by (cases "\ chain X \ maxchain X") (auto dest: chain_sucD) lemma suc_Union_closed_in_carrier: assumes "X \ \" shows "X \ A" using assms - by (induct) (auto dest: suc_in_carrier) + by induct (auto dest: suc_in_carrier) text \All elements of @{term \} are chains.\ lemma suc_Union_closed_chain: assumes "X \ \" shows "chain X" -using assms -proof (induct) - case (suc X) then show ?case using not_maxchain_Some by (simp add: suc_def) + using assms +proof induct + case (suc X) + then show ?case + using not_maxchain_Some by (simp add: suc_def) next case (Union X) - then have "\X \ A" by (auto dest: suc_Union_closed_in_carrier) + then have "\X \ A" + by (auto dest: suc_Union_closed_in_carrier) moreover have "\x\\X. \y\\X. x \ y \ y \ x" proof (intro ballI) fix x y assume "x \ \X" and "y \ \X" - then obtain u v where "x \ u" and "u \ X" and "y \ v" and "v \ X" by blast - with Union have "u \ \" and "v \ \" and "chain u" and "chain v" by blast+ - with suc_Union_closed_total have "u \ v \ v \ u" by blast + then obtain u v where "x \ u" and "u \ X" and "y \ v" and "v \ X" + by blast + with Union have "u \ \" and "v \ \" and "chain u" and "chain v" + by blast+ + with suc_Union_closed_total have "u \ v \ v \ u" + by blast then show "x \ y \ y \ x" proof assume "u \ v" @@ -290,18 +314,17 @@ subsubsection \Hausdorff's Maximum Principle\ -text \There exists a maximal totally ordered subset of @{term A}. (Note that we do not -require @{term A} to be partially ordered.)\ +text \There exists a maximal totally ordered subset of \A\. (Note that we do not + require \A\ to be partially ordered.)\ theorem Hausdorff: "\C. maxchain C" proof - let ?M = "\\" have "maxchain ?M" proof (rule ccontr) - assume "\ maxchain ?M" + assume "\ ?thesis" then have "suc ?M \ ?M" - using suc_not_equals and - suc_Union_closed_chain [OF suc_Union_closed_Union] by simp + using suc_not_equals and suc_Union_closed_chain [OF suc_Union_closed_Union] by simp moreover have "suc ?M = ?M" using eq_suc_Union [OF suc_Union_closed_Union] by simp ultimately show False by contradiction @@ -310,34 +333,35 @@ qed text \Make notation @{term \} available again.\ -no_notation suc_Union_closed ("\") +no_notation suc_Union_closed ("\") -lemma chain_extend: - "chain C \ z \ A \ \x\C. x \ z \ chain ({z} \ C)" +lemma chain_extend: "chain C \ z \ A \ \x\C. x \ z \ chain ({z} \ C)" unfolding chain_def by blast -lemma maxchain_imp_chain: - "maxchain C \ chain C" +lemma maxchain_imp_chain: "maxchain C \ chain C" by (simp add: maxchain_def) end text \Hide constant @{const pred_on.suc_Union_closed}, which was just needed -for the proof of Hausforff's maximum principle.\ + for the proof of Hausforff's maximum principle.\ hide_const pred_on.suc_Union_closed lemma chain_mono: - assumes "\x y. \x \ A; y \ A; P x y\ \ Q x y" + assumes "\x y. x \ A \ y \ A \ P x y \ Q x y" and "pred_on.chain A P C" shows "pred_on.chain A Q C" using assms unfolding pred_on.chain_def by blast + subsubsection \Results for the proper subset relation\ interpretation subset: pred_on "A" "op \" for A . lemma subset_maxchain_max: - assumes "subset.maxchain A C" and "X \ A" and "\C \ X" + assumes "subset.maxchain A C" + and "X \ A" + and "\C \ X" shows "\C = X" proof (rule ccontr) let ?C = "{X} \ C" @@ -352,6 +376,7 @@ ultimately show False using * by blast qed + subsubsection \Zorn's lemma\ text \If every chain has an upper bound, then there is a maximal set.\ @@ -360,19 +385,23 @@ shows "\M\A. \X\A. M \ X \ X = M" proof - from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. - then have "subset.chain A M" by (rule subset.maxchain_imp_chain) - with assms obtain Y where "Y \ A" and "\X\M. X \ Y" by blast + then have "subset.chain A M" + by (rule subset.maxchain_imp_chain) + with assms obtain Y where "Y \ A" and "\X\M. X \ Y" + by blast moreover have "\X\A. Y \ X \ Y = X" proof (intro ballI impI) fix X assume "X \ A" and "Y \ X" show "Y = X" proof (rule ccontr) - assume "Y \ X" + assume "\ ?thesis" with \Y \ X\ have "\ X \ Y" by blast from subset.chain_extend [OF \subset.chain A M\ \X \ A\] and \\X\M. X \ Y\ - have "subset.chain A ({X} \ M)" using \Y \ X\ by auto - moreover have "M \ {X} \ M" using \\X\M. X \ Y\ and \\ X \ Y\ by auto + have "subset.chain A ({X} \ M)" + using \Y \ X\ by auto + moreover have "M \ {X} \ M" + using \\X\M. X \ Y\ and \\ X \ Y\ by auto ultimately show False using \subset.maxchain A M\ by (auto simp: subset.maxchain_def) qed @@ -380,13 +409,14 @@ ultimately show ?thesis by blast qed -text\Alternative version of Zorn's lemma for the subset relation.\ +text \Alternative version of Zorn's lemma for the subset relation.\ lemma subset_Zorn': assumes "\C. subset.chain A C \ \C \ A" shows "\M\A. \X\A. M \ X \ X = M" proof - from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. - then have "subset.chain A M" by (rule subset.maxchain_imp_chain) + then have "subset.chain A M" + by (rule subset.maxchain_imp_chain) with assms have "\M \ A" . moreover have "\Z\A. \M \ Z \ \M = Z" proof (intro ballI impI) @@ -403,19 +433,17 @@ text \Relate old to new definitions.\ -(* Define globally? In Set.thy? *) -definition chain_subset :: "'a set set \ bool" ("chain\<^sub>\") where - "chain\<^sub>\ C \ (\A\C. \B\C. A \ B \ B \ A)" +definition chain_subset :: "'a set set \ bool" ("chain\<^sub>\") (* Define globally? In Set.thy? *) + where "chain\<^sub>\ C \ (\A\C. \B\C. A \ B \ B \ A)" -definition chains :: "'a set set \ 'a set set set" where - "chains A = {C. C \ A \ chain\<^sub>\ C}" +definition chains :: "'a set set \ 'a set set set" + where "chains A = {C. C \ A \ chain\<^sub>\ C}" -(* Define globally? In Relation.thy? *) -definition Chains :: "('a \ 'a) set \ 'a set set" where - "Chains r = {C. \a\C. \b\C. (a, b) \ r \ (b, a) \ r}" +definition Chains :: "('a \ 'a) set \ 'a set set" (* Define globally? In Relation.thy? *) + where "Chains r = {C. \a\C. \b\C. (a, b) \ r \ (b, a) \ r}" -lemma chains_extend: - "[| c \ chains S; z \ S; \x \ c. x \ (z:: 'a set) |] ==> {z} Un c \ chains S" +lemma chains_extend: "c \ chains S \ z \ S \ \x \ c. x \ z \ {z} \ c \ chains S" + for z :: "'a set" unfolding chains_def chain_subset_def by blast lemma mono_Chains: "r \ s \ Chains r \ Chains s" @@ -427,8 +455,7 @@ lemma chains_alt_def: "chains A = {C. subset.chain A C}" by (simp add: chains_def chain_subset_alt_def subset.chain_def) -lemma Chains_subset: - "Chains r \ {C. pred_on.chain UNIV (\x y. (x, y) \ r) C}" +lemma Chains_subset: "Chains r \ {C. pred_on.chain UNIV (\x y. (x, y) \ r) C}" by (force simp add: Chains_def pred_on.chain_def) lemma Chains_subset': @@ -442,20 +469,18 @@ shows "Chains r = {C. pred_on.chain UNIV (\x y. (x, y) \ r) C}" using assms Chains_subset Chains_subset' by blast -lemma Zorn_Lemma: - "\C\chains A. \C \ A \ \M\A. \X\A. M \ X \ X = M" +lemma Zorn_Lemma: "\C\chains A. \C \ A \ \M\A. \X\A. M \ X \ X = M" using subset_Zorn' [of A] by (force simp: chains_alt_def) -lemma Zorn_Lemma2: - "\C\chains A. \U\A. \X\C. X \ U \ \M\A. \X\A. M \ X \ X = M" +lemma Zorn_Lemma2: "\C\chains A. \U\A. \X\C. X \ U \ \M\A. \X\A. M \ X \ X = M" using subset_Zorn [of A] by (auto simp: chains_alt_def) -text\Various other lemmas\ +text \Various other lemmas\ -lemma chainsD: "[| c \ chains S; x \ c; y \ c |] ==> x \ y | y \ x" +lemma chainsD: "c \ chains S \ x \ c \ y \ c \ x \ y \ y \ x" unfolding chains_def chain_subset_def by blast -lemma chainsD2: "!!(c :: 'a set set). c \ chains S ==> c \ S" +lemma chainsD2: "c \ chains S \ c \ S" unfolding chains_def by blast lemma Zorns_po_lemma: @@ -463,42 +488,49 @@ and u: "\C\Chains r. \u\Field r. \a\C. (a, u) \ r" shows "\m\Field r. \a\Field r. (m, a) \ r \ a = m" proof - - have "Preorder r" using po by (simp add: partial_order_on_def) -\\Mirror r in the set of subsets below (wrt r) elements of A\ - let ?B = "%x. r\ `` {x}" let ?S = "?B ` Field r" - { - fix C assume 1: "C \ ?S" and 2: "\A\C. \B\C. A \ B \ B \ A" + have "Preorder r" + using po by (simp add: partial_order_on_def) + txt \Mirror \r\ in the set of subsets below (wrt \r\) elements of \A\.\ + let ?B = "\x. r\ `` {x}" + let ?S = "?B ` Field r" + have "\u\Field r. \A\C. A \ r\ `` {u}" (is "\u\Field r. ?P u") + if 1: "C \ ?S" and 2: "\A\C. \B\C. A \ B \ B \ A" for C + proof - let ?A = "{x\Field r. \M\C. M = ?B x}" - have "C = ?B ` ?A" using 1 by (auto simp: image_def) + from 1 have "C = ?B ` ?A" by (auto simp: image_def) have "?A \ Chains r" proof (simp add: Chains_def, intro allI impI, elim conjE) fix a b assume "a \ Field r" and "?B a \ C" and "b \ Field r" and "?B b \ C" - hence "?B a \ ?B b \ ?B b \ ?B a" using 2 by auto - thus "(a, b) \ r \ (b, a) \ r" + with 2 have "?B a \ ?B b \ ?B b \ ?B a" by auto + then show "(a, b) \ r \ (b, a) \ r" using \Preorder r\ and \a \ Field r\ and \b \ Field r\ by (simp add:subset_Image1_Image1_iff) qed - then obtain u where uA: "u \ Field r" "\a\?A. (a, u) \ r" using u by auto - have "\A\C. A \ r\ `` {u}" (is "?P u") + with u obtain u where uA: "u \ Field r" "\a\?A. (a, u) \ r" by auto + have "?P u" proof auto fix a B assume aB: "B \ C" "a \ B" with 1 obtain x where "x \ Field r" and "B = r\ `` {x}" by auto - thus "(a, u) \ r" using uA and aB and \Preorder r\ + then show "(a, u) \ r" + using uA and aB and \Preorder r\ unfolding preorder_on_def refl_on_def by simp (fast dest: transD) qed - then have "\u\Field r. ?P u" using \u \ Field r\ by blast - } + then show ?thesis + using \u \ Field r\ by blast + qed then have "\C\chains ?S. \U\?S. \A\C. A \ U" by (auto simp: chains_def chain_subset_def) - from Zorn_Lemma2 [OF this] - obtain m B where "m \ Field r" and "B = r\ `` {m}" - and "\x\Field r. B \ r\ `` {x} \ r\ `` {x} = B" + from Zorn_Lemma2 [OF this] obtain m B + where "m \ Field r" + and "B = r\ `` {m}" + and "\x\Field r. B \ r\ `` {x} \ r\ `` {x} = B" by auto - hence "\a\Field r. (m, a) \ r \ a = m" + then have "\a\Field r. (m, a) \ r \ a = m" using po and \Preorder r\ and \m \ Field r\ by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) - thus ?thesis using \m \ Field r\ by blast + then show ?thesis + using \m \ Field r\ by blast qed @@ -509,13 +541,12 @@ Definition correct/most general? Naming? *) -definition init_seg_of :: "(('a \ 'a) set \ ('a \ 'a) set) set" where - "init_seg_of = {(r, s). r \ s \ (\a b c. (a, b) \ s \ (b, c) \ r \ (a, b) \ r)}" +definition init_seg_of :: "(('a \ 'a) set \ ('a \ 'a) set) set" + where "init_seg_of = {(r, s). r \ s \ (\a b c. (a, b) \ s \ (b, c) \ r \ (a, b) \ r)}" -abbreviation - initialSegmentOf :: "('a \ 'a) set \ ('a \ 'a) set \ bool" (infix "initial'_segment'_of" 55) -where - "r initial_segment_of s \ (r, s) \ init_seg_of" +abbreviation initial_segment_of_syntax :: "('a \ 'a) set \ ('a \ 'a) set \ bool" + (infix "initial'_segment'_of" 55) + where "r initial_segment_of s \ (r, s) \ init_seg_of" lemma refl_on_init_seg_of [simp]: "r initial_segment_of r" by (simp add: init_seg_of_def) @@ -524,85 +555,97 @@ "r initial_segment_of s \ s initial_segment_of t \ r initial_segment_of t" by (simp (no_asm_use) add: init_seg_of_def) blast -lemma antisym_init_seg_of: - "r initial_segment_of s \ s initial_segment_of r \ r = s" +lemma antisym_init_seg_of: "r initial_segment_of s \ s initial_segment_of r \ r = s" unfolding init_seg_of_def by safe -lemma Chains_init_seg_of_Union: - "R \ Chains init_seg_of \ r\R \ r initial_segment_of \R" +lemma Chains_init_seg_of_Union: "R \ Chains init_seg_of \ r\R \ r initial_segment_of \R" by (auto simp: init_seg_of_def Ball_def Chains_def) blast lemma chain_subset_trans_Union: assumes "chain\<^sub>\ R" "\r\R. trans r" shows "trans (\R)" proof (intro transI, elim UnionE) - fix S1 S2 :: "'a rel" and x y z :: 'a + fix S1 S2 :: "'a rel" and x y z :: 'a assume "S1 \ R" "S2 \ R" - with assms(1) have "S1 \ S2 \ S2 \ S1" unfolding chain_subset_def by blast + with assms(1) have "S1 \ S2 \ S2 \ S1" + unfolding chain_subset_def by blast moreover assume "(x, y) \ S1" "(y, z) \ S2" - ultimately have "((x, y) \ S1 \ (y, z) \ S1) \ ((x, y) \ S2 \ (y, z) \ S2)" by blast - with \S1 \ R\ \S2 \ R\ assms(2) show "(x, z) \ \R" by (auto elim: transE) + ultimately have "((x, y) \ S1 \ (y, z) \ S1) \ ((x, y) \ S2 \ (y, z) \ S2)" + by blast + with \S1 \ R\ \S2 \ R\ assms(2) show "(x, z) \ \R" + by (auto elim: transE) qed lemma chain_subset_antisym_Union: assumes "chain\<^sub>\ R" "\r\R. antisym r" shows "antisym (\R)" proof (intro antisymI, elim UnionE) - fix S1 S2 :: "'a rel" and x y :: 'a + fix S1 S2 :: "'a rel" and x y :: 'a assume "S1 \ R" "S2 \ R" - with assms(1) have "S1 \ S2 \ S2 \ S1" unfolding chain_subset_def by blast + with assms(1) have "S1 \ S2 \ S2 \ S1" + unfolding chain_subset_def by blast moreover assume "(x, y) \ S1" "(y, x) \ S2" - ultimately have "((x, y) \ S1 \ (y, x) \ S1) \ ((x, y) \ S2 \ (y, x) \ S2)" by blast - with \S1 \ R\ \S2 \ R\ assms(2) show "x = y" unfolding antisym_def by auto + ultimately have "((x, y) \ S1 \ (y, x) \ S1) \ ((x, y) \ S2 \ (y, x) \ S2)" + by blast + with \S1 \ R\ \S2 \ R\ assms(2) show "x = y" + unfolding antisym_def by auto qed lemma chain_subset_Total_Union: assumes "chain\<^sub>\ R" and "\r\R. Total r" shows "Total (\R)" proof (simp add: total_on_def Ball_def, auto del: disjCI) - fix r s a b assume A: "r \ R" "s \ R" "a \ Field r" "b \ Field s" "a \ b" + fix r s a b + assume A: "r \ R" "s \ R" "a \ Field r" "b \ Field s" "a \ b" from \chain\<^sub>\ R\ and \r \ R\ and \s \ R\ have "r \ s \ s \ r" by (auto simp add: chain_subset_def) - thus "(\r\R. (a, b) \ r) \ (\r\R. (b, a) \ r)" + then show "(\r\R. (a, b) \ r) \ (\r\R. (b, a) \ r)" proof - assume "r \ s" hence "(a, b) \ s \ (b, a) \ s" using assms(2) A mono_Field[of r s] + assume "r \ s" + then have "(a, b) \ s \ (b, a) \ s" + using assms(2) A mono_Field[of r s] by (auto simp add: total_on_def) - thus ?thesis using \s \ R\ by blast + then show ?thesis + using \s \ R\ by blast next - assume "s \ r" hence "(a, b) \ r \ (b, a) \ r" using assms(2) A mono_Field[of s r] + assume "s \ r" + then have "(a, b) \ r \ (b, a) \ r" + using assms(2) A mono_Field[of s r] by (fastforce simp add: total_on_def) - thus ?thesis using \r \ R\ by blast + then show ?thesis + using \r \ R\ by blast qed qed lemma wf_Union_wf_init_segs: - assumes "R \ Chains init_seg_of" and "\r\R. wf r" + assumes "R \ Chains init_seg_of" + and "\r\R. wf r" shows "wf (\R)" -proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto) - fix f assume 1: "\i. \r\R. (f (Suc i), f i) \ r" +proof (simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto) + fix f + assume 1: "\i. \r\R. (f (Suc i), f i) \ r" then obtain r where "r \ R" and "(f (Suc 0), f 0) \ r" by auto - { fix i have "(f (Suc i), f i) \ r" - proof (induct i) - case 0 show ?case by fact - next - case (Suc i) - then obtain s where s: "s \ R" "(f (Suc (Suc i)), f(Suc i)) \ s" - using 1 by auto - then have "s initial_segment_of r \ r initial_segment_of s" - using assms(1) \r \ R\ by (simp add: Chains_def) - with Suc s show ?case by (simp add: init_seg_of_def) blast - qed - } - thus False using assms(2) and \r \ R\ + have "(f (Suc i), f i) \ r" for i + proof (induct i) + case 0 + show ?case by fact + next + case (Suc i) + then obtain s where s: "s \ R" "(f (Suc (Suc i)), f(Suc i)) \ s" + using 1 by auto + then have "s initial_segment_of r \ r initial_segment_of s" + using assms(1) \r \ R\ by (simp add: Chains_def) + with Suc s show ?case by (simp add: init_seg_of_def) blast + qed + then show False + using assms(2) and \r \ R\ by (simp add: wf_iff_no_infinite_down_chain) blast qed -lemma initial_segment_of_Diff: - "p initial_segment_of q \ p - s initial_segment_of q - s" +lemma initial_segment_of_Diff: "p initial_segment_of q \ p - s initial_segment_of q - s" unfolding init_seg_of_def by blast -lemma Chains_inits_DiffI: - "R \ Chains init_seg_of \ {r - s |r. r \ R} \ Chains init_seg_of" +lemma Chains_inits_DiffI: "R \ Chains init_seg_of \ {r - s |r. r \ R} \ Chains init_seg_of" unfolding Chains_def by (blast intro: initial_segment_of_Diff) theorem well_ordering: "\r::'a rel. Well_order r \ Field r = UNIV" @@ -610,24 +653,28 @@ \ \The initial segment relation on well-orders:\ let ?WO = "{r::'a rel. Well_order r}" define I where "I = init_seg_of \ ?WO \ ?WO" - have I_init: "I \ init_seg_of" by (auto simp: I_def) - hence subch: "\R. R \ Chains I \ chain\<^sub>\ R" + then have I_init: "I \ init_seg_of" by simp + then have subch: "\R. R \ Chains I \ chain\<^sub>\ R" unfolding init_seg_of_def chain_subset_def Chains_def by blast have Chains_wo: "\R r. R \ Chains I \ r \ R \ Well_order r" by (simp add: Chains_def I_def) blast - have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def) - hence 0: "Partial_order I" + have FI: "Field I = ?WO" + by (auto simp add: I_def init_seg_of_def Field_def) + then have 0: "Partial_order I" by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def - trans_def I_def elim!: trans_init_seg_of) -\ \I-chains have upper bounds in ?WO wrt I: their Union\ - { fix R assume "R \ Chains I" - hence Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast - have subch: "chain\<^sub>\ R" using \R : Chains I\ I_init - by (auto simp: init_seg_of_def chain_subset_def Chains_def) + trans_def I_def elim!: trans_init_seg_of) +\ \\I\-chains have upper bounds in \?WO\ wrt \I\: their Union\ + have "\R \ ?WO \ (\r\R. (r, \R) \ I)" if "R \ Chains I" for R + proof - + from that have Ris: "R \ Chains init_seg_of" + using mono_Chains [OF I_init] by blast + have subch: "chain\<^sub>\ R" + using \R : Chains I\ I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def) have "\r\R. Refl r" and "\r\R. trans r" and "\r\R. antisym r" and "\r\R. Total r" and "\r\R. wf (r - Id)" using Chains_wo [OF \R \ Chains I\] by (simp_all add: order_on_defs) - have "Refl (\R)" using \\r\R. Refl r\ unfolding refl_on_def by fastforce + have "Refl (\R)" + using \\r\R. Refl r\ unfolding refl_on_def by fastforce moreover have "trans (\R)" by (rule chain_subset_trans_Union [OF subch \\r\R. trans r\]) moreover have "antisym (\R)" @@ -640,21 +687,25 @@ with \\r\R. wf (r - Id)\ and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] show ?thesis by fastforce qed - ultimately have "Well_order (\R)" by(simp add:order_on_defs) - moreover have "\r \ R. r initial_segment_of \R" using Ris - by(simp add: Chains_init_seg_of_Union) - ultimately have "\R \ ?WO \ (\r\R. (r, \R) \ I)" + ultimately have "Well_order (\R)" + by (simp add:order_on_defs) + moreover have "\r \ R. r initial_segment_of \R" + using Ris by (simp add: Chains_init_seg_of_Union) + ultimately show ?thesis using mono_Chains [OF I_init] Chains_wo[of R] and \R \ Chains I\ unfolding I_def by blast - } - hence 1: "\R \ Chains I. \u\Field I. \r\R. (r, u) \ I" by (subst FI) blast -\\Zorn's Lemma yields a maximal well-order m:\ - then obtain m::"'a rel" where "Well_order m" and - max: "\r. Well_order r \ (m, r) \ I \ r = m" + qed + then have 1: "\R \ Chains I. \u\Field I. \r\R. (r, u) \ I" + by (subst FI) blast +\\Zorn's Lemma yields a maximal well-order \m\:\ + then obtain m :: "'a rel" + where "Well_order m" + and max: "\r. Well_order r \ (m, r) \ I \ r = m" using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce -\\Now show by contradiction that m covers the whole type:\ - { fix x::'a assume "x \ Field m" -\\We assume that x is not covered and extend m at the top with x\ +\\Now show by contradiction that \m\ covers the whole type:\ + have False if "x \ Field m" for x :: 'a + proof - +\\Assuming that \x\ is not covered and extend \m\ at the top with \x\\ have "m \ {}" proof assume "m = {}" @@ -663,10 +714,10 @@ ultimately show False using max by (auto simp: I_def init_seg_of_def simp del: Field_insert) qed - hence "Field m \ {}" by(auto simp:Field_def) - moreover have "wf (m - Id)" using \Well_order m\ - by (simp add: well_order_on_def) -\\The extension of m by x:\ + then have "Field m \ {}" by (auto simp: Field_def) + moreover have "wf (m - Id)" + using \Well_order m\ by (simp add: well_order_on_def) +\\The extension of \m\ by \x\:\ let ?s = "{(a, x) | a. a \ Field m}" let ?m = "insert (x, x) m \ ?s" have Fm: "Field ?m = insert x (Field m)" @@ -674,49 +725,58 @@ have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" using \Well_order m\ by (simp_all add: order_on_defs) \\We show that the extension is a well-order\ - have "Refl ?m" using \Refl m\ Fm unfolding refl_on_def by blast + have "Refl ?m" + using \Refl m\ Fm unfolding refl_on_def by blast moreover have "trans ?m" using \trans m\ and \x \ Field m\ unfolding trans_def Field_def by blast - moreover have "antisym ?m" using \antisym m\ and \x \ Field m\ - unfolding antisym_def Field_def by blast - moreover have "Total ?m" using \Total m\ and Fm by (auto simp: total_on_def) + moreover have "antisym ?m" + using \antisym m\ and \x \ Field m\ unfolding antisym_def Field_def by blast + moreover have "Total ?m" + using \Total m\ and Fm by (auto simp: total_on_def) moreover have "wf (?m - Id)" proof - - have "wf ?s" using \x \ Field m\ - by (auto simp: wf_eq_minimal Field_def Bex_def) - thus ?thesis using \wf (m - Id)\ and \x \ Field m\ - wf_subset [OF \wf ?s\ Diff_subset] + have "wf ?s" + using \x \ Field m\ by (auto simp: wf_eq_minimal Field_def Bex_def) + then show ?thesis + using \wf (m - Id)\ and \x \ Field m\ wf_subset [OF \wf ?s\ Diff_subset] by (auto simp: Un_Diff Field_def intro: wf_Un) qed - ultimately have "Well_order ?m" by (simp add: order_on_defs) -\\We show that the extension is above m\ - moreover have "(m, ?m) \ I" using \Well_order ?m\ and \Well_order m\ and \x \ Field m\ + ultimately have "Well_order ?m" + by (simp add: order_on_defs) +\\We show that the extension is above \m\\ + moreover have "(m, ?m) \ I" + using \Well_order ?m\ and \Well_order m\ and \x \ Field m\ by (fastforce simp: I_def init_seg_of_def Field_def) ultimately -\\This contradicts maximality of m:\ - have False using max and \x \ Field m\ unfolding Field_def by blast - } - hence "Field m = UNIV" by auto +\\This contradicts maximality of \m\:\ + show False + using max and \x \ Field m\ unfolding Field_def by blast + qed + then have "Field m = UNIV" by auto with \Well_order m\ show ?thesis by blast qed corollary well_order_on: "\r::'a rel. well_order_on A r" proof - - obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV" + obtain r :: "'a rel" where wo: "Well_order r" and univ: "Field r = UNIV" using well_ordering [where 'a = "'a"] by blast let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}" - have 1: "Field ?r = A" using wo univ - by (fastforce simp: Field_def order_on_defs refl_on_def) - have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)" - using \Well_order r\ by (simp_all add: order_on_defs) - have "Refl ?r" using \Refl r\ by (auto simp: refl_on_def 1 univ) - moreover have "trans ?r" using \trans r\ + have 1: "Field ?r = A" + using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def) + from \Well_order r\ have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" + by (simp_all add: order_on_defs) + from \Refl r\ have "Refl ?r" + by (auto simp: refl_on_def 1 univ) + moreover from \trans r\ have "trans ?r" unfolding trans_def by blast - moreover have "antisym ?r" using \antisym r\ + moreover from \antisym r\ have "antisym ?r" unfolding antisym_def by blast - moreover have "Total ?r" using \Total r\ by (simp add:total_on_def 1 univ) - moreover have "wf (?r - Id)" by (rule wf_subset [OF \wf (r - Id)\]) blast - ultimately have "Well_order ?r" by (simp add: order_on_defs) + moreover from \Total r\ have "Total ?r" + by (simp add:total_on_def 1 univ) + moreover have "wf (?r - Id)" + by (rule wf_subset [OF \wf (r - Id)\]) blast + ultimately have "Well_order ?r" + by (simp add: order_on_defs) with 1 show ?thesis by auto qed @@ -727,15 +787,16 @@ lemma dependent_wf_choice: fixes P :: "('a \ 'b) \ 'a \ 'b \ bool" - assumes "wf R" and adm: "\f g x r. (\z. (z, x) \ R \ f z = g z) \ P f x r = P g x r" - assumes P: "\x f. (\y. (y, x) \ R \ P f y (f y)) \ \r. P f x r" + assumes "wf R" + and adm: "\f g x r. (\z. (z, x) \ R \ f z = g z) \ P f x r = P g x r" + and P: "\x f. (\y. (y, x) \ R \ P f y (f y)) \ \r. P f x r" shows "\f. \x. P f x (f x)" proof (intro exI allI) - fix x + fix x define f where "f \ wfrec R (\f x. SOME r. P f x r)" from \wf R\ show "P f x (f x)" proof (induct x) - fix x assume "\y. (y, x) \ R \ P f y (f y)" + case (less x) show "P f x (f x)" proof (subst (2) wfrec_def_adm[OF f_def \wf R\]) show "adm_wf R (\f x. SOME r. P f x r)" @@ -748,7 +809,7 @@ lemma (in wellorder) dependent_wellorder_choice: assumes "\r f g x. (\y. y < x \ f y = g y) \ P f x r = P g x r" - assumes P: "\x f. (\y. y < x \ P f y (f y)) \ \r. P f x r" + and P: "\x f. (\y. y < x \ P f y (f y)) \ \r. P f x r" shows "\f. \x. P f x (f x)" using wf by (rule dependent_wf_choice) (auto intro!: assms)