# HG changeset patch # User wenzelm # Date 1228943158 -3600 # Node ID edaef19665e698b440b383849e06d36223a8b178 # Parent 6f61794f1ff7b96505253a8395fbfe6d18a85e43# Parent 9dbf8249d979a67aac1e79a481b3819323264057 merged diff -r 6f61794f1ff7 -r edaef19665e6 doc-src/IsarAdvanced/Classes/classes.tex --- a/doc-src/IsarAdvanced/Classes/classes.tex Mon Dec 08 08:56:30 2008 +0100 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 10 22:05:58 2008 +0100 @@ -1,5 +1,3 @@ - -%% $Id$ \documentclass[12pt,a4paper,fleqn]{report} \usepackage{latexsym,graphicx} @@ -10,40 +8,10 @@ \usepackage{../../pdfsetup} -%% setup - -% hyphenation \hyphenation{Isabelle} \hyphenation{Isar} - -% logical markup -\newcommand{\strong}[1]{{\bfseries {#1}}} -\newcommand{\qn}[1]{\emph{#1}} - -% typographic conventions -\newcommand{\qt}[1]{``{#1}''} - -% verbatim text -\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} - -% invisibility \isadroptag{theory} -% quoted segments -\makeatletter -\isakeeptag{quote} -\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}} -\renewcommand{\isatagquote}{\begin{quotesegment}} -\renewcommand{\endisatagquote}{\end{quotesegment}} -\makeatother - -%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}} -%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}} -%\renewcommand{\isasymotimes}{\isamath{\circ}} - - -%% content - \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] Haskell-style type classes with Isabelle/Isar} \author{\emph{Florian Haftmann}} @@ -69,7 +37,6 @@ \input{Thy/document/Classes.tex} \begingroup -%\tocentry{\bibname} \bibliographystyle{plain} \small\raggedright\frenchspacing \bibliography{../../manual} \endgroup diff -r 6f61794f1ff7 -r edaef19665e6 doc-src/IsarAdvanced/Classes/style.sty --- a/doc-src/IsarAdvanced/Classes/style.sty Mon Dec 08 08:56:30 2008 +0100 +++ b/doc-src/IsarAdvanced/Classes/style.sty Wed Dec 10 22:05:58 2008 +0100 @@ -1,5 +1,3 @@ - -%% $Id$ %% toc \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} @@ -7,54 +5,37 @@ %% references \newcommand{\secref}[1]{\S\ref{#1}} -\newcommand{\chref}[1]{chapter~\ref{#1}} \newcommand{\figref}[1]{figure~\ref{#1}} -%% glossary -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}} -\newcommand{\seeglossary}[1]{\emph{#1}} -\newcommand{\glossaryname}{Glossary} -\renewcommand{\nomname}{\glossaryname} -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}} +%% logical markup +\newcommand{\strong}[1]{{\bfseries {#1}}} +\newcommand{\qn}[1]{\emph{#1}} + +%% typographic conventions +\newcommand{\qt}[1]{``{#1}''} + +%% verbatim text +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} -%% index -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}} -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}} -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}} -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}} +%% quoted segments +\makeatletter +\isakeeptag{quote} +\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}} +\renewcommand{\isatagquote}{\begin{quotesegment}} +\renewcommand{\endisatagquote}{\end{quotesegment}} +\makeatother -%% math -\newcommand{\text}[1]{\mbox{#1}} -\newcommand{\isasymvartheta}{\isamath{\theta}} -\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}} - +%% presentation \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} \pagestyle{headings} -\sloppy \binperiod \underscoreon \renewcommand{\isadigit}[1]{\isamath{#1}} -\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup} - -\isafoldtag{FIXME} -\isakeeptag{mlref} -\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small} -\renewcommand{\endisatagmlref}{\endgroup} +\isabellestyle{it} -\newcommand{\isasymGUESS}{\isakeyword{guess}} -\newcommand{\isasymOBTAIN}{\isakeyword{obtain}} -\newcommand{\isasymTHEORY}{\isakeyword{theory}} -\newcommand{\isasymUSES}{\isakeyword{uses}} -\newcommand{\isasymEND}{\isakeyword{end}} -\newcommand{\isasymCONSTS}{\isakeyword{consts}} -\newcommand{\isasymDEFS}{\isakeyword{defs}} -\newcommand{\isasymTHEOREM}{\isakeyword{theorem}} -\newcommand{\isasymDEFINITION}{\isakeyword{definition}} - -\isabellestyle{it} %%% Local Variables: %%% mode: latex diff -r 6f61794f1ff7 -r edaef19665e6 doc-src/IsarAdvanced/Codegen/codegen.tex --- a/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Dec 08 08:56:30 2008 +0100 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Wed Dec 10 22:05:58 2008 +0100 @@ -1,5 +1,3 @@ - -%% $Id$ \documentclass[12pt,a4paper,fleqn]{report} \usepackage{latexsym,graphicx} @@ -12,43 +10,10 @@ \usepackage{tikz} \usepackage{../../pdfsetup} -%% setup - -% hyphenation \hyphenation{Isabelle} \hyphenation{Isar} - -% logical markup -\newcommand{\strong}[1]{{\bfseries {#1}}} -\newcommand{\qn}[1]{\emph{#1}} - -% typographic conventions -\newcommand{\qt}[1]{``{#1}''} - -% verbatim text -\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} - -% invisibility \isadroptag{theory} -% quoted segments -\makeatletter -\isakeeptag{quote} -\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}} -\renewcommand{\isatagquote}{\begin{quotesegment}} -\renewcommand{\endisatagquote}{\end{quotesegment}} -\makeatother - -\isakeeptag{quotett} -\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle} -\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle} - -% hack -\newcommand{\isasymSML}{SML} - - -%% contents - \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] Code generation from Isabelle/HOL theories} \author{\emph{Florian Haftmann}} @@ -75,7 +40,6 @@ \input{Thy/document/ML.tex} \begingroup -%\tocentry{\bibname} \bibliographystyle{plain} \small\raggedright\frenchspacing \bibliography{../../manual} \endgroup diff -r 6f61794f1ff7 -r edaef19665e6 doc-src/IsarAdvanced/Codegen/style.sty --- a/doc-src/IsarAdvanced/Codegen/style.sty Mon Dec 08 08:56:30 2008 +0100 +++ b/doc-src/IsarAdvanced/Codegen/style.sty Wed Dec 10 22:05:58 2008 +0100 @@ -1,5 +1,3 @@ - -%% $Id$ %% toc \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} @@ -7,15 +5,6 @@ %% references \newcommand{\secref}[1]{\S\ref{#1}} -\newcommand{\chref}[1]{chapter~\ref{#1}} -\newcommand{\figref}[1]{figure~\ref{#1}} - -%% glossary -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}} -\newcommand{\seeglossary}[1]{\emph{#1}} -\newcommand{\glossaryname}{Glossary} -\renewcommand{\nomname}{\glossaryname} -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}} %% index \newcommand{\indexml}[1]{\index{\emph{#1}|bold}} @@ -23,38 +12,49 @@ \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}} \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}} -%% math -\newcommand{\text}[1]{\mbox{#1}} -\newcommand{\isasymvartheta}{\isamath{\theta}} -\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}} +%% logical markup +\newcommand{\strong}[1]{{\bfseries {#1}}} +\newcommand{\qn}[1]{\emph{#1}} + +%% typographic conventions +\newcommand{\qt}[1]{``{#1}''} + +%% verbatim text +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} +%% quoted segments +\makeatletter +\isakeeptag{quote} +\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}} +\renewcommand{\isatagquote}{\begin{quotesegment}} +\renewcommand{\endisatagquote}{\end{quotesegment}} +\makeatother + +\isakeeptag{quotett} +\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle} +\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle} + +%% a trick +\newcommand{\isasymSML}{SML} + +%% presentation \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} \pagestyle{headings} -\sloppy \binperiod \underscoreon \renewcommand{\isadigit}[1]{\isamath{#1}} +%% ml reference \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup} -\isafoldtag{FIXME} \isakeeptag{mlref} \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small} \renewcommand{\endisatagmlref}{\endgroup} -\newcommand{\isasymGUESS}{\isakeyword{guess}} -\newcommand{\isasymOBTAIN}{\isakeyword{obtain}} -\newcommand{\isasymTHEORY}{\isakeyword{theory}} -\newcommand{\isasymUSES}{\isakeyword{uses}} -\newcommand{\isasymEND}{\isakeyword{end}} -\newcommand{\isasymCONSTS}{\isakeyword{consts}} -\newcommand{\isasymDEFS}{\isakeyword{defs}} -\newcommand{\isasymTHEOREM}{\isakeyword{theorem}} -\newcommand{\isasymDEFINITION}{\isakeyword{definition}} +\isabellestyle{it} -\isabellestyle{it} %%% Local Variables: %%% mode: latex diff -r 6f61794f1ff7 -r edaef19665e6 src/FOL/ex/NewLocaleSetup.thy --- a/src/FOL/ex/NewLocaleSetup.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/FOL/ex/NewLocaleSetup.thy Wed Dec 10 22:05:58 2008 +0100 @@ -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 @@ -41,11 +43,19 @@ val _ = OuterSyntax.command "interpretation" - "prove and register interpretation of locale expression in theory" K.thy_goal - (P.!!! Expression.parse_expression + "prove interpretation of locale expression in theory" K.thy_goal + (P.!!! SpecParse.locale_expression >> (fn expr => Toplevel.print o Toplevel.theory_to_proof (Expression.interpretation_cmd expr))); +val _ = + OuterSyntax.command "interpret" + "prove interpretation of locale expression in proof context" + (K.tag_proof K.prf_goal) + (P.!!! SpecParse.locale_expression + >> (fn expr => Toplevel.print o + Toplevel.proof' (fn int => Expression.interpret_cmd expr int))); + end *} diff -r 6f61794f1ff7 -r edaef19665e6 src/FOL/ex/NewLocaleTest.thy --- a/src/FOL/ex/NewLocaleTest.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/FOL/ex/NewLocaleTest.thy Wed Dec 10 22:05:58 2008 +0100 @@ -113,6 +113,62 @@ 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 = + fixes land (infixl "&&" 55) + and lor (infixl "||" 50) + and lnot ("-- _" [60] 60) + assumes assoc: "(x && y) && z = x && (y && z)" + and notnot: "-- (-- x) = x" + 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: @@ -341,4 +397,24 @@ thm two.assoc + +text {* Interpretation in proofs *} + +lemma True +proof + interpret "local": lgrp "op +" "0" "minus" + by unfold_locales (* subsumed *) + { + fix zero :: int + assume "!!x. zero + x = x" "!!x. (-x) + x = zero" + then interpret local_fixed: lgrp "op +" zero "minus" + by unfold_locales + thm local_fixed.lone + } + assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero" + then interpret local_free: lgrp "op +" zero "minus" for zero + by unfold_locales + thm local_free.lone [where ?zero = 0] +qed + end diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Arith_Tools.thy --- a/src/HOL/Arith_Tools.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Arith_Tools.thy Wed Dec 10 22:05:58 2008 +0100 @@ -40,7 +40,7 @@ text{*No longer required as a simprule because of the @{text inverse_fold} simproc*} lemma Suc_diff_number_of: - "neg (number_of (uminus v)::int) ==> + "Int.Pls < v ==> Suc m - (number_of v) = m - (number_of (Int.pred v))" apply (subst Suc_diff_eq_diff_pred) apply simp diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Complex_Main.thy --- a/src/HOL/Complex_Main.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Complex_Main.thy Wed Dec 10 22:05:58 2008 +0100 @@ -8,7 +8,6 @@ theory Complex_Main imports Main - ContNotDenum Real "~~/src/HOL/Complex/Fundamental_Theorem_Algebra" Log diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/ContNotDenum.thy --- a/src/HOL/ContNotDenum.thy Mon Dec 08 08:56:30 2008 +0100 +++ /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 6f61794f1ff7 -r edaef19665e6 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Datatype.thy Wed Dec 10 22:05:58 2008 +0100 @@ -605,6 +605,9 @@ lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" by (rule set_ext, case_tac x) auto +lemma inj_Some [simp]: "inj_on Some A" + by (rule inj_onI) simp + subsubsection {* Operations *} diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Finite_Set.thy Wed Dec 10 22:05:58 2008 +0100 @@ -1828,6 +1828,18 @@ by (simp add: card_cartesian_product) +subsubsection {* Cardinality of sums *} + +lemma card_Plus: + assumes "finite A" and "finite B" + shows "card (A <+> B) = card A + card B" +proof - + have "Inl`A \ Inr`B = {}" by fast + with assms show ?thesis + unfolding Plus_def + by (simp add: card_Un_disjoint card_image) +qed + subsubsection {* Cardinality of the Powerset *} diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Groebner_Basis.thy Wed Dec 10 22:05:58 2008 +0100 @@ -178,7 +178,8 @@ lemma not_iszero_Numeral1: "\ iszero (Numeral1::'a::number_ring)" by (simp add: numeral_1_eq_1) -lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False +lemmas comp_arith = + Let_def arith_simps nat_arith rel_simps neg_simps if_False if_True add_0 add_Suc add_number_of_left mult_number_of_left numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1 numeral_0_eq_0[symmetric] numerals[symmetric] diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Int.thy Wed Dec 10 22:05:58 2008 +0100 @@ -1076,47 +1076,17 @@ text {* First version by Norbert Voelker *} -definition - neg :: "'a\ordered_idom \ bool" -where - "neg Z \ Z < 0" - definition (*for simplifying equalities*) iszero :: "'a\semiring_1 \ bool" where "iszero z \ z = 0" -lemma not_neg_int [simp]: "~ neg (of_nat n)" -by (simp add: neg_def) - -lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))" -by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc) - -lemmas neg_eq_less_0 = neg_def - -lemma not_neg_eq_ge_0: "(~neg x) = (0 \ x)" -by (simp add: neg_def linorder_not_less) - -text{*To simplify inequalities when Numeral1 can get simplified to 1*} - -lemma not_neg_0: "~ neg 0" -by (simp add: One_int_def neg_def) - -lemma not_neg_1: "~ neg 1" -by (simp add: neg_def linorder_not_less zero_le_one) - lemma iszero_0: "iszero 0" by (simp add: iszero_def) lemma not_iszero_1: "~ iszero 1" by (simp add: iszero_def eq_commute) -lemma neg_nat: "neg z ==> nat z = 0" -by (simp add: neg_def order_less_imp_le) - -lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z" -by (simp add: linorder_not_less neg_def) - lemma eq_number_of_eq: "((number_of x::'a::number_ring) = number_of y) = iszero (number_of (x + uminus y) :: 'a)" @@ -1196,26 +1166,6 @@ subsubsection {* The Less-Than Relation *} -lemma less_number_of_eq_neg: - "((number_of x::'a::{ordered_idom,number_ring}) < number_of y) - = neg (number_of (x + uminus y) :: 'a)" -apply (subst less_iff_diff_less_0) -apply (simp add: neg_def diff_minus number_of_add number_of_minus) -done - -text {* - If @{term Numeral0} is rewritten to 0 then this rule can't be applied: - @{term Numeral0} IS @{term "number_of Pls"} -*} - -lemma not_neg_number_of_Pls: - "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})" - by (simp add: neg_def numeral_0_eq_0) - -lemma neg_number_of_Min: - "neg (number_of Min ::'a::{ordered_idom,number_ring})" - by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1) - lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))" proof - @@ -1238,27 +1188,6 @@ add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric]) qed -lemma neg_number_of_Bit0: - "neg (number_of (Bit0 w)::'a) = - neg (number_of w :: 'a::{ordered_idom,number_ring})" -by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff) - -lemma neg_number_of_Bit1: - "neg (number_of (Bit1 w)::'a) = - neg (number_of w :: 'a::{ordered_idom,number_ring})" -proof - - have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))" - by simp - also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0) - finally show ?thesis - by (simp add: neg_def number_of_eq numeral_simps) -qed - -lemmas neg_simps = - not_neg_0 not_neg_1 - not_neg_number_of_Pls neg_number_of_Min - neg_number_of_Bit0 neg_number_of_Bit1 - text {* Less-Than or Equals *} text {* Reduces @{term "a\b"} to @{term "~ (b number_of y) - = (~ (neg (number_of (y + uminus x) :: 'a)))" -by (simp add: le_number_of_eq_not_less less_number_of_eq_neg) - text {* Absolute value (@{term abs}) *} @@ -1325,7 +1249,7 @@ less_number_of less_bin_simps le_number_of le_bin_simps eq_number_of_eq eq_bin_simps - iszero_simps neg_simps + iszero_simps subsubsection {* Simplification of arithmetic when nested to the right. *} diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/IsaMakefile Wed Dec 10 22:05:58 2008 +0100 @@ -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 6f61794f1ff7 -r edaef19665e6 src/HOL/Library/ContNotDenum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/ContNotDenum.thy Wed Dec 10 22:05:58 2008 +0100 @@ -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 6f61794f1ff7 -r edaef19665e6 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Library/Enum.thy Wed Dec 10 22:05:58 2008 +0100 @@ -365,4 +365,15 @@ end -end \ No newline at end of file +instantiation option :: (enum) enum +begin + +definition + "enum = None # map Some enum" + +instance by default + (auto simp add: enum_all enum_option_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct) + +end + +end diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Library/Float.thy Wed Dec 10 22:05:58 2008 +0100 @@ -514,7 +514,7 @@ by simp lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)" - by (rule less_number_of_eq_neg) + unfolding neg_def number_of_is_id by simp lemma int_not_neg_number_of_Pls: "\ (neg (Numeral0::int))" by simp diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Library/Library.thy Wed Dec 10 22:05:58 2008 +0100 @@ -14,6 +14,7 @@ Coinductive_List Commutative_Ring Continuity + ContNotDenum Countable Dense_Linear_Order Efficient_Nat diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Library/Nat_Infinity.thy --- a/src/HOL/Library/Nat_Infinity.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Library/Nat_Infinity.thy Wed Dec 10 22:05:58 2008 +0100 @@ -146,8 +146,8 @@ by (simp_all add: plus_inat_def zero_inat_def split: inat.splits) lemma plus_inat_number [simp]: - "(number_of k \ inat) + number_of l = (if neg (number_of k \ int) then number_of l - else if neg (number_of l \ int) then number_of k else number_of (k + l))" + "(number_of k \ inat) + number_of l = (if k < Int.Pls then number_of l + else if l < Int.Pls then number_of k else number_of (k + l))" unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] .. lemma iSuc_number [simp]: @@ -165,6 +165,67 @@ unfolding iSuc_plus_1 by (simp_all add: add_ac) +subsection {* Multiplication *} + +instantiation inat :: comm_semiring_1 +begin + +definition + times_inat_def [code del]: + "m * n = (case m of \ \ if n = 0 then 0 else \ | Fin m \ + (case n of \ \ if m = 0 then 0 else \ | Fin n \ Fin (m * n)))" + +lemma times_inat_simps [simp, code]: + "Fin m * Fin n = Fin (m * n)" + "\ * \ = \" + "\ * Fin n = (if n = 0 then 0 else \)" + "Fin m * \ = (if m = 0 then 0 else \)" + unfolding times_inat_def zero_inat_def + by (simp_all split: inat.split) + +instance proof + fix a b c :: inat + show "(a * b) * c = a * (b * c)" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "a * b = b * a" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "1 * a = a" + unfolding times_inat_def zero_inat_def one_inat_def + by (simp split: inat.split) + show "(a + b) * c = a * c + b * c" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split add: left_distrib) + show "0 * a = 0" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "a * 0 = 0" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "(0::inat) \ 1" + unfolding zero_inat_def one_inat_def + by simp +qed + +end + +lemma mult_iSuc: "iSuc m * n = n + m * n" + unfolding iSuc_plus_1 by (simp add: ring_simps) + +lemma mult_iSuc_right: "m * iSuc n = m + m * n" + unfolding iSuc_plus_1 by (simp add: ring_simps) + +lemma of_nat_eq_Fin: "of_nat n = Fin n" + apply (induct n) + apply (simp add: Fin_0) + apply (simp add: plus_1_iSuc iSuc_Fin) + done + +instance inat :: semiring_char_0 + by default (simp add: of_nat_eq_Fin) + + subsection {* Ordering *} instantiation inat :: ordered_ab_semigroup_add @@ -201,6 +262,15 @@ end +instance inat :: pordered_comm_semiring +proof + fix a b c :: inat + assume "a \ b" and "0 \ c" + thus "c * a \ c * b" + unfolding times_inat_def less_eq_inat_def zero_inat_def + by (simp split: inat.splits) +qed + lemma inat_ord_number [simp]: "(number_of m \ inat) \ number_of n \ (number_of m \ nat) \ number_of n" "(number_of m \ inat) < number_of n \ (number_of m \ nat) < number_of n" diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Wed Dec 10 22:05:58 2008 +0100 @@ -14,23 +14,6 @@ subsection {* Preliminary lemmas *} (* These should be moved elsewhere *) -lemma inj_Inl [simp]: "inj_on Inl A" - by (rule inj_onI, simp) - -lemma inj_Inr [simp]: "inj_on Inr A" - by (rule inj_onI, simp) - -lemma inj_Some [simp]: "inj_on Some A" - by (rule inj_onI, simp) - -lemma card_Plus: - "[| finite A; finite B |] ==> card (A <+> B) = card A + card B" - unfolding Plus_def - apply (subgoal_tac "Inl ` A \ Inr ` B = {}") - apply (simp add: card_Un_disjoint card_image) - apply fast - done - lemma (in type_definition) univ: "UNIV = Abs ` A" proof diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/NatBin.thy Wed Dec 10 22:05:58 2008 +0100 @@ -39,6 +39,63 @@ square ("(_\)" [1000] 999) +subsection {* Predicate for negative binary numbers *} + +definition + neg :: "int \ bool" +where + "neg Z \ Z < 0" + +lemma not_neg_int [simp]: "~ neg (of_nat n)" +by (simp add: neg_def) + +lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))" +by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc) + +lemmas neg_eq_less_0 = neg_def + +lemma not_neg_eq_ge_0: "(~neg x) = (0 \ x)" +by (simp add: neg_def linorder_not_less) + +text{*To simplify inequalities when Numeral1 can get simplified to 1*} + +lemma not_neg_0: "~ neg 0" +by (simp add: One_int_def neg_def) + +lemma not_neg_1: "~ neg 1" +by (simp add: neg_def linorder_not_less zero_le_one) + +lemma neg_nat: "neg z ==> nat z = 0" +by (simp add: neg_def order_less_imp_le) + +lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z" +by (simp add: linorder_not_less neg_def) + +text {* + If @{term Numeral0} is rewritten to 0 then this rule can't be applied: + @{term Numeral0} IS @{term "number_of Pls"} +*} + +lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)" + by (simp add: neg_def) + +lemma neg_number_of_Min: "neg (number_of Int.Min)" + by (simp add: neg_def) + +lemma neg_number_of_Bit0: + "neg (number_of (Int.Bit0 w)) = neg (number_of w)" + by (simp add: neg_def) + +lemma neg_number_of_Bit1: + "neg (number_of (Int.Bit1 w)) = neg (number_of w)" + by (simp add: neg_def) + +lemmas neg_simps [simp] = + not_neg_0 not_neg_1 + not_neg_number_of_Pls neg_number_of_Min + neg_number_of_Bit0 neg_number_of_Bit1 + + subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} declare nat_0 [simp] nat_1 [simp] @@ -141,10 +198,10 @@ (*"neg" is used in rewrite rules for binary comparisons*) lemma add_nat_number_of [simp]: "(number_of v :: nat) + number_of v' = - (if neg (number_of v :: int) then number_of v' - else if neg (number_of v' :: int) then number_of v + (if v < Int.Pls then number_of v' + else if v' < Int.Pls then number_of v else number_of (v + v'))" - unfolding nat_number_of_def number_of_is_id neg_def + unfolding nat_number_of_def number_of_is_id numeral_simps by (simp add: nat_add_distrib) @@ -160,19 +217,19 @@ lemma diff_nat_number_of [simp]: "(number_of v :: nat) - number_of v' = - (if neg (number_of v' :: int) then number_of v + (if v' < Int.Pls then number_of v else let d = number_of (v + uminus v') in if neg d then 0 else nat d)" -by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) - + unfolding nat_number_of_def number_of_is_id numeral_simps neg_def + by auto subsubsection{*Multiplication *} lemma mult_nat_number_of [simp]: "(number_of v :: nat) * number_of v' = - (if neg (number_of v :: int) then 0 else number_of (v * v'))" - unfolding nat_number_of_def number_of_is_id neg_def + (if v < Int.Pls then 0 else number_of (v * v'))" + unfolding nat_number_of_def number_of_is_id numeral_simps by (simp add: nat_mult_distrib) @@ -258,15 +315,21 @@ subsubsection{*Less-than (<) *} -(*"neg" is used in rewrite rules for binary comparisons*) lemma less_nat_number_of [simp]: - "((number_of v :: nat) < number_of v') = - (if neg (number_of v :: int) then neg (number_of (uminus v') :: int) - else neg (number_of (v + uminus v') :: int))" - unfolding neg_def nat_number_of_def number_of_is_id + "(number_of v :: nat) < number_of v' \ + (if v < v' then Int.Pls < v' else False)" + unfolding nat_number_of_def number_of_is_id numeral_simps by auto +subsubsection{*Less-than-or-equal *} + +lemma le_nat_number_of [simp]: + "(number_of v :: nat) \ number_of v' \ + (if v \ v' then True else v \ Int.Pls)" + unfolding nat_number_of_def number_of_is_id numeral_simps + by auto + (*Maps #n to n for n = 0, 1, 2*) lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2 @@ -440,17 +503,18 @@ text{*Simplification already does @{term "n<0"}, @{term "n\0"} and @{term "0\n"}.*} lemma eq_number_of_0 [simp]: - "number_of v = (0::nat) \ number_of v \ (0::int)" - unfolding nat_number_of_def number_of_is_id by auto + "number_of v = (0::nat) \ v \ Int.Pls" + unfolding nat_number_of_def number_of_is_id numeral_simps + by auto lemma eq_0_number_of [simp]: - "(0::nat) = number_of v \ number_of v \ (0::int)" + "(0::nat) = number_of v \ v \ Int.Pls" by (rule trans [OF eq_sym_conv eq_number_of_0]) lemma less_0_number_of [simp]: - "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)" -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def) - + "(0::nat) < number_of v \ Int.Pls < v" + unfolding nat_number_of_def number_of_is_id numeral_simps + by simp lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)" by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric]) @@ -620,9 +684,8 @@ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, lessD = lessD, neqE = neqE, - simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, - @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min}, - @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]}) + simpset = simpset addsimps @{thms neg_simps} @ + [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]}) *} declaration {* K nat_bin_arith_setup *} @@ -699,7 +762,7 @@ lemma nat_number_of_mult_left: "number_of v * (number_of v' * (k::nat)) = - (if neg (number_of v :: int) then 0 + (if v < Int.Pls then 0 else number_of (v * v') * k)" by simp diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Real.thy --- a/src/HOL/Real.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Real.thy Wed Dec 10 22:05:58 2008 +0100 @@ -1,5 +1,5 @@ theory Real -imports ContNotDenum "~~/src/HOL/Real/RealVector" +imports "~~/src/HOL/Real/RealVector" begin end diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Sum_Type.thy Wed Dec 10 22:05:58 2008 +0100 @@ -93,16 +93,17 @@ lemma Inr_Rep_inject: "Inr_Rep(b) = Inr_Rep(d) ==> b=d" by (auto simp add: Inr_Rep_def expand_fun_eq) -lemma inj_Inl: "inj(Inl)" +lemma inj_Inl [simp]: "inj_on Inl A" apply (simp add: Inl_def) apply (rule inj_onI) apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inl_Rep_inject]) apply (rule Inl_RepI) apply (rule Inl_RepI) done + lemmas Inl_inject = inj_Inl [THEN injD, standard] -lemma inj_Inr: "inj(Inr)" +lemma inj_Inr [simp]: "inj_on Inr A" apply (simp add: Inr_def) apply (rule inj_onI) apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inr_Rep_inject]) diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Tools/ComputeNumeral.thy --- a/src/HOL/Tools/ComputeNumeral.thy Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Tools/ComputeNumeral.thy Wed Dec 10 22:05:58 2008 +0100 @@ -29,63 +29,13 @@ lemmas bitlezero = lezero1 lezero2 lezero3 lezero4 (* equality for bit strings *) -lemma biteq1: "(Int.Pls = Int.Pls) = True" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq2: "(Int.Min = Int.Min) = True" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq11: "(Int.Min = Int.Bit0 x) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq15: "(Int.Bit0 x = Int.Min) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16 +lemmas biteq = eq_bin_simps (* x < y for bit strings *) -lemma bitless1: "(Int.Pls < Int.Min) = False" by (simp add: less_int_code) -lemma bitless2: "(Int.Pls < Int.Pls) = False" by (simp add: less_int_code) -lemma bitless3: "(Int.Min < Int.Pls) = True" by (simp add: less_int_code) -lemma bitless4: "(Int.Min < Int.Min) = False" by (simp add: less_int_code) -lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (simp add: less_int_code) -lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (simp add: less_int_code) -lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \ y)" by (simp add: less_int_code) -lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (simp add: less_int_code) -lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (simp add: less_int_code) -lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \ x)" by (simp add: less_int_code) -lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \ x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (simp add: less_int_code) -lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (simp add: less_int_code) -lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (simp add: less_int_code) -lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (simp add: less_int_code) -lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8 - bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16 +lemmas bitless = less_bin_simps (* x \ y for bit strings *) -lemma bitle1: "(Int.Pls \ Int.Min) = False" by (simp add: less_eq_int_code) -lemma bitle2: "(Int.Pls \ Int.Pls) = True" by (simp add: less_eq_int_code) -lemma bitle3: "(Int.Min \ Int.Pls) = True" by (simp add: less_eq_int_code) -lemma bitle4: "(Int.Min \ Int.Min) = True" by (simp add: less_eq_int_code) -lemma bitle5: "(Int.Bit0 x \ Int.Bit0 y) = (x \ y)" by (simp add: less_eq_int_code) -lemma bitle6: "(Int.Bit1 x \ Int.Bit1 y) = (x \ y)" by (simp add: less_eq_int_code) -lemma bitle7: "(Int.Bit0 x \ Int.Bit1 y) = (x \ y)" by (simp add: less_eq_int_code) -lemma bitle8: "(Int.Bit1 x \ Int.Bit0 y) = (x < y)" by (simp add: less_eq_int_code) -lemma bitle9: "(Int.Pls \ Int.Bit0 x) = (Int.Pls \ x)" by (simp add: less_eq_int_code) -lemma bitle10: "(Int.Pls \ Int.Bit1 x) = (Int.Pls \ x)" by (simp add: less_eq_int_code) -lemma bitle11: "(Int.Min \ Int.Bit0 x) = (Int.Pls \ x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma bitle12: "(Int.Min \ Int.Bit1 x) = (Int.Min \ x)" by (simp add: less_eq_int_code) -lemma bitle13: "(Int.Bit0 x \ Int.Pls) = (x \ Int.Pls)" by (simp add: less_eq_int_code) -lemma bitle14: "(Int.Bit1 x \ Int.Pls) = (x < Int.Pls)" by (simp add: less_eq_int_code) -lemma bitle15: "(Int.Bit0 x \ Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger -lemma bitle16: "(Int.Bit1 x \ Int.Min) = (x \ Int.Min)" by (simp add: less_eq_int_code) -lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8 - bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16 +lemmas bitle = le_bin_simps (* succ for bit strings *) lemmas bitsucc = succ_bin_simps @@ -129,7 +79,8 @@ (* Addition for nat *) lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))" - by (auto simp add: number_of_is_id) + unfolding nat_number_of_def number_of_is_id neg_def + by auto (* Subtraction for nat *) lemma natsub: "(number_of x) - ((number_of y)::nat) = @@ -140,18 +91,14 @@ (* Multiplication for nat *) lemma natmul: "(number_of x) * ((number_of y)::nat) = (if neg x then 0 else (if neg y then 0 else number_of (x * y)))" - apply (auto simp add: number_of_is_id neg_def iszero_def) - apply (case_tac "x > 0") - apply auto - apply (rule order_less_imp_le) - apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified]) - done + unfolding nat_number_of_def number_of_is_id neg_def + by (simp add: nat_mult_distrib) lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \ lezero y) \ (x = y))" by (auto simp add: iszero_def lezero_def neg_def number_of_is_id) lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \ (\ (lezero y)))" - by (auto simp add: number_of_is_id neg_def lezero_def) + by (simp add: lezero_def numeral_simps not_le) lemma natle: "(((number_of x)::nat) \ (number_of y)) = (y < x \ lezero x)" by (auto simp add: number_of_is_id lezero_def nat_number_of_def) diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Tools/int_factor_simprocs.ML Wed Dec 10 22:05:58 2008 +0100 @@ -19,7 +19,7 @@ and d = gcd(m,m') and n=m/d and n'=m'/d. *) -val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of_eq_neg}, @{thm le_number_of_eq}]; +val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}]; local open Int_Numeral_Simprocs diff -r 6f61794f1ff7 -r edaef19665e6 src/HOL/Tools/nat_simprocs.ML --- a/src/HOL/Tools/nat_simprocs.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/HOL/Tools/nat_simprocs.ML Wed Dec 10 22:05:58 2008 +0100 @@ -53,7 +53,7 @@ @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, @{thm less_nat_number_of}, @{thm Let_number_of}, @{thm nat_number_of}] @ - @{thms arith_simps} @ @{thms rel_simps}; + @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; fun prep_simproc (name, pats, proc) = Simplifier.simproc (the_context ()) name pats proc; diff -r 6f61794f1ff7 -r edaef19665e6 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/Pure/Isar/class.ML Wed Dec 10 22:05:58 2008 +0100 @@ -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 6f61794f1ff7 -r edaef19665e6 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/Pure/Isar/expression.ML Wed Dec 10 22:05:58 2008 +0100 @@ -19,23 +19,19 @@ (* 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; val sublocale: string -> expression_i -> theory -> Proof.state; val interpretation_cmd: expression -> theory -> Proof.state; val interpretation: expression_i -> theory -> Proof.state; -(* - val interpret_cmd: Morphism.morphism -> expression -> bool -> Proof.state -> Proof.state; - val interpret: Morphism.morphism -> 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 *) + val interpret_cmd: expression -> bool -> Proof.state -> Proof.state; + val interpret: expression_i -> bool -> Proof.state -> Proof.state; end; @@ -57,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; @@ -135,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. *) @@ -166,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; @@ -331,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 @@ -371,7 +309,8 @@ val rev_frees = Term.fold_aterms (fn Free (x, T) => if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t []; - in Term.list_all_free (rev rev_frees, t) end; + in Term.list_all_free (rev rev_frees, t) end; (* FIXME use fold Logic.all *) + (* FIXME consider closing in syntactic phase *) fun no_binds [] = [] | no_binds _ = error "Illegal term bindings in context element"; @@ -379,8 +318,11 @@ (case elem of Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) - | Defines defs => Defines (defs |> map (fn (a, (t, ps)) => - (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) + | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => + let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t) + in + ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps)) + end)) | e => e) end; @@ -492,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 @@ -538,14 +479,12 @@ fun prep_declaration prep activate raw_import raw_elems context = let - val thy = ProofContext.theory_of context; - val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) = prep false true context raw_import raw_elems []; (* Declare parameters and imported facts *) val context' = context |> ProofContext.add_fixes_i fixed |> snd |> - NewLocale.clear_local_idents |> fold (NewLocale.activate_local_facts thy) deps; + 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; @@ -582,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' = @@ -686,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 @@ -693,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 @@ -708,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 @@ -733,26 +673,20 @@ |> 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, [([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 = let - val thy_ctxt = ProofContext.init thy; val name = Sign.full_bname thy bname; val _ = NewLocale.test_locale thy name andalso error ("Duplicate definition of locale " ^ quote name); val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) = - prep_decl raw_imprt raw_body thy_ctxt; + 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, map prop_of defs) ([], []) + (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 @@ -837,6 +781,7 @@ end; + (** Interpretation in theories **) local @@ -846,7 +791,7 @@ let val ctxt = ProofContext.init thy; - val ((propss, deps, export), goal_ctxt) = prep_expr expression ctxt; + val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; fun store_reg ((name, morph), thms) = let @@ -857,7 +802,7 @@ end; fun after_qed results = - ProofContext.theory (fold store_reg (deps ~~ prep_result propss results)); + ProofContext.theory (fold store_reg (regs ~~ prep_result propss results)); in goal_ctxt |> Proof.theorem_i NONE after_qed (prep_propp propss) |> @@ -871,5 +816,41 @@ end; + +(** Interpretation in proof contexts **) + +local + +fun gen_interpret prep_expr + expression int state = + let + val _ = Proof.assert_forward_or_chain state; + val ctxt = Proof.context_of state; + + val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; + + fun store_reg ((name, morph), thms) = + let + val morph' = morph $> Element.satisfy_morphism thms $> export; + in + NewLocale.activate_local_facts (name, morph') + end; + + fun after_qed results = + Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single; + in + state |> Proof.map_context (K goal_ctxt) |> + Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i + "interpret" NONE after_qed (map (pair (Binding.empty, [])) (prep_propp propss)) |> + Element.refine_witness |> Seq.hd + end; + +in + +fun interpret_cmd x = gen_interpret read_goal_expression x; +fun interpret x = gen_interpret cert_goal_expression x; + end; +end; + diff -r 6f61794f1ff7 -r edaef19665e6 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Dec 10 22:05:58 2008 +0100 @@ -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 6f61794f1ff7 -r edaef19665e6 src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/Pure/Isar/new_locale.ML Wed Dec 10 22:05:58 2008 +0100 @@ -37,11 +37,8 @@ (* Activation *) val activate_declarations: theory -> string * Morphism.morphism -> Proof.context -> Proof.context - val activate_global_facts: string * Morphism.morphism -> - theory -> theory - val activate_local_facts: theory -> string * Morphism.morphism -> - Proof.context -> Proof.context -(* val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *) + val activate_global_facts: string * Morphism.morphism -> theory -> theory + val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context val init: string -> theory -> Proof.context (* Reasoning about locales *) @@ -355,13 +352,14 @@ fun activate_declarations thy dep ctxt = roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents; - + fun activate_global_facts dep thy = roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |> uncurry put_global_idents; -fun activate_local_facts thy dep ctxt = - roundup thy (activate_notes init_local_elem) dep (get_local_idents ctxt, ctxt) |> +fun activate_local_facts dep ctxt = + roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep + (get_local_idents ctxt, ctxt) |> uncurry put_local_idents; fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |> @@ -454,8 +452,9 @@ "back-chain all introduction rules of locales")])); -(*** Registrations: interpretations in theories and proof contexts ***) +(*** Registrations: interpretations in theories ***) +(* FIXME only global variant needed *) structure RegistrationsData = GenericDataFun ( type T = ((string * Morphism.morphism) * stamp) list; @@ -470,6 +469,5 @@ fun add_global_registration reg = (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ())); - end; diff -r 6f61794f1ff7 -r edaef19665e6 src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Mon Dec 08 08:56:30 2008 +0100 +++ b/src/Pure/Isar/spec_parse.ML Wed Dec 10 22:05:58 2008 +0100 @@ -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;