# HG changeset patch # User wenzelm # Date 1468346598 -7200 # Node ID d7610beb98bc978edb8b8721d7755d77f6b28fe4 # Parent 9d4dbb7a548a9939ed903a32f43625545fb09cae misc tuning and modernization; diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Continuum_Not_Denumerable.thy --- a/src/HOL/Library/Continuum_Not_Denumerable.thy Tue Jul 12 19:12:17 2016 +0200 +++ b/src/HOL/Library/Continuum_Not_Denumerable.thy Tue Jul 12 20:03:18 2016 +0200 @@ -11,36 +11,38 @@ subsection \Abstract\ -text \The following document presents a proof that the Continuum is -uncountable. It is formalised in the Isabelle/Isar theorem proving -system. +text \ + The following document presents a proof that the Continuum is uncountable. + It is formalised in the Isabelle/Isar theorem proving system. -{\em Theorem:} The Continuum \\\ is not denumerable. In other -words, there does not exist a function \f: \ \ \\ such that f is -surjective. + \<^bold>\Theorem:\ The Continuum \\\ is not denumerable. In other words, there does + not exist a function \f: \ \ \\ such that f is surjective. + + \<^bold>\Outline:\ An elegant informal proof of this result uses Cantor's + Diagonalisation argument. The proof presented here is not this one. -{\em Outline:} An elegant informal proof of this result uses Cantor's -Diagonalisation argument. The proof presented here is not this -one. First we formalise some properties of closed intervals, then we -prove the Nested Interval Property. This property relies on the -completeness of the Real numbers and is the foundation for our -argument. Informally it states that an intersection of countable -closed intervals (where each successive interval is a subset of the -last) is non-empty. We then assume a surjective function \f: \ \ \\ exists and find a real x such that x is not in the range of f -by generating a sequence of closed intervals then using the NIP.\ + First we formalise some properties of closed intervals, then we prove the + Nested Interval Property. This property relies on the completeness of the + Real numbers and is the foundation for our argument. Informally it states + that an intersection of countable closed intervals (where each successive + interval is a subset of the last) is non-empty. We then assume a surjective + function \f: \ \ \\ exists and find a real \x\ such that \x\ is not in the + range of \f\ by generating a sequence of closed intervals then using the + NIP. +\ -theorem real_non_denum: "\ (\f :: nat \ real. surj f)" +theorem real_non_denum: "\f :: nat \ real. surj f" proof assume "\f::nat \ real. surj f" then obtain f :: "nat \ real" where "surj f" .. txt \First we construct a sequence of nested intervals, ignoring @{term "range f"}.\ - have "\a b c::real. a < b \ (\ka kb. ka < kb \ {ka..kb} \ {a..b} \ c \ {ka..kb})" + have "a < b \ \ka kb. ka < kb \ {ka..kb} \ {a..b} \ c \ {ka..kb}" for a b c :: real by (auto simp add: not_le cong: conj_cong) - (metis dense le_less_linear less_linear less_trans order_refl) + (metis dense le_less_linear less_linear less_trans order_refl) then obtain i j where ij: - "a < b \ i a b c < j a b c" + "a < b \ i a b c < j a b c" "a < b \ {i a b c .. j a b c} \ {a .. b}" "a < b \ c \ {i a b c .. j a b c}" for a b c :: real @@ -50,29 +52,31 @@ rec_nat (f 0 + 1, f 0 + 2) (\n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))" define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n - have ivl[simp]: + have ivl [simp]: "ivl 0 = (f 0 + 1, f 0 + 2)" "\n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))" unfolding ivl_def by simp_all txt \This is a decreasing sequence of non-empty intervals.\ - { fix n have "fst (ivl n) < snd (ivl n)" - by (induct n) (auto intro!: ij) } - note less = this + have less: "fst (ivl n) < snd (ivl n)" for n + by (induct n) (auto intro!: ij) have "decseq I" - unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less) + unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv + by (intro ij allI less) txt \Now we apply the finite intersection property of compact sets.\ have "I 0 \ (\i. I i) \ {}" proof (rule compact_imp_fip_image) - fix S :: "nat set" assume fin: "finite S" + fix S :: "nat set" + assume fin: "finite S" have "{} \ I (Max (insert 0 S))" unfolding I_def using less[of "Max (insert 0 S)"] by auto also have "I (Max (insert 0 S)) \ (\i\insert 0 S. I i)" - using fin decseqD[OF \decseq I\, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff) + using fin decseqD[OF \decseq I\, of _ "Max (insert 0 S)"] + by (auto simp: Max_ge_iff) also have "(\i\insert 0 S. I i) = I 0 \ (\i\S. I i)" by auto finally show "I 0 \ (\i\S. I i) \ {}" @@ -88,7 +92,7 @@ unfolding I_def ivl fst_conv snd_conv by auto qed -lemma uncountable_UNIV_real: "uncountable (UNIV::real set)" +lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)" using real_non_denum unfolding uncountable_def by auto lemma bij_betw_open_intervals: @@ -97,31 +101,29 @@ shows "\f. bij_betw f {a<.. a < b" +lemma uncountable_open_interval: "uncountable {a<.. a < b" for a b :: real proof - assume "uncountable {a<..a < b\, of "-pi/2" "pi/2"] by auto @@ -130,38 +132,44 @@ qed qed -lemma uncountable_half_open_interval_1: - fixes a :: real shows "uncountable {a.. a a < b" for a b :: real apply auto - using atLeastLessThan_empty_iff apply fastforce + using atLeastLessThan_empty_iff + apply fastforce using uncountable_open_interval [of a b] - by (metis countable_Un_iff ivl_disj_un_singleton(3)) + apply (metis countable_Un_iff ivl_disj_un_singleton(3)) + done -lemma uncountable_half_open_interval_2: - fixes a :: real shows "uncountable {a<..b} \ a a < b" for a b :: real apply auto - using atLeastLessThan_empty_iff apply fastforce + using atLeastLessThan_empty_iff + apply fastforce using uncountable_open_interval [of a b] - by (metis countable_Un_iff ivl_disj_un_singleton(4)) + apply (metis countable_Un_iff ivl_disj_un_singleton(4)) + done lemma real_interval_avoid_countable_set: fixes a b :: real and A :: "real set" assumes "a < b" and "countable A" shows "\x\{a<.. A" proof - - from \countable A\ have "countable (A \ {a<..a < b\ have "\ countable {a<..countable A\ have "countable (A \ {a<..a < b\ have "\ countable {a<.. {a<.. {a<.. {a<.. {a<..x. x \ {a<.. {a<.. {a<.. {a<.. {a<.. {a<..x. x \ {a<.. {a<.. {}" "open S" + fixes S A :: "real set" + assumes "countable A" "S \ {}" "open S" shows "\x\S. x \ A" proof - obtain x where "x \ S" diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Prefix_Order.thy --- a/src/HOL/Library/Prefix_Order.thy Tue Jul 12 19:12:17 2016 +0200 +++ b/src/HOL/Library/Prefix_Order.thy Tue Jul 12 20:03:18 2016 +0200 @@ -11,16 +11,16 @@ instantiation list :: (type) order begin -definition "(xs::'a list) \ ys \ prefix xs ys" -definition "(xs::'a list) < ys \ xs \ ys \ \ (ys \ xs)" +definition "xs \ ys \ prefix xs ys" for xs ys :: "'a list" +definition "xs < ys \ xs \ ys \ \ (ys \ xs)" for xs ys :: "'a list" instance by standard (auto simp: less_eq_list_def less_list_def) end -lemma less_list_def': "(xs::'a list) < ys \ strict_prefix xs ys" -by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le) +lemma less_list_def': "xs < ys \ strict_prefix xs ys" for xs ys :: "'a list" + by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le) lemmas prefixI [intro?] = prefixI [folded less_eq_list_def] lemmas prefixE [elim?] = prefixE [folded less_eq_list_def] diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Preorder.thy --- a/src/HOL/Library/Preorder.thy Tue Jul 12 19:12:17 2016 +0200 +++ b/src/HOL/Library/Preorder.thy Tue Jul 12 20:03:18 2016 +0200 @@ -9,24 +9,21 @@ class preorder_equiv = preorder begin -definition equiv :: "'a \ 'a \ bool" where - "equiv x y \ x \ y \ y \ x" +definition equiv :: "'a \ 'a \ bool" + where "equiv x y \ x \ y \ y \ x" notation equiv ("op \") and equiv ("(_/ \ _)" [51, 51] 50) -lemma refl [iff]: - "x \ x" - unfolding equiv_def by simp +lemma refl [iff]: "x \ x" + by (simp add: equiv_def) -lemma trans: - "x \ y \ y \ z \ x \ z" - unfolding equiv_def by (auto intro: order_trans) +lemma trans: "x \ y \ y \ z \ x \ z" + by (auto simp: equiv_def intro: order_trans) -lemma antisym: - "x \ y \ y \ x \ x \ y" - unfolding equiv_def .. +lemma antisym: "x \ y \ y \ x \ x \ y" + by (simp only: equiv_def) lemma less_le: "x < y \ x \ y \ \ x \ y" by (auto simp add: equiv_def less_le_not_le) diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Quadratic_Discriminant.thy --- a/src/HOL/Library/Quadratic_Discriminant.thy Tue Jul 12 19:12:17 2016 +0200 +++ b/src/HOL/Library/Quadratic_Discriminant.thy Tue Jul 12 20:03:18 2016 +0200 @@ -10,8 +10,8 @@ imports Complex_Main begin -definition discrim :: "[real,real,real] \ real" where - "discrim a b c \ b\<^sup>2 - 4 * a * c" +definition discrim :: "real \ real \ real \ real" + where "discrim a b c \ b\<^sup>2 - 4 * a * c" lemma complete_square: fixes a b c x :: "real" @@ -23,20 +23,22 @@ with \a \ 0\ have "a * x\<^sup>2 + b * x + c = 0 \ 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0" by simp - thus "a * x\<^sup>2 + b * x + c = 0 \ (2 * a * x + b)\<^sup>2 = discrim a b c" - unfolding discrim_def - by (simp add: power2_eq_square algebra_simps) + then show "a * x\<^sup>2 + b * x + c = 0 \ (2 * a * x + b)\<^sup>2 = discrim a b c" + by (simp add: discrim_def power2_eq_square algebra_simps) qed lemma discriminant_negative: fixes a b c x :: real assumes "a \ 0" - and "discrim a b c < 0" + and "discrim a b c < 0" shows "a * x\<^sup>2 + b * x + c \ 0" proof - - have "(2 * a * x + b)\<^sup>2 \ 0" by simp - with \discrim a b c < 0\ have "(2 * a * x + b)\<^sup>2 \ discrim a b c" by arith - with complete_square and \a \ 0\ show "a * x\<^sup>2 + b * x + c \ 0" by simp + have "(2 * a * x + b)\<^sup>2 \ 0" + by simp + with \discrim a b c < 0\ have "(2 * a * x + b)\<^sup>2 \ discrim a b c" + by arith + with complete_square and \a \ 0\ show "a * x\<^sup>2 + b * x + c \ 0" + by simp qed lemma plus_or_minus_sqrt: @@ -45,13 +47,18 @@ shows "x\<^sup>2 = y \ x = sqrt y \ x = - sqrt y" proof assume "x\<^sup>2 = y" - hence "sqrt (x\<^sup>2) = sqrt y" by simp - hence "sqrt y = \x\" by simp - thus "x = sqrt y \ x = - sqrt y" by auto + then have "sqrt (x\<^sup>2) = sqrt y" + by simp + then have "sqrt y = \x\" + by simp + then show "x = sqrt y \ x = - sqrt y" + by auto next assume "x = sqrt y \ x = - sqrt y" - hence "x\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2" by auto - with \y \ 0\ show "x\<^sup>2 = y" by simp + then have "x\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2" + by auto + with \y \ 0\ show "x\<^sup>2 = y" + by simp qed lemma divide_non_zero: @@ -59,20 +66,19 @@ assumes "x \ 0" shows "x * y = z \ y = z / x" proof - assume "x * y = z" - with \x \ 0\ show "y = z / x" by (simp add: field_simps) -next - assume "y = z / x" - with \x \ 0\ show "x * y = z" by simp + show "y = z / x" if "x * y = z" + using \x \ 0\ that by (simp add: field_simps) + show "x * y = z" if "y = z / x" + using \x \ 0\ that by simp qed lemma discriminant_nonneg: fixes a b c x :: real assumes "a \ 0" - and "discrim a b c \ 0" + and "discrim a b c \ 0" shows "a * x\<^sup>2 + b * x + c = 0 \ - x = (-b + sqrt (discrim a b c)) / (2 * a) \ - x = (-b - sqrt (discrim a b c)) / (2 * a)" + x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a)" proof - from complete_square and plus_or_minus_sqrt and assms have "a * x\<^sup>2 + b * x + c = 0 \ @@ -94,88 +100,93 @@ lemma discriminant_zero: fixes a b c x :: real assumes "a \ 0" - and "discrim a b c = 0" + and "discrim a b c = 0" shows "a * x\<^sup>2 + b * x + c = 0 \ x = -b / (2 * a)" - using discriminant_nonneg and assms - by simp + by (simp add: discriminant_nonneg assms) theorem discriminant_iff: fixes a b c x :: real assumes "a \ 0" shows "a * x\<^sup>2 + b * x + c = 0 \ - discrim a b c \ 0 \ - (x = (-b + sqrt (discrim a b c)) / (2 * a) \ - x = (-b - sqrt (discrim a b c)) / (2 * a))" + discrim a b c \ 0 \ + (x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a))" proof assume "a * x\<^sup>2 + b * x + c = 0" - with discriminant_negative and \a \ 0\ have "\(discrim a b c < 0)" by auto - hence "discrim a b c \ 0" by simp + with discriminant_negative and \a \ 0\ have "\(discrim a b c < 0)" + by auto + then have "discrim a b c \ 0" + by simp with discriminant_nonneg and \a * x\<^sup>2 + b * x + c = 0\ and \a \ 0\ have "x = (-b + sqrt (discrim a b c)) / (2 * a) \ - x = (-b - sqrt (discrim a b c)) / (2 * a)" + x = (-b - sqrt (discrim a b c)) / (2 * a)" by simp with \discrim a b c \ 0\ show "discrim a b c \ 0 \ (x = (-b + sqrt (discrim a b c)) / (2 * a) \ - x = (-b - sqrt (discrim a b c)) / (2 * a))" .. + x = (-b - sqrt (discrim a b c)) / (2 * a))" .. next assume "discrim a b c \ 0 \ (x = (-b + sqrt (discrim a b c)) / (2 * a) \ - x = (-b - sqrt (discrim a b c)) / (2 * a))" - hence "discrim a b c \ 0" and + x = (-b - sqrt (discrim a b c)) / (2 * a))" + then have "discrim a b c \ 0" and "x = (-b + sqrt (discrim a b c)) / (2 * a) \ - x = (-b - sqrt (discrim a b c)) / (2 * a)" + x = (-b - sqrt (discrim a b c)) / (2 * a)" by simp_all - with discriminant_nonneg and \a \ 0\ show "a * x\<^sup>2 + b * x + c = 0" by simp + with discriminant_nonneg and \a \ 0\ show "a * x\<^sup>2 + b * x + c = 0" + by simp qed lemma discriminant_nonneg_ex: fixes a b c :: real assumes "a \ 0" - and "discrim a b c \ 0" + and "discrim a b c \ 0" shows "\ x. a * x\<^sup>2 + b * x + c = 0" - using discriminant_nonneg and assms - by auto + by (auto simp: discriminant_nonneg assms) lemma discriminant_pos_ex: fixes a b c :: real assumes "a \ 0" - and "discrim a b c > 0" - shows "\ x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ a * y\<^sup>2 + b * y + c = 0" + and "discrim a b c > 0" + shows "\x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ a * y\<^sup>2 + b * y + c = 0" proof - let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)" let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)" - from \discrim a b c > 0\ have "sqrt (discrim a b c) \ 0" by simp - hence "sqrt (discrim a b c) \ - sqrt (discrim a b c)" by arith - with \a \ 0\ have "?x \ ?y" by simp - moreover - from discriminant_nonneg [of a b c ?x] - and discriminant_nonneg [of a b c ?y] - and assms - have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all - ultimately - show "\ x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ a * y\<^sup>2 + b * y + c = 0" by blast + from \discrim a b c > 0\ have "sqrt (discrim a b c) \ 0" + by simp + then have "sqrt (discrim a b c) \ - sqrt (discrim a b c)" + by arith + with \a \ 0\ have "?x \ ?y" + by simp + moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" + using discriminant_nonneg [of a b c ?x] + and discriminant_nonneg [of a b c ?y] + by simp_all + ultimately show ?thesis + by blast qed lemma discriminant_pos_distinct: fixes a b c x :: real - assumes "a \ 0" and "discrim a b c > 0" + assumes "a \ 0" + and "discrim a b c > 0" shows "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" proof - from discriminant_pos_ex and \a \ 0\ and \discrim a b c > 0\ obtain w and z where "w \ z" and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0" by blast - show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" - proof cases - assume "x = w" - with \w \ z\ have "x \ z" by simp - with \a * z\<^sup>2 + b * z + c = 0\ - show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" by auto + show "\y. x \ y \ a * y\<^sup>2 + b * y + c = 0" + proof (cases "x = w") + case True + with \w \ z\ have "x \ z" + by simp + with \a * z\<^sup>2 + b * z + c = 0\ show ?thesis + by auto next - assume "x \ w" - with \a * w\<^sup>2 + b * w + c = 0\ - show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" by auto + case False + with \a * w\<^sup>2 + b * w + c = 0\ show ?thesis + by auto qed qed diff -r 9d4dbb7a548a -r d7610beb98bc src/HOL/Library/Sublist_Order.thy --- a/src/HOL/Library/Sublist_Order.thy Tue Jul 12 19:12:17 2016 +0200 +++ b/src/HOL/Library/Sublist_Order.thy Tue Jul 12 20:03:18 2016 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/Library/Sublist_Order.thy - Authors: Peter Lammich, Uni Muenster - Florian Haftmann, Tobias Nipkow, TU Muenchen + Author: Peter Lammich, Uni Muenster + Author: Florian Haftmann, , TU Muenchen + Author: Tobias Nipkow, TU Muenchen *) section \Sublist Ordering\ @@ -10,9 +11,8 @@ begin text \ - This theory defines sublist ordering on lists. - A list \ys\ is a sublist of a list \xs\, - iff one obtains \ys\ by erasing some elements from \xs\. + This theory defines sublist ordering on lists. A list \ys\ is a sublist of a + list \xs\, iff one obtains \ys\ by erasing some elements from \xs\. \ subsection \Definitions and basic lemmas\ @@ -20,11 +20,8 @@ instantiation list :: (type) ord begin -definition - "(xs :: 'a list) \ ys \ sublisteq xs ys" - -definition - "(xs :: 'a list) < ys \ xs \ ys \ \ ys \ xs" +definition "xs \ ys \ sublisteq xs ys" for xs ys :: "'a list" +definition "xs < ys \ xs \ ys \ \ ys \ xs" for xs ys :: "'a list" instance .. @@ -32,19 +29,15 @@ instance list :: (type) order proof - fix xs ys :: "'a list" - show "xs < ys \ xs \ ys \ \ ys \ xs" unfolding less_list_def .. -next - fix xs :: "'a list" - show "xs \ xs" by (simp add: less_eq_list_def) -next - fix xs ys :: "'a list" - assume "xs <= ys" and "ys <= xs" - thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym) -next fix xs ys zs :: "'a list" - assume "xs <= ys" and "ys <= zs" - thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans) + show "xs < ys \ xs \ ys \ \ ys \ xs" + unfolding less_list_def .. + show "xs \ xs" + by (simp add: less_eq_list_def) + show "xs = ys" if "xs \ ys" and "ys \ xs" + using that unfolding less_eq_list_def by (rule sublisteq_antisym) + show "xs \ zs" if "xs \ ys" and "ys \ zs" + using that unfolding less_eq_list_def by (rule sublisteq_trans) qed lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = @@ -71,7 +64,8 @@ by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def) lemma less_list_drop_many: "xs < ys \ xs < zs @ ys" - by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def) + by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le + self_append_conv2 less_eq_list_def) lemma less_list_take_many_iff: "zs @ xs < zs @ ys \ xs < ys" by (metis less_list_def less_eq_list_def sublisteq_append')