# HG changeset patch # User huffman # Date 1228919650 28800 # Node ID 9dbf8249d979a67aac1e79a481b3819323264057 # Parent 286c669d3a7a0f3c091b7009aba08ca15f55aaca# Parent df1113d916db73bcdc8f2b6a62da441fdce905f6 merged. diff -r 286c669d3a7a -r 9dbf8249d979 src/FOL/ex/NewLocaleSetup.thy --- a/src/FOL/ex/NewLocaleSetup.thy Tue Dec 09 22:13:16 2008 -0800 +++ b/src/FOL/ex/NewLocaleSetup.thy Wed Dec 10 06:34:10 2008 -0800 @@ -16,7 +16,7 @@ val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; val locale_val = - Expression.parse_expression -- + SpecParse.locale_expression -- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || Scan.repeat1 SpecParse.context_element >> pair ([], []); @@ -27,7 +27,9 @@ (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin >> (fn ((name, (expr, elems)), begin) => (begin ? Toplevel.print) o Toplevel.begin_local_theory begin - (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin))); + (Expression.add_locale_cmd name name expr elems #> + (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes)))); val _ = OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag @@ -42,7 +44,7 @@ val _ = OuterSyntax.command "interpretation" "prove interpretation of locale expression in theory" K.thy_goal - (P.!!! Expression.parse_expression + (P.!!! SpecParse.locale_expression >> (fn expr => Toplevel.print o Toplevel.theory_to_proof (Expression.interpretation_cmd expr))); @@ -50,7 +52,7 @@ OuterSyntax.command "interpret" "prove interpretation of locale expression in proof context" (K.tag_proof K.prf_goal) - (P.!!! Expression.parse_expression + (P.!!! SpecParse.locale_expression >> (fn expr => Toplevel.print o Toplevel.proof' (fn int => Expression.interpret_cmd expr int))); diff -r 286c669d3a7a -r 9dbf8249d979 src/FOL/ex/NewLocaleTest.thy --- a/src/FOL/ex/NewLocaleTest.thy Tue Dec 09 22:13:16 2008 -0800 +++ b/src/FOL/ex/NewLocaleTest.thy Wed Dec 10 06:34:10 2008 -0800 @@ -113,6 +113,12 @@ print_locale! use_decl thm use_decl_def +text {* Foundational versions of theorems *} + +thm logic.assoc +thm logic.lor_def + + text {* Defines *} locale logic_def = @@ -124,12 +130,45 @@ defines "x || y == --(-- x && -- y)" begin +thm lor_def +(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *) + +lemma "x || y = --(-- x && --y)" + by (unfold lor_def) (rule refl) + +end + +(* Inheritance of defines *) + +locale logic_def2 = logic_def +begin + lemma "x || y = --(-- x && --y)" by (unfold lor_def) (rule refl) end +text {* Notes *} + +(* A somewhat arcane homomorphism example *) + +definition semi_hom where + "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" + +lemma semi_hom_mult: + "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" + by (simp add: semi_hom_def) + +locale semi_hom_loc = prod: semi prod + sum: semi sum + for prod and sum and h + + assumes semi_homh: "semi_hom(prod, sum, h)" + notes semi_hom_mult = semi_hom_mult [OF semi_homh] + +lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" + by (rule semi_hom_mult) + + text {* Theorem statements *} lemma (in lgrp) lcancel: diff -r 286c669d3a7a -r 9dbf8249d979 src/HOL/Complex_Main.thy --- a/src/HOL/Complex_Main.thy Tue Dec 09 22:13:16 2008 -0800 +++ b/src/HOL/Complex_Main.thy Wed Dec 10 06:34:10 2008 -0800 @@ -8,7 +8,6 @@ theory Complex_Main imports Main - ContNotDenum Real "~~/src/HOL/Complex/Fundamental_Theorem_Algebra" Log diff -r 286c669d3a7a -r 9dbf8249d979 src/HOL/ContNotDenum.thy --- a/src/HOL/ContNotDenum.thy Tue Dec 09 22:13:16 2008 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,579 +0,0 @@ -(* Title : HOL/ContNonDenum - Author : Benjamin Porter, Monash University, NICTA, 2005 -*) - -header {* Non-denumerability of the Continuum. *} - -theory ContNotDenum -imports RComplete Hilbert_Choice -begin - -subsection {* Abstract *} - -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 @{text "\"} is not denumerable. In other -words, there does not exist a function f:@{text "\\\"} such that f is -surjective. - -{\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:@{text -"\\\"} 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. *} - -subsection {* Closed Intervals *} - -text {* This section formalises some properties of closed intervals. *} - -subsubsection {* Definition *} - -definition - closed_int :: "real \ real \ real set" where - "closed_int x y = {z. x \ z \ z \ y}" - -subsubsection {* Properties *} - -lemma closed_int_subset: - assumes xy: "x1 \ x0" "y1 \ y0" - shows "closed_int x1 y1 \ closed_int x0 y0" -proof - - { - fix x::real - assume "x \ closed_int x1 y1" - hence "x \ x1 \ x \ y1" by (simp add: closed_int_def) - with xy have "x \ x0 \ x \ y0" by auto - hence "x \ closed_int x0 y0" by (simp add: closed_int_def) - } - thus ?thesis by auto -qed - -lemma closed_int_least: - assumes a: "a \ b" - shows "a \ closed_int a b \ (\x \ closed_int a b. a \ x)" -proof - from a have "a\{x. a\x \ x\b}" by simp - thus "a \ closed_int a b" by (unfold closed_int_def) -next - have "\x\{x. a\x \ x\b}. a\x" by simp - thus "\x \ closed_int a b. a \ x" by (unfold closed_int_def) -qed - -lemma closed_int_most: - assumes a: "a \ b" - shows "b \ closed_int a b \ (\x \ closed_int a b. x \ b)" -proof - from a have "b\{x. a\x \ x\b}" by simp - thus "b \ closed_int a b" by (unfold closed_int_def) -next - have "\x\{x. a\x \ x\b}. x\b" by simp - thus "\x \ closed_int a b. x\b" by (unfold closed_int_def) -qed - -lemma closed_not_empty: - shows "a \ b \ \x. x \ closed_int a b" - by (auto dest: closed_int_least) - -lemma closed_mem: - assumes "a \ c" and "c \ b" - shows "c \ closed_int a b" - using assms unfolding closed_int_def by auto - -lemma closed_subset: - assumes ac: "a \ b" "c \ d" - assumes closed: "closed_int a b \ closed_int c d" - shows "b \ c" -proof - - from closed have "\x\closed_int a b. x\closed_int c d" by auto - hence "\x. a\x \ x\b \ c\x \ x\d" by (unfold closed_int_def, auto) - with ac have "c\b \ b\d" by simp - thus ?thesis by auto -qed - - -subsection {* Nested Interval Property *} - -theorem NIP: - fixes f::"nat \ real set" - assumes subset: "\n. f (Suc n) \ f n" - and closed: "\n. \a b. f n = closed_int a b \ a \ b" - shows "(\n. f n) \ {}" -proof - - let ?g = "\n. (SOME c. c\(f n) \ (\x\(f n). c \ x))" - have ne: "\n. \x. x\(f n)" - proof - fix n - from closed have "\a b. f n = closed_int a b \ a \ b" by simp - then obtain a and b where fn: "f n = closed_int a b \ a \ b" by auto - hence "a \ b" .. - with closed_not_empty have "\x. x\closed_int a b" by simp - with fn show "\x. x\(f n)" by simp - qed - - have gdef: "\n. (?g n)\(f n) \ (\x\(f n). (?g n)\x)" - proof - fix n - from closed have "\a b. f n = closed_int a b \ a \ b" .. - then obtain a and b where ff: "f n = closed_int a b" and "a \ b" by auto - hence "a \ b" by simp - hence "a\closed_int a b \ (\x\closed_int a b. a \ x)" by (rule closed_int_least) - with ff have "a\(f n) \ (\x\(f n). a \ x)" by simp - hence "\c. c\(f n) \ (\x\(f n). c \ x)" .. - thus "(?g n)\(f n) \ (\x\(f n). (?g n)\x)" by (rule someI_ex) - qed - - -- "A denotes the set of all left-most points of all the intervals ..." - moreover obtain A where Adef: "A = ?g ` \" by simp - ultimately have "\x. x\A" - proof - - have "(0::nat) \ \" by simp - moreover have "?g 0 = ?g 0" by simp - ultimately have "?g 0 \ ?g ` \" by (rule rev_image_eqI) - with Adef have "?g 0 \ A" by simp - thus ?thesis .. - qed - - -- "Now show that A is bounded above ..." - moreover have "\y. isUb (UNIV::real set) A y" - proof - - { - fix n - from ne have ex: "\x. x\(f n)" .. - from gdef have "(?g n)\(f n) \ (\x\(f n). (?g n)\x)" by simp - moreover - from closed have "\a b. f n = closed_int a b \ a \ b" .. - then obtain a and b where "f n = closed_int a b \ a \ b" by auto - hence "b\(f n) \ (\x\(f n). x \ b)" using closed_int_most by blast - ultimately have "\x\(f n). (?g n) \ b" by simp - with ex have "(?g n) \ b" by auto - hence "\b. (?g n) \ b" by auto - } - hence aux: "\n. \b. (?g n) \ b" .. - - have fs: "\n::nat. f n \ f 0" - proof (rule allI, induct_tac n) - show "f 0 \ f 0" by simp - next - fix n - assume "f n \ f 0" - moreover from subset have "f (Suc n) \ f n" .. - ultimately show "f (Suc n) \ f 0" by simp - qed - have "\n. (?g n)\(f 0)" - proof - fix n - from gdef have "(?g n)\(f n) \ (\x\(f n). (?g n)\x)" by simp - hence "?g n \ f n" .. - with fs show "?g n \ f 0" by auto - qed - moreover from closed - obtain a and b where "f 0 = closed_int a b" and alb: "a \ b" by blast - ultimately have "\n. ?g n \ closed_int a b" by auto - with alb have "\n. ?g n \ b" using closed_int_most by blast - with Adef have "\y\A. y\b" by auto - hence "A *<= b" by (unfold setle_def) - moreover have "b \ (UNIV::real set)" by simp - ultimately have "A *<= b \ b \ (UNIV::real set)" by simp - hence "isUb (UNIV::real set) A b" by (unfold isUb_def) - thus ?thesis by auto - qed - -- "by the Axiom Of Completeness, A has a least upper bound ..." - ultimately have "\t. isLub UNIV A t" by (rule reals_complete) - - -- "denote this least upper bound as t ..." - then obtain t where tdef: "isLub UNIV A t" .. - - -- "and finally show that this least upper bound is in all the intervals..." - have "\n. t \ f n" - proof - fix n::nat - from closed obtain a and b where - int: "f n = closed_int a b" and alb: "a \ b" by blast - - have "t \ a" - proof - - have "a \ A" - proof - - (* by construction *) - from alb int have ain: "a\f n \ (\x\f n. a \ x)" - using closed_int_least by blast - moreover have "\e. e\f n \ (\x\f n. e \ x) \ e = a" - proof clarsimp - fix e - assume ein: "e \ f n" and lt: "\x\f n. e \ x" - from lt ain have aux: "\x\f n. a \ x \ e \ x" by auto - - from ein aux have "a \ e \ e \ e" by auto - moreover from ain aux have "a \ a \ e \ a" by auto - ultimately show "e = a" by simp - qed - hence "\e. e\f n \ (\x\f n. e \ x) \ e = a" by simp - ultimately have "(?g n) = a" by (rule some_equality) - moreover - { - have "n = of_nat n" by simp - moreover have "of_nat n \ \" by simp - ultimately have "n \ \" - apply - - apply (subst(asm) eq_sym_conv) - apply (erule subst) - . - } - with Adef have "(?g n) \ A" by auto - ultimately show ?thesis by simp - qed - with tdef show "a \ t" by (rule isLubD2) - qed - moreover have "t \ b" - proof - - have "isUb UNIV A b" - proof - - { - from alb int have - ain: "b\f n \ (\x\f n. x \ b)" using closed_int_most by blast - - have subsetd: "\m. \n. f (n + m) \ f n" - proof (rule allI, induct_tac m) - show "\n. f (n + 0) \ f n" by simp - next - fix m n - assume pp: "\p. f (p + n) \ f p" - { - fix p - from pp have "f (p + n) \ f p" by simp - moreover from subset have "f (Suc (p + n)) \ f (p + n)" by auto - hence "f (p + (Suc n)) \ f (p + n)" by simp - ultimately have "f (p + (Suc n)) \ f p" by simp - } - thus "\p. f (p + Suc n) \ f p" .. - qed - have subsetm: "\\ \. \ \ \ \ (f \) \ (f \)" - proof ((rule allI)+, rule impI) - fix \::nat and \::nat - assume "\ \ \" - hence "\k. \ = \ + k" by (simp only: le_iff_add) - then obtain k where "\ = \ + k" .. - moreover - from subsetd have "f (\ + k) \ f \" by simp - ultimately show "f \ \ f \" by auto - qed - - fix m - { - assume "m \ n" - with subsetm have "f m \ f n" by simp - with ain have "\x\f m. x \ b" by auto - moreover - from gdef have "?g m \ f m \ (\x\f m. ?g m \ x)" by simp - ultimately have "?g m \ b" by auto - } - moreover - { - assume "\(m \ n)" - hence "m < n" by simp - with subsetm have sub: "(f n) \ (f m)" by simp - from closed obtain ma and mb where - "f m = closed_int ma mb \ ma \ mb" by blast - hence one: "ma \ mb" and fm: "f m = closed_int ma mb" by auto - from one alb sub fm int have "ma \ b" using closed_subset by blast - moreover have "(?g m) = ma" - proof - - from gdef have "?g m \ f m \ (\x\f m. ?g m \ x)" .. - moreover from one have - "ma \ closed_int ma mb \ (\x\closed_int ma mb. ma \ x)" - by (rule closed_int_least) - with fm have "ma\f m \ (\x\f m. ma \ x)" by simp - ultimately have "ma \ ?g m \ ?g m \ ma" by auto - thus "?g m = ma" by auto - qed - ultimately have "?g m \ b" by simp - } - ultimately have "?g m \ b" by (rule case_split) - } - with Adef have "\y\A. y\b" by auto - hence "A *<= b" by (unfold setle_def) - moreover have "b \ (UNIV::real set)" by simp - ultimately have "A *<= b \ b \ (UNIV::real set)" by simp - thus "isUb (UNIV::real set) A b" by (unfold isUb_def) - qed - with tdef show "t \ b" by (rule isLub_le_isUb) - qed - ultimately have "t \ closed_int a b" by (rule closed_mem) - with int show "t \ f n" by simp - qed - hence "t \ (\n. f n)" by auto - thus ?thesis by auto -qed - -subsection {* Generating the intervals *} - -subsubsection {* Existence of non-singleton closed intervals *} - -text {* This lemma asserts that given any non-singleton closed -interval (a,b) and any element c, there exists a closed interval that -is a subset of (a,b) and that does not contain c and is a -non-singleton itself. *} - -lemma closed_subset_ex: - fixes c::real - assumes alb: "a < b" - shows - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" -proof - - { - assume clb: "c < b" - { - assume cla: "c < a" - from alb cla clb have "c \ closed_int a b" by (unfold closed_int_def, auto) - with alb have - "a < b \ closed_int a b \ closed_int a b \ c \ closed_int a b" - by auto - hence - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by auto - } - moreover - { - assume ncla: "\(c < a)" - with clb have cdef: "a \ c \ c < b" by simp - obtain ka where kadef: "ka = (c + b)/2" by blast - - from kadef clb have kalb: "ka < b" by auto - moreover from kadef cdef have kagc: "ka > c" by simp - ultimately have "c\(closed_int ka b)" by (unfold closed_int_def, auto) - moreover from cdef kagc have "ka \ a" by simp - hence "closed_int ka b \ closed_int a b" by (unfold closed_int_def, auto) - ultimately have - "ka < b \ closed_int ka b \ closed_int a b \ c \ closed_int ka b" - using kalb by auto - hence - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by auto - - } - ultimately have - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by (rule case_split) - } - moreover - { - assume "\ (c < b)" - hence cgeb: "c \ b" by simp - - obtain kb where kbdef: "kb = (a + b)/2" by blast - with alb have kblb: "kb < b" by auto - with kbdef cgeb have "a < kb \ kb < c" by auto - moreover hence "c \ (closed_int a kb)" by (unfold closed_int_def, auto) - moreover from kblb have - "closed_int a kb \ closed_int a b" by (unfold closed_int_def, auto) - ultimately have - "a < kb \ closed_int a kb \ closed_int a b \ c\closed_int a kb" - by simp - hence - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by auto - } - ultimately show ?thesis by (rule case_split) -qed - -subsection {* newInt: Interval generation *} - -text {* Given a function f:@{text "\\\"}, newInt (Suc n) f returns a -closed interval such that @{text "newInt (Suc n) f \ newInt n f"} and -does not contain @{text "f (Suc n)"}. With the base case defined such -that @{text "(f 0)\newInt 0 f"}. *} - -subsubsection {* Definition *} - -primrec newInt :: "nat \ (nat \ real) \ (real set)" where - "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" - | "newInt (Suc n) f = - (SOME e. (\e1 e2. - e1 < e2 \ - e = closed_int e1 e2 \ - e \ (newInt n f) \ - (f (Suc n)) \ e) - )" - -declare newInt.simps [code del] - -subsubsection {* Properties *} - -text {* We now show that every application of newInt returns an -appropriate interval. *} - -lemma newInt_ex: - "\a b. a < b \ - newInt (Suc n) f = closed_int a b \ - newInt (Suc n) f \ newInt n f \ - f (Suc n) \ newInt (Suc n) f" -proof (induct n) - case 0 - - let ?e = "SOME e. \e1 e2. - e1 < e2 \ - e = closed_int e1 e2 \ - e \ closed_int (f 0 + 1) (f 0 + 2) \ - f (Suc 0) \ e" - - have "newInt (Suc 0) f = ?e" by auto - moreover - have "f 0 + 1 < f 0 + 2" by simp - with closed_subset_ex have - "\ka kb. ka < kb \ closed_int ka kb \ closed_int (f 0 + 1) (f 0 + 2) \ - f (Suc 0) \ (closed_int ka kb)" . - hence - "\e. \ka kb. ka < kb \ e = closed_int ka kb \ - e \ closed_int (f 0 + 1) (f 0 + 2) \ f (Suc 0) \ e" by simp - hence - "\ka kb. ka < kb \ ?e = closed_int ka kb \ - ?e \ closed_int (f 0 + 1) (f 0 + 2) \ f (Suc 0) \ ?e" - by (rule someI_ex) - ultimately have "\e1 e2. e1 < e2 \ - newInt (Suc 0) f = closed_int e1 e2 \ - newInt (Suc 0) f \ closed_int (f 0 + 1) (f 0 + 2) \ - f (Suc 0) \ newInt (Suc 0) f" by simp - thus - "\a b. a < b \ newInt (Suc 0) f = closed_int a b \ - newInt (Suc 0) f \ newInt 0 f \ f (Suc 0) \ newInt (Suc 0) f" - by simp -next - case (Suc n) - hence "\a b. - a < b \ - newInt (Suc n) f = closed_int a b \ - newInt (Suc n) f \ newInt n f \ - f (Suc n) \ newInt (Suc n) f" by simp - then obtain a and b where ab: "a < b \ - newInt (Suc n) f = closed_int a b \ - newInt (Suc n) f \ newInt n f \ - f (Suc n) \ newInt (Suc n) f" by auto - hence cab: "closed_int a b = newInt (Suc n) f" by simp - - let ?e = "SOME e. \e1 e2. - e1 < e2 \ - e = closed_int e1 e2 \ - e \ closed_int a b \ - f (Suc (Suc n)) \ e" - from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto - - from ab have "a < b" by simp - with closed_subset_ex have - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ - f (Suc (Suc n)) \ closed_int ka kb" . - hence - "\e. \ka kb. ka < kb \ e = closed_int ka kb \ - closed_int ka kb \ closed_int a b \ f (Suc (Suc n)) \ closed_int ka kb" - by simp - hence - "\e. \ka kb. ka < kb \ e = closed_int ka kb \ - e \ closed_int a b \ f (Suc (Suc n)) \ e" by simp - hence - "\ka kb. ka < kb \ ?e = closed_int ka kb \ - ?e \ closed_int a b \ f (Suc (Suc n)) \ ?e" by (rule someI_ex) - with ab ni show - "\ka kb. ka < kb \ - newInt (Suc (Suc n)) f = closed_int ka kb \ - newInt (Suc (Suc n)) f \ newInt (Suc n) f \ - f (Suc (Suc n)) \ newInt (Suc (Suc n)) f" by auto -qed - -lemma newInt_subset: - "newInt (Suc n) f \ newInt n f" - using newInt_ex by auto - - -text {* Another fundamental property is that no element in the range -of f is in the intersection of all closed intervals generated by -newInt. *} - -lemma newInt_inter: - "\n. f n \ (\n. newInt n f)" -proof - fix n::nat - { - assume n0: "n = 0" - moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp - ultimately have "f n \ newInt n f" by (unfold closed_int_def, simp) - } - moreover - { - assume "\ n = 0" - hence "n > 0" by simp - then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc) - - from newInt_ex have - "\a b. a < b \ (newInt (Suc m) f) = closed_int a b \ - newInt (Suc m) f \ newInt m f \ f (Suc m) \ newInt (Suc m) f" . - then have "f (Suc m) \ newInt (Suc m) f" by auto - with ndef have "f n \ newInt n f" by simp - } - ultimately have "f n \ newInt n f" by (rule case_split) - thus "f n \ (\n. newInt n f)" by auto -qed - - -lemma newInt_notempty: - "(\n. newInt n f) \ {}" -proof - - let ?g = "\n. newInt n f" - have "\n. ?g (Suc n) \ ?g n" - proof - fix n - show "?g (Suc n) \ ?g n" by (rule newInt_subset) - qed - moreover have "\n. \a b. ?g n = closed_int a b \ a \ b" - proof - fix n::nat - { - assume "n = 0" - then have - "?g n = closed_int (f 0 + 1) (f 0 + 2) \ (f 0 + 1 \ f 0 + 2)" - by simp - hence "\a b. ?g n = closed_int a b \ a \ b" by blast - } - moreover - { - assume "\ n = 0" - then have "n > 0" by simp - then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc) - - have - "\a b. a < b \ (newInt (Suc m) f) = closed_int a b \ - (newInt (Suc m) f) \ (newInt m f) \ (f (Suc m)) \ (newInt (Suc m) f)" - by (rule newInt_ex) - then obtain a and b where - "a < b \ (newInt (Suc m) f) = closed_int a b" by auto - with nd have "?g n = closed_int a b \ a \ b" by auto - hence "\a b. ?g n = closed_int a b \ a \ b" by blast - } - ultimately show "\a b. ?g n = closed_int a b \ a \ b" by (rule case_split) - qed - ultimately show ?thesis by (rule NIP) -qed - - -subsection {* Final Theorem *} - -theorem real_non_denum: - shows "\ (\f::nat\real. surj f)" -proof -- "by contradiction" - assume "\f::nat\real. surj f" - then obtain f::"nat\real" where "surj f" by auto - hence rangeF: "range f = UNIV" by (rule surj_range) - -- "We now produce a real number x that is not in the range of f, using the properties of newInt. " - have "\x. x \ (\n. newInt n f)" using newInt_notempty by blast - moreover have "\n. f n \ (\n. newInt n f)" by (rule newInt_inter) - ultimately obtain x where "x \ (\n. newInt n f)" and "\n. f n \ x" by blast - moreover from rangeF have "x \ range f" by simp - ultimately show False by blast -qed - -end diff -r 286c669d3a7a -r 9dbf8249d979 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 09 22:13:16 2008 -0800 +++ b/src/HOL/IsaMakefile Wed Dec 10 06:34:10 2008 -0800 @@ -274,7 +274,6 @@ Order_Relation.thy \ Parity.thy \ Univ_Poly.thy \ - ContNotDenum.thy \ Lubs.thy \ PReal.thy \ Rational.thy \ @@ -299,7 +298,7 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy \ Library/Abstract_Rat.thy \ - Library/BigO.thy Library/Ramsey.thy Library/Efficient_Nat.thy \ + Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \ Library/Executable_Set.thy Library/Infinite_Set.thy \ Library/FuncSet.thy \ Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \ @@ -307,7 +306,7 @@ Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \ Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \ Library/README.html Library/Continuity.thy \ - Library/Nested_Environment.thy Library/Zorn.thy \ + Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \ Library/Library/ROOT.ML Library/Library/document/root.tex \ Library/Library/document/root.bib Library/While_Combinator.thy \ Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \ diff -r 286c669d3a7a -r 9dbf8249d979 src/HOL/Library/ContNotDenum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/ContNotDenum.thy Wed Dec 10 06:34:10 2008 -0800 @@ -0,0 +1,579 @@ +(* Title : HOL/ContNonDenum + Author : Benjamin Porter, Monash University, NICTA, 2005 +*) + +header {* Non-denumerability of the Continuum. *} + +theory ContNotDenum +imports RComplete Hilbert_Choice +begin + +subsection {* Abstract *} + +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 @{text "\"} is not denumerable. In other +words, there does not exist a function f:@{text "\\\"} such that f is +surjective. + +{\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:@{text +"\\\"} 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. *} + +subsection {* Closed Intervals *} + +text {* This section formalises some properties of closed intervals. *} + +subsubsection {* Definition *} + +definition + closed_int :: "real \ real \ real set" where + "closed_int x y = {z. x \ z \ z \ y}" + +subsubsection {* Properties *} + +lemma closed_int_subset: + assumes xy: "x1 \ x0" "y1 \ y0" + shows "closed_int x1 y1 \ closed_int x0 y0" +proof - + { + fix x::real + assume "x \ closed_int x1 y1" + hence "x \ x1 \ x \ y1" by (simp add: closed_int_def) + with xy have "x \ x0 \ x \ y0" by auto + hence "x \ closed_int x0 y0" by (simp add: closed_int_def) + } + thus ?thesis by auto +qed + +lemma closed_int_least: + assumes a: "a \ b" + shows "a \ closed_int a b \ (\x \ closed_int a b. a \ x)" +proof + from a have "a\{x. a\x \ x\b}" by simp + thus "a \ closed_int a b" by (unfold closed_int_def) +next + have "\x\{x. a\x \ x\b}. a\x" by simp + thus "\x \ closed_int a b. a \ x" by (unfold closed_int_def) +qed + +lemma closed_int_most: + assumes a: "a \ b" + shows "b \ closed_int a b \ (\x \ closed_int a b. x \ b)" +proof + from a have "b\{x. a\x \ x\b}" by simp + thus "b \ closed_int a b" by (unfold closed_int_def) +next + have "\x\{x. a\x \ x\b}. x\b" by simp + thus "\x \ closed_int a b. x\b" by (unfold closed_int_def) +qed + +lemma closed_not_empty: + shows "a \ b \ \x. x \ closed_int a b" + by (auto dest: closed_int_least) + +lemma closed_mem: + assumes "a \ c" and "c \ b" + shows "c \ closed_int a b" + using assms unfolding closed_int_def by auto + +lemma closed_subset: + assumes ac: "a \ b" "c \ d" + assumes closed: "closed_int a b \ closed_int c d" + shows "b \ c" +proof - + from closed have "\x\closed_int a b. x\closed_int c d" by auto + hence "\x. a\x \ x\b \ c\x \ x\d" by (unfold closed_int_def, auto) + with ac have "c\b \ b\d" by simp + thus ?thesis by auto +qed + + +subsection {* Nested Interval Property *} + +theorem NIP: + fixes f::"nat \ real set" + assumes subset: "\n. f (Suc n) \ f n" + and closed: "\n. \a b. f n = closed_int a b \ a \ b" + shows "(\n. f n) \ {}" +proof - + let ?g = "\n. (SOME c. c\(f n) \ (\x\(f n). c \ x))" + have ne: "\n. \x. x\(f n)" + proof + fix n + from closed have "\a b. f n = closed_int a b \ a \ b" by simp + then obtain a and b where fn: "f n = closed_int a b \ a \ b" by auto + hence "a \ b" .. + with closed_not_empty have "\x. x\closed_int a b" by simp + with fn show "\x. x\(f n)" by simp + qed + + have gdef: "\n. (?g n)\(f n) \ (\x\(f n). (?g n)\x)" + proof + fix n + from closed have "\a b. f n = closed_int a b \ a \ b" .. + then obtain a and b where ff: "f n = closed_int a b" and "a \ b" by auto + hence "a \ b" by simp + hence "a\closed_int a b \ (\x\closed_int a b. a \ x)" by (rule closed_int_least) + with ff have "a\(f n) \ (\x\(f n). a \ x)" by simp + hence "\c. c\(f n) \ (\x\(f n). c \ x)" .. + thus "(?g n)\(f n) \ (\x\(f n). (?g n)\x)" by (rule someI_ex) + qed + + -- "A denotes the set of all left-most points of all the intervals ..." + moreover obtain A where Adef: "A = ?g ` \" by simp + ultimately have "\x. x\A" + proof - + have "(0::nat) \ \" by simp + moreover have "?g 0 = ?g 0" by simp + ultimately have "?g 0 \ ?g ` \" by (rule rev_image_eqI) + with Adef have "?g 0 \ A" by simp + thus ?thesis .. + qed + + -- "Now show that A is bounded above ..." + moreover have "\y. isUb (UNIV::real set) A y" + proof - + { + fix n + from ne have ex: "\x. x\(f n)" .. + from gdef have "(?g n)\(f n) \ (\x\(f n). (?g n)\x)" by simp + moreover + from closed have "\a b. f n = closed_int a b \ a \ b" .. + then obtain a and b where "f n = closed_int a b \ a \ b" by auto + hence "b\(f n) \ (\x\(f n). x \ b)" using closed_int_most by blast + ultimately have "\x\(f n). (?g n) \ b" by simp + with ex have "(?g n) \ b" by auto + hence "\b. (?g n) \ b" by auto + } + hence aux: "\n. \b. (?g n) \ b" .. + + have fs: "\n::nat. f n \ f 0" + proof (rule allI, induct_tac n) + show "f 0 \ f 0" by simp + next + fix n + assume "f n \ f 0" + moreover from subset have "f (Suc n) \ f n" .. + ultimately show "f (Suc n) \ f 0" by simp + qed + have "\n. (?g n)\(f 0)" + proof + fix n + from gdef have "(?g n)\(f n) \ (\x\(f n). (?g n)\x)" by simp + hence "?g n \ f n" .. + with fs show "?g n \ f 0" by auto + qed + moreover from closed + obtain a and b where "f 0 = closed_int a b" and alb: "a \ b" by blast + ultimately have "\n. ?g n \ closed_int a b" by auto + with alb have "\n. ?g n \ b" using closed_int_most by blast + with Adef have "\y\A. y\b" by auto + hence "A *<= b" by (unfold setle_def) + moreover have "b \ (UNIV::real set)" by simp + ultimately have "A *<= b \ b \ (UNIV::real set)" by simp + hence "isUb (UNIV::real set) A b" by (unfold isUb_def) + thus ?thesis by auto + qed + -- "by the Axiom Of Completeness, A has a least upper bound ..." + ultimately have "\t. isLub UNIV A t" by (rule reals_complete) + + -- "denote this least upper bound as t ..." + then obtain t where tdef: "isLub UNIV A t" .. + + -- "and finally show that this least upper bound is in all the intervals..." + have "\n. t \ f n" + proof + fix n::nat + from closed obtain a and b where + int: "f n = closed_int a b" and alb: "a \ b" by blast + + have "t \ a" + proof - + have "a \ A" + proof - + (* by construction *) + from alb int have ain: "a\f n \ (\x\f n. a \ x)" + using closed_int_least by blast + moreover have "\e. e\f n \ (\x\f n. e \ x) \ e = a" + proof clarsimp + fix e + assume ein: "e \ f n" and lt: "\x\f n. e \ x" + from lt ain have aux: "\x\f n. a \ x \ e \ x" by auto + + from ein aux have "a \ e \ e \ e" by auto + moreover from ain aux have "a \ a \ e \ a" by auto + ultimately show "e = a" by simp + qed + hence "\e. e\f n \ (\x\f n. e \ x) \ e = a" by simp + ultimately have "(?g n) = a" by (rule some_equality) + moreover + { + have "n = of_nat n" by simp + moreover have "of_nat n \ \" by simp + ultimately have "n \ \" + apply - + apply (subst(asm) eq_sym_conv) + apply (erule subst) + . + } + with Adef have "(?g n) \ A" by auto + ultimately show ?thesis by simp + qed + with tdef show "a \ t" by (rule isLubD2) + qed + moreover have "t \ b" + proof - + have "isUb UNIV A b" + proof - + { + from alb int have + ain: "b\f n \ (\x\f n. x \ b)" using closed_int_most by blast + + have subsetd: "\m. \n. f (n + m) \ f n" + proof (rule allI, induct_tac m) + show "\n. f (n + 0) \ f n" by simp + next + fix m n + assume pp: "\p. f (p + n) \ f p" + { + fix p + from pp have "f (p + n) \ f p" by simp + moreover from subset have "f (Suc (p + n)) \ f (p + n)" by auto + hence "f (p + (Suc n)) \ f (p + n)" by simp + ultimately have "f (p + (Suc n)) \ f p" by simp + } + thus "\p. f (p + Suc n) \ f p" .. + qed + have subsetm: "\\ \. \ \ \ \ (f \) \ (f \)" + proof ((rule allI)+, rule impI) + fix \::nat and \::nat + assume "\ \ \" + hence "\k. \ = \ + k" by (simp only: le_iff_add) + then obtain k where "\ = \ + k" .. + moreover + from subsetd have "f (\ + k) \ f \" by simp + ultimately show "f \ \ f \" by auto + qed + + fix m + { + assume "m \ n" + with subsetm have "f m \ f n" by simp + with ain have "\x\f m. x \ b" by auto + moreover + from gdef have "?g m \ f m \ (\x\f m. ?g m \ x)" by simp + ultimately have "?g m \ b" by auto + } + moreover + { + assume "\(m \ n)" + hence "m < n" by simp + with subsetm have sub: "(f n) \ (f m)" by simp + from closed obtain ma and mb where + "f m = closed_int ma mb \ ma \ mb" by blast + hence one: "ma \ mb" and fm: "f m = closed_int ma mb" by auto + from one alb sub fm int have "ma \ b" using closed_subset by blast + moreover have "(?g m) = ma" + proof - + from gdef have "?g m \ f m \ (\x\f m. ?g m \ x)" .. + moreover from one have + "ma \ closed_int ma mb \ (\x\closed_int ma mb. ma \ x)" + by (rule closed_int_least) + with fm have "ma\f m \ (\x\f m. ma \ x)" by simp + ultimately have "ma \ ?g m \ ?g m \ ma" by auto + thus "?g m = ma" by auto + qed + ultimately have "?g m \ b" by simp + } + ultimately have "?g m \ b" by (rule case_split) + } + with Adef have "\y\A. y\b" by auto + hence "A *<= b" by (unfold setle_def) + moreover have "b \ (UNIV::real set)" by simp + ultimately have "A *<= b \ b \ (UNIV::real set)" by simp + thus "isUb (UNIV::real set) A b" by (unfold isUb_def) + qed + with tdef show "t \ b" by (rule isLub_le_isUb) + qed + ultimately have "t \ closed_int a b" by (rule closed_mem) + with int show "t \ f n" by simp + qed + hence "t \ (\n. f n)" by auto + thus ?thesis by auto +qed + +subsection {* Generating the intervals *} + +subsubsection {* Existence of non-singleton closed intervals *} + +text {* This lemma asserts that given any non-singleton closed +interval (a,b) and any element c, there exists a closed interval that +is a subset of (a,b) and that does not contain c and is a +non-singleton itself. *} + +lemma closed_subset_ex: + fixes c::real + assumes alb: "a < b" + shows + "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" +proof - + { + assume clb: "c < b" + { + assume cla: "c < a" + from alb cla clb have "c \ closed_int a b" by (unfold closed_int_def, auto) + with alb have + "a < b \ closed_int a b \ closed_int a b \ c \ closed_int a b" + by auto + hence + "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" + by auto + } + moreover + { + assume ncla: "\(c < a)" + with clb have cdef: "a \ c \ c < b" by simp + obtain ka where kadef: "ka = (c + b)/2" by blast + + from kadef clb have kalb: "ka < b" by auto + moreover from kadef cdef have kagc: "ka > c" by simp + ultimately have "c\(closed_int ka b)" by (unfold closed_int_def, auto) + moreover from cdef kagc have "ka \ a" by simp + hence "closed_int ka b \ closed_int a b" by (unfold closed_int_def, auto) + ultimately have + "ka < b \ closed_int ka b \ closed_int a b \ c \ closed_int ka b" + using kalb by auto + hence + "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" + by auto + + } + ultimately have + "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" + by (rule case_split) + } + moreover + { + assume "\ (c < b)" + hence cgeb: "c \ b" by simp + + obtain kb where kbdef: "kb = (a + b)/2" by blast + with alb have kblb: "kb < b" by auto + with kbdef cgeb have "a < kb \ kb < c" by auto + moreover hence "c \ (closed_int a kb)" by (unfold closed_int_def, auto) + moreover from kblb have + "closed_int a kb \ closed_int a b" by (unfold closed_int_def, auto) + ultimately have + "a < kb \ closed_int a kb \ closed_int a b \ c\closed_int a kb" + by simp + hence + "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" + by auto + } + ultimately show ?thesis by (rule case_split) +qed + +subsection {* newInt: Interval generation *} + +text {* Given a function f:@{text "\\\"}, newInt (Suc n) f returns a +closed interval such that @{text "newInt (Suc n) f \ newInt n f"} and +does not contain @{text "f (Suc n)"}. With the base case defined such +that @{text "(f 0)\newInt 0 f"}. *} + +subsubsection {* Definition *} + +primrec newInt :: "nat \ (nat \ real) \ (real set)" where + "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" + | "newInt (Suc n) f = + (SOME e. (\e1 e2. + e1 < e2 \ + e = closed_int e1 e2 \ + e \ (newInt n f) \ + (f (Suc n)) \ e) + )" + +declare newInt.simps [code del] + +subsubsection {* Properties *} + +text {* We now show that every application of newInt returns an +appropriate interval. *} + +lemma newInt_ex: + "\a b. a < b \ + newInt (Suc n) f = closed_int a b \ + newInt (Suc n) f \ newInt n f \ + f (Suc n) \ newInt (Suc n) f" +proof (induct n) + case 0 + + let ?e = "SOME e. \e1 e2. + e1 < e2 \ + e = closed_int e1 e2 \ + e \ closed_int (f 0 + 1) (f 0 + 2) \ + f (Suc 0) \ e" + + have "newInt (Suc 0) f = ?e" by auto + moreover + have "f 0 + 1 < f 0 + 2" by simp + with closed_subset_ex have + "\ka kb. ka < kb \ closed_int ka kb \ closed_int (f 0 + 1) (f 0 + 2) \ + f (Suc 0) \ (closed_int ka kb)" . + hence + "\e. \ka kb. ka < kb \ e = closed_int ka kb \ + e \ closed_int (f 0 + 1) (f 0 + 2) \ f (Suc 0) \ e" by simp + hence + "\ka kb. ka < kb \ ?e = closed_int ka kb \ + ?e \ closed_int (f 0 + 1) (f 0 + 2) \ f (Suc 0) \ ?e" + by (rule someI_ex) + ultimately have "\e1 e2. e1 < e2 \ + newInt (Suc 0) f = closed_int e1 e2 \ + newInt (Suc 0) f \ closed_int (f 0 + 1) (f 0 + 2) \ + f (Suc 0) \ newInt (Suc 0) f" by simp + thus + "\a b. a < b \ newInt (Suc 0) f = closed_int a b \ + newInt (Suc 0) f \ newInt 0 f \ f (Suc 0) \ newInt (Suc 0) f" + by simp +next + case (Suc n) + hence "\a b. + a < b \ + newInt (Suc n) f = closed_int a b \ + newInt (Suc n) f \ newInt n f \ + f (Suc n) \ newInt (Suc n) f" by simp + then obtain a and b where ab: "a < b \ + newInt (Suc n) f = closed_int a b \ + newInt (Suc n) f \ newInt n f \ + f (Suc n) \ newInt (Suc n) f" by auto + hence cab: "closed_int a b = newInt (Suc n) f" by simp + + let ?e = "SOME e. \e1 e2. + e1 < e2 \ + e = closed_int e1 e2 \ + e \ closed_int a b \ + f (Suc (Suc n)) \ e" + from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto + + from ab have "a < b" by simp + with closed_subset_ex have + "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ + f (Suc (Suc n)) \ closed_int ka kb" . + hence + "\e. \ka kb. ka < kb \ e = closed_int ka kb \ + closed_int ka kb \ closed_int a b \ f (Suc (Suc n)) \ closed_int ka kb" + by simp + hence + "\e. \ka kb. ka < kb \ e = closed_int ka kb \ + e \ closed_int a b \ f (Suc (Suc n)) \ e" by simp + hence + "\ka kb. ka < kb \ ?e = closed_int ka kb \ + ?e \ closed_int a b \ f (Suc (Suc n)) \ ?e" by (rule someI_ex) + with ab ni show + "\ka kb. ka < kb \ + newInt (Suc (Suc n)) f = closed_int ka kb \ + newInt (Suc (Suc n)) f \ newInt (Suc n) f \ + f (Suc (Suc n)) \ newInt (Suc (Suc n)) f" by auto +qed + +lemma newInt_subset: + "newInt (Suc n) f \ newInt n f" + using newInt_ex by auto + + +text {* Another fundamental property is that no element in the range +of f is in the intersection of all closed intervals generated by +newInt. *} + +lemma newInt_inter: + "\n. f n \ (\n. newInt n f)" +proof + fix n::nat + { + assume n0: "n = 0" + moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp + ultimately have "f n \ newInt n f" by (unfold closed_int_def, simp) + } + moreover + { + assume "\ n = 0" + hence "n > 0" by simp + then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc) + + from newInt_ex have + "\a b. a < b \ (newInt (Suc m) f) = closed_int a b \ + newInt (Suc m) f \ newInt m f \ f (Suc m) \ newInt (Suc m) f" . + then have "f (Suc m) \ newInt (Suc m) f" by auto + with ndef have "f n \ newInt n f" by simp + } + ultimately have "f n \ newInt n f" by (rule case_split) + thus "f n \ (\n. newInt n f)" by auto +qed + + +lemma newInt_notempty: + "(\n. newInt n f) \ {}" +proof - + let ?g = "\n. newInt n f" + have "\n. ?g (Suc n) \ ?g n" + proof + fix n + show "?g (Suc n) \ ?g n" by (rule newInt_subset) + qed + moreover have "\n. \a b. ?g n = closed_int a b \ a \ b" + proof + fix n::nat + { + assume "n = 0" + then have + "?g n = closed_int (f 0 + 1) (f 0 + 2) \ (f 0 + 1 \ f 0 + 2)" + by simp + hence "\a b. ?g n = closed_int a b \ a \ b" by blast + } + moreover + { + assume "\ n = 0" + then have "n > 0" by simp + then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc) + + have + "\a b. a < b \ (newInt (Suc m) f) = closed_int a b \ + (newInt (Suc m) f) \ (newInt m f) \ (f (Suc m)) \ (newInt (Suc m) f)" + by (rule newInt_ex) + then obtain a and b where + "a < b \ (newInt (Suc m) f) = closed_int a b" by auto + with nd have "?g n = closed_int a b \ a \ b" by auto + hence "\a b. ?g n = closed_int a b \ a \ b" by blast + } + ultimately show "\a b. ?g n = closed_int a b \ a \ b" by (rule case_split) + qed + ultimately show ?thesis by (rule NIP) +qed + + +subsection {* Final Theorem *} + +theorem real_non_denum: + shows "\ (\f::nat\real. surj f)" +proof -- "by contradiction" + assume "\f::nat\real. surj f" + then obtain f::"nat\real" where "surj f" by auto + hence rangeF: "range f = UNIV" by (rule surj_range) + -- "We now produce a real number x that is not in the range of f, using the properties of newInt. " + have "\x. x \ (\n. newInt n f)" using newInt_notempty by blast + moreover have "\n. f n \ (\n. newInt n f)" by (rule newInt_inter) + ultimately obtain x where "x \ (\n. newInt n f)" and "\n. f n \ x" by blast + moreover from rangeF have "x \ range f" by simp + ultimately show False by blast +qed + +end diff -r 286c669d3a7a -r 9dbf8249d979 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Dec 09 22:13:16 2008 -0800 +++ b/src/HOL/Library/Library.thy Wed Dec 10 06:34:10 2008 -0800 @@ -14,6 +14,7 @@ Coinductive_List Commutative_Ring Continuity + ContNotDenum Countable Dense_Linear_Order Efficient_Nat diff -r 286c669d3a7a -r 9dbf8249d979 src/HOL/Real.thy --- a/src/HOL/Real.thy Tue Dec 09 22:13:16 2008 -0800 +++ b/src/HOL/Real.thy Wed Dec 10 06:34:10 2008 -0800 @@ -1,5 +1,5 @@ theory Real -imports ContNotDenum "~~/src/HOL/Real/RealVector" +imports "~~/src/HOL/Real/RealVector" begin end diff -r 286c669d3a7a -r 9dbf8249d979 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Dec 09 22:13:16 2008 -0800 +++ b/src/Pure/Isar/class.ML Wed Dec 10 06:34:10 2008 -0800 @@ -394,7 +394,8 @@ end; fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] + intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE + Locale.intro_locales_tac true ctxt [] | default_intro_tac _ _ = no_tac; fun default_tac rules ctxt facts = diff -r 286c669d3a7a -r 9dbf8249d979 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Dec 09 22:13:16 2008 -0800 +++ b/src/Pure/Isar/expression.ML Wed Dec 10 06:34:10 2008 -0800 @@ -19,9 +19,11 @@ (* Declaring locales *) val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory -> - string * Proof.context + (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) * + Proof.context val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory -> - string * Proof.context + (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) * + Proof.context (* Interpretation *) val sublocale_cmd: string -> expression -> theory -> Proof.state; @@ -30,10 +32,6 @@ val interpretation: expression_i -> theory -> Proof.state; val interpret_cmd: expression -> bool -> Proof.state -> Proof.state; val interpret: expression_i -> bool -> Proof.state -> Proof.state; - - (* Debugging and development *) - val parse_expression: OuterParse.token list -> expression * OuterParse.token list - (* FIXME to spec_parse.ML *) end; @@ -55,63 +53,6 @@ type expression_i = term expr * (Binding.T * typ option * mixfix) list; -(** Parsing and printing **) - -local - -structure P = OuterParse; - -val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || - P.$$$ "defines" || P.$$$ "notes"; -fun plus1_unless test scan = - scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)); - -val prefix = P.name --| P.$$$ ":"; -val named = P.name -- (P.$$$ "=" |-- P.term); -val position = P.maybe P.term; -val instance = P.$$$ "where" |-- P.and_list1 named >> Named || - Scan.repeat1 position >> Positional; - -in - -val parse_expression = - let - fun expr2 x = P.xname x; - fun expr1 x = (Scan.optional prefix "" -- expr2 -- - Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; - fun expr0 x = (plus1_unless loc_keyword expr1) x; - in expr0 -- P.for_fixes end; - -end; - -fun pretty_expr thy expr = - let - fun pretty_pos NONE = Pretty.str "_" - | pretty_pos (SOME x) = Pretty.str x; - fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=", - Pretty.brk 1, Pretty.str y] |> Pretty.block; - fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |> - map pretty_pos |> Pretty.breaks - | pretty_ren (Named []) = [] - | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 :: - (ps |> map pretty_named |> Pretty.separate "and"); - fun pretty_rename (loc, ("", ren)) = - Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) - | pretty_rename (loc, (prfx, ren)) = - Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) :: - Pretty.brk 1 :: pretty_ren ren); - in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end; - -fun err_in_expr thy msg expr = - let - val err_msg = - if null expr then msg - else msg ^ "\n" ^ Pretty.string_of (Pretty.block - [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1, - pretty_expr thy expr]) - in error err_msg end; - - (** Internalise locale names in expr **) fun intern thy instances = map (apfst (NewLocale.intern thy)) instances; @@ -133,6 +74,13 @@ end; fun match_bind (n, b) = (n = Binding.base_name b); + fun parm_eq ((b1, mx1), (b2, mx2)) = + (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *) + (Binding.base_name b1 = Binding.base_name b2) andalso + (if mx1 = mx2 then true + else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^ + " in expression.")); + fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2); (* FIXME: cannot compare bindings for equality. *) @@ -164,12 +112,7 @@ val (is', ps') = fold_map (fn i => fn ps => let val (ps', i') = params_inst i; - val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) => - (* FIXME: should check for bindings being the same. - Instead we check for equal name and syntax. *) - if mx1 = mx2 then mx1 - else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^ - " in expression.")) (ps, ps') + val ps'' = distinct parm_eq (ps @ ps'); in (i', ps'') end) is [] in (ps', is') end; @@ -329,21 +272,18 @@ val norm_term = Envir.beta_norm oo Term.subst_atomic; -fun abstract_thm thy eq = - Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; - -fun bind_def ctxt eq (xs, env, ths) = +fun bind_def ctxt eq (xs, env, eqs) = let + val _ = LocalDefs.cert_def ctxt eq; val ((y, T), b) = LocalDefs.abs_def eq; val b' = norm_term env b; - val th = abstract_thm (ProofContext.theory_of ctxt) eq; fun err msg = error (msg ^ ": " ^ quote y); in exists (fn (x, _) => x = y) xs andalso err "Attempt to define previously specified variable"; exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso err "Attempt to redefine variable"; - (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) + (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) end; fun eval_text _ _ (Fixes _) text = text @@ -494,8 +434,7 @@ env: list of term pairs encoding substitutions, where the first term is a free variable; substitutions represent defines elements and the rhs is normalised wrt. the previous env - defs: theorems representing the substitutions from defines elements - (thms are normalised wrt. env). + defs: the equations from the defines elements elems is an updated version of raw_elems: - type info added to Fixes and modified in Constrains - axiom and definition statement replaced by corresponding one @@ -548,7 +487,6 @@ NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps; val ((elems', _), _) = activate elems (ProofContext.set_stmt true context'); in ((fixed, deps, elems'), (parms, spec, defs)) end; - (* FIXME check if defs used somewhere *) in @@ -583,7 +521,6 @@ val export = Variable.export_morphism goal_ctxt context; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; -(* val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *) val exp_term = Drule.term_rule thy (singleton exp_fact); val exp_typ = Logic.type_map exp_term; val export' = @@ -687,6 +624,8 @@ fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy = let + val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs; + val (a_pred, a_intro, a_axioms, thy'') = if null exts then (NONE, NONE, [], thy) else @@ -694,7 +633,7 @@ val aname = if null ints then pname else pname ^ "_" ^ axiomsN; val ((statement, intro, axioms), thy') = thy - |> def_pred aname parms defs exts exts'; + |> def_pred aname parms defs' exts exts'; val (_, thy'') = thy' |> Sign.add_path aname @@ -709,7 +648,7 @@ let val ((statement, intro, axioms), thy''') = thy'' - |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred); + |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val (_, thy'''') = thy''' |> Sign.add_path pname @@ -734,15 +673,10 @@ |> apfst (curry Notes Thm.assumptionK) | assumes_to_notes e axms = (e, axms); -fun defines_to_notes thy (Defines defs) defns = - let - val defs' = map (fn (_, (def, _)) => def) defs - val notes = map (fn (a, (def, _)) => - (a, [([Assumption.assume (cterm_of thy def)], [])])) defs - in - (Notes (Thm.definitionK, notes), defns @ defs') - end - | defines_to_notes _ e defns = (e, defns); +fun defines_to_notes thy (Defines defs) = + Notes (Thm.definitionK, map (fn (a, (def, _)) => + (a, [([Assumption.assume (cterm_of thy def)], [])])) defs) + | defines_to_notes _ e = e; fun gen_add_locale prep_decl bname predicate_name raw_imprt raw_body thy = @@ -751,7 +685,7 @@ val _ = NewLocale.test_locale thy name andalso error ("Duplicate definition of locale " ^ quote name); - val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), _)) = + val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) = prep_decl raw_imprt raw_body (ProofContext.init thy); val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_name text thy; @@ -760,29 +694,39 @@ val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ quote bname); - val satisfy = Element.satisfy_morphism b_axioms; + val a_satisfy = Element.satisfy_morphism a_axioms; + val b_satisfy = Element.satisfy_morphism b_axioms; val params = fixed @ (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat); val asm = if is_some b_statement then b_statement else a_statement; - val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems []; - val notes = body_elems' |> + + (* These are added immediately. *) + val notes = + if is_some asm + then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []), + [([Assumption.assume (cterm_of thy' (the asm))], + [(Attrib.internal o K) NewLocale.witness_attrib])])])] + else []; + + (* These will be added in the local theory. *) + val notes' = body_elems |> + map (defines_to_notes thy') |> + map (Element.morph_ctxt a_satisfy) |> (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |> - fst |> map (Element.morph_ctxt satisfy) |> - map_filter (fn Notes notes => SOME notes | _ => NONE) |> - (if is_some asm - then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []), - [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])]) - else I); + fst |> + map (Element.morph_ctxt b_satisfy) |> + map_filter (fn Notes notes => SOME notes | _ => NONE); - val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps; + val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; val loc_ctxt = thy' |> NewLocale.register_locale bname (extraTs, params) - (asm, defns) ([], []) + (asm, rev defs) ([], []) (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |> - NewLocale.init name - in (name, loc_ctxt) end; + NewLocale.init name; + + in ((name, notes'), loc_ctxt) end; in diff -r 286c669d3a7a -r 9dbf8249d979 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Dec 09 22:13:16 2008 -0800 +++ b/src/Pure/Isar/isar_syn.ML Wed Dec 10 06:34:10 2008 -0800 @@ -401,7 +401,7 @@ val _ = OuterSyntax.command "sublocale" "prove sublocale relation between a locale and a locale expression" K.thy_goal - (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! Expression.parse_expression + (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! SpecParse.locale_expression >> (fn (loc, expr) => Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)))); diff -r 286c669d3a7a -r 9dbf8249d979 src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Tue Dec 09 22:13:16 2008 -0800 +++ b/src/Pure/Isar/new_locale.ML Wed Dec 10 06:34:10 2008 -0800 @@ -39,7 +39,6 @@ Proof.context -> Proof.context val activate_global_facts: string * Morphism.morphism -> theory -> theory val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context -(* val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *) val init: string -> theory -> Proof.context (* Reasoning about locales *) diff -r 286c669d3a7a -r 9dbf8249d979 src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Tue Dec 09 22:13:16 2008 -0800 +++ b/src/Pure/Isar/spec_parse.ML Wed Dec 10 06:34:10 2008 -0800 @@ -26,6 +26,7 @@ val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list val class_expr: token list -> string list * token list val locale_expr: token list -> Locale.expr * token list + val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list val locale_keyword: token list -> string * token list val context_element: token list -> Element.context * token list val statement: token list -> (Attrib.binding * (string * string list) list) list * token list @@ -103,6 +104,12 @@ val rename = P.name -- Scan.option P.mixfix; +val prefix = P.name --| P.$$$ ":"; +val named = P.name -- (P.$$$ "=" |-- P.term); +val position = P.maybe P.term; +val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named || + Scan.repeat1 position >> Expression.Positional; + in val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || @@ -117,6 +124,14 @@ and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x; in expr0 end; +val locale_expression = + let + fun expr2 x = P.xname x; + fun expr1 x = (Scan.optional prefix "" -- expr2 -- + Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; + fun expr0 x = (plus1_unless locale_keyword expr1) x; + in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end; + val context_element = P.group "context element" loc_element; end;