diff -r 8f84a608883d -r ea97aa6aeba2 Admin/Mercurial/misc.diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Mercurial/misc.diff Tue Dec 30 11:10:01 2008 +0100
@@ -0,0 +1,20 @@
+diff -r hgweb/webcommands.py hgweb/webcommands.py
+653c653
+< desc = templatefilters.firstline(ctx.description())
+---
+> desc = ctx.description()
+diff -r templates/atom/changelogentry.tmpl templates/atom/changelogentry.tmpl
+2c2
+< #desc|strip|firstline|strip|escape#
+---
+> #desc|strip|escape#
+diff -r templates/rss/changelogentry.tmpl templates/rss/changelogentry.tmpl
+2c2
+< #desc|strip|firstline|strip|escape#
+---
+> #desc|strip|escape#
+diff -r templates/rss/filelogentry.tmpl templates/rss/filelogentry.tmpl
+2c2
+< #desc|strip|firstline|strip|escape#
+---
+> #desc|strip|escape#
diff -r 8f84a608883d -r ea97aa6aeba2 Admin/build
--- a/Admin/build Tue Dec 30 08:18:54 2008 +0100
+++ b/Admin/build Tue Dec 30 11:10:01 2008 +0100
@@ -7,7 +7,7 @@
#paranoia setting for sunbroy
PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH"
-PATH="/home/scala/scala/bin:$PATH"
+PATH="/home/scala/current/bin:$PATH"
## directory layout
@@ -101,15 +101,6 @@
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
"$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
popd >/dev/null
-
- if [ -d "$HOME/lib/jedit/current" ]; then
- pushd "$ISABELLE_HOME/lib/jedit/plugin" >/dev/null
- ./mk
- [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
- popd >/dev/null
- else
- echo "Warning: skipping jedit plugin"
- fi
}
diff -r 8f84a608883d -r ea97aa6aeba2 Admin/isatest/settings/at-mac-poly-5.1-para
--- a/Admin/isatest/settings/at-mac-poly-5.1-para Tue Dec 30 08:18:54 2008 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Tue Dec 30 11:10:01 2008 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 2000"
+ ML_OPTIONS="--immutable 800 --mutable 1200"
ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e
diff -r 8f84a608883d -r ea97aa6aeba2 CONTRIBUTORS
--- a/CONTRIBUTORS Tue Dec 30 08:18:54 2008 +0100
+++ b/CONTRIBUTORS Tue Dec 30 11:10:01 2008 +0100
@@ -7,6 +7,9 @@
Contributions to this Isabelle version
--------------------------------------
+* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
+ Method "sizechange" for advanced termination proofs.
+
* November 2008: Timothy Bourke, NICTA
Performance improvement (factor 50) for find_theorems.
@@ -204,5 +207,3 @@
* 2004/2005: Tjark Weber, TUM
SAT solver method using zChaff.
Improved version of HOL/refute.
-
-$Id$
diff -r 8f84a608883d -r ea97aa6aeba2 INSTALL
--- a/INSTALL Tue Dec 30 08:18:54 2008 +0100
+++ b/INSTALL Tue Dec 30 11:10:01 2008 +0100
@@ -85,6 +85,3 @@
Note that the site-wide Isabelle installation may already provide
Isabelle executables in some global bin directory (such as
/usr/local/bin).
-
-
-$Id$
diff -r 8f84a608883d -r ea97aa6aeba2 NEWS
--- a/NEWS Tue Dec 30 08:18:54 2008 +0100
+++ b/NEWS Tue Dec 30 11:10:01 2008 +0100
@@ -42,6 +42,11 @@
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
Isabelle distribution.
+* Proofs of fully specified statements are run in parallel on
+multi-core systems. A speedup factor of 2-3 can be expected on a
+regular 4-core machine, if the initial heap space is made reasonably
+large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later]
+
* The Isabelle System Manual (system) has been updated, with formally
checked references as hyperlinks.
@@ -55,8 +60,8 @@
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML
interface instead.
-* There is a new lexical item "float" with syntax ["-"] digit+ "." digit+,
-without spaces.
+* There is a new syntactic category "float_const" for signed decimal
+fractions (e.g. 123.45 or -123.45).
*** Pure ***
@@ -152,11 +157,12 @@
*** HOL ***
-* Made repository layout more coherent with logical
-distribution structure:
+* Made source layout more coherent with logical distribution
+structure:
src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy
src/HOL/Library/Code_Message.thy ~> src/HOL/
+ src/HOL/Library/Dense_Linear_Order.thy ~> src/HOL/
src/HOL/Library/GCD.thy ~> src/HOL/
src/HOL/Library/Order_Relation.thy ~> src/HOL/
src/HOL/Library/Parity.thy ~> src/HOL/
@@ -172,6 +178,7 @@
src/HOL/Complex/Complex_Main.thy ~> src/HOL/
src/HOL/Complex/Complex.thy ~> src/HOL/
src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/
+ src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/
src/HOL/Hyperreal/Deriv.thy ~> src/HOL/
src/HOL/Hyperreal/Fact.thy ~> src/HOL/
src/HOL/Hyperreal/Integration.thy ~> src/HOL/
@@ -181,9 +188,12 @@
src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/
src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/
src/HOL/Hyperreal/Series.thy ~> src/HOL/
+ src/HOL/Hyperreal/SEQ.thy ~> src/HOL/
src/HOL/Hyperreal/Taylor.thy ~> src/HOL/
src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/
src/HOL/Real/Float ~> src/HOL/Library/
+ src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach
+ src/HOL/Real/RealVector.thy ~> src/HOL/
src/HOL/arith_data.ML ~> src/HOL/Tools
src/HOL/hologic.ML ~> src/HOL/Tools
@@ -239,6 +249,10 @@
mechanisms may be specified (currently, [SML], [code] or [nbe]). See
further src/HOL/ex/Eval_Examples.thy.
+* New method "sizechange" to automate termination proofs using (a
+modification of) the size-change principle. Requires SAT solver. See
+src/HOL/ex/Termination.thy for examples.
+
* HOL/Orderings: class "wellorder" moved here, with explicit induction
rule "less_induct" as assumption. For instantiation of "wellorder" by
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.
@@ -388,6 +402,14 @@
*** ML ***
+* High-level support for concurrent ML programming, see
+src/Pure/Cuncurrent. The data-oriented model of "future values" is
+particularly convenient to organize independent functional
+computations. The concept of "synchronized variables" provides a
+higher-order interface for components with shared state, avoiding the
+delicate details of mutexes and condition variables. [Poly/ML 5.2.1
+or later]
+
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
to 'a -> thm, while results are always tagged with an authentic oracle
name. The Isar command 'oracle' is now polymorphic, no argument type
@@ -857,8 +879,8 @@
print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY.
* Functions system/system_out provide a robust way to invoke external
-shell commands, with propagation of interrupts (requires Poly/ML 5.2).
-Do not use OS.Process.system etc. from the basis library!
+shell commands, with propagation of interrupts (requires Poly/ML
+5.2.1). Do not use OS.Process.system etc. from the basis library!
*** System ***
@@ -5953,6 +5975,3 @@
types;
:mode=text:wrap=hard:maxLineLen=72:
-
-
-$Id$
diff -r 8f84a608883d -r ea97aa6aeba2 build
--- a/build Tue Dec 30 08:18:54 2008 +0100
+++ b/build Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# build - compile the Isabelle system and object-logics
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarAdvanced/Classes/style.sty
--- a/doc-src/IsarAdvanced/Classes/style.sty Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/style.sty Tue Dec 30 11:10:01 2008 +0100
@@ -30,7 +30,7 @@
\pagestyle{headings}
\binperiod
-\underscoreon
+\underscoreoff
\renewcommand{\isadigit}[1]{\isamath{#1}}
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarAdvanced/Codegen/style.sty
--- a/doc-src/IsarAdvanced/Codegen/style.sty Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/style.sty Tue Dec 30 11:10:01 2008 +0100
@@ -42,7 +42,7 @@
\pagestyle{headings}
\binperiod
-\underscoreon
+\underscoreoff
\renewcommand{\isadigit}[1]{\isamath{#1}}
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Dec 30 11:10:01 2008 +0100
@@ -107,18 +107,23 @@
section {* Thread-safe programming *}
text {*
- Recent versions of Poly/ML (5.2 or later) support multithreaded
- execution based on native operating system threads of the underlying
- platform. Thus threads will actually be executed in parallel on
- multi-core systems. A speedup-factor of approximately 2--4 can be
- expected for large well-structured Isabelle sessions, where theories
- are organized as a graph with sufficiently many independent nodes.
+ Recent versions of Poly/ML (5.2.1 or later) support robust
+ multithreaded execution, based on native operating system threads of
+ the underlying platform. Thus threads will actually be executed in
+ parallel on multi-core systems. A speedup-factor of approximately
+ 1.5--3 can be expected on a regular 4-core machine.\footnote{There
+ is some inherent limitation of the speedup factor due to garbage
+ collection, which is still sequential. It helps to provide initial
+ heap space generously, using the \texttt{-H} option of Poly/ML.}
+ Threads also help to organize advanced operations of the system,
+ with explicit communication between sub-components, real-time
+ conditions, time-outs etc.
- Threads lack the memory protection of separate processes, but
+ Threads lack the memory protection of separate processes, and
operate concurrently on shared heap memory. This has the advantage
that results of independent computations are immediately available
- to other threads, without requiring explicit communication,
- reloading, or even recoding of data.
+ to other threads, without requiring untyped character streams,
+ awkward serialization etc.
On the other hand, some programming guidelines need to be observed
in order to make unprotected parallelism work out smoothly. While
@@ -143,27 +148,29 @@
\end{itemize}
- Note that ML bindings within the toplevel environment (@{verbatim
- "type"}, @{verbatim val}, @{verbatim "structure"} etc.) due to
- run-time invocation of the compiler are non-critical, because
- Isabelle/Isar incorporates such bindings within the theory or proof
- context.
-
The majority of tools implemented within the Isabelle/Isar framework
will not require any of these critical elements: nothing special
needs to be observed when staying in the purely functional fragment
of ML. Note that output via the official Isabelle channels does not
- even count as direct I/O in the above sense, so the operations @{ML
- "writeln"}, @{ML "warning"}, @{ML "tracing"} etc.\ are safe.
+ count as direct I/O, so the operations @{ML "writeln"}, @{ML
+ "warning"}, @{ML "tracing"} etc.\ are safe.
- \paragraph{Multithreading in Isabelle/Isar.} Our parallel execution
- model is centered around the theory loader. Whenever a given
- subgraph of theories needs to be updated, the system schedules a
- number of threads to process the sources as required, while
- observing their dependencies. Thus concurrency is limited to
- independent nodes according to the theory import relation.
+ Moreover, ML bindings within the toplevel environment (@{verbatim
+ "type"}, @{verbatim val}, @{verbatim "structure"} etc.) due to
+ run-time invocation of the compiler are also safe, because
+ Isabelle/Isar manages this as part of the theory or proof context.
- Any user-code that works relatively to the present background theory
+ \paragraph{Multithreading in Isabelle/Isar.} The theory loader
+ automatically exploits the overall parallelism of independent nodes
+ in the development graph, as well as the inherent irrelevance of
+ proofs for goals being fully specified in advance. This means,
+ checking of individual Isar proofs is parallelized by default.
+ Beyond that, very sophisticated proof tools may use local
+ parallelism internally, via the general programming model of
+ ``future values'' (see also @{"file"
+ "~~/src/Pure/Concurrent/future.ML"}).
+
+ Any ML code that works relatively to the present background theory
is already safe. Contextual data may be easily stored within the
theory or proof context, thanks to the generic data concept of
Isabelle/Isar (see \secref{sec:context-data}). This greatly
@@ -179,9 +186,13 @@
quickly, otherwise parallel execution performance may degrade
significantly.
- Despite this potential bottle-neck, we refrain from fine-grained
- locking mechanism within user-code: the restriction to a single lock
- prevents deadlocks without demanding special precautions.
+ Despite this potential bottle-neck, centralized locking is
+ convenient, because it prevents deadlocks without demanding special
+ precautions. Explicit communication demands other means, though.
+ The high-level abstraction of synchronized variables @{"file"
+ "~~/src/Pure/Concurrent/synchronized.ML"} enables parallel
+ components to communicate via shared state; see also @{"file"
+ "~~/src/Pure/Concurrent/mailbox.ML"} as canonical example.
\paragraph{Good conduct of impure programs.} The following
guidelines enable non-functional programs to participate in
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Dec 30 11:10:01 2008 +0100
@@ -128,18 +128,23 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Recent versions of Poly/ML (5.2 or later) support multithreaded
- execution based on native operating system threads of the underlying
- platform. Thus threads will actually be executed in parallel on
- multi-core systems. A speedup-factor of approximately 2--4 can be
- expected for large well-structured Isabelle sessions, where theories
- are organized as a graph with sufficiently many independent nodes.
+Recent versions of Poly/ML (5.2.1 or later) support robust
+ multithreaded execution, based on native operating system threads of
+ the underlying platform. Thus threads will actually be executed in
+ parallel on multi-core systems. A speedup-factor of approximately
+ 1.5--3 can be expected on a regular 4-core machine.\footnote{There
+ is some inherent limitation of the speedup factor due to garbage
+ collection, which is still sequential. It helps to provide initial
+ heap space generously, using the \texttt{-H} option of Poly/ML.}
+ Threads also help to organize advanced operations of the system,
+ with explicit communication between sub-components, real-time
+ conditions, time-outs etc.
- Threads lack the memory protection of separate processes, but
+ Threads lack the memory protection of separate processes, and
operate concurrently on shared heap memory. This has the advantage
that results of independent computations are immediately available
- to other threads, without requiring explicit communication,
- reloading, or even recoding of data.
+ to other threads, without requiring untyped character streams,
+ awkward serialization etc.
On the other hand, some programming guidelines need to be observed
in order to make unprotected parallelism work out smoothly. While
@@ -163,25 +168,26 @@
\end{itemize}
- Note that ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
- run-time invocation of the compiler are non-critical, because
- Isabelle/Isar incorporates such bindings within the theory or proof
- context.
-
The majority of tools implemented within the Isabelle/Isar framework
will not require any of these critical elements: nothing special
needs to be observed when staying in the purely functional fragment
of ML. Note that output via the official Isabelle channels does not
- even count as direct I/O in the above sense, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe.
+ count as direct I/O, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe.
- \paragraph{Multithreading in Isabelle/Isar.} Our parallel execution
- model is centered around the theory loader. Whenever a given
- subgraph of theories needs to be updated, the system schedules a
- number of threads to process the sources as required, while
- observing their dependencies. Thus concurrency is limited to
- independent nodes according to the theory import relation.
+ Moreover, ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
+ run-time invocation of the compiler are also safe, because
+ Isabelle/Isar manages this as part of the theory or proof context.
- Any user-code that works relatively to the present background theory
+ \paragraph{Multithreading in Isabelle/Isar.} The theory loader
+ automatically exploits the overall parallelism of independent nodes
+ in the development graph, as well as the inherent irrelevance of
+ proofs for goals being fully specified in advance. This means,
+ checking of individual Isar proofs is parallelized by default.
+ Beyond that, very sophisticated proof tools may use local
+ parallelism internally, via the general programming model of
+ ``future values'' (see also \hyperlink{file.~~/src/Pure/Concurrent/future.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}future{\isachardot}ML}}}}).
+
+ Any ML code that works relatively to the present background theory
is already safe. Contextual data may be easily stored within the
theory or proof context, thanks to the generic data concept of
Isabelle/Isar (see \secref{sec:context-data}). This greatly
@@ -197,9 +203,11 @@
quickly, otherwise parallel execution performance may degrade
significantly.
- Despite this potential bottle-neck, we refrain from fine-grained
- locking mechanism within user-code: the restriction to a single lock
- prevents deadlocks without demanding special precautions.
+ Despite this potential bottle-neck, centralized locking is
+ convenient, because it prevents deadlocks without demanding special
+ precautions. Explicit communication demands other means, though.
+ The high-level abstraction of synchronized variables \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} enables parallel
+ components to communicate via shared state; see also \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} as canonical example.
\paragraph{Good conduct of impure programs.} The following
guidelines enable non-functional programs to participate in
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Dec 30 11:10:01 2008 +0100
@@ -804,12 +804,15 @@
@{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \"} \\
@{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \"} \\
@{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \"} \\
+ @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \"} \\
@{method_def (HOL) metis} & : & @{text method} \\
\end{matharray}
\begin{rail}
'sledgehammer' (nameref *)
;
+ 'atp\_messages' ('(' nat ')')?
+ ;
'metis' thmrefs
;
@@ -842,6 +845,12 @@
\item @{command (HOL) atp_kill} terminates all presently running
provers.
+ \item @{command (HOL) atp_messages} displays recent messages issued
+ by automated theorem provers. This allows to examine results that
+ might have got lost due to the asynchronous nature of default
+ @{command (HOL) sledgehammer} output. An optional message limit may
+ be specified (default 5).
+
\item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
with the given facts. Metis is an automated proof tool of medium
strength, but is fully integrated into Isabelle/HOL, with explicit
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Dec 30 11:10:01 2008 +0100
@@ -683,17 +683,23 @@
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
@{syntax_def (inner) num} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\
+ @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
@{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\
@{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\"} @{verbatim "''"} \\
\end{supertabular}
\end{center}
- The token categories @{syntax_ref (inner) num}, @{syntax_ref (inner)
- xnum}, and @{syntax_ref (inner) xstr} are not used in Pure.
- Object-logics may implement numerals and string constants by adding
- appropriate syntax declarations, together with some translation
- functions (e.g.\ see Isabelle/HOL).
+ The token categories @{syntax (inner) num}, @{syntax (inner)
+ float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are
+ not used in Pure. Object-logics may implement numerals and string
+ constants by adding appropriate syntax declarations, together with
+ some translation functions (e.g.\ see Isabelle/HOL).
+
+ The derived categories @{syntax_def (inner) num_const} and
+ @{syntax_def (inner) float_const} provide robust access to @{syntax
+ (inner) num}, and @{syntax (inner) float_token}, respectively: the
+ syntax tree holds a syntactic constant instead of a free variable.
*}
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Dec 30 11:10:01 2008 +0100
@@ -814,12 +814,15 @@
\indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
\end{matharray}
\begin{rail}
'sledgehammer' (nameref *)
;
+ 'atp\_messages' ('(' nat ')')?
+ ;
'metis' thmrefs
;
@@ -850,6 +853,12 @@
\item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
provers.
+ \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
+ by automated theorem provers. This allows to examine results that
+ might have got lost due to the asynchronous nature of default
+ \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may
+ be specified (default 5).
+
\item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
with the given facts. Metis is an automated proof tool of medium
strength, but is fully integrated into Isabelle/HOL, with explicit
diff -r 8f84a608883d -r ea97aa6aeba2 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Dec 30 08:18:54 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Dec 30 11:10:01 2008 +0100
@@ -702,16 +702,21 @@
\indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\
\indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\
\indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
+ \indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
\indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
\indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\
\end{supertabular}
\end{center}
- The token categories \indexref{inner}{syntax}{num}\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \indexref{inner}{syntax}{xnum}\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \indexref{inner}{syntax}{xstr}\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are not used in Pure.
- Object-logics may implement numerals and string constants by adding
- appropriate syntax declarations, together with some translation
- functions (e.g.\ see Isabelle/HOL).%
+ The token categories \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, \hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are
+ not used in Pure. Object-logics may implement numerals and string
+ constants by adding appropriate syntax declarations, together with
+ some translation functions (e.g.\ see Isabelle/HOL).
+
+ The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isacharunderscore}const}}}} and
+ \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isacharunderscore}const}}}} provide robust access to \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, and \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, respectively: the
+ syntax tree holds a syntactic constant instead of a free variable.%
\end{isamarkuptext}%
\isamarkuptrue%
%
diff -r 8f84a608883d -r ea97aa6aeba2 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el Tue Dec 30 08:18:54 2008 +0100
+++ b/etc/isar-keywords-ZF.el Tue Dec 30 11:10:01 2008 +0100
@@ -200,7 +200,6 @@
"use"
"use_thy"
"using"
- "value"
"welcome"
"with"
"{"
@@ -323,7 +322,6 @@
"typ"
"unused_thms"
"use_thy"
- "value"
"welcome"))
(defconst isar-keywords-theory-begin
diff -r 8f84a608883d -r ea97aa6aeba2 etc/isar-keywords.el
--- a/etc/isar-keywords.el Tue Dec 30 08:18:54 2008 +0100
+++ b/etc/isar-keywords.el Tue Dec 30 11:10:01 2008 +0100
@@ -32,6 +32,7 @@
"atom_decl"
"atp_info"
"atp_kill"
+ "atp_messages"
"automaton"
"ax_specification"
"axclass"
@@ -334,6 +335,7 @@
"ML_val"
"atp_info"
"atp_kill"
+ "atp_messages"
"cd"
"class_deps"
"code_deps"
diff -r 8f84a608883d -r ea97aa6aeba2 etc/proofgeneral-settings.el
--- a/etc/proofgeneral-settings.el Tue Dec 30 08:18:54 2008 +0100
+++ b/etc/proofgeneral-settings.el Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,3 @@
-;;;
-;;; $Id$
-;;;
;;; Options for Proof General
;; Examples for sensible settings:
diff -r 8f84a608883d -r ea97aa6aeba2 etc/settings
--- a/etc/settings Tue Dec 30 08:18:54 2008 +0100
+++ b/etc/settings Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
# -*- shell-script -*- :mode=shellscript:
-# $Id$
#
# Isabelle settings -- site defaults.
#
@@ -202,9 +201,8 @@
"/opt/ProofGeneral" \
"")
-PROOFGENERAL_EMACS=$(choosefrom /Applications/Emacs.app/Contents/MacOS/Emacs emacs22)
-PROOFGENERAL_OPTIONS="-p $PROOFGENERAL_EMACS"
-#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true -p $PROOFGENERAL_EMACS"
+PROOFGENERAL_OPTIONS=""
+#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
# Automatic setup of remote fonts
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
diff -r 8f84a608883d -r ea97aa6aeba2 etc/symbols
--- a/etc/symbols Tue Dec 30 08:18:54 2008 +0100
+++ b/etc/symbols Tue Dec 30 11:10:01 2008 +0100
@@ -1,4 +1,3 @@
-# $Id$
# Default interpretation of some Isabelle symbols
\ code: 0x01d7ec font: Isabelle
diff -r 8f84a608883d -r ea97aa6aeba2 etc/user-settings.sample
--- a/etc/user-settings.sample Tue Dec 30 08:18:54 2008 +0100
+++ b/etc/user-settings.sample Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
# -*- shell-script -*-
-# $Id$
#
# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/browser
--- a/lib/Tools/browser Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/browser Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: Isabelle graph browser
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/codegen
--- a/lib/Tools/codegen Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/codegen Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Florian Haftmann, TUM
#
# DESCRIPTION: issue code generation from shell
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/dimacs2hol
--- a/lib/Tools/dimacs2hol Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/dimacs2hol Tue Dec 30 11:10:01 2008 +0100
@@ -1,8 +1,6 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Tjark Weber
-# Copyright 2004
#
# DESCRIPTION: convert DIMACS CNF files into Isabelle/HOL theories
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/display
--- a/lib/Tools/display Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/display Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: display document (in DVI or PDF format)
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/doc
--- a/lib/Tools/doc Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/doc Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: view Isabelle documentation
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/document
--- a/lib/Tools/document Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/document Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: prepare theory session document
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/emacs
--- a/lib/Tools/emacs Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/emacs Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: Proof General / Emacs interface wrapper
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/env
--- a/lib/Tools/env Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/env Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: run a program in a modified environment
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/findlogics
--- a/lib/Tools/findlogics Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/findlogics Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: collect heap names from ISABELLE_PATH
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/getenv
--- a/lib/Tools/getenv Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/getenv Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: get values from Isabelle settings environment
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/install
--- a/lib/Tools/install Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/install Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: install standalone Isabelle executables
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/java
--- a/lib/Tools/java Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/java Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: invoke Java within the Isabelle environment
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/jedit
--- a/lib/Tools/jedit Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/jedit Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: Isabelle/jEdit interface wrapper
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/keywords
--- a/lib/Tools/keywords Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/keywords Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: generate outer syntax keyword files from session logs
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/latex
--- a/lib/Tools/latex Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/latex Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: run LaTeX (and related tools)
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/logo
--- a/lib/Tools/logo Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/logo Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: create an instance of the Isabelle logo
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/make
--- a/lib/Tools/make Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/make Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: Isabelle make utility
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/makeall
--- a/lib/Tools/makeall Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/makeall Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: apply make utility to all logics
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/mkdir
--- a/lib/Tools/mkdir Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/mkdir Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: prepare logic session directory
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/mkfifo
--- a/lib/Tools/mkfifo Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/mkfifo Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: create named pipe
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/mkproject
--- a/lib/Tools/mkproject Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/mkproject Tue Dec 30 11:10:01 2008 +0100
@@ -1,7 +1,6 @@
#!/usr/bin/env bash
#
-# $Id$
-# Author: David Aspinall and Makarius Wenzel
+# Author: David Aspinall
#
# DESCRIPTION: prepare a session directory for PG-Eclipse
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/print
--- a/lib/Tools/print Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/print Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: print document
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/rmfifo
--- a/lib/Tools/rmfifo Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/rmfifo Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: remove named pipe
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/scala
--- a/lib/Tools/scala Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/scala Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: invoke Scala within the Isabelle environment
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/tty
--- a/lib/Tools/tty Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/tty Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: run Isabelle process with plain tty interaction
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/unsymbolize
--- a/lib/Tools/unsymbolize Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/unsymbolize Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: remove unreadable symbol names from sources
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/usedir
--- a/lib/Tools/usedir Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/usedir Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: build object-logic or run examples
@@ -40,6 +39,11 @@
echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
echo " HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
echo
+ echo " ML_PLATFORM=$ML_PLATFORM"
+ echo " ML_HOME=$ML_HOME"
+ echo " ML_SYSTEM=$ML_SYSTEM"
+ echo " ML_OPTIONS=$ML_OPTIONS"
+ echo
exit 1
}
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/version
--- a/lib/Tools/version Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/version Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Stefan Berghofer, TU Muenchen
#
# DESCRIPTION: display Isabelle version
diff -r 8f84a608883d -r ea97aa6aeba2 lib/Tools/yxml
--- a/lib/Tools/yxml Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/Tools/yxml Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: simple XML to YXML converter
diff -r 8f84a608883d -r ea97aa6aeba2 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/jedit/isabelle.xml Tue Dec 30 11:10:01 2008 +0100
@@ -56,6 +56,7 @@
atom_decl
+
attachautomatonavoids
@@ -154,7 +155,6 @@
ifimportsin
- includesinductioninductiveinductive_cases
@@ -286,6 +286,7 @@
statespacestructuresubclass
+ sublocalesubsectsubsectionsubsubsect
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/dimacs2hol.pl
--- a/lib/scripts/dimacs2hol.pl Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/dimacs2hol.pl Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,3 @@
-#
-# $Id$
#
# dimacs2hol.pl - convert files in DIMACS CNF format [1] into Isabelle/HOL
# theories
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/feeder
--- a/lib/scripts/feeder Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/feeder Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# feeder - feed isabelle session
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/feeder.pl
--- a/lib/scripts/feeder.pl Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/feeder.pl Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# feeder.pl - feed isabelle session
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/fileident
--- a/lib/scripts/fileident Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/fileident Tue Dec 30 11:10:01 2008 +0100
@@ -1,7 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
-#
# fileident --- produce file identification based
FILE="$1"
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/getsettings
--- a/lib/scripts/getsettings Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/getsettings Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,5 @@
# -*- shell-script -*- :mode=shellscript:
-# $Id$
+#
# Author: Markus Wenzel, TU Muenchen
#
# getsettings - bash source script to augment current env.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/keywords.pl
--- a/lib/scripts/keywords.pl Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/keywords.pl Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
#
-# $Id$
# Author: Makarius
#
# keywords.pl - generate outer syntax keyword files from session logs
@@ -79,8 +78,6 @@
print ";; Generated from ${sessions}.\n";
print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
print ";;\n";
- print ";; \$", "Id\$\n";
- print ";;\n";
for my $kind (@kinds) {
my @names;
@@ -154,7 +151,6 @@
EOF
print "\n";
print "\n";
- print "\n";
print <<'EOF';
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/polyml-platform
--- a/lib/scripts/polyml-platform Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/polyml-platform Tue Dec 30 11:10:01 2008 +0100
@@ -1,7 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
-#
# polyml-platform --- determine Poly/ML's idea of current hardware and
# operating system type
#
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/polyml-version
--- a/lib/scripts/polyml-version Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/polyml-version Tue Dec 30 11:10:01 2008 +0100
@@ -1,7 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
-#
# polyml-version --- determine Poly/ML runtime system version
echo -n polyml
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-mosml
--- a/lib/scripts/run-mosml Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-mosml Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# Moscow ML 2.00 startup script
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-polyml Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# Poly/ML 5.1/5.2 startup script.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-polyml-4.1.3
--- a/lib/scripts/run-polyml-4.1.3 Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-polyml-4.1.3 Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# Poly/ML 4.x startup script.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-polyml-4.1.4
--- a/lib/scripts/run-polyml-4.1.4 Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-polyml-4.1.4 Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# Poly/ML 4.x startup script.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-polyml-4.2.0
--- a/lib/scripts/run-polyml-4.2.0 Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-polyml-4.2.0 Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# Poly/ML 4.x startup script.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0 Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-polyml-5.0 Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# Poly/ML 5.0 startup script.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/run-smlnj Tue Dec 30 11:10:01 2008 +0100
@@ -1,6 +1,5 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# SML/NJ startup script (for 110 or later).
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/system.pl
--- a/lib/scripts/system.pl Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/system.pl Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
#
-# $Id$
# Author: Makarius
#
# system.pl - invoke shell command line (with robust signal handling)
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/timestart.bash
--- a/lib/scripts/timestart.bash Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/timestart.bash Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,5 @@
# -*- shell-script -*-
-# $Id$
+#
# Author: Makarius
#
# timestart - setup bash environment for timing.
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/timestop.bash
--- a/lib/scripts/timestop.bash Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/timestop.bash Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,5 @@
# -*- shell-script -*-
-# $Id$
+#
# Author: Makarius
#
# timestop - report timing based on environment (cf. timestart.bash)
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/unsymbolize.pl
--- a/lib/scripts/unsymbolize.pl Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/unsymbolize.pl Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
#
-# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# unsymbolize.pl - remove unreadable symbol names from sources
diff -r 8f84a608883d -r ea97aa6aeba2 lib/scripts/yxml.pl
--- a/lib/scripts/yxml.pl Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/scripts/yxml.pl Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,4 @@
#
-# $Id$
# Author: Makarius
#
# yxml.pl - simple XML to YXML converter
diff -r 8f84a608883d -r ea97aa6aeba2 lib/texinputs/draft.tex
--- a/lib/texinputs/draft.tex Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/texinputs/draft.tex Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,3 @@
-%%
-%% $Id$
%%
%% root for draft documents
%%
diff -r 8f84a608883d -r ea97aa6aeba2 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/texinputs/isabelle.sty Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,3 @@
-%%
-%% $Id$
%%
%% macros for Isabelle generated LaTeX output
%%
diff -r 8f84a608883d -r ea97aa6aeba2 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/texinputs/isabellesym.sty Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,3 @@
-%%
-%% $Id$
%%
%% definitions of standard Isabelle symbols
%%
diff -r 8f84a608883d -r ea97aa6aeba2 lib/texinputs/pdfsetup.sty
--- a/lib/texinputs/pdfsetup.sty Tue Dec 30 08:18:54 2008 +0100
+++ b/lib/texinputs/pdfsetup.sty Tue Dec 30 11:10:01 2008 +0100
@@ -1,5 +1,3 @@
-%%
-%% $Id$
%%
%% default hyperref setup (both for pdf and dvi output)
%%
diff -r 8f84a608883d -r ea97aa6aeba2 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy Tue Dec 30 08:18:54 2008 +0100
+++ b/src/HOL/Code_Setup.thy Tue Dec 30 11:10:01 2008 +0100
@@ -198,6 +198,10 @@
subsection {* Evaluation and normalization by evaluation *}
+setup {*
+ Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
+*}
+
ML {*
structure Eval_Method =
struct
@@ -240,6 +244,10 @@
subsection {* Quickcheck *}
+setup {*
+ Quickcheck.add_generator ("SML", Codegen.test_term)
+*}
+
quickcheck_params [size = 5, iterations = 50]
end
diff -r 8f84a608883d -r ea97aa6aeba2 src/HOL/Complex/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Tue Dec 30 08:18:54 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1329 +0,0 @@
-(* Title: Fundamental_Theorem_Algebra.thy
- Author: Amine Chaieb
-*)
-
-header{*Fundamental Theorem of Algebra*}
-
-theory Fundamental_Theorem_Algebra
-imports "~~/src/HOL/Univ_Poly" "~~/src/HOL/Library/Dense_Linear_Order" "~~/src/HOL/Complex"
-begin
-
-subsection {* Square root of complex numbers *}
-definition csqrt :: "complex \ complex" where
-"csqrt z = (if Im z = 0 then
- if 0 \ Re z then Complex (sqrt(Re z)) 0
- else Complex 0 (sqrt(- Re z))
- else Complex (sqrt((cmod z + Re z) /2))
- ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
-
-lemma csqrt[algebra]: "csqrt z ^ 2 = z"
-proof-
- obtain x y where xy: "z = Complex x y" by (cases z, simp_all)
- {assume y0: "y = 0"
- {assume x0: "x \ 0"
- then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
- by (simp add: csqrt_def power2_eq_square)}
- moreover
- {assume "\ x \ 0" hence x0: "- x \ 0" by arith
- then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
- by (simp add: csqrt_def power2_eq_square) }
- ultimately have ?thesis by blast}
- moreover
- {assume y0: "y\0"
- {fix x y
- let ?z = "Complex x y"
- from abs_Re_le_cmod[of ?z] have tha: "abs x \ cmod ?z" by auto
- hence "cmod ?z - x \ 0" "cmod ?z + x \ 0" by arith+
- hence "(sqrt (x * x + y * y) + x) / 2 \ 0" "(sqrt (x * x + y * y) - x) / 2 \ 0" by (simp_all add: power2_eq_square) }
- note th = this
- have sq4: "\x::real. x^2 / 4 = (x / 2) ^ 2"
- by (simp add: power2_eq_square)
- from th[of x y]
- have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
- then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
- unfolding power2_eq_square by simp
- have "sqrt 4 = sqrt (2^2)" by simp
- hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
- have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \y\ = y"
- using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
- unfolding power2_eq_square
- by (simp add: ring_simps real_sqrt_divide sqrt4)
- from y0 xy have ?thesis apply (simp add: csqrt_def power2_eq_square)
- apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric])
- using th1 th2 ..}
- ultimately show ?thesis by blast
-qed
-
-
-subsection{* More lemmas about module of complex numbers *}
-
-lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
- by (rule of_real_power [symmetric])
-
-lemma real_down2: "(0::real) < d1 \ 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
- apply ferrack apply arith done
-
-text{* The triangle inequality for cmod *}
-lemma complex_mod_triangle_sub: "cmod w \ cmod (w + z) + norm z"
- using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
-
-subsection{* Basic lemmas about complex polynomials *}
-
-lemma poly_bound_exists:
- shows "\m. m > 0 \ (\z. cmod z <= r \ cmod (poly p z) \ m)"
-proof(induct p)
- case Nil thus ?case by (rule exI[where x=1], simp)
-next
- case (Cons c cs)
- from Cons.hyps obtain m where m: "\z. cmod z \ r \ cmod (poly cs z) \ m"
- by blast
- let ?k = " 1 + cmod c + \r * m\"
- have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
- {fix z
- assume H: "cmod z \ r"
- from m H have th: "cmod (poly cs z) \ m" by blast
- from H have rp: "r \ 0" using norm_ge_zero[of z] by arith
- have "cmod (poly (c # cs) z) \ cmod c + cmod (z* poly cs z)"
- using norm_triangle_ineq[of c "z* poly cs z"] by simp
- also have "\ \ cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
- also have "\ \ ?k" by simp
- finally have "cmod (poly (c # cs) z) \ ?k" .}
- with kp show ?case by blast
-qed
-
-
-text{* Offsetting the variable in a polynomial gives another of same degree *}
- (* FIXME : Lemma holds also in locale --- fix it later *)
-lemma poly_offset_lemma:
- shows "\b q. (length q = length p) \ (\x. poly (b#q) (x::complex) = (a + x) * poly p x)"
-proof(induct p)
- case Nil thus ?case by simp
-next
- case (Cons c cs)
- from Cons.hyps obtain b q where
- bq: "length q = length cs" "\x. poly (b # q) x = (a + x) * poly cs x"
- by blast
- let ?b = "a*c"
- let ?q = "(b+c)#q"
- have lg: "length ?q = length (c#cs)" using bq(1) by simp
- {fix x
- from bq(2)[rule_format, of x]
- have "x*poly (b # q) x = x*((a + x) * poly cs x)" by simp
- hence "poly (?b# ?q) x = (a + x) * poly (c # cs) x"
- by (simp add: ring_simps)}
- with lg show ?case by blast
-qed
-
- (* FIXME : This one too*)
-lemma poly_offset: "\ q. length q = length p \ (\x. poly q (x::complex) = poly p (a + x))"
-proof (induct p)
- case Nil thus ?case by simp
-next
- case (Cons c cs)
- from Cons.hyps obtain q where q: "length q = length cs" "\x. poly q x = poly cs (a + x)" by blast
- from poly_offset_lemma[of q a] obtain b p where
- bp: "length p = length q" "\x. poly (b # p) x = (a + x) * poly q x"
- by blast
- thus ?case using q bp by - (rule exI[where x="(c + b)#p"], simp)
-qed
-
-text{* An alternative useful formulation of completeness of the reals *}
-lemma real_sup_exists: assumes ex: "\x. P x" and bz: "\z. \x. P x \ x < z"
- shows "\(s::real). \y. (\x. P x \ y < x) \ y < s"
-proof-
- from ex bz obtain x Y where x: "P x" and Y: "\x. P x \ x < Y" by blast
- from ex have thx:"\x. x \ Collect P" by blast
- from bz have thY: "\Y. isUb UNIV (Collect P) Y"
- by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
- from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
- by blast
- from Y[OF x] have xY: "x < Y" .
- from L have L': "\x. P x \ x \ L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
- from Y have Y': "\x. P x \ x \ Y"
- apply (clarsimp, atomize (full)) by auto
- from L Y' have "L \ Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
- {fix y
- {fix z assume z: "P z" "y < z"
- from L' z have "y < L" by auto }
- moreover
- {assume yL: "y < L" "\z. P z \ \ y < z"
- hence nox: "\z. P z \ y \ z" by auto
- from nox L have "y \ L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
- with yL(1) have False by arith}
- ultimately have "(\x. P x \ y < x) \ y < L" by blast}
- thus ?thesis by blast
-qed
-
-
-subsection{* Some theorems about Sequences*}
-text{* Given a binary function @{text "f:: nat \ 'a \ 'a"}, its values are uniquely determined by a function g *}
-
-lemma num_Axiom: "EX! g. g 0 = e \ (\n. g (Suc n) = f n (g n))"
- unfolding Ex1_def
- apply (rule_tac x="nat_rec e f" in exI)
- apply (rule conjI)+
-apply (rule def_nat_rec_0, simp)
-apply (rule allI, rule def_nat_rec_Suc, simp)
-apply (rule allI, rule impI, rule ext)
-apply (erule conjE)
-apply (induct_tac x)
-apply (simp add: nat_rec_0)
-apply (erule_tac x="n" in allE)
-apply (simp)
-done
-
- text{* An equivalent formulation of monotony -- Not used here, but might be useful *}
-lemma mono_Suc: "mono f = (\n. (f n :: 'a :: order) \ f (Suc n))"
-unfolding mono_def
-proof auto
- fix A B :: nat
- assume H: "\n. f n \ f (Suc n)" "A \ B"
- hence "\k. B = A + k" apply - apply (thin_tac "\n. f n \ f (Suc n)")
- by presburger
- then obtain k where k: "B = A + k" by blast
- {fix a k
- have "f a \ f (a + k)"
- proof (induct k)
- case 0 thus ?case by simp
- next
- case (Suc k)
- from Suc.hyps H(1)[rule_format, of "a + k"] show ?case by simp
- qed}
- with k show "f A \ f B" by blast
-qed
-
-text{* for any sequence, there is a mootonic subsequence *}
-lemma seq_monosub: "\f. subseq f \ monoseq (\ n. (s (f n)))"
-proof-
- {assume H: "\n. \p >n. \ m\p. s m \ s p"
- let ?P = "\ p n. p > n \ (\m \ p. s m \ s p)"
- from num_Axiom[of "SOME p. ?P p 0" "\p n. SOME p. ?P p n"]
- obtain f where f: "f 0 = (SOME p. ?P p 0)" "\n. f (Suc n) = (SOME p. ?P p (f n))" by blast
- have "?P (f 0) 0" unfolding f(1) some_eq_ex[of "\p. ?P p 0"]
- using H apply -
- apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
- unfolding order_le_less by blast
- hence f0: "f 0 > 0" "\m \ f 0. s m \ s (f 0)" by blast+
- {fix n
- have "?P (f (Suc n)) (f n)"
- unfolding f(2)[rule_format, of n] some_eq_ex[of "\p. ?P p (f n)"]
- using H apply -
- apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
- unfolding order_le_less by blast
- hence "f (Suc n) > f n" "\m \ f (Suc n). s m \ s (f (Suc n))" by blast+}
- note fSuc = this
- {fix p q assume pq: "p \ f q"
- have "s p \ s(f(q))" using f0(2)[rule_format, of p] pq fSuc
- by (cases q, simp_all) }
- note pqth = this
- {fix q
- have "f (Suc q) > f q" apply (induct q)
- using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
- note fss = this
- from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
- {fix a b
- have "f a \ f (a + b)"
- proof(induct b)
- case 0 thus ?case by simp
- next
- case (Suc b)
- from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
- qed}
- note fmon0 = this
- have "monoseq (\n. s (f n))"
- proof-
- {fix n
- have "s (f n) \ s (f (Suc n))"
- proof(cases n)
- case 0
- assume n0: "n = 0"
- from fSuc(1)[of 0] have th0: "f 0 \ f (Suc 0)" by simp
- from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp
- next
- case (Suc m)
- assume m: "n = Suc m"
- from fSuc(1)[of n] m have th0: "f (Suc m) \ f (Suc (Suc m))" by simp
- from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
- qed}
- thus "monoseq (\n. s (f n))" unfolding monoseq_Suc by blast
- qed
- with th1 have ?thesis by blast}
- moreover
- {fix N assume N: "\p >N. \ m\p. s m > s p"
- {fix p assume p: "p \ Suc N"
- hence pN: "p > N" by arith with N obtain m where m: "m \ p" "s m > s p" by blast
- have "m \ p" using m(2) by auto
- with m have "\m>p. s p < s m" by - (rule exI[where x=m], auto)}
- note th0 = this
- let ?P = "\m x. m > x \ s x < s m"
- from num_Axiom[of "SOME x. ?P x (Suc N)" "\m x. SOME y. ?P y x"]
- obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
- "\n. f (Suc n) = (SOME m. ?P m (f n))" by blast
- have "?P (f 0) (Suc N)" unfolding f(1) some_eq_ex[of "\p. ?P p (Suc N)"]
- using N apply -
- apply (erule allE[where x="Suc N"], clarsimp)
- apply (rule_tac x="m" in exI)
- apply auto
- apply (subgoal_tac "Suc N \ m")
- apply simp
- apply (rule ccontr, simp)
- done
- hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
- {fix n
- have "f n > N \ ?P (f (Suc n)) (f n)"
- unfolding f(2)[rule_format, of n] some_eq_ex[of "\p. ?P p (f n)"]
- proof (induct n)
- case 0 thus ?case
- using f0 N apply auto
- apply (erule allE[where x="f 0"], clarsimp)
- apply (rule_tac x="m" in exI, simp)
- by (subgoal_tac "f 0 \ m", auto)
- next
- case (Suc n)
- from Suc.hyps have Nfn: "N < f n" by blast
- from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
- with Nfn have mN: "m > N" by arith
- note key = Suc.hyps[unfolded some_eq_ex[of "\p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
-
- from key have th0: "f (Suc n) > N" by simp
- from N[rule_format, OF th0]
- obtain m' where m': "m' \ f (Suc n)" "s (f (Suc n)) < s m'" by blast
- have "m' \ f (Suc (n))" apply (rule ccontr) using m'(2) by auto
- hence "m' > f (Suc n)" using m'(1) by simp
- with key m'(2) show ?case by auto
- qed}
- note fSuc = this
- {fix n
- have "f n \ Suc N \ f(Suc n) > f n \ s(f n) < s(f(Suc n))" using fSuc[of n] by auto
- hence "f n \ Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
- note thf = this
- have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
- have "monoseq (\n. s (f n))" unfolding monoseq_Suc using thf
- apply -
- apply (rule disjI1)
- apply auto
- apply (rule order_less_imp_le)
- apply blast
- done
- then have ?thesis using sqf by blast}
- ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
-qed
-
-lemma seq_suble: assumes sf: "subseq f" shows "n \ f n"
-proof(induct n)
- case 0 thus ?case by simp
-next
- case (Suc n)
- from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
- have "n < f (Suc n)" by arith
- thus ?case by arith
-qed
-
-subsection {* Fundamental theorem of algebra *}
-lemma unimodular_reduce_norm:
- assumes md: "cmod z = 1"
- shows "cmod (z + 1) < 1 \ cmod (z - 1) < 1 \ cmod (z + ii) < 1 \ cmod (z - ii) < 1"
-proof-
- obtain x y where z: "z = Complex x y " by (cases z, auto)
- from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
- {assume C: "cmod (z + 1) \ 1" "cmod (z - 1) \ 1" "cmod (z + ii) \ 1" "cmod (z - ii) \ 1"
- from C z xy have "2*x \ 1" "2*x \ -1" "2*y \ 1" "2*y \ -1"
- by (simp_all add: cmod_def power2_eq_square ring_simps)
- hence "abs (2*x) \ 1" "abs (2*y) \ 1" by simp_all
- hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
- by - (rule power_mono, simp, simp)+
- hence th0: "4*x^2 \ 1" "4*y^2 \ 1"
- by (simp_all add: power2_abs power_mult_distrib)
- from add_mono[OF th0] xy have False by simp }
- thus ?thesis unfolding linorder_not_le[symmetric] by blast
-qed
-
-text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
-lemma reduce_poly_simple:
- assumes b: "b \ 0" and n: "n\0"
- shows "\z. cmod (1 + b * z^n) < 1"
-using n
-proof(induct n rule: nat_less_induct)
- fix n
- assume IH: "\m 0 \ (\z. cmod (1 + b * z ^ m) < 1)" and n: "n \ 0"
- let ?P = "\z n. cmod (1 + b * z ^ n) < 1"
- {assume e: "even n"
- hence "\m. n = 2*m" by presburger
- then obtain m where m: "n = 2*m" by blast
- from n m have "m\0" "m < n" by presburger+
- with IH[rule_format, of m] obtain z where z: "?P z m" by blast
- from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
- hence "\z. ?P z n" ..}
- moreover
- {assume o: "odd n"
- from b have b': "b^2 \ 0" unfolding power2_eq_square by simp
- have "Im (inverse b) * (Im (inverse b) * \Im b * Im b + Re b * Re b\) +
- Re (inverse b) * (Re (inverse b) * \Im b * Im b + Re b * Re b\) =
- ((Re (inverse b))^2 + (Im (inverse b))^2) * \Im b * Im b + Re b * Re b\" by algebra
- also have "\ = cmod (inverse b) ^2 * cmod b ^ 2"
- apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
- by (simp add: power2_eq_square)
- finally
- have th0: "Im (inverse b) * (Im (inverse b) * \Im b * Im b + Re b * Re b\) +
- Re (inverse b) * (Re (inverse b) * \Im b * Im b + Re b * Re b\) =
- 1"
- apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
- using right_inverse[OF b']
- by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] ring_simps)
- have th0: "cmod (complex_of_real (cmod b) / b) = 1"
- apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse ring_simps )
- by (simp add: real_sqrt_mult[symmetric] th0)
- from o have "\m. n = Suc (2*m)" by presburger+
- then obtain m where m: "n = Suc (2*m)" by blast
- from unimodular_reduce_norm[OF th0] o
- have "\v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
- apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
- apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
- apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
- apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
- apply (rule_tac x="- ii" in exI, simp add: m power_mult)
- apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
- apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
- done
- then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
- let ?w = "v / complex_of_real (root n (cmod b))"
- from odd_real_root_pow[OF o, of "cmod b"]
- have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
- by (simp add: power_divide complex_of_real_power)
- have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
- hence th3: "cmod (complex_of_real (cmod b) / b) \ 0" by simp
- have th4: "cmod (complex_of_real (cmod b) / b) *
- cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
- < cmod (complex_of_real (cmod b) / b) * 1"
- apply (simp only: norm_mult[symmetric] right_distrib)
- using b v by (simp add: th2)
-
- from mult_less_imp_less_left[OF th4 th3]
- have "?P ?w n" unfolding th1 .
- hence "\z. ?P z n" .. }
- ultimately show "\z. ?P z n" by blast
-qed
-
-
-text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
-
-lemma metric_bound_lemma: "cmod (x - y) <= \Re x - Re y\ + \Im x - Im y\"
- using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
- unfolding cmod_def by simp
-
-lemma bolzano_weierstrass_complex_disc:
- assumes r: "\n. cmod (s n) \ r"
- shows "\f z. subseq f \ (\e >0. \N. \n \ N. cmod (s (f n) - z) < e)"
-proof-
- from seq_monosub[of "Re o s"]
- obtain f g where f: "subseq f" "monoseq (\n. Re (s (f n)))"
- unfolding o_def by blast
- from seq_monosub[of "Im o s o f"]
- obtain g where g: "subseq g" "monoseq (\n. Im (s(f(g n))))" unfolding o_def by blast
- let ?h = "f o g"
- from r[rule_format, of 0] have rp: "r \ 0" using norm_ge_zero[of "s 0"] by arith
- have th:"\n. r + 1 \ \ Re (s n)\"
- proof
- fix n
- from abs_Re_le_cmod[of "s n"] r[rule_format, of n] show "\Re (s n)\ \ r + 1" by arith
- qed
- have conv1: "convergent (\n. Re (s ( f n)))"
- apply (rule Bseq_monoseq_convergent)
- apply (simp add: Bseq_def)
- apply (rule exI[where x= "r + 1"])
- using th rp apply simp
- using f(2) .
- have th:"\n. r + 1 \ \ Im (s n)\"
- proof
- fix n
- from abs_Im_le_cmod[of "s n"] r[rule_format, of n] show "\Im (s n)\ \ r + 1" by arith
- qed
-
- have conv2: "convergent (\n. Im (s (f (g n))))"
- apply (rule Bseq_monoseq_convergent)
- apply (simp add: Bseq_def)
- apply (rule exI[where x= "r + 1"])
- using th rp apply simp
- using g(2) .
-
- from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\n. Re (s (f n))) x"
- by blast
- hence x: "\r>0. \n0. \n\n0. \ Re (s (f n)) - x \ < r"
- unfolding LIMSEQ_def real_norm_def .
-
- from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\n. Im (s (f (g n)))) y"
- by blast
- hence y: "\r>0. \n0. \n\n0. \ Im (s (f (g n))) - y \ < r"
- unfolding LIMSEQ_def real_norm_def .
- let ?w = "Complex x y"
- from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
- {fix e assume ep: "e > (0::real)"
- hence e2: "e/2 > 0" by simp
- from x[rule_format, OF e2] y[rule_format, OF e2]
- obtain N1 N2 where N1: "\n\N1. \Re (s (f n)) - x\ < e / 2" and N2: "\n\N2. \Im (s (f (g n))) - y\ < e / 2" by blast
- {fix n assume nN12: "n \ N1 + N2"
- hence nN1: "g n \ N1" and nN2: "n \ N2" using seq_suble[OF g(1), of n] by arith+
- from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
- have "cmod (s (?h n) - ?w) < e"
- using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
- hence "\