--- a/Admin/isatest/isatest-lint Fri Dec 03 14:46:58 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Florian Haftmann, TUM
-#
-# Do consistency and quality checks on the isabelle sources
-#
-
-use strict;
-use File::Find;
-use File::Basename;
-
-# configuration
-my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
-my @suffices = ('\.thy', '\.ml', '\.ML');
-
-# lint main procedure
-sub lint() {
- my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
- if ($ext) {
- open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
- my $found = 0;
- while (<ISTREAM>) {
- $found ||= m/\$Id[^\$]*\$/;
- last if $found;
- }
- close ISTREAM;
- my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
- if (! $found) {
- print "Found no CVS id in $relname\n";
- }
- }
-}
-
-# first argument =^= isabelle repository root
-if (@ARGV) {
- $isabelleRoot = $ARGV[0];
-}
-
-find(\&lint, $isabelleRoot);
-
--- a/NEWS Fri Dec 03 14:46:58 2010 +0100
+++ b/NEWS Fri Dec 03 22:40:26 2010 +0100
@@ -6,15 +6,15 @@
*** General ***
-* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
-(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
-while the default heap location within that directory lacks that extra
-suffix. This isolates multiple Isabelle installations from each
-other, avoiding problems with old settings in new versions.
-INCOMPATIBILITY, need to copy/upgrade old user settings manually.
-
* Significantly improved Isabelle/Isar implementation manual.
+* Source files are always encoded as UTF-8, instead of old-fashioned
+ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require
+the following package declarations:
+
+ \usepackage[utf8]{inputenc}
+ \usepackage{textcomp}
+
* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
a Unicode character is treated as a single symbol, not a sequence of
non-ASCII bytes as before. Since Isabelle/ML string literals may
@@ -23,6 +23,13 @@
consistent view on symbols, while raw explode (or String.explode)
merely give a byte-oriented representation.
+* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
+(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
+while the default heap location within that directory lacks that extra
+suffix. This isolates multiple Isabelle installations from each
+other, avoiding problems with old settings in new versions.
+INCOMPATIBILITY, need to copy/upgrade old user settings manually.
+
* Theory loading: only the master source file is looked-up in the
implicit load path, all other files are addressed relatively to its
directory. Minor INCOMPATIBILITY, subtle change in semantics.
@@ -64,18 +71,18 @@
"no_abbrevs" with inverted meaning.
* More systematic naming of some configuration options.
- INCOMPATIBILTY.
+INCOMPATIBILTY.
trace_simp ~> simp_trace
debug_simp ~> simp_debug
-
-*** Pure ***
-
* Support for real valued configuration options, using simplistic
floating-point notation that coincides with the inner syntax for
float_token.
+
+*** Pure ***
+
* Support for real valued preferences (with approximative PGIP type).
* Interpretation command 'interpret' accepts a list of equations like
@@ -89,7 +96,7 @@
Sign.root_path and Sign.local_path may be applied directly where this
feature is still required for historical reasons.
-* Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use
+* Discontinued obsolete 'constdefs' command. INCOMPATIBILITY, use
'definition' instead.
* Document antiquotations @{class} and @{type} print classes and type
@@ -101,55 +108,62 @@
*** HOL ***
-* Quickcheck now by default uses exhaustive testing instead of random testing.
-Random testing can be invoked by quickcheck[random],
+* Quickcheck now by default uses exhaustive testing instead of random
+testing. Random testing can be invoked by quickcheck[random],
exhaustive testing by quickcheck[exhaustive].
-* Quickcheck instantiates polymorphic types with small finite datatypes
-by default. This enables a simple execution mechanism to handle
-quantifiers and function equality over the finite datatypes.
-
-* Functions can be declared as coercions and type inference will add them
-as necessary upon input of a term. In Complex_Main, real :: nat => real
-and real :: int => real are declared as coercions. A new coercion function
-f is declared like this:
-
-declare [[coercion f]]
+* Quickcheck instantiates polymorphic types with small finite
+datatypes by default. This enables a simple execution mechanism to
+handle quantifiers and function equality over the finite datatypes.
+
+* Functions can be declared as coercions and type inference will add
+them as necessary upon input of a term. In theory Complex_Main,
+real :: nat => real and real :: int => real are declared as
+coercions. A new coercion function f is declared like this:
+
+ declare [[coercion f]]
To lift coercions through type constructors (eg from nat => real to
nat list => real list), map functions can be declared, e.g.
-declare [[coercion_map map]]
-
-Currently coercion inference is activated only in theories including real
-numbers, i.e. descendants of Complex_Main. In other theories it needs to be
-loaded explicitly: uses "~~/src/Tools/subtyping.ML"
-
-* Abandoned locales equiv, congruent and congruent2 for equivalence relations.
-INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).
-
-* Code generator: globbing constant expressions "*" and "Theory.*" have been
-replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY.
-
-* Theory Enum (for explicit enumerations of finite types) is now part of
-the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now
-have to be referred to by its qualified name.
- constants
- enum -> Enum.enum
- nlists -> Enum.nlists
- product -> Enum.product
+ declare [[coercion_map map]]
+
+Currently coercion inference is activated only in theories including
+real numbers, i.e. descendants of Complex_Main. This is controlled by
+the configuration option "infer_coercions", e.g. it can be enabled in
+other theories like this:
+
+ declare [[coercion_enabled]]
+
+* Abandoned locales equiv, congruent and congruent2 for equivalence
+relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same
+for congruent(2)).
+
+* Code generator: globbing constant expressions "*" and "Theory.*"
+have been replaced by the more idiomatic "_" and "Theory._".
+INCOMPATIBILITY.
+
+* Theory Enum (for explicit enumerations of finite types) is now part
+of the HOL-Main image. INCOMPATIBILITY: all constants of the Enum
+theory now have to be referred to by its qualified name.
+
+ enum ~> Enum.enum
+ nlists ~> Enum.nlists
+ product ~> Enum.product
* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
avoid confusion with finite sets. INCOMPATIBILITY.
-* Quickcheck's generator for random generation is renamed from "code" to
-"random". INCOMPATIBILITY.
-
-* Theory Multiset provides stable quicksort implementation of sort_key.
-
-* Quickcheck now has a configurable time limit which is set to 30 seconds
-by default. This can be changed by adding [timeout = n] to the quickcheck
-command. The time limit for Auto Quickcheck is still set independently.
+* Quickcheck's generator for random generation is renamed from "code"
+to "random". INCOMPATIBILITY.
+
+* Quickcheck now has a configurable time limit which is set to 30
+seconds by default. This can be changed by adding [timeout = n] to the
+quickcheck command. The time limit for Auto Quickcheck is still set
+independently.
+
+* Theory Multiset provides stable quicksort implementation of
+sort_key.
* New command 'partial_function' provides basic support for recursive
function definitions over complete partial orders. Concrete instances
@@ -158,11 +172,11 @@
HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
examples.
-* Predicates `distinct` and `sorted` now defined inductively, with nice
-induction rules. INCOMPATIBILITY: former distinct.simps and sorted.simps
-now named distinct_simps and sorted_simps.
-
-* Constant `contents` renamed to `the_elem`, to free the generic name
+* Predicates "distinct" and "sorted" now defined inductively, with
+nice induction rules. INCOMPATIBILITY: former distinct.simps and
+sorted.simps now named distinct_simps and sorted_simps.
+
+* Constant "contents" renamed to "the_elem", to free the generic name
contents for other uses. INCOMPATIBILITY.
* Dropped syntax for old primrec package. INCOMPATIBILITY.
@@ -172,36 +186,34 @@
* String.literal is a type, but not a datatype. INCOMPATIBILITY.
-* Renamed lemmas:
- expand_fun_eq -> fun_eq_iff
- expand_set_eq -> set_eq_iff
- set_ext -> set_eqI
- INCOMPATIBILITY.
-
-* Renamed lemma list: nat_number -> eval_nat_numeral
-
-* Renamed class eq and constant eq (for code generation) to class equal
-and constant equal, plus renaming of related facts and various tuning.
-INCOMPATIBILITY.
-
-* Scala (2.8 or higher) has been added to the target languages of
-the code generator.
+* Renamed facts:
+ expand_fun_eq ~> fun_eq_iff
+ expand_set_eq ~> set_eq_iff
+ set_ext ~> set_eqI
+ nat_number ~> eval_nat_numeral
+
+* Renamed class eq and constant eq (for code generation) to class
+equal and constant equal, plus renaming of related facts and various
+tuning. INCOMPATIBILITY.
+
+* Scala (2.8 or higher) has been added to the target languages of the
+code generator.
* Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.
-* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
-
-* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
-canonical names for instance definitions for functions; various improvements.
-INCOMPATIBILITY.
-
-* Records: logical foundation type for records do not carry a '_type' suffix
-any longer. INCOMPATIBILITY.
-
-* Code generation for records: more idiomatic representation of record types.
-Warning: records are not covered by ancient SML code generation any longer.
-INCOMPATIBILITY. In cases of need, a suitable rep_datatype declaration
-helps to succeed then:
+* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
+
+* Theory SetsAndFunctions has been split into Function_Algebras and
+Set_Algebras; canonical names for instance definitions for functions;
+various improvements. INCOMPATIBILITY.
+
+* Records: logical foundation type for records do not carry a '_type'
+suffix any longer. INCOMPATIBILITY.
+
+* Code generation for records: more idiomatic representation of record
+types. Warning: records are not covered by ancient SML code
+generation any longer. INCOMPATIBILITY. In cases of need, a suitable
+rep_datatype declaration helps to succeed then:
record 'a foo = ...
...
@@ -213,24 +225,24 @@
* Quickcheck in locales considers interpretations of that locale for
counter example search.
-* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
-in Library/State_Monad has been changed to avoid ambiguities.
+* Theory Library/Monad_Syntax provides do-syntax for monad types.
+Syntax in Library/State_Monad has been changed to avoid ambiguities.
INCOMPATIBILITY.
* Code generator: export_code without explicit file declaration prints
to standard output. INCOMPATIBILITY.
-* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
-respectively. INCOMPATIBILITY.
-
-* Name "Plus" of disjoint sum operator "<+>" is now hidden.
- Write Sum_Type.Plus.
-
-* Constant "split" has been merged with constant "prod_case"; names
-of ML functions, facts etc. involving split have been retained so far,
+* Abolished some non-alphabetic type names: "prod" and "sum" replace
+"*" and "+" respectively. INCOMPATIBILITY.
+
+* Name "Plus" of disjoint sum operator "<+>" is now hidden. Write
+Sum_Type.Plus.
+
+* Constant "split" has been merged with constant "prod_case"; names of
+ML functions, facts etc. involving split have been retained so far,
though. INCOMPATIBILITY.
-* Dropped old infix syntax "mem" for List.member; use "in set"
+* Dropped old infix syntax "mem" for List.member; use "in set"
instead. INCOMPATIBILITY.
* Refactoring of code-generation specific operations in List.thy
@@ -243,7 +255,7 @@
null_empty ~> null_def
INCOMPATIBILITY. Note that these were not suppossed to be used
-regularly unless for striking reasons; their main purpose was code
+regularly unless for striking reasons; their main purpose was code
generation.
* Some previously unqualified names have been qualified:
@@ -282,9 +294,8 @@
* Removed simplifier congruence rule of "prod_case", as has for long
been the case with "split". INCOMPATIBILITY.
-* Datatype package: theorems generated for executable equality
-(class eq) carry proper names and are treated as default code
-equations.
+* Datatype package: theorems generated for executable equality (class
+eq) carry proper names and are treated as default code equations.
* Removed lemma Option.is_none_none (Duplicate of is_none_def).
INCOMPATIBILITY.
@@ -294,15 +305,15 @@
* Multiset.thy: renamed empty_idemp -> empty_neutral
-* code_simp.ML and method code_simp: simplification with rules determined
-by code generator.
+* code_simp.ML and method code_simp: simplification with rules
+determined by code generator.
* code generator: do not print function definitions for case
combinators any longer.
-* Multivariate Analysis: Introduced a type class for euclidean space. Most
-theorems are now stated in terms of euclidean spaces instead of finite
-cartesian products.
+* Multivariate Analysis: Introduced a type class for euclidean
+space. Most theorems are now stated in terms of euclidean spaces
+instead of finite cartesian products.
types
real ^ 'n ~> 'a::real_vector
@@ -315,31 +326,32 @@
\<chi> x. _ ~> \<chi>\<chi> x. _
CARD('n) ~> DIM('a)
-Also note that the indices are now natural numbers and not from some finite
-type. Finite cartesian products of euclidean spaces, products of euclidean
-spaces the real and complex numbers are instantiated to be euclidean_spaces.
-INCOMPATIBILITY.
-
-* Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal
-as value for measures. Introduce the Radon-Nikodym derivative, product spaces
-and Fubini's theorem for arbitrary sigma finite measures. Introduces Lebesgue
-measure based on the integral in Multivariate Analysis.
-INCOMPATIBILITY.
-
-* Inductive package: offers new command "inductive_simps" to automatically
-derive instantiated and simplified equations for inductive predicates,
-similar to inductive_cases.
+Also note that the indices are now natural numbers and not from some
+finite type. Finite cartesian products of euclidean spaces, products
+of euclidean spaces the real and complex numbers are instantiated to
+be euclidean_spaces. INCOMPATIBILITY.
+
+* Probability: Introduced pinfreal as real numbers with infinity. Use
+pinfreal as value for measures. Introduce the Radon-Nikodym
+derivative, product spaces and Fubini's theorem for arbitrary sigma
+finite measures. Introduces Lebesgue measure based on the integral in
+Multivariate Analysis. INCOMPATIBILITY.
+
+* Inductive package: offers new command 'inductive_simps' to
+automatically derive instantiated and simplified equations for
+inductive predicates, similar to 'inductive_cases'.
* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f"
is now an abbreviation of "range f = UNIV". The theorems bij_def and
surj_def are unchanged. INCOMPATIBILITY.
-* Function package: .psimps rules are no longer implicitly declared [simp].
-INCOMPATIBILITY.
-
-* Weaker versions of the "meson" and "metis" proof methods are now available in
- "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become
- more powerful after "Hilbert_Choice" is loaded in "HOL-Main".
+* Function package: .psimps rules are no longer implicitly declared
+[simp]. INCOMPATIBILITY.
+
+* Weaker versions of the "meson" and "metis" proof methods are now
+available in "HOL-Plain", without dependency on "Hilbert_Choice". The
+proof methods become more powerful after "Hilbert_Choice" is loaded in
+"HOL-Main".
* MESON: Renamed lemmas:
meson_not_conjD ~> Meson.not_conjD
@@ -363,8 +375,8 @@
meson_disj_FalseD2 ~> Meson.disj_FalseD2
INCOMPATIBILITY.
-* Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as
- "solve_direct".
+* Auto Solve: Renamed "Auto Solve Direct". The tool is now available
+manually as command 'solve_direct'.
* Sledgehammer:
- Added "smt" and "remote_smt" provers based on the "smt" proof method. See
@@ -393,8 +405,9 @@
(and "ms" and "min" are no longer supported)
INCOMPATIBILITY.
-* Metis and Meson now have configuration options "meson_trace", "metis_trace",
- and "metis_verbose" that can be enabled to diagnose these tools. E.g.
+* Metis and Meson now have configuration options "meson_trace",
+"metis_trace", and "metis_verbose" that can be enabled to diagnose
+these tools. E.g.
using [[metis_trace = true]]
@@ -425,8 +438,8 @@
cvc3_options
yices_options
-* Boogie output files (.b2i files) need to be declared in the
-theory header.
+* Boogie output files (.b2i files) need to be declared in the theory
+header.
* Removed [split_format ... and ... and ...] version of
[split_format]. Potential INCOMPATIBILITY.
@@ -477,7 +490,7 @@
cont2cont_Rep_CFun ~> cont2cont_APP
* The Abs and Rep functions for various types have changed names.
-Related theorem names have also changed to match. INCOMPATIBILITY.
+Related theorem names have also changed to match. INCOMPATIBILITY.
Rep_CFun ~> Rep_cfun
Abs_CFun ~> Abs_cfun
Rep_Sprod ~> Rep_sprod
@@ -495,8 +508,8 @@
- Variable names in bisim_def and coinduct rules have changed.
INCOMPATIBILITY.
-* Case combinators generated by the domain package for type 'foo'
-are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
+* Case combinators generated by the domain package for type 'foo' are
+now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
* Several theorems have been renamed to more accurately reflect the
names of constants and types involved. INCOMPATIBILITY.
@@ -562,12 +575,7 @@
less_sinrD ~> below_sinrD
-*** FOL ***
-
-* All constant names are now qualified. INCOMPATIBILITY.
-
-
-*** ZF ***
+*** FOL and ZF ***
* All constant names are now qualified. INCOMPATIBILITY.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Dec 03 22:40:26 2010 +0100
@@ -948,14 +948,21 @@
and \emph{code} for code generation in SML.
\item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
- counter examples using a series of arbitrary assignments for its
+ counter examples using a series of assignments for its
free variables; by default the first subgoal is tested, an other
can be selected explicitly using an optional goal index.
+ Assignments can be chosen exhausting the search space upto a given
+ size or using a fixed number of random assignments in the search space.
+ By default, quickcheck uses exhaustive testing.
A number of configuration options are supported for
\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
\begin{description}
+ \item[\isa{tester}] specifies how to explore the search space
+ (e.g. exhaustive or random).
+ An unknown configuration option is treated as an argument to tester,
+ making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.
\item[\isa{size}] specifies the maximum size of the search space
for assignment values.
--- a/doc-src/IsarRef/isar-ref.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,7 +1,6 @@
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{amssymb}
\usepackage[greek,english]{babel}
-\usepackage[latin1]{inputenc}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{textcomp}
\usepackage{latexsym}
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Dec 03 22:40:26 2010 +0100
@@ -78,13 +78,13 @@
\label{introduction}
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
-and satisfiability-modulo-theory (SMT) solvers on the current goal. The
+and satisfiability-modulo-theories (SMT) solvers on the current goal. The
supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK
\cite{snark}. The ATPs are run either locally or remotely via the
System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the
-\textit{smt} proof method (which typically relies on the Z3 SMT solver
-\cite{z3}) is tried as well.
+SMT solvers Z3 \cite{z3} is used, and you can tell Sledgehammer to try Yices
+\cite{yices} and CVC3 \cite{cvc3} as well.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -226,12 +226,17 @@
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
+%
+Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
+$([a] = [b]) = (a = b)$ \\
+Try this command: \textbf{by} (\textit{metis hd.simps}) \\
+To minimize the number of lemmas, try this: \\
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
\postw
-Sledgehammer ran E, SPASS, Vampire, SInE-E, and the \textit{smt} proof method in
-parallel. Depending on which provers are installed and how many processor cores
-are available, some of the provers might be missing or present with a
-\textit{remote\_} prefix.
+Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
+which provers are installed and how many processor cores are available, some of
+the provers might be missing or present with a \textit{remote\_} prefix.
For each successful prover, Sledgehammer gives a one-liner proof that uses the
\textit{metis} or \textit{smt} method. You can click the proof to insert it into
@@ -416,10 +421,24 @@
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
-that contains the \texttt{vampire} executable.
+that contains the \texttt{vampire} executable. Sledgehammer has been tested with
+versions 11, 0.6, and 1.0.
+
+\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
+Microsoft Research \cite{z3}. To use Z3, set the environment variable
+\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
+name. Sledgehammer has been tested with 2.7 to 2.15.
-\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method invokes an
-external SMT prover (usually Z3 \cite{z3}).
+\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
+SRI \cite{yices}. To use Yices, set the environment variable
+\texttt{YICES\_SOLVER} to the complete path of the executable, including the
+file name. Sledgehammer has been tested with version 1.0.
+
+\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
+Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
+set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
+executable, including the file name. Sledgehammer has been tested with version
+2.2.
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
@@ -435,13 +454,17 @@
developed by Stickel et al.\ \cite{snark}. The remote version of
SNARK runs on Geoff Sutcliffe's Miami servers.
-\item[$\bullet$] \textbf{\textit{remote\_smt}:} The remote version of the
-\textit{smt} proof method runs the SMT solver on servers at the TU M\"unchen (or
-wherever \texttt{REMOTE\_SMT\_URL} is set to point).
+\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
+servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
+point).
+\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
+on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
+point).
\end{enum}
-By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and \textit{smt} in
+By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
+the SMT module's \emph{smt\_solver} configuration option is set to) in
parallel---either locally or remotely, depending on the number of processor
cores available. For historical reasons, the default value of this option can be
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
--- a/doc-src/TutorialI/Overview/Slides/main.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/doc-src/TutorialI/Overview/Slides/main.tex Fri Dec 03 22:40:26 2010 +0100
@@ -4,7 +4,7 @@
\documentclass[pdf,nototal,myframes,slideColor,colorBG]{prosper}
\usepackage{pstricks,pst-node,pst-text,pst-3d}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage{amsmath}
@@ -21,7 +21,7 @@
\author{Tobias Nipkow
\\{\small joint work with Larry Paulson and Markus Wenzel}
}
-\institution{Technische Universität München
+\institution{Technische Universität München
\\ \vspace{0.5cm}\includegraphics[scale=.4]{isabelle_hol}
}
\maketitle
--- a/doc-src/isabellesym.sty Fri Dec 03 14:46:58 2010 +0100
+++ b/doc-src/isabellesym.sty Fri Dec 03 22:40:26 2010 +0100
@@ -324,12 +324,12 @@
\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymonesuperior}{\isamath{{}^1}}
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires textcomp
+\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires textcomp
+\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires textcomp
\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
\newcommand{\isasymsection}{\isatext{\rm\S}}
@@ -341,7 +341,7 @@
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires textcomp
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
--- a/doc-src/manual.bib Fri Dec 03 14:46:58 2010 +0100
+++ b/doc-src/manual.bib Fri Dec 03 22:40:26 2010 +0100
@@ -159,6 +159,18 @@
editor = {A. Robinson and A. Voronkov}
}
+@inproceedings{cvc3,
+ author = {Clark Barrett and Cesare Tinelli},
+ title = {{CVC3}},
+ booktitle = {CAV},
+ editor = {Werner Damm and Holger Hermanns},
+ volume = {4590},
+ series = LNCS,
+ pages = {298--302},
+ publisher = {Springer},
+ year = {2007}
+}
+
@incollection{basin91,
author = {David Basin and Matt Kaufmann},
title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
@@ -392,6 +404,12 @@
year = 1977,
publisher = {Oxford University Press}}
+@misc{yices,
+ author = {Bruno Dutertre and Leonardo de Moura},
+ title = {The {Yices} {SMT} Solver},
+ publisher = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
+ year = 2006}
+
@incollection{dybjer91,
author = {Peter Dybjer},
title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
--- a/lib/Tools/latex Fri Dec 03 14:46:58 2010 +0100
+++ b/lib/Tools/latex Fri Dec 03 22:40:26 2010 +0100
@@ -88,7 +88,7 @@
function extract_syms ()
{
perl -n \
- -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
+ -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
"$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
perl -n \
-e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
--- a/lib/Tools/mkdir Fri Dec 03 14:46:58 2010 +0100
+++ b/lib/Tools/mkdir Fri Dec 03 22:40:26 2010 +0100
@@ -221,10 +221,6 @@
%option greek for \<euro>
%option english (default language) for \<guillemotleft>, \<guillemotright>
-%\usepackage[latin1]{inputenc}
- %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
- %\<threesuperior>, \<threequarters>, \<degree>
-
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
@@ -232,7 +228,8 @@
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
- %for \<cent>, \<currency>
+ %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+ %\<currency>
% this should be the last package used
\usepackage{pdfsetup}
--- a/lib/texinputs/draft.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/lib/texinputs/draft.tex Fri Dec 03 22:40:26 2010 +0100
@@ -6,7 +6,6 @@
\usepackage{isabelle,isabellesym,pdfsetup}
%packages for unusual symbols according to 'isabelle latex -o syms'
-\usepackage[latin1]{inputenc}
\usepackage{amssymb}
\usepackage{textcomp}
--- a/lib/texinputs/isabellesym.sty Fri Dec 03 14:46:58 2010 +0100
+++ b/lib/texinputs/isabellesym.sty Fri Dec 03 22:40:26 2010 +0100
@@ -324,12 +324,12 @@
\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymonesuperior}{\isamath{{}^1}}
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires textcomp
+\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires textcomp
+\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires textcomp
\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
\newcommand{\isasymsection}{\isatext{\rm\S}}
@@ -341,7 +341,7 @@
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires textcomp
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
--- a/src/HOL/Algebra/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Algebra/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -2,7 +2,8 @@
\usepackage{graphicx}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
+\usepackage[utf8]{inputenc}
\usepackage[only,bigsqcap]{stmaryrd}
%\usepackage{amsmath}
@@ -17,8 +18,8 @@
\title{The Isabelle/HOL Algebra Library}
\author{Clemens Ballarin (Editor)}
-\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
- Florian Kammüller and Lawrence C Paulson \\
+\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
+ Florian Kammüller and Lawrence C Paulson \\
\today}
\maketitle
--- a/src/HOL/Auth/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Auth/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,7 +1,7 @@
\documentclass[10pt,a4paper,twoside]{article}
\usepackage{graphicx}
\usepackage{amssymb}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
\usepackage{latexsym,theorem}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}\urlstyle{rm}
--- a/src/HOL/Bali/Trans.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Bali/Trans.thy Fri Dec 03 22:40:26 2010 +0100
@@ -364,7 +364,7 @@
(* Equivalenzen:
Bigstep zu Smallstep komplett.
- Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
+ Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
*)
(*
@@ -372,8 +372,8 @@
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
*)
-(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
- Sowas blödes:
+(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
+ Sowas blödes:
Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
the_vals definieren\<dots>
G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
--- a/src/HOL/Equiv_Relations.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy Fri Dec 03 22:40:26 2010 +0100
@@ -315,7 +315,7 @@
subsection {* Quotients and finiteness *}
-text {*Suggested by Florian Kammüller*}
+text {*Suggested by Florian Kammüller*}
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
-- {* recall @{thm equiv_type} *}
--- a/src/HOL/Finite_Set.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Finite_Set.thy Fri Dec 03 22:40:26 2010 +0100
@@ -2277,7 +2277,7 @@
apply (blast elim!: equalityE)
done
-text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *}
+text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *}
lemma dvd_partition:
"finite (Union C) ==>
--- a/src/HOL/HOL.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOL.thy Fri Dec 03 22:40:26 2010 +0100
@@ -33,9 +33,11 @@
"Tools/try.ML"
("Tools/cnf_funcs.ML")
("Tools/type_mapper.ML")
+ "~~/src/Tools/subtyping.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
+setup Subtyping.setup
subsection {* Primitive logic *}
--- a/src/HOL/HOLCF/IMP/HoareEx.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy Fri Dec 03 22:40:26 2010 +0100
@@ -8,7 +8,7 @@
theory HoareEx imports Denotational begin
text {*
- An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
+ An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
\cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing
the correctness of the Hoare rule for while-loops.
*}
--- a/src/HOL/HOLCF/IMP/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IMP/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,7 +1,7 @@
-
\documentclass[11pt,a4paper]{article}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage{isabelle,isabellesym}
+\usepackage{textcomp}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Abschannel.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The transmission channel *}
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Abschannels.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The transmission channel -- finite version *}
--- a/src/HOL/HOLCF/IOA/ABP/Action.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Action.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The set of all actions of the system *}
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Correctness.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The main correctness proof: System_fin implements System *}
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The environment *}
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The implementation *}
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The implementation *}
--- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Lemmas.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
theory Lemmas
--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Packet.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Packets *}
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Receiver.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The implementation: receiver *}
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Sender.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The implementation: sender *}
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Spec.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The specification of reliable transmission *}
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/IOA/NTP/Abschannel.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The (faulty) transmission channel (both directions) *}
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/ABP/Action.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The set of all actions of the system *}
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/IOA/example/Correctness.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Correctness Proof *}
--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/IOA/example/Spec.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The implementation of a memory *}
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/IOA/example/Spec.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The specification of a memory *}
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/TrivEx.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Trivial Abstraction Example *}
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/TrivEx.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Trivial Abstraction Example with fairness *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Abstraction Theory -- tailored for I/O automata *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/IOA/meta_theory/Asig.thy
- Author: Olaf Müller, Tobias Nipkow & Konrad Slind
+ Author: Olaf Müller, Tobias Nipkow & Konrad Slind
*)
header {* Action signatures *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Automata.thy
- Author: Olaf Müller, Konrad Slind, Tobias Nipkow
+ Author: Olaf Müller, Konrad Slind, Tobias Nipkow
*)
header {* The I/O automata of Lynch and Tuttle in HOLCF *}
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Compositionality on Execution level *}
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Compositionality on Schedule level *}
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Compositionality on Trace level *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Compositionality of I/O automata *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Deadlock.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Deadlock freedom of I/O Automata *}
--- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/IOA.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* The theory of I/O automata in HOLCF *}
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Live I/O automata -- specified by temproal formulas *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Pred.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Logical Connectives lifted to predicates *}
--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Correctness of Refinement Mappings in HOLCF/IOA *}
--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Refinement Mappings in HOLCF/IOA *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Seq.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.thy
- Author: Olaf Müller
+ Author: Olaf Müller
Sequences over flat domains with lifted elements.
*)
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
theory ShortExecutions
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Correctness of Simulations in HOLCF/IOA *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Simulations.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Simulations in HOLCF/IOA *}
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/TLS.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* A General Temporal Logic *}
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/TLS.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Temporal Logic of Steps -- tailored for I/O automata *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Traces.thy
- Author: Olaf Müller
+ Author: Olaf Müller
*)
header {* Executions and Traces of I/O automata in HOLCF *}
--- a/src/HOL/HOLCF/Tutorial/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/Tutorial/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -4,7 +4,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/HOLCF/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -4,7 +4,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/HOLCF/ex/Dagstuhl.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/HOLCF/ex/Dagstuhl.thy Fri Dec 03 22:40:26 2010 +0100
@@ -63,7 +63,7 @@
done
(* ------------------------------------------------------------------------ *)
-(* Zweite L"osung: Bernhard Möller *)
+(* Zweite L"osung: Bernhard Möller *)
(* statt Beweis von wir_moel "uber take_lemma beidseitige Inclusion *)
(* verwendet lemma5 *)
(* ------------------------------------------------------------------------ *)
--- a/src/HOL/IsaMakefile Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/IsaMakefile Fri Dec 03 22:40:26 2010 +0100
@@ -156,6 +156,14 @@
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
+ $(SRC)/Provers/Arith/cancel_div_mod.ML \
+ $(SRC)/Provers/Arith/cancel_sums.ML \
+ $(SRC)/Provers/Arith/fast_lin_arith.ML \
+ $(SRC)/Provers/order.ML \
+ $(SRC)/Provers/trancl.ML \
+ $(SRC)/Tools/Metis/metis.ML \
+ $(SRC)/Tools/rat.ML \
+ $(SRC)/Tools/subtyping.ML \
Complete_Lattice.thy \
Complete_Partial_Order.thy \
Datatype.thy \
@@ -182,10 +190,7 @@
SAT.thy \
Set.thy \
Sum_Type.thy \
- Tools/abel_cancel.ML \
- Tools/arith_data.ML \
- Tools/async_manager.ML \
- Tools/cnf_funcs.ML \
+ Tools/Datatype/datatype.ML \
Tools/Datatype/datatype_abs_proofs.ML \
Tools/Datatype/datatype_aux.ML \
Tools/Datatype/datatype_case.ML \
@@ -193,14 +198,12 @@
Tools/Datatype/datatype_data.ML \
Tools/Datatype/datatype_prop.ML \
Tools/Datatype/datatype_realizer.ML \
- Tools/Datatype/datatype.ML \
- Tools/dseq.ML \
Tools/Function/context_tree.ML \
+ Tools/Function/fun.ML \
+ Tools/Function/function.ML \
Tools/Function/function_common.ML \
Tools/Function/function_core.ML \
Tools/Function/function_lib.ML \
- Tools/Function/function.ML \
- Tools/Function/fun.ML \
Tools/Function/induction_schema.ML \
Tools/Function/lexicographic_order.ML \
Tools/Function/measure_functions.ML \
@@ -214,17 +217,22 @@
Tools/Function/size.ML \
Tools/Function/sum_tree.ML \
Tools/Function/termination.ML \
- Tools/inductive_codegen.ML \
- Tools/inductive.ML \
- Tools/inductive_realizer.ML \
- Tools/inductive_set.ML \
- Tools/lin_arith.ML \
Tools/Meson/meson.ML \
Tools/Meson/meson_clausify.ML \
Tools/Meson/meson_tactic.ML \
Tools/Metis/metis_reconstruct.ML \
+ Tools/Metis/metis_tactics.ML \
Tools/Metis/metis_translate.ML \
- Tools/Metis/metis_tactics.ML \
+ Tools/abel_cancel.ML \
+ Tools/arith_data.ML \
+ Tools/async_manager.ML \
+ Tools/cnf_funcs.ML \
+ Tools/dseq.ML \
+ Tools/inductive.ML \
+ Tools/inductive_codegen.ML \
+ Tools/inductive_realizer.ML \
+ Tools/inductive_set.ML \
+ Tools/lin_arith.ML \
Tools/nat_arith.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
@@ -237,14 +245,7 @@
Tools/typedef.ML \
Transitive_Closure.thy \
Typedef.thy \
- Wellfounded.thy \
- $(SRC)/Provers/Arith/cancel_div_mod.ML \
- $(SRC)/Provers/Arith/cancel_sums.ML \
- $(SRC)/Provers/Arith/fast_lin_arith.ML \
- $(SRC)/Provers/order.ML \
- $(SRC)/Provers/trancl.ML \
- $(SRC)/Tools/Metis/metis.ML \
- $(SRC)/Tools/rat.ML
+ Wellfounded.thy
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
@@ -385,7 +386,6 @@
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
- $(SRC)/Tools/subtyping.ML \
Archimedean_Field.thy \
Complex.thy \
Complex_Main.thy \
--- a/src/HOL/Library/More_List.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Library/More_List.thy Fri Dec 03 22:40:26 2010 +0100
@@ -3,7 +3,7 @@
header {* Operations on lists beyond the standard List theory *}
theory More_List
-imports Main
+imports Main Multiset
begin
hide_const (open) Finite_Set.fold
@@ -78,10 +78,33 @@
"fold g (map f xs) = fold (g o f) xs"
by (induct xs) simp_all
+lemma fold_remove1_split:
+ assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+ and x: "x \<in> set xs"
+ shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
+ using assms by (induct xs) (auto simp add: o_assoc [symmetric])
+
+lemma fold_multiset_equiv:
+ assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+ and equiv: "multiset_of xs = multiset_of ys"
+ shows "fold f xs = fold f ys"
+using f equiv [symmetric] proof (induct xs arbitrary: ys)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs)
+ then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
+ have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+ by (rule Cons.prems(1)) (simp_all add: *)
+ moreover from * have "x \<in> set ys" by simp
+ ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
+ moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
+ ultimately show ?case by simp
+qed
+
lemma fold_rev:
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
shows "fold f (rev xs) = fold f xs"
- using assms by (induct xs) (simp_all del: o_apply add: fold_commute)
+ by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set)
lemma foldr_fold:
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
--- a/src/HOL/Library/Multiset.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Dec 03 22:40:26 2010 +0100
@@ -725,7 +725,7 @@
lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
by (induct x) auto
-lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
+lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
by (induct x) auto
lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
@@ -739,6 +739,10 @@
"multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
by (induct xs) simp_all
+lemma multiset_of_rev [simp]:
+ "multiset_of (rev xs) = multiset_of xs"
+ by (induct xs) simp_all
+
lemma surj_multiset_of: "surj multiset_of"
apply (unfold surj_def)
apply (rule allI)
--- a/src/HOL/Library/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Library/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,8 +1,8 @@
\documentclass[11pt,a4paper]{article}
\usepackage{ifthen}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
+\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Dec 03 22:40:26 2010 +0100
@@ -316,11 +316,10 @@
fun get_prover ctxt args =
let
- val thy = ProofContext.theory_of ctxt
fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
- fun get_prover name = (name, Sledgehammer.get_prover thy false name)
+ fun get_prover name = (name, Sledgehammer.get_prover ctxt false name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
@@ -356,10 +355,11 @@
[("verbose", "true"),
("timeout", Int.toString timeout)]
val default_max_relevant =
- Sledgehammer.default_max_relevant_for_prover thy prover_name
+ Sledgehammer.default_max_relevant_for_prover ctxt prover_name
val is_built_in_const =
Sledgehammer.is_built_in_const_for_prover ctxt prover_name
- val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
+ val relevance_fudge =
+ Sledgehammer.relevance_fudge_for_prover ctxt prover_name
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val facts =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Dec 03 22:40:26 2010 +0100
@@ -106,16 +106,15 @@
SOME proofs =>
let
val {context = ctxt, facts, goal} = Proof.goal pre
- val thy = ProofContext.theory_of ctxt
val prover = AList.lookup (op =) args "prover"
|> the_default default_prover
val default_max_relevant =
- Sledgehammer.default_max_relevant_for_prover thy prover
+ Sledgehammer.default_max_relevant_for_prover ctxt prover
val is_built_in_const =
Sledgehammer.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
extract_relevance_fudge args
- (Sledgehammer.relevance_fudge_for_prover prover)
+ (Sledgehammer.relevance_fudge_for_prover ctxt prover)
val relevance_override = {add = [], del = [], only = false}
val {relevance_thresholds, full_types, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt args
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Fri Dec 03 22:40:26 2010 +0100
@@ -16,19 +16,18 @@
fun run_atp force_full_types timeout i n ctxt goal name =
let
- val thy = ProofContext.theory_of ctxt
val chained_ths = [] (* a tactic has no chained ths *)
val params as {full_types, relevance_thresholds, max_relevant, ...} =
((if force_full_types then [("full_types", "true")] else [])
@ [("timeout", Int.toString (Time.toSeconds timeout))])
@ [("overlord", "true")]
|> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer.get_prover thy false name
+ val prover = Sledgehammer.get_prover ctxt false name
val default_max_relevant =
- Sledgehammer.default_max_relevant_for_prover thy name
+ Sledgehammer.default_max_relevant_for_prover ctxt name
val is_built_in_const =
Sledgehammer.is_built_in_const_for_prover ctxt name
- val relevance_fudge = Sledgehammer.relevance_fudge_for_prover name
+ val relevance_fudge = Sledgehammer.relevance_fudge_for_prover ctxt name
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val facts =
@@ -75,7 +74,6 @@
fun sledgehammer_with_metis_tac ctxt i th =
let
- val thy = ProofContext.theory_of ctxt
val timeout = Time.fromSeconds 30
in
case run_atp false timeout i i ctxt th atp of
--- a/src/HOL/Multivariate_Analysis/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -2,9 +2,8 @@
% HOL/Multivariate_Analysis/document/root.tex
\documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Fri Dec 03 22:40:26 2010 +0100
@@ -26,7 +26,7 @@
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
-ML {* Auto_Tools.time_limit := 10 *}
+ML {* Auto_Tools.time_limit := 10.0 *}
ML {* val mtds = [
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 22:40:26 2010 +0100
@@ -114,13 +114,14 @@
(** quickcheck **)
fun invoke_quickcheck change_options quickcheck_generator thy t =
- TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
+ TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
(fn _ =>
case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
false [] [t] of
(NONE, _) => (NoCex, ([], NONE))
| (SOME _, _) => (GenuineCex, ([], NONE))) ()
- handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
+ handle TimeLimit.TimeOut =>
+ (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE))
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
--- a/src/HOL/NSA/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/NSA/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,9 +1,5 @@
-
-% $Id$
-
\documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
-\usepackage[latin1]{inputenc}
+\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy Fri Dec 03 22:40:26 2010 +0100
@@ -4,7 +4,7 @@
(* This formalisation follows with some very slight exceptions *)
(* the version of this proof given by Randy Pollack in the paper: *)
(* *)
-(* Polishing Up the Tait-Martin Löf Proof of the *)
+(* Polishing Up the Tait-Martin Löf Proof of the *)
(* Church-Rosser Theorem (1995). *)
theory CR_Takahashi
--- a/src/HOL/Old_Number_Theory/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Old_Number_Theory/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,8 +1,7 @@
-
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage{isabelle,isabellesym,pdfsetup}
-\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
\urlstyle{rm}
\isabellestyle{it}
--- a/src/HOL/Probability/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Probability/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -2,9 +2,9 @@
% HOL/Multivariate_Analysis/document/root.tex
\documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/Proofs/Lambda/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Proofs/Lambda/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,8 +1,8 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage[english]{babel}
-\usepackage[latin1]{inputenc}
\usepackage{amssymb}
+\usepackage{textcomp}
\usepackage{isabelle,isabellesym,pdfsetup}
\isabellestyle{it}
--- a/src/HOL/RealDef.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/RealDef.thy Fri Dec 03 22:40:26 2010 +0100
@@ -9,7 +9,6 @@
theory RealDef
imports Rat
-uses "~~/src/Tools/subtyping.ML"
begin
text {*
@@ -1110,8 +1109,7 @@
real_of_nat_def [code_unfold]: "real == real_of_nat"
real_of_int_def [code_unfold]: "real == real_of_int"
-setup Subtyping.setup
-
+declare [[coercion_enabled]]
declare [[coercion "real::nat\<Rightarrow>real"]]
declare [[coercion "real::int\<Rightarrow>real"]]
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 03 22:40:26 2010 +0100
@@ -383,9 +383,8 @@
"set and display the default parameters for Nitpick"
Keyword.thy_decl parse_nitpick_params_command
-fun auto_nitpick state =
- if not (!auto) then (false, state) else pick_nits [] true 1 0 state
+val auto_nitpick = pick_nits [] true 1 0
-val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick)
+val setup = Auto_Tools.register_tool (auto, auto_nitpick)
end;
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Dec 03 22:40:26 2010 +0100
@@ -27,8 +27,11 @@
type solver = bool option -> Proof.context -> (int * thm) list ->
int list * thm
val add_solver: solver_config -> theory -> theory
+ val solver_name_of: Proof.context -> string
val solver_of: Proof.context -> solver
- val is_locally_installed: Proof.context -> bool
+ val available_solvers_of: Proof.context -> string list
+ val is_locally_installed: Proof.context -> string -> bool
+ val is_remotely_available: Proof.context -> string -> bool
(*filter*)
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
@@ -295,14 +298,19 @@
let val name = C.solver_of ctxt
in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
+val solver_name_of = fst o name_and_solver_of
fun solver_of ctxt =
let val (name, raw_solver) = name_and_solver_of ctxt
in gen_solver name raw_solver end
-fun is_locally_installed ctxt =
- let val (_, {env_var, ...}) = name_and_solver_of ctxt
+val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
+
+fun is_locally_installed ctxt name =
+ let val {env_var, ...} = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
in is_some (get_local_solver env_var) end
+fun is_remotely_available ctxt name =
+ #is_remote (the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name))
(* filter *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Dec 03 22:40:26 2010 +0100
@@ -50,21 +50,20 @@
type prover = params -> minimize_command -> prover_problem -> prover_result
- val smtN : string
- val is_prover_available : theory -> string -> bool
+ val is_prover_available : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
- val default_max_relevant_for_prover : theory -> string -> int
+ val default_max_relevant_for_prover : Proof.context -> string -> int
val is_built_in_const_for_prover :
Proof.context -> string -> string * typ -> bool
- val relevance_fudge_for_prover : string -> relevance_fudge
+ val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
- val available_provers : theory -> unit
+ val available_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val get_prover : theory -> bool -> string -> prover
+ val get_prover : Proof.context -> bool -> string -> prover
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -90,27 +89,43 @@
"Async_Manager". *)
val das_Tool = "Sledgehammer"
-val smtN = "smt"
-val smt_prover_names = [smtN, remote_prefix ^ smtN]
+fun is_smt_prover ctxt name =
+ let val smts = SMT_Solver.available_solvers_of ctxt in
+ case try (unprefix remote_prefix) name of
+ SOME suffix => member (op =) smts suffix andalso
+ SMT_Solver.is_remotely_available ctxt suffix
+ | NONE => member (op =) smts name
+ end
-val is_smt_prover = member (op =) smt_prover_names
-
-fun is_prover_available thy name =
- is_smt_prover name orelse member (op =) (available_atps thy) name
+fun is_prover_available ctxt name =
+ let val thy = ProofContext.theory_of ctxt in
+ is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
+ end
fun is_prover_installed ctxt name =
let val thy = ProofContext.theory_of ctxt in
- if is_smt_prover name then SMT_Solver.is_locally_installed ctxt
- else is_atp_installed thy name
+ if is_smt_prover ctxt name then
+ String.isPrefix remote_prefix name orelse
+ SMT_Solver.is_locally_installed ctxt name
+ else
+ is_atp_installed thy name
+ end
+
+fun available_smt_solvers ctxt =
+ let val smts = SMT_Solver.available_solvers_of ctxt in
+ smts @ map (prefix remote_prefix)
+ (filter (SMT_Solver.is_remotely_available ctxt) smts)
end
(* FUDGE *)
val smt_default_max_relevant = 225
val auto_max_relevant_divisor = 2
-fun default_max_relevant_for_prover thy name =
- if is_smt_prover name then smt_default_max_relevant
- else #default_max_relevant (get_atp thy name)
+fun default_max_relevant_for_prover ctxt name =
+ let val thy = ProofContext.theory_of ctxt in
+ if is_smt_prover ctxt name then smt_default_max_relevant
+ else #default_max_relevant (get_atp thy name)
+ end
(* These are typically simplified away by "Meson.presimplify". Equality is
handled specially via "fequal". *)
@@ -119,7 +134,7 @@
@{const_name HOL.eq}]
fun is_built_in_const_for_prover ctxt name (s, T) =
- if is_smt_prover name then SMT_Builtin.is_builtin ctxt (s, T)
+ if is_smt_prover ctxt name then SMT_Builtin.is_builtin ctxt (s, T)
else member (op =) atp_irrelevant_consts s
(* FUDGE *)
@@ -162,13 +177,15 @@
threshold_divisor = #threshold_divisor atp_relevance_fudge,
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
-fun relevance_fudge_for_prover name =
- if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge
+fun relevance_fudge_for_prover ctxt name =
+ if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
-fun available_provers thy =
+fun available_provers ctxt =
let
+ val thy = ProofContext.theory_of ctxt
val (remote_provers, local_provers) =
- sort_strings (available_atps thy) @ smt_prover_names
+ sort_strings (available_atps thy) @
+ sort_strings (available_smt_solvers ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
Output.urgent_message ("Available provers: " ^
@@ -523,11 +540,16 @@
(Config.put Metis_Tactics.verbose debug
#> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
-fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
+fun run_smt_solver auto name (params as {debug, ...}) minimize_command
({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
+ val (remote, suffix) =
+ case try (unprefix remote_prefix) name of
+ SOME suffix => (true, suffix)
+ | NONE => (false, name)
val repair_context =
- Config.put SMT_Config.verbose debug
+ Context.proof_map (SMT_Config.select_solver suffix)
+ #> Config.put SMT_Config.verbose debug
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
val state = state |> Proof.map_context repair_context
val thy = Proof.theory_of state
@@ -558,30 +580,34 @@
run_time_in_msecs = run_time_in_msecs, message = message}
end
-fun get_prover thy auto name =
- if is_smt_prover name then
- run_smt_solver auto (String.isPrefix remote_prefix name)
- else
- run_atp auto name (get_atp thy name)
+fun get_prover ctxt auto name =
+ let val thy = ProofContext.theory_of ctxt in
+ if is_smt_prover ctxt name then
+ run_smt_solver auto name
+ else if member (op =) (available_atps thy) name then
+ run_atp auto name (get_atp thy name)
+ else
+ error ("No such prover: " ^ name ^ ".")
+ end
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
auto minimize_command
(problem as {state, goal, subgoal, subgoal_count, facts, ...})
name =
let
- val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
val max_relevant =
- the_default (default_max_relevant_for_prover thy name) max_relevant
+ the_default (default_max_relevant_for_prover ctxt name) max_relevant
val num_facts = Int.min (length facts, max_relevant)
val desc =
prover_description ctxt params name num_facts subgoal subgoal_count goal
+ val prover = get_prover ctxt auto name
fun go () =
let
fun really_go () =
- get_prover thy auto name params (minimize_command name) problem
+ prover params (minimize_command name) problem
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some", message))
val (outcome_code, message) =
@@ -629,13 +655,15 @@
| n =>
let
val _ = Proof.assert_backward state
- val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val {facts = chained_ths, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val _ = () |> not blocking ? kill_provers
+ val _ = case find_first (not o is_prover_available ctxt) provers of
+ SOME name => error ("No such prover: " ^ name ^ ".")
+ | NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
- val (smts, atps) = provers |> List.partition is_smt_prover
+ val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
fun run_provers label full_types relevance_fudge maybe_translate provers
(res as (success, state)) =
if success orelse null provers then
@@ -646,7 +674,7 @@
case max_relevant of
SOME n => n
| NONE =>
- 0 |> fold (Integer.max o default_max_relevant_for_prover thy)
+ 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
provers
|> auto ? (fn n => n div auto_max_relevant_divisor)
val is_built_in_const =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 22:40:26 2010 +0100
@@ -130,39 +130,36 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
-fun remotify_prover_if_available_and_not_already_remote thy name =
+fun remotify_prover_if_available_and_not_already_remote ctxt name =
if String.isPrefix remote_prefix name then
SOME name
else
let val remote_name = remote_prefix ^ name in
- if is_prover_available thy remote_name then SOME remote_name else NONE
+ if is_prover_available ctxt remote_name then SOME remote_name else NONE
end
fun remotify_prover_if_not_installed ctxt name =
- let val thy = ProofContext.theory_of ctxt in
- if is_prover_available thy name andalso is_prover_installed ctxt name then
- SOME name
- else
- remotify_prover_if_available_and_not_already_remote thy name
- end
+ if is_prover_available ctxt name andalso is_prover_installed ctxt name then
+ SOME name
+ else
+ remotify_prover_if_available_and_not_already_remote ctxt name
fun avoid_too_many_local_threads _ _ [] = []
- | avoid_too_many_local_threads thy 0 provers =
- map_filter (remotify_prover_if_available_and_not_already_remote thy) provers
- | avoid_too_many_local_threads thy n (prover :: provers) =
+ | avoid_too_many_local_threads ctxt 0 provers =
+ map_filter (remotify_prover_if_available_and_not_already_remote ctxt)
+ provers
+ | avoid_too_many_local_threads ctxt n (prover :: provers) =
let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
- prover :: avoid_too_many_local_threads thy n provers
+ prover :: avoid_too_many_local_threads ctxt n provers
end
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value ctxt =
- let val thy = ProofContext.theory_of ctxt in
- [spassN, eN, vampireN, sine_eN, smtN]
- |> map_filter (remotify_prover_if_not_installed ctxt)
- |> avoid_too_many_local_threads thy (Multithreading.max_threads_value ())
- |> space_implode " "
- end
+ [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
+ |> map_filter (remotify_prover_if_not_installed ctxt)
+ |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
+ |> space_implode " "
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
fun default_raw_params ctxt =
@@ -270,7 +267,6 @@
fun hammer_away override_params subcommand opt_i relevance_override state =
let
val ctxt = Proof.context_of state
- val thy = Proof.theory_of state
val _ = app check_raw_param override_params
in
if subcommand = runN then
@@ -286,7 +282,7 @@
else if subcommand = messagesN then
messages opt_i
else if subcommand = available_proversN then
- available_provers thy
+ available_provers ctxt
else if subcommand = running_proversN then
running_provers ()
else if subcommand = kill_proversN then
@@ -347,14 +343,11 @@
parse_sledgehammer_params_command
fun auto_sledgehammer state =
- if not (!auto) then
- (false, state)
- else
- let val ctxt = Proof.context_of state in
- run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
- (minimize_command [] 1) state
- end
+ let val ctxt = Proof.context_of state in
+ run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
+ (minimize_command [] 1) state
+ end
-val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
+val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 03 22:40:26 2010 +0100
@@ -92,7 +92,8 @@
state facts =
let
val thy = Proof.theory_of state
- val prover = get_prover thy false prover_name
+ val ctxt = Proof.context_of state
+ val prover = get_prover ctxt false prover_name
val msecs = Time.toMilliseconds timeout
val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
val {goal, ...} = Proof.goal state
--- a/src/HOL/Tools/try.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/Tools/try.ML Fri Dec 03 22:40:26 2010 +0100
@@ -110,8 +110,8 @@
(Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
o Toplevel.proof_of)))
-fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
+val auto_try = do_try true NONE
-val setup = Auto_Tools.register_tool (tryN, auto_try)
+val setup = Auto_Tools.register_tool (auto, auto_try)
end;
--- a/src/HOL/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -2,9 +2,10 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage{amssymb}
+\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/ex/ROOT.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Dec 03 22:40:26 2010 +0100
@@ -8,7 +8,10 @@
"Efficient_Nat_examples",
"FuncSet",
"Eval_Examples",
- "Normalization_by_Evaluation"
+ "Normalization_by_Evaluation",
+ "Hebrew",
+ "Chinese",
+ "Serbian"
];
use_thys [
@@ -71,9 +74,6 @@
"Birthday_Paradoxon"
];
-HTML.with_charset "utf-8" (no_document use_thys)
- ["Hebrew", "Chinese", "Serbian"];
-
use_thy "SVC_Oracle";
if getenv "SVC_HOME" = "" then ()
else use_thy "svc_test";
--- a/src/HOL/ex/SVC_Oracle.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Dec 03 22:40:26 2010 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
-Based upon the work of Søren T. Heilmann.
+Based upon the work of Søren T. Heilmann.
*)
header {* Installing an oracle for SVC (Stanford Validity Checker) *}
@@ -28,7 +28,7 @@
The following code merely CALLS the oracle;
the soundness-critical functions are at svc_funcs.ML
-Based upon the work of Søren T. Heilmann
+Based upon the work of Søren T. Heilmann
*)
--- a/src/HOL/ex/Tarski.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/ex/Tarski.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/ex/Tarski.thy
ID: $Id$
- Author: Florian Kammüller, Cambridge University Computer Laboratory
+ Author: Florian Kammüller, Cambridge University Computer Laboratory
*)
header {* The Full Theorem of Tarski *}
--- a/src/HOL/ex/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/ex/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -3,7 +3,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{textcomp}
\usepackage{amssymb}
--- a/src/HOL/ex/set.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/HOL/ex/set.thy Fri Dec 03 22:40:26 2010 +0100
@@ -4,7 +4,7 @@
Copyright 1991 University of Cambridge
*)
-header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
+header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
theory set imports Main begin
@@ -73,7 +73,7 @@
by best
-subsection {* The Schröder-Berstein Theorem *}
+subsection {* The Schröder-Berstein Theorem *}
lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
by blast
--- a/src/Pure/Concurrent/bash.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Pure/Concurrent/bash.ML Fri Dec 03 22:40:26 2010 +0100
@@ -64,8 +64,7 @@
in () end;
fun cleanup () =
- (terminate ();
- Simple_Thread.interrupt system_thread;
+ (Simple_Thread.interrupt system_thread;
try File.rm script_path;
try File.rm output_path;
try File.rm pid_path);
@@ -79,6 +78,6 @@
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
val _ = cleanup ();
in (output, rc) end
- handle exn => (cleanup (); reraise exn)
+ handle exn => (terminate(); cleanup (); reraise exn)
end);
--- a/src/Pure/Thy/html.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Pure/Thy/html.ML Fri Dec 03 22:40:26 2010 +0100
@@ -20,7 +20,6 @@
val para: text -> text
val preform: text -> text
val verbatim: string -> text
- val with_charset: string -> ('a -> 'b) -> 'a -> 'b
val begin_document: string -> text
val end_document: text
val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
@@ -276,25 +275,20 @@
(* document *)
-val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = Unsynchronized.setmp charset s; (* FIXME unreliable *)
-
fun begin_document title =
- let val cs = ! charset in
- "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
- \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
- \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
- \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
- \<head>\n\
- \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\
- \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
- \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
- \</head>\n\
- \\n\
- \<body>\n\
- \<div class=\"head\">\
- \<h1>" ^ plain title ^ "</h1>\n"
- end;
+ "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
+ \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
+ \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
+ \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
+ \<head>\n\
+ \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
+ \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
+ \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
+ \</head>\n\
+ \\n\
+ \<body>\n\
+ \<div class=\"head\">\
+ \<h1>" ^ plain title ^ "</h1>\n";
val end_document = "\n</div>\n</body>\n</html>\n";
--- a/src/Pure/Thy/present.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Pure/Thy/present.ML Fri Dec 03 22:40:26 2010 +0100
@@ -489,7 +489,7 @@
-(** draft document output **)
+(** draft document output **) (* FIXME doc_path etc. not thread-safe *)
fun drafts doc_format src_paths =
let
--- a/src/Pure/library.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Pure/library.ML Fri Dec 03 22:40:26 2010 +0100
@@ -727,13 +727,11 @@
(*simple quoting (does not escape special chars)*)
val quote = enclose "\"" "\"";
-(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
fun space_implode a bs = implode (separate a bs);
val commas = space_implode ", ";
val commas_quote = commas o map quote;
-(*concatenate messages, one per line, into a string*)
val cat_lines = space_implode "\n";
(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
--- a/src/Tools/auto_tools.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Tools/auto_tools.ML Fri Dec 03 22:40:26 2010 +0100
@@ -6,10 +6,11 @@
signature AUTO_TOOLS =
sig
- val time_limit: int Unsynchronized.ref
+ val time_limit: real Unsynchronized.ref
val register_tool :
- string * (Proof.state -> bool * Proof.state) -> theory -> theory
+ bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
+ -> theory
end;
structure Auto_Tools : AUTO_TOOLS =
@@ -17,20 +18,20 @@
(* preferences *)
-val time_limit = Unsynchronized.ref 4000
+val time_limit = Unsynchronized.ref 4.0
+val auto_tools_time_limitN = "auto-tools-time-limit"
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.nat_pref time_limit
- "auto-tools-time-limit"
- "Time limit for automatic tools (in milliseconds).")
+ (Preferences.real_pref time_limit
+ auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
(* configuration *)
structure Data = Theory_Data
(
- type T = (string * (Proof.state -> bool * Proof.state)) list
+ type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
val empty = []
val extend = I
fun merge data : T = AList.merge (op =) (K true) data
@@ -41,18 +42,30 @@
(* automatic testing *)
+fun run_tools tools state =
+ tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
+ |> Par_List.get_some (fn tool =>
+ case try tool state of
+ SOME (true, state) => SOME state
+ | _ => NONE)
+ |> the_default state
+
+(* Too large values are understood as milliseconds, ensuring compatibility with
+ old setting files. No users can possibly in their right mind want the user
+ interface to block for more than 100 seconds. *)
+fun smart_seconds r =
+ seconds (if r >= 100.0 then
+ (legacy_feature (quote auto_tools_time_limitN ^
+ " expressed in milliseconds -- use seconds instead"); 0.001 * r)
+ else
+ r)
+
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- case !time_limit of
- 0 => state
- | ms =>
- TimeLimit.timeLimit (Time.fromMilliseconds ms)
- (fn () =>
- if interact andalso not (!Toplevel.quiet) then
- fold_rev (fn (_, tool) => fn (true, state) => (true, state)
- | (false, state) => tool state)
- (Data.get (Proof.theory_of state)) (false, state) |> snd
- else
- state) ()
- handle TimeLimit.TimeOut => state))
+ if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
+ TimeLimit.timeLimit (smart_seconds (!time_limit))
+ (run_tools (Data.get (Proof.theory_of state))) state
+ handle TimeLimit.TimeOut => state
+ else
+ state))
end;
--- a/src/Tools/jEdit/dist-template/README.html Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Tools/jEdit/dist-template/README.html Fri Dec 03 22:40:26 2010 +0100
@@ -15,7 +15,7 @@
<li>The original jEdit look-and-feel is generally preserved, although
some default properties have been changed to accommodate Isabelle
- (e.g. main the text area font).</li>
+ (e.g. the text area font).</li>
<li>Formal Isabelle/Isar text is checked asynchronously while editing.
The user is in full command of the editor, and the prover refrains
--- a/src/Tools/quickcheck.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Tools/quickcheck.ML Fri Dec 03 22:40:26 2010 +0100
@@ -303,24 +303,21 @@
(* automatic testing *)
fun auto_quickcheck state =
- if not (!auto) then
- (false, state)
- else
- let
- val ctxt = Proof.context_of state;
- val res =
- state
- |> Proof.map_context (Config.put report false #> Config.put quiet true)
- |> try (test_goal [] 1);
- in
- case res of
- NONE => (false, state)
- | SOME (NONE, report) => (false, state)
- | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
- end
+ let
+ val ctxt = Proof.context_of state;
+ val res =
+ state
+ |> Proof.map_context (Config.put report false #> Config.put quiet true)
+ |> try (test_goal [] 1);
+ in
+ case res of
+ NONE => (false, state)
+ | SOME (NONE, report) => (false, state)
+ | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+ Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
+ end
-val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
+val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
#> setup_config
(* Isar commands *)
--- a/src/Tools/solve_direct.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Tools/solve_direct.ML Fri Dec 03 22:40:26 2010 +0100
@@ -97,9 +97,8 @@
(* hook *)
-fun auto_solve_direct state =
- if not (! auto) then (false, state) else solve_direct true state;
+val auto_solve_direct = solve_direct true
-val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);
+val setup = Auto_Tools.register_tool (auto, auto_solve_direct);
end;
--- a/src/Tools/subtyping.ML Fri Dec 03 14:46:58 2010 +0100
+++ b/src/Tools/subtyping.ML Fri Dec 03 22:40:26 2010 +0100
@@ -7,6 +7,7 @@
signature SUBTYPING =
sig
datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT
+ val coercion_enabled: bool Config.T
val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
term list -> term list
val add_type_map: term -> Context.generic -> Context.generic
@@ -685,11 +686,11 @@
raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
in (tu, V, tye_idx'') end;
- fun infer_single t (ts, tye_idx) =
+ fun infer_single t tye_idx =
let val (t, _, tye_idx') = inf [] t tye_idx;
- in (ts @ [t], tye_idx') end;
+ in (t, tye_idx') end;
- val (ts', (tye, _)) = (fold infer_single ts ([], (Vartab.empty, idx))
+ val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
handle TYPE_INFERENCE_ERROR err =>
let
fun gen_single t (tye_idx, constraints) =
@@ -716,11 +717,15 @@
(try (Consts.the_constraint (ProofContext.consts_of ctxt)))
(ProofContext.def_type ctxt);
+val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
+
val add_term_check =
Syntax.add_term_check ~100 "coercions"
(fn xs => fn ctxt =>
- let val xs' = coercion_infer_types ctxt xs
- in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end);
+ if Config.get ctxt coercion_enabled then
+ let val xs' = coercion_infer_types ctxt xs
+ in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end
+ else NONE);
(* declarations *)
@@ -821,6 +826,7 @@
(* theory setup *)
val setup =
+ coercion_enabled_setup #>
Context.theory_map add_term_check #>
Attrib.setup @{binding coercion}
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
--- a/src/ZF/AC/WO6_WO1.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Fri Dec 03 22:40:26 2010 +0100
@@ -6,7 +6,7 @@
Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear"
by Rubin & Rubin (page 2).
-They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
+They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
Fortunately order types made this proof also very easy.
*)
--- a/src/ZF/IMP/Com.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/IMP/Com.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: ZF/IMP/Com.thy
- Author: Heiko Loetzbeyer and Robert Sandner, TU München
+ Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
header {* Arithmetic expressions, boolean expressions, commands *}
--- a/src/ZF/IMP/Denotation.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/IMP/Denotation.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: ZF/IMP/Denotation.thy
- Author: Heiko Loetzbeyer and Robert Sandner, TU München
+ Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
header {* Denotational semantics of expressions and commands *}
--- a/src/ZF/IMP/Equiv.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/IMP/Equiv.thy Fri Dec 03 22:40:26 2010 +0100
@@ -1,5 +1,5 @@
(* Title: ZF/IMP/Equiv.thy
- Author: Heiko Loetzbeyer and Robert Sandner, TU München
+ Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
header {* Equivalence *}
--- a/src/ZF/Induct/Brouwer.thy Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/Induct/Brouwer.thy Fri Dec 03 22:40:26 2010 +0100
@@ -39,7 +39,7 @@
done
-subsection {* The Martin-Löf wellordering type *}
+subsection {* The Martin-Löf wellordering type *}
consts
Well :: "[i, i => i] => i"
--- a/src/ZF/Induct/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/Induct/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,7 +1,6 @@
-
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/ZF/document/root.tex Fri Dec 03 14:46:58 2010 +0100
+++ b/src/ZF/document/root.tex Fri Dec 03 22:40:26 2010 +0100
@@ -1,49 +1,38 @@
-
-\documentclass[11pt,a4paper]{article}
-\usepackage{graphicx,isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-%\usepackage{latexsym}
-\usepackage{amssymb}
-%\usepackage[english]{babel}
-%\usepackage[latin1]{inputenc}
-%\usepackage[only,bigsqcap]{stmaryrd}
-%\usepackage{wasysym}
-%\usepackage{eufrak}
-%\usepackage{textcomp}
-%\usepackage{marvosym}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% proper setup for best-style documents
-\urlstyle{rm}
-\isabellestyle{it}
-
-
-\begin{document}
-
-\title{ZF}
-\author{Lawrence C Paulson and others}
-\maketitle
-
-\tableofcontents
-
-\begin{center}
- \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
-\end{center}
-
-\newpage
-
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
-
-\parindent 0pt\parskip 0.5ex
-
-% include generated text of all theories
-\input{session}
-
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
-\end{document}
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx,isabelle,isabellesym}
+\usepackage{amssymb}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% proper setup for best-style documents
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{ZF}
+\author{Lawrence C Paulson and others}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+ \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
+\end{center}
+
+\newpage
+
+\renewcommand{\isamarkupheader}[1]%
+{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+
+\parindent 0pt\parskip 0.5ex
+
+% include generated text of all theories
+\input{session}
+
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}