merge
authorblanchet
Tue Nov 24 10:33:21 2009 +0100 (2009-11-24)
changeset 338806cc01403f78a
parent 33879 8dfc55999130
parent 33875 e5e7faaed7ad
child 33881 d8958955ecb5
merge
     1.1 --- a/ANNOUNCE	Tue Nov 24 10:33:02 2009 +0100
     1.2 +++ b/ANNOUNCE	Tue Nov 24 10:33:21 2009 +0100
     1.3 @@ -7,7 +7,34 @@
     1.4  file in the distribution for more details.  Some important changes
     1.5  are:
     1.6  
     1.7 -* FIXME
     1.8 +* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
     1.9 +on a given logic image.
    1.10 +
    1.11 +* HOL-SMT: proof method "smt" for a combination of first-order logic
    1.12 +with equality, linear and nonlinear (natural/integer/real) arithmetic,
    1.13 +and fixed-size bitvectors.
    1.14 +
    1.15 +* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    1.16 +
    1.17 +* HOL: Counterexample generator tool Nitpick based on the Kodkod
    1.18 +relational model finder.
    1.19 +
    1.20 +* HOL: predicate compiler turning inductive into (executable)
    1.21 +equational specifications.
    1.22 +
    1.23 +* HOL: refined number theory.
    1.24 +
    1.25 +* HOL: various parts of multivariate analysis.
    1.26 +
    1.27 +* HOLCF: new definitional domain package.
    1.28 +
    1.29 +* Revised tutorial on locales.
    1.30 +
    1.31 +* Support for Poly/ML 5.3.0, with improved reporting of compiler
    1.32 +errors and run-time exceptions, including detailed source positions.
    1.33 +
    1.34 +* Parallel checking of nested Isar proofs, with improved scalability
    1.35 +up to 8 cores.
    1.36  
    1.37  
    1.38  You may get Isabelle2009-1 from the following mirror sites:
     2.1 --- a/Admin/E/README	Tue Nov 24 10:33:02 2009 +0100
     2.2 +++ b/Admin/E/README	Tue Nov 24 10:33:21 2009 +0100
     2.3 @@ -1,4 +1,3 @@
     2.4 -
     2.5  This distribution of E 1.0-004 has been compiled according to the
     2.6  README included in the official version from
     2.7  http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
     2.8 @@ -8,23 +7,12 @@
     2.9    $ ./configure
    2.10    $ make
    2.11  
    2.12 -The resulting PROVER/eproof executable has been changed to be
    2.13 -relocatable:
    2.14 -
    2.15 -  $ diff eproof-orig eproof
    2.16 -  1c1
    2.17 -  < #!/bin/bash -f
    2.18 -  ---
    2.19 -  > #!/usr/bin/env bash
    2.20 -  3c3,4
    2.21 -  < EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER
    2.22 -  ---
    2.23 -  > set -o noglob
    2.24 -  > EXECPATH="$(cd "$(dirname "$0")"; pwd)"
    2.25 +The PROVER/eproof executable has been replaced by a version written in
    2.26 +perl (by Sascha Boehme).
    2.27  
    2.28  Now the main executables in PROVER/ are moved to the platform-specific
    2.29  target directory (E/x86-linux etc.).
    2.30  
    2.31  
    2.32 -	Makarius
    2.33 -	07-Apr-2009
    2.34 +        Makarius
    2.35 +        23-Nov-2009
     3.1 --- a/INSTALL	Tue Nov 24 10:33:02 2009 +0100
     3.2 +++ b/INSTALL	Tue Nov 24 10:33:21 2009 +0100
     3.3 @@ -17,7 +17,7 @@
     3.4  site installation of Isabelle on Linux/x86 works like this:
     3.5  
     3.6    tar -C /usr/local -xzf Isabelle.tar.gz
     3.7 -  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
     3.8 +  tar -C /usr/local -xzf polyml.tar.gz
     3.9    tar -C /usr/local -xzf HOL_x86-linux.tar.gz
    3.10  
    3.11  The install prefix given above may be changed as appropriate; there is
     4.1 --- a/NEWS	Tue Nov 24 10:33:02 2009 +0100
     4.2 +++ b/NEWS	Tue Nov 24 10:33:21 2009 +0100
     4.3 @@ -114,19 +114,17 @@
     4.4  fixpoint theorem.
     4.5  
     4.6  * Reorganization of number theory, INCOMPATIBILITY:
     4.7 -  - new number theory development for nat and int, in
     4.8 -    theories Divides and GCD as well as in new session
     4.9 -    Number_Theory
    4.10 -  - some constants and facts now suffixed with _nat and
    4.11 -    _int accordingly
    4.12 -  - former session NumberTheory now named Old_Number_Theory,
    4.13 -    including theories Legacy_GCD and Primes (prefer Number_Theory
    4.14 -    if possible)
    4.15 +  - new number theory development for nat and int, in theories Divides
    4.16 +    and GCD as well as in new session Number_Theory
    4.17 +  - some constants and facts now suffixed with _nat and _int
    4.18 +    accordingly
    4.19 +  - former session NumberTheory now named Old_Number_Theory, including
    4.20 +    theories Legacy_GCD and Primes (prefer Number_Theory if possible)
    4.21    - moved theory Pocklington from src/HOL/Library to
    4.22      src/HOL/Old_Number_Theory
    4.23  
    4.24 -* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
    4.25 -of finite and infinite sets. It is shown that they form a complete
    4.26 +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
    4.27 +lcm of finite and infinite sets. It is shown that they form a complete
    4.28  lattice.
    4.29  
    4.30  * Class semiring_div requires superclass no_zero_divisors and proof of
    4.31 @@ -198,8 +196,6 @@
    4.32  abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
    4.33  INCOMPATIBILITY.
    4.34  
    4.35 ---
    4.36 -
    4.37  * Most rules produced by inductive and datatype package have mandatory
    4.38  prefixes.  INCOMPATIBILITY.
    4.39  
    4.40 @@ -208,8 +204,9 @@
    4.41  DERIV_intros assumes composition with an additional function and
    4.42  matches a variable to the derivative, which has to be solved by the
    4.43  Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
    4.44 -of most elementary terms.  Former Maclauren.DERIV_tac and Maclauren.deriv_tac
    4.45 -should be replaced by (auto intro!: DERIV_intros).  INCOMPATIBILITY.
    4.46 +of most elementary terms.  Former Maclauren.DERIV_tac and
    4.47 +Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
    4.48 +INCOMPATIBILITY.
    4.49  
    4.50  * Code generator attributes follow the usual underscore convention:
    4.51      code_unfold     replaces    code unfold
    4.52 @@ -274,7 +271,8 @@
    4.53  * The 'fixrec' package now supports "bottom patterns".  Bottom
    4.54  patterns can be used to generate strictness rules, or to make
    4.55  functions more strict (much like the bang-patterns supported by the
    4.56 -Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for examples.
    4.57 +Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
    4.58 +examples.
    4.59  
    4.60  
    4.61  *** ML ***
     5.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Tue Nov 24 10:33:02 2009 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Tue Nov 24 10:33:21 2009 +0100
     5.3 @@ -456,13 +456,10 @@
     5.4    \secref{sec:object-logic}).  Separate introduction rules @{text
     5.5    loc_axioms.intro} and @{text loc.intro} are provided as well.
     5.6    
     5.7 -  \item @{command "print_locale"}~@{text "import + body"} prints the
     5.8 -  specified locale expression in a flattened form.  The notable
     5.9 -  special case @{command "print_locale"}~@{text loc} just prints the
    5.10 -  contents of the named locale, but keep in mind that type-inference
    5.11 -  will normalize type variables according to the usual alphabetical
    5.12 -  order.  The command omits @{element "notes"} elements by default.
    5.13 -  Use @{command "print_locale"}@{text "!"} to get them included.
    5.14 +  \item @{command "print_locale"}~@{text "locale"} prints the
    5.15 +  contents of the named locale.  The command omits @{element "notes"}
    5.16 +  elements by default.  Use @{command "print_locale"}@{text "!"} to
    5.17 +  have them included.
    5.18  
    5.19    \item @{command "print_locales"} prints the names of all locales
    5.20    of the current theory.
    5.21 @@ -537,7 +534,7 @@
    5.22    qualifier, although only for fragments of @{text expr} that are not
    5.23    interpreted in the theory already.
    5.24  
    5.25 -  \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
    5.26 +  \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
    5.27    interprets @{text expr} in the theory.  The command generates proof
    5.28    obligations for the instantiated specifications (assumes and defines
    5.29    elements).  Once these are discharged by the user, instantiated
    5.30 @@ -563,19 +560,24 @@
    5.31    interpretations dynamically participate in any facts added to
    5.32    locales.
    5.33  
    5.34 -  \item @{command "interpret"}~@{text "expr insts"}
    5.35 +  \item @{command "interpret"}~@{text "expr"}
    5.36    interprets @{text expr} in the proof context and is otherwise
    5.37    similar to interpretation in theories.
    5.38  
    5.39 +  \item @{command "print_interps"}~@{text "locale"} lists all
    5.40 +  interpretations of @{text "locale"} in the current theory, including
    5.41 +  those due to a combination of an @{command "interpretation"} and
    5.42 +  one or several @{command "sublocale"} declarations.
    5.43 +
    5.44    \end{description}
    5.45  
    5.46    \begin{warn}
    5.47      Since attributes are applied to interpreted theorems,
    5.48      interpretation may modify the context of common proof tools, e.g.\
    5.49 -    the Simplifier or Classical Reasoner.  Since the behavior of such
    5.50 -    automated reasoning tools is \emph{not} stable under
    5.51 -    interpretation morphisms, manual declarations might have to be
    5.52 -    added to revert such declarations.
    5.53 +    the Simplifier or Classical Reasoner.  As the behavior of such
    5.54 +    tools is \emph{not} stable under interpretation morphisms, manual
    5.55 +    declarations might have to be added to the target context of the
    5.56 +    interpretation to revert such declarations.
    5.57    \end{warn}
    5.58  
    5.59    \begin{warn}
     6.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Nov 24 10:33:02 2009 +0100
     6.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Nov 24 10:33:21 2009 +0100
     6.3 @@ -478,13 +478,10 @@
     6.4    \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
     6.5    \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
     6.6    
     6.7 -  \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
     6.8 -  specified locale expression in a flattened form.  The notable
     6.9 -  special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
    6.10 -  contents of the named locale, but keep in mind that type-inference
    6.11 -  will normalize type variables according to the usual alphabetical
    6.12 -  order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
    6.13 -  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
    6.14 +  \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
    6.15 +  contents of the named locale.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
    6.16 +  elements by default.  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
    6.17 +  have them included.
    6.18  
    6.19    \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
    6.20    of the current theory.
    6.21 @@ -559,7 +556,7 @@
    6.22    qualifier, although only for fragments of \isa{expr} that are not
    6.23    interpreted in the theory already.
    6.24  
    6.25 -  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
    6.26 +  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
    6.27    interprets \isa{expr} in the theory.  The command generates proof
    6.28    obligations for the instantiated specifications (assumes and defines
    6.29    elements).  Once these are discharged by the user, instantiated
    6.30 @@ -585,19 +582,24 @@
    6.31    interpretations dynamically participate in any facts added to
    6.32    locales.
    6.33  
    6.34 -  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
    6.35 +  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
    6.36    interprets \isa{expr} in the proof context and is otherwise
    6.37    similar to interpretation in theories.
    6.38  
    6.39 +  \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
    6.40 +  interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
    6.41 +  those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
    6.42 +  one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
    6.43 +
    6.44    \end{description}
    6.45  
    6.46    \begin{warn}
    6.47      Since attributes are applied to interpreted theorems,
    6.48      interpretation may modify the context of common proof tools, e.g.\
    6.49 -    the Simplifier or Classical Reasoner.  Since the behavior of such
    6.50 -    automated reasoning tools is \emph{not} stable under
    6.51 -    interpretation morphisms, manual declarations might have to be
    6.52 -    added to revert such declarations.
    6.53 +    the Simplifier or Classical Reasoner.  As the behavior of such
    6.54 +    tools is \emph{not} stable under interpretation morphisms, manual
    6.55 +    declarations might have to be added to the target context of the
    6.56 +    interpretation to revert such declarations.
    6.57    \end{warn}
    6.58  
    6.59    \begin{warn}
     7.1 --- a/doc-src/Locales/Locales/Examples3.thy	Tue Nov 24 10:33:02 2009 +0100
     7.2 +++ b/doc-src/Locales/Locales/Examples3.thy	Tue Nov 24 10:33:21 2009 +0100
     7.3 @@ -591,7 +591,7 @@
     7.4    ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
     7.5    \textit{instance} & ::=
     7.6    & [ \textit{qualifier} ``\textbf{:}'' ]
     7.7 -    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     7.8 +    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     7.9    \textit{expression}  & ::= 
    7.10    & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
    7.11      [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
    7.12 @@ -625,8 +625,8 @@
    7.13  
    7.14    \textit{toplevel} & ::=
    7.15    & \textbf{print\_locales} \\
    7.16 -  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
    7.17 -  & | & \textbf{print\_interps} \textit{locale}
    7.18 +  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
    7.19 +  & | & \textbf{print\_interps} \textit{name}
    7.20  \end{tabular}
    7.21  \end{center}
    7.22  \hrule
     8.1 --- a/doc-src/Locales/Locales/document/Examples3.tex	Tue Nov 24 10:33:02 2009 +0100
     8.2 +++ b/doc-src/Locales/Locales/document/Examples3.tex	Tue Nov 24 10:33:21 2009 +0100
     8.3 @@ -882,7 +882,7 @@
     8.4    ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
     8.5    \textit{instance} & ::=
     8.6    & [ \textit{qualifier} ``\textbf{:}'' ]
     8.7 -    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     8.8 +    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     8.9    \textit{expression}  & ::= 
    8.10    & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
    8.11      [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
    8.12 @@ -916,8 +916,8 @@
    8.13  
    8.14    \textit{toplevel} & ::=
    8.15    & \textbf{print\_locales} \\
    8.16 -  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
    8.17 -  & | & \textbf{print\_interps} \textit{locale}
    8.18 +  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
    8.19 +  & | & \textbf{print\_interps} \textit{name}
    8.20  \end{tabular}
    8.21  \end{center}
    8.22  \hrule
     9.1 --- a/etc/isar-keywords-ZF.el	Tue Nov 24 10:33:02 2009 +0100
     9.2 +++ b/etc/isar-keywords-ZF.el	Tue Nov 24 10:33:21 2009 +0100
     9.3 @@ -19,6 +19,7 @@
     9.4      "ProofGeneral\\.inform_file_processed"
     9.5      "ProofGeneral\\.inform_file_retracted"
     9.6      "ProofGeneral\\.kill_proof"
     9.7 +    "ProofGeneral\\.pr"
     9.8      "ProofGeneral\\.process_pgip"
     9.9      "ProofGeneral\\.restart"
    9.10      "ProofGeneral\\.undo"
    9.11 @@ -271,6 +272,7 @@
    9.12  (defconst isar-keywords-diag
    9.13    '("ML_command"
    9.14      "ML_val"
    9.15 +    "ProofGeneral\\.pr"
    9.16      "cd"
    9.17      "class_deps"
    9.18      "commit"
    10.1 --- a/etc/isar-keywords.el	Tue Nov 24 10:33:02 2009 +0100
    10.2 +++ b/etc/isar-keywords.el	Tue Nov 24 10:33:21 2009 +0100
    10.3 @@ -19,6 +19,7 @@
    10.4      "ProofGeneral\\.inform_file_processed"
    10.5      "ProofGeneral\\.inform_file_retracted"
    10.6      "ProofGeneral\\.kill_proof"
    10.7 +    "ProofGeneral\\.pr"
    10.8      "ProofGeneral\\.process_pgip"
    10.9      "ProofGeneral\\.restart"
   10.10      "ProofGeneral\\.undo"
   10.11 @@ -345,6 +346,7 @@
   10.12  (defconst isar-keywords-diag
   10.13    '("ML_command"
   10.14      "ML_val"
   10.15 +    "ProofGeneral\\.pr"
   10.16      "atp_info"
   10.17      "atp_kill"
   10.18      "atp_messages"
    11.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Tue Nov 24 10:33:02 2009 +0100
    11.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Tue Nov 24 10:33:21 2009 +0100
    11.3 @@ -185,7 +185,7 @@
    11.4      by (auto simp add: rtranclp_eq_rtrancl_path)
    11.5  qed
    11.6  
    11.7 -declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
    11.8 +declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
    11.9  
   11.10  declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
   11.11  
   11.12 @@ -224,7 +224,11 @@
   11.13  values "{x. test\<^sup>*\<^sup>* A x}"
   11.14  values "{x. test\<^sup>*\<^sup>* x C}"
   11.15  
   11.16 -hide const test
   11.17 +value "test\<^sup>*\<^sup>* A C"
   11.18 +value "test\<^sup>*\<^sup>* C A"
   11.19 +
   11.20 +hide type ty
   11.21 +hide const test A B C
   11.22  
   11.23  end
   11.24  
    12.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Nov 24 10:33:02 2009 +0100
    12.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Nov 24 10:33:21 2009 +0100
    12.3 @@ -190,6 +190,12 @@
    12.4  
    12.5  local structure P = OuterParse and K = OuterKeyword in
    12.6  
    12.7 +fun prP () =
    12.8 +  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
    12.9 +    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
   12.10 +      if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
   12.11 +      else (Toplevel.quiet := false; Toplevel.print_state true state))));
   12.12 +
   12.13  fun undoP () = (*undo without output -- historical*)
   12.14    OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   12.15      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
   12.16 @@ -219,7 +225,8 @@
   12.17        (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
   12.18  
   12.19  fun init_outer_syntax () = List.app (fn f => f ())
   12.20 -  [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
   12.21 +  [prP, undoP, restartP, kill_proofP, inform_file_processedP,
   12.22 +    inform_file_retractedP, process_pgipP];
   12.23  
   12.24  end;
   12.25