--- 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
--- 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
--- 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
--- 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
--- 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
*}
--- 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
--- 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
--- 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
--- 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 "\<real>"} is not denumerable. In other
-words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} 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
-"\<nat>\<Rightarrow>\<real>"} 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 \<Rightarrow> real \<Rightarrow> real set" where
- "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
-
-subsubsection {* Properties *}
-
-lemma closed_int_subset:
- assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
- shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
-proof -
- {
- fix x::real
- assume "x \<in> closed_int x1 y1"
- hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
- with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
- hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
- }
- thus ?thesis by auto
-qed
-
-lemma closed_int_least:
- assumes a: "a \<le> b"
- shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
-proof
- from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
- thus "a \<in> closed_int a b" by (unfold closed_int_def)
-next
- have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
- thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
-qed
-
-lemma closed_int_most:
- assumes a: "a \<le> b"
- shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
-proof
- from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
- thus "b \<in> closed_int a b" by (unfold closed_int_def)
-next
- have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
- thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
-qed
-
-lemma closed_not_empty:
- shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"
- by (auto dest: closed_int_least)
-
-lemma closed_mem:
- assumes "a \<le> c" and "c \<le> b"
- shows "c \<in> closed_int a b"
- using assms unfolding closed_int_def by auto
-
-lemma closed_subset:
- assumes ac: "a \<le> b" "c \<le> d"
- assumes closed: "closed_int a b \<subseteq> closed_int c d"
- shows "b \<ge> c"
-proof -
- from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
- hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
- with ac have "c\<le>b \<and> b\<le>d" by simp
- thus ?thesis by auto
-qed
-
-
-subsection {* Nested Interval Property *}
-
-theorem NIP:
- fixes f::"nat \<Rightarrow> real set"
- assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
- and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
- shows "(\<Inter>n. f n) \<noteq> {}"
-proof -
- let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
- have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
- proof
- fix n
- from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
- then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
- hence "a \<le> b" ..
- with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
- with fn show "\<exists>x. x\<in>(f n)" by simp
- qed
-
- have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
- proof
- fix n
- from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
- then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
- hence "a \<le> b" by simp
- hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
- with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
- hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
- thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>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 ` \<nat>" by simp
- ultimately have "\<exists>x. x\<in>A"
- proof -
- have "(0::nat) \<in> \<nat>" by simp
- moreover have "?g 0 = ?g 0" by simp
- ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
- with Adef have "?g 0 \<in> A" by simp
- thus ?thesis ..
- qed
-
- -- "Now show that A is bounded above ..."
- moreover have "\<exists>y. isUb (UNIV::real set) A y"
- proof -
- {
- fix n
- from ne have ex: "\<exists>x. x\<in>(f n)" ..
- from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
- moreover
- from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
- then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
- hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
- ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
- with ex have "(?g n) \<le> b" by auto
- hence "\<exists>b. (?g n) \<le> b" by auto
- }
- hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
-
- have fs: "\<forall>n::nat. f n \<subseteq> f 0"
- proof (rule allI, induct_tac n)
- show "f 0 \<subseteq> f 0" by simp
- next
- fix n
- assume "f n \<subseteq> f 0"
- moreover from subset have "f (Suc n) \<subseteq> f n" ..
- ultimately show "f (Suc n) \<subseteq> f 0" by simp
- qed
- have "\<forall>n. (?g n)\<in>(f 0)"
- proof
- fix n
- from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
- hence "?g n \<in> f n" ..
- with fs show "?g n \<in> f 0" by auto
- qed
- moreover from closed
- obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
- ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
- with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
- with Adef have "\<forall>y\<in>A. y\<le>b" by auto
- hence "A *<= b" by (unfold setle_def)
- moreover have "b \<in> (UNIV::real set)" by simp
- ultimately have "A *<= b \<and> b \<in> (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 "\<exists>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 "\<forall>n. t \<in> f n"
- proof
- fix n::nat
- from closed obtain a and b where
- int: "f n = closed_int a b" and alb: "a \<le> b" by blast
-
- have "t \<ge> a"
- proof -
- have "a \<in> A"
- proof -
- (* by construction *)
- from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
- using closed_int_least by blast
- moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
- proof clarsimp
- fix e
- assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
- from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
-
- from ein aux have "a \<le> e \<and> e \<le> e" by auto
- moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
- ultimately show "e = a" by simp
- qed
- hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> 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 \<in> \<nat>" by simp
- ultimately have "n \<in> \<nat>"
- apply -
- apply (subst(asm) eq_sym_conv)
- apply (erule subst)
- .
- }
- with Adef have "(?g n) \<in> A" by auto
- ultimately show ?thesis by simp
- qed
- with tdef show "a \<le> t" by (rule isLubD2)
- qed
- moreover have "t \<le> b"
- proof -
- have "isUb UNIV A b"
- proof -
- {
- from alb int have
- ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
-
- have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
- proof (rule allI, induct_tac m)
- show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
- next
- fix m n
- assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
- {
- fix p
- from pp have "f (p + n) \<subseteq> f p" by simp
- moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
- hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
- ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
- }
- thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
- qed
- have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
- proof ((rule allI)+, rule impI)
- fix \<alpha>::nat and \<beta>::nat
- assume "\<beta> \<le> \<alpha>"
- hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
- then obtain k where "\<alpha> = \<beta> + k" ..
- moreover
- from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
- ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
- qed
-
- fix m
- {
- assume "m \<ge> n"
- with subsetm have "f m \<subseteq> f n" by simp
- with ain have "\<forall>x\<in>f m. x \<le> b" by auto
- moreover
- from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
- ultimately have "?g m \<le> b" by auto
- }
- moreover
- {
- assume "\<not>(m \<ge> n)"
- hence "m < n" by simp
- with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
- from closed obtain ma and mb where
- "f m = closed_int ma mb \<and> ma \<le> mb" by blast
- hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
- from one alb sub fm int have "ma \<le> b" using closed_subset by blast
- moreover have "(?g m) = ma"
- proof -
- from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
- moreover from one have
- "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
- by (rule closed_int_least)
- with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
- ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
- thus "?g m = ma" by auto
- qed
- ultimately have "?g m \<le> b" by simp
- }
- ultimately have "?g m \<le> b" by (rule case_split)
- }
- with Adef have "\<forall>y\<in>A. y\<le>b" by auto
- hence "A *<= b" by (unfold setle_def)
- moreover have "b \<in> (UNIV::real set)" by simp
- ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
- thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
- qed
- with tdef show "t \<le> b" by (rule isLub_le_isUb)
- qed
- ultimately have "t \<in> closed_int a b" by (rule closed_mem)
- with int show "t \<in> f n" by simp
- qed
- hence "t \<in> (\<Inter>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
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-proof -
- {
- assume clb: "c < b"
- {
- assume cla: "c < a"
- from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
- with alb have
- "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
- by auto
- hence
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by auto
- }
- moreover
- {
- assume ncla: "\<not>(c < a)"
- with clb have cdef: "a \<le> c \<and> 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\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
- moreover from cdef kagc have "ka \<ge> a" by simp
- hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
- ultimately have
- "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
- using kalb by auto
- hence
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by auto
-
- }
- ultimately have
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by (rule case_split)
- }
- moreover
- {
- assume "\<not> (c < b)"
- hence cgeb: "c \<ge> 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 \<and> kb < c" by auto
- moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
- moreover from kblb have
- "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
- ultimately have
- "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
- by simp
- hence
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by auto
- }
- ultimately show ?thesis by (rule case_split)
-qed
-
-subsection {* newInt: Interval generation *}
-
-text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
-closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
-does not contain @{text "f (Suc n)"}. With the base case defined such
-that @{text "(f 0)\<notin>newInt 0 f"}. *}
-
-subsubsection {* Definition *}
-
-primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
- "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
- | "newInt (Suc n) f =
- (SOME e. (\<exists>e1 e2.
- e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> (newInt n f) \<and>
- (f (Suc n)) \<notin> e)
- )"
-
-declare newInt.simps [code del]
-
-subsubsection {* Properties *}
-
-text {* We now show that every application of newInt returns an
-appropriate interval. *}
-
-lemma newInt_ex:
- "\<exists>a b. a < b \<and>
- newInt (Suc n) f = closed_int a b \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f"
-proof (induct n)
- case 0
-
- let ?e = "SOME e. \<exists>e1 e2.
- e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
- f (Suc 0) \<notin> e"
-
- have "newInt (Suc 0) f = ?e" by auto
- moreover
- have "f 0 + 1 < f 0 + 2" by simp
- with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
- f (Suc 0) \<notin> (closed_int ka kb)" .
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
- e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
- hence
- "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
- ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
- by (rule someI_ex)
- ultimately have "\<exists>e1 e2. e1 < e2 \<and>
- newInt (Suc 0) f = closed_int e1 e2 \<and>
- newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
- f (Suc 0) \<notin> newInt (Suc 0) f" by simp
- thus
- "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
- newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
- by simp
-next
- case (Suc n)
- hence "\<exists>a b.
- a < b \<and>
- newInt (Suc n) f = closed_int a b \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f" by simp
- then obtain a and b where ab: "a < b \<and>
- newInt (Suc n) f = closed_int a b \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f" by auto
- hence cab: "closed_int a b = newInt (Suc n) f" by simp
-
- let ?e = "SOME e. \<exists>e1 e2.
- e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> closed_int a b \<and>
- f (Suc (Suc n)) \<notin> 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
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
- f (Suc (Suc n)) \<notin> closed_int ka kb" .
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
- closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
- by simp
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
- e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
- hence
- "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
- ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
- with ab ni show
- "\<exists>ka kb. ka < kb \<and>
- newInt (Suc (Suc n)) f = closed_int ka kb \<and>
- newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
- f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
-qed
-
-lemma newInt_subset:
- "newInt (Suc n) f \<subseteq> 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:
- "\<forall>n. f n \<notin> (\<Inter>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 \<notin> newInt n f" by (unfold closed_int_def, simp)
- }
- moreover
- {
- assume "\<not> 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
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
- newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
- then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
- with ndef have "f n \<notin> newInt n f" by simp
- }
- ultimately have "f n \<notin> newInt n f" by (rule case_split)
- thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
-qed
-
-
-lemma newInt_notempty:
- "(\<Inter>n. newInt n f) \<noteq> {}"
-proof -
- let ?g = "\<lambda>n. newInt n f"
- have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
- proof
- fix n
- show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
- qed
- moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
- proof
- fix n::nat
- {
- assume "n = 0"
- then have
- "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
- by simp
- hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
- }
- moreover
- {
- assume "\<not> n = 0"
- then have "n > 0" by simp
- then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
- have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
- (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
- by (rule newInt_ex)
- then obtain a and b where
- "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
- with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
- hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
- }
- ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
- qed
- ultimately show ?thesis by (rule NIP)
-qed
-
-
-subsection {* Final Theorem *}
-
-theorem real_non_denum:
- shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
-proof -- "by contradiction"
- assume "\<exists>f::nat\<Rightarrow>real. surj f"
- then obtain f::"nat\<Rightarrow>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 "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
- moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
- ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
- moreover from rangeF have "x \<in> range f" by simp
- ultimately show False by blast
-qed
-
-end
--- 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 *}
--- 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 \<inter> 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 *}
--- 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: "\<not> 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]
--- 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\<Colon>ordered_idom \<Rightarrow> bool"
-where
- "neg Z \<longleftrightarrow> Z < 0"
-
definition (*for simplifying equalities*)
iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
where
"iszero z \<longleftrightarrow> 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 \<le> 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\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
@@ -1267,11 +1196,6 @@
linorder_not_less [of "number_of w" "number_of v", symmetric,
standard]
-lemma le_number_of_eq:
- "((number_of x::'a::{ordered_idom,number_ring}) \<le> 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. *}
--- 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 \
--- /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 "\<real>"} is not denumerable. In other
+words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} 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
+"\<nat>\<Rightarrow>\<real>"} 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 \<Rightarrow> real \<Rightarrow> real set" where
+ "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
+
+subsubsection {* Properties *}
+
+lemma closed_int_subset:
+ assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
+ shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
+proof -
+ {
+ fix x::real
+ assume "x \<in> closed_int x1 y1"
+ hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
+ with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
+ hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
+ }
+ thus ?thesis by auto
+qed
+
+lemma closed_int_least:
+ assumes a: "a \<le> b"
+ shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
+proof
+ from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
+ thus "a \<in> closed_int a b" by (unfold closed_int_def)
+next
+ have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
+ thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
+qed
+
+lemma closed_int_most:
+ assumes a: "a \<le> b"
+ shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
+proof
+ from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
+ thus "b \<in> closed_int a b" by (unfold closed_int_def)
+next
+ have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
+ thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
+qed
+
+lemma closed_not_empty:
+ shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"
+ by (auto dest: closed_int_least)
+
+lemma closed_mem:
+ assumes "a \<le> c" and "c \<le> b"
+ shows "c \<in> closed_int a b"
+ using assms unfolding closed_int_def by auto
+
+lemma closed_subset:
+ assumes ac: "a \<le> b" "c \<le> d"
+ assumes closed: "closed_int a b \<subseteq> closed_int c d"
+ shows "b \<ge> c"
+proof -
+ from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
+ hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
+ with ac have "c\<le>b \<and> b\<le>d" by simp
+ thus ?thesis by auto
+qed
+
+
+subsection {* Nested Interval Property *}
+
+theorem NIP:
+ fixes f::"nat \<Rightarrow> real set"
+ assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
+ and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
+ shows "(\<Inter>n. f n) \<noteq> {}"
+proof -
+ let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
+ have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
+ proof
+ fix n
+ from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
+ then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
+ hence "a \<le> b" ..
+ with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
+ with fn show "\<exists>x. x\<in>(f n)" by simp
+ qed
+
+ have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
+ proof
+ fix n
+ from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
+ then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
+ hence "a \<le> b" by simp
+ hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
+ with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
+ hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
+ thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>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 ` \<nat>" by simp
+ ultimately have "\<exists>x. x\<in>A"
+ proof -
+ have "(0::nat) \<in> \<nat>" by simp
+ moreover have "?g 0 = ?g 0" by simp
+ ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
+ with Adef have "?g 0 \<in> A" by simp
+ thus ?thesis ..
+ qed
+
+ -- "Now show that A is bounded above ..."
+ moreover have "\<exists>y. isUb (UNIV::real set) A y"
+ proof -
+ {
+ fix n
+ from ne have ex: "\<exists>x. x\<in>(f n)" ..
+ from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
+ moreover
+ from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
+ then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
+ hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
+ ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
+ with ex have "(?g n) \<le> b" by auto
+ hence "\<exists>b. (?g n) \<le> b" by auto
+ }
+ hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
+
+ have fs: "\<forall>n::nat. f n \<subseteq> f 0"
+ proof (rule allI, induct_tac n)
+ show "f 0 \<subseteq> f 0" by simp
+ next
+ fix n
+ assume "f n \<subseteq> f 0"
+ moreover from subset have "f (Suc n) \<subseteq> f n" ..
+ ultimately show "f (Suc n) \<subseteq> f 0" by simp
+ qed
+ have "\<forall>n. (?g n)\<in>(f 0)"
+ proof
+ fix n
+ from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
+ hence "?g n \<in> f n" ..
+ with fs show "?g n \<in> f 0" by auto
+ qed
+ moreover from closed
+ obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
+ ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
+ with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
+ with Adef have "\<forall>y\<in>A. y\<le>b" by auto
+ hence "A *<= b" by (unfold setle_def)
+ moreover have "b \<in> (UNIV::real set)" by simp
+ ultimately have "A *<= b \<and> b \<in> (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 "\<exists>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 "\<forall>n. t \<in> f n"
+ proof
+ fix n::nat
+ from closed obtain a and b where
+ int: "f n = closed_int a b" and alb: "a \<le> b" by blast
+
+ have "t \<ge> a"
+ proof -
+ have "a \<in> A"
+ proof -
+ (* by construction *)
+ from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
+ using closed_int_least by blast
+ moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
+ proof clarsimp
+ fix e
+ assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
+ from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
+
+ from ein aux have "a \<le> e \<and> e \<le> e" by auto
+ moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
+ ultimately show "e = a" by simp
+ qed
+ hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> 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 \<in> \<nat>" by simp
+ ultimately have "n \<in> \<nat>"
+ apply -
+ apply (subst(asm) eq_sym_conv)
+ apply (erule subst)
+ .
+ }
+ with Adef have "(?g n) \<in> A" by auto
+ ultimately show ?thesis by simp
+ qed
+ with tdef show "a \<le> t" by (rule isLubD2)
+ qed
+ moreover have "t \<le> b"
+ proof -
+ have "isUb UNIV A b"
+ proof -
+ {
+ from alb int have
+ ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
+
+ have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
+ proof (rule allI, induct_tac m)
+ show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
+ next
+ fix m n
+ assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
+ {
+ fix p
+ from pp have "f (p + n) \<subseteq> f p" by simp
+ moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
+ hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
+ ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
+ }
+ thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
+ qed
+ have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
+ proof ((rule allI)+, rule impI)
+ fix \<alpha>::nat and \<beta>::nat
+ assume "\<beta> \<le> \<alpha>"
+ hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
+ then obtain k where "\<alpha> = \<beta> + k" ..
+ moreover
+ from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
+ ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
+ qed
+
+ fix m
+ {
+ assume "m \<ge> n"
+ with subsetm have "f m \<subseteq> f n" by simp
+ with ain have "\<forall>x\<in>f m. x \<le> b" by auto
+ moreover
+ from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
+ ultimately have "?g m \<le> b" by auto
+ }
+ moreover
+ {
+ assume "\<not>(m \<ge> n)"
+ hence "m < n" by simp
+ with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
+ from closed obtain ma and mb where
+ "f m = closed_int ma mb \<and> ma \<le> mb" by blast
+ hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
+ from one alb sub fm int have "ma \<le> b" using closed_subset by blast
+ moreover have "(?g m) = ma"
+ proof -
+ from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
+ moreover from one have
+ "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
+ by (rule closed_int_least)
+ with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
+ ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
+ thus "?g m = ma" by auto
+ qed
+ ultimately have "?g m \<le> b" by simp
+ }
+ ultimately have "?g m \<le> b" by (rule case_split)
+ }
+ with Adef have "\<forall>y\<in>A. y\<le>b" by auto
+ hence "A *<= b" by (unfold setle_def)
+ moreover have "b \<in> (UNIV::real set)" by simp
+ ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
+ thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
+ qed
+ with tdef show "t \<le> b" by (rule isLub_le_isUb)
+ qed
+ ultimately have "t \<in> closed_int a b" by (rule closed_mem)
+ with int show "t \<in> f n" by simp
+ qed
+ hence "t \<in> (\<Inter>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
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+proof -
+ {
+ assume clb: "c < b"
+ {
+ assume cla: "c < a"
+ from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
+ with alb have
+ "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
+ by auto
+ hence
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by auto
+ }
+ moreover
+ {
+ assume ncla: "\<not>(c < a)"
+ with clb have cdef: "a \<le> c \<and> 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\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
+ moreover from cdef kagc have "ka \<ge> a" by simp
+ hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
+ ultimately have
+ "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
+ using kalb by auto
+ hence
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by auto
+
+ }
+ ultimately have
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by (rule case_split)
+ }
+ moreover
+ {
+ assume "\<not> (c < b)"
+ hence cgeb: "c \<ge> 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 \<and> kb < c" by auto
+ moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
+ moreover from kblb have
+ "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
+ ultimately have
+ "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
+ by simp
+ hence
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
+ by auto
+ }
+ ultimately show ?thesis by (rule case_split)
+qed
+
+subsection {* newInt: Interval generation *}
+
+text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
+closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
+does not contain @{text "f (Suc n)"}. With the base case defined such
+that @{text "(f 0)\<notin>newInt 0 f"}. *}
+
+subsubsection {* Definition *}
+
+primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
+ "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
+ | "newInt (Suc n) f =
+ (SOME e. (\<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> (newInt n f) \<and>
+ (f (Suc n)) \<notin> e)
+ )"
+
+declare newInt.simps [code del]
+
+subsubsection {* Properties *}
+
+text {* We now show that every application of newInt returns an
+appropriate interval. *}
+
+lemma newInt_ex:
+ "\<exists>a b. a < b \<and>
+ newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
+proof (induct n)
+ case 0
+
+ let ?e = "SOME e. \<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ f (Suc 0) \<notin> e"
+
+ have "newInt (Suc 0) f = ?e" by auto
+ moreover
+ have "f 0 + 1 < f 0 + 2" by simp
+ with closed_subset_ex have
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ f (Suc 0) \<notin> (closed_int ka kb)" .
+ hence
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
+ e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
+ hence
+ "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
+ ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
+ by (rule someI_ex)
+ ultimately have "\<exists>e1 e2. e1 < e2 \<and>
+ newInt (Suc 0) f = closed_int e1 e2 \<and>
+ newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
+ f (Suc 0) \<notin> newInt (Suc 0) f" by simp
+ thus
+ "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
+ newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
+ by simp
+next
+ case (Suc n)
+ hence "\<exists>a b.
+ a < b \<and>
+ newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f" by simp
+ then obtain a and b where ab: "a < b \<and>
+ newInt (Suc n) f = closed_int a b \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f" by auto
+ hence cab: "closed_int a b = newInt (Suc n) f" by simp
+
+ let ?e = "SOME e. \<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> closed_int a b \<and>
+ f (Suc (Suc n)) \<notin> 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
+ "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
+ f (Suc (Suc n)) \<notin> closed_int ka kb" .
+ hence
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
+ closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
+ by simp
+ hence
+ "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
+ e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
+ hence
+ "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
+ ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
+ with ab ni show
+ "\<exists>ka kb. ka < kb \<and>
+ newInt (Suc (Suc n)) f = closed_int ka kb \<and>
+ newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
+ f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
+qed
+
+lemma newInt_subset:
+ "newInt (Suc n) f \<subseteq> 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:
+ "\<forall>n. f n \<notin> (\<Inter>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 \<notin> newInt n f" by (unfold closed_int_def, simp)
+ }
+ moreover
+ {
+ assume "\<not> 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
+ "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
+ newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
+ then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
+ with ndef have "f n \<notin> newInt n f" by simp
+ }
+ ultimately have "f n \<notin> newInt n f" by (rule case_split)
+ thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
+qed
+
+
+lemma newInt_notempty:
+ "(\<Inter>n. newInt n f) \<noteq> {}"
+proof -
+ let ?g = "\<lambda>n. newInt n f"
+ have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
+ proof
+ fix n
+ show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
+ qed
+ moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
+ proof
+ fix n::nat
+ {
+ assume "n = 0"
+ then have
+ "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
+ by simp
+ hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+ }
+ moreover
+ {
+ assume "\<not> n = 0"
+ then have "n > 0" by simp
+ then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
+
+ have
+ "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
+ (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
+ by (rule newInt_ex)
+ then obtain a and b where
+ "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
+ with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
+ hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+ }
+ ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
+ qed
+ ultimately show ?thesis by (rule NIP)
+qed
+
+
+subsection {* Final Theorem *}
+
+theorem real_non_denum:
+ shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
+proof -- "by contradiction"
+ assume "\<exists>f::nat\<Rightarrow>real. surj f"
+ then obtain f::"nat\<Rightarrow>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 "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
+ moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
+ ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
+ moreover from rangeF have "x \<in> range f" by simp
+ ultimately show False by blast
+qed
+
+end
--- 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
--- 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: "\<not> (neg (Numeral0::int))"
by simp
--- 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
--- 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 \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
- else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
+ "(number_of k \<Colon> 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 \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
+ (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
+
+lemma times_inat_simps [simp, code]:
+ "Fin m * Fin n = Fin (m * n)"
+ "\<infinity> * \<infinity> = \<infinity>"
+ "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
+ "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
+ 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) \<noteq> 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 \<le> b" and "0 \<le> c"
+ thus "c * a \<le> 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 \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
"(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
--- 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 \<inter> Inr ` B = {}")
- apply (simp add: card_Un_disjoint card_image)
- apply fast
- done
-
lemma (in type_definition) univ:
"UNIV = Abs ` A"
proof
--- 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 ("(_\<twosuperior>)" [1000] 999)
+subsection {* Predicate for negative binary numbers *}
+
+definition
+ neg :: "int \<Rightarrow> bool"
+where
+ "neg Z \<longleftrightarrow> 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 \<le> 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' \<longleftrightarrow>
+ (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) \<le> number_of v' \<longleftrightarrow>
+ (if v \<le> v' then True else v \<le> 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\<le>0"} and @{term "0\<le>n"}.*}
lemma eq_number_of_0 [simp]:
- "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"
- unfolding nat_number_of_def number_of_is_id by auto
+ "number_of v = (0::nat) \<longleftrightarrow> v \<le> 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 \<longleftrightarrow> number_of v \<le> (0::int)"
+ "(0::nat) = number_of v \<longleftrightarrow> v \<le> 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 \<longleftrightarrow> 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
--- 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
--- 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])
--- 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 \<le> 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 \<le> x)" by (simp add: less_int_code)
-lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> 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 \<le> y for bit strings *)
-lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (simp add: less_eq_int_code)
-lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (simp add: less_eq_int_code)
-lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (simp add: less_eq_int_code)
-lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (simp add: less_eq_int_code)
-lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (simp add: less_eq_int_code)
-lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (simp add: less_eq_int_code)
-lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (simp add: less_eq_int_code)
-lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (simp add: less_eq_int_code)
-lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (simp add: less_eq_int_code)
-lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (simp add: less_eq_int_code)
-lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (simp add: less_eq_int_code)
-lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (simp add: less_eq_int_code)
-lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (simp add: less_eq_int_code)
-lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> 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 \<and> lezero y) \<or> (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) \<and> (\<not> (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) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
--- 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
--- 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;
--- 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 =
--- 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;
+
--- 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.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
+ (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression
>> (fn (loc, expr) =>
Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
--- 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;
--- 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;