# HG changeset patch # User blanchet # Date 1259055201 -3600 # Node ID 6cc01403f78ac37e37ec71a78b86796ae5327258 # Parent 8dfc55999130b016d8a54709c656f0d552976085# Parent e5e7faaed7adbfe8c44b90d996e6f883c3c6c26a merge diff -r 8dfc55999130 -r 6cc01403f78a ANNOUNCE --- a/ANNOUNCE Tue Nov 24 10:33:02 2009 +0100 +++ b/ANNOUNCE Tue Nov 24 10:33:21 2009 +0100 @@ -7,7 +7,34 @@ file in the distribution for more details. Some important changes are: -* FIXME +* Isabelle tool "wwwfind" provides web interface for 'find_theorems' +on a given logic image. + +* HOL-SMT: proof method "smt" for a combination of first-order logic +with equality, linear and nonlinear (natural/integer/real) arithmetic, +and fixed-size bitvectors. + +* HOL-Boogie: an interactive prover back-end for Boogie and VCC. + +* HOL: Counterexample generator tool Nitpick based on the Kodkod +relational model finder. + +* HOL: predicate compiler turning inductive into (executable) +equational specifications. + +* HOL: refined number theory. + +* HOL: various parts of multivariate analysis. + +* HOLCF: new definitional domain package. + +* Revised tutorial on locales. + +* Support for Poly/ML 5.3.0, with improved reporting of compiler +errors and run-time exceptions, including detailed source positions. + +* Parallel checking of nested Isar proofs, with improved scalability +up to 8 cores. You may get Isabelle2009-1 from the following mirror sites: diff -r 8dfc55999130 -r 6cc01403f78a Admin/E/README --- a/Admin/E/README Tue Nov 24 10:33:02 2009 +0100 +++ b/Admin/E/README Tue Nov 24 10:33:21 2009 +0100 @@ -1,4 +1,3 @@ - This distribution of E 1.0-004 has been compiled according to the README included in the official version from http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html @@ -8,23 +7,12 @@ $ ./configure $ make -The resulting PROVER/eproof executable has been changed to be -relocatable: - - $ diff eproof-orig eproof - 1c1 - < #!/bin/bash -f - --- - > #!/usr/bin/env bash - 3c3,4 - < EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER - --- - > set -o noglob - > EXECPATH="$(cd "$(dirname "$0")"; pwd)" +The PROVER/eproof executable has been replaced by a version written in +perl (by Sascha Boehme). Now the main executables in PROVER/ are moved to the platform-specific target directory (E/x86-linux etc.). - Makarius - 07-Apr-2009 + Makarius + 23-Nov-2009 diff -r 8dfc55999130 -r 6cc01403f78a INSTALL --- a/INSTALL Tue Nov 24 10:33:02 2009 +0100 +++ b/INSTALL Tue Nov 24 10:33:21 2009 +0100 @@ -17,7 +17,7 @@ site installation of Isabelle on Linux/x86 works like this: tar -C /usr/local -xzf Isabelle.tar.gz - tar -C /usr/local -xzf polyml_x86-linux.tar.gz + tar -C /usr/local -xzf polyml.tar.gz tar -C /usr/local -xzf HOL_x86-linux.tar.gz The install prefix given above may be changed as appropriate; there is diff -r 8dfc55999130 -r 6cc01403f78a NEWS --- a/NEWS Tue Nov 24 10:33:02 2009 +0100 +++ b/NEWS Tue Nov 24 10:33:21 2009 +0100 @@ -114,19 +114,17 @@ fixpoint theorem. * Reorganization of number theory, INCOMPATIBILITY: - - new number theory development for nat and int, in - theories Divides and GCD as well as in new session - Number_Theory - - some constants and facts now suffixed with _nat and - _int accordingly - - former session NumberTheory now named Old_Number_Theory, - including theories Legacy_GCD and Primes (prefer Number_Theory - if possible) + - new number theory development for nat and int, in theories Divides + and GCD as well as in new session Number_Theory + - some constants and facts now suffixed with _nat and _int + accordingly + - former session NumberTheory now named Old_Number_Theory, including + theories Legacy_GCD and Primes (prefer Number_Theory if possible) - moved theory Pocklington from src/HOL/Library to src/HOL/Old_Number_Theory -* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm -of finite and infinite sets. It is shown that they form a complete +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and +lcm of finite and infinite sets. It is shown that they form a complete lattice. * Class semiring_div requires superclass no_zero_divisors and proof of @@ -198,8 +196,6 @@ abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. INCOMPATIBILITY. --- - * Most rules produced by inductive and datatype package have mandatory prefixes. INCOMPATIBILITY. @@ -208,8 +204,9 @@ DERIV_intros assumes composition with an additional function and matches a variable to the derivative, which has to be solved by the Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative -of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac -should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY. +of most elementary terms. Former Maclauren.DERIV_tac and +Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros). +INCOMPATIBILITY. * Code generator attributes follow the usual underscore convention: code_unfold replaces code unfold @@ -274,7 +271,8 @@ * The 'fixrec' package now supports "bottom patterns". Bottom patterns can be used to generate strictness rules, or to make functions more strict (much like the bang-patterns supported by the -Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for examples. +Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for +examples. *** ML *** diff -r 8dfc55999130 -r 6cc01403f78a doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Tue Nov 24 10:33:02 2009 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Tue Nov 24 10:33:21 2009 +0100 @@ -456,13 +456,10 @@ \secref{sec:object-logic}). Separate introduction rules @{text loc_axioms.intro} and @{text loc.intro} are provided as well. - \item @{command "print_locale"}~@{text "import + body"} prints the - specified locale expression in a flattened form. The notable - special case @{command "print_locale"}~@{text loc} just prints the - contents of the named locale, but keep in mind that type-inference - will normalize type variables according to the usual alphabetical - order. The command omits @{element "notes"} elements by default. - Use @{command "print_locale"}@{text "!"} to get them included. + \item @{command "print_locale"}~@{text "locale"} prints the + contents of the named locale. The command omits @{element "notes"} + elements by default. Use @{command "print_locale"}@{text "!"} to + have them included. \item @{command "print_locales"} prints the names of all locales of the current theory. @@ -537,7 +534,7 @@ qualifier, although only for fragments of @{text expr} that are not interpreted in the theory already. - \item @{command "interpretation"}~@{text "expr insts \ eqns"} + \item @{command "interpretation"}~@{text "expr \ eqns"} interprets @{text expr} in the theory. The command generates proof obligations for the instantiated specifications (assumes and defines elements). Once these are discharged by the user, instantiated @@ -563,19 +560,24 @@ interpretations dynamically participate in any facts added to locales. - \item @{command "interpret"}~@{text "expr insts"} + \item @{command "interpret"}~@{text "expr"} interprets @{text expr} in the proof context and is otherwise similar to interpretation in theories. + \item @{command "print_interps"}~@{text "locale"} lists all + interpretations of @{text "locale"} in the current theory, including + those due to a combination of an @{command "interpretation"} and + one or several @{command "sublocale"} declarations. + \end{description} \begin{warn} Since attributes are applied to interpreted theorems, interpretation may modify the context of common proof tools, e.g.\ - the Simplifier or Classical Reasoner. Since the behavior of such - automated reasoning tools is \emph{not} stable under - interpretation morphisms, manual declarations might have to be - added to revert such declarations. + the Simplifier or Classical Reasoner. As the behavior of such + tools is \emph{not} stable under interpretation morphisms, manual + declarations might have to be added to the target context of the + interpretation to revert such declarations. \end{warn} \begin{warn} diff -r 8dfc55999130 -r 6cc01403f78a doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 24 10:33:02 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 24 10:33:21 2009 +0100 @@ -478,13 +478,10 @@ \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well. - \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the - specified locale expression in a flattened form. The notable - special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the - contents of the named locale, but keep in mind that type-inference - will normalize type variables according to the usual alphabetical - order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default. - Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included. + \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the + contents of the named locale. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} + elements by default. Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to + have them included. \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales of the current theory. @@ -559,7 +556,7 @@ qualifier, although only for fragments of \isa{expr} that are not interpreted in the theory already. - \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}} + \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}} interprets \isa{expr} in the theory. The command generates proof obligations for the instantiated specifications (assumes and defines elements). Once these are discharged by the user, instantiated @@ -585,19 +582,24 @@ interpretations dynamically participate in any facts added to locales. - \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}} + \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}} interprets \isa{expr} in the proof context and is otherwise similar to interpretation in theories. + \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all + interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including + those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and + one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations. + \end{description} \begin{warn} Since attributes are applied to interpreted theorems, interpretation may modify the context of common proof tools, e.g.\ - the Simplifier or Classical Reasoner. Since the behavior of such - automated reasoning tools is \emph{not} stable under - interpretation morphisms, manual declarations might have to be - added to revert such declarations. + the Simplifier or Classical Reasoner. As the behavior of such + tools is \emph{not} stable under interpretation morphisms, manual + declarations might have to be added to the target context of the + interpretation to revert such declarations. \end{warn} \begin{warn} diff -r 8dfc55999130 -r 6cc01403f78a doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Tue Nov 24 10:33:02 2009 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Tue Nov 24 10:33:21 2009 +0100 @@ -591,7 +591,7 @@ ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ \textit{instance} & ::= & [ \textit{qualifier} ``\textbf{:}'' ] - \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ + \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ \textit{expression} & ::= & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] @@ -625,8 +625,8 @@ \textit{toplevel} & ::= & \textbf{print\_locales} \\ - & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ - & | & \textbf{print\_interps} \textit{locale} + & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\ + & | & \textbf{print\_interps} \textit{name} \end{tabular} \end{center} \hrule diff -r 8dfc55999130 -r 6cc01403f78a doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Tue Nov 24 10:33:02 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Tue Nov 24 10:33:21 2009 +0100 @@ -882,7 +882,7 @@ ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ \textit{instance} & ::= & [ \textit{qualifier} ``\textbf{:}'' ] - \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ + \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ \textit{expression} & ::= & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] @@ -916,8 +916,8 @@ \textit{toplevel} & ::= & \textbf{print\_locales} \\ - & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ - & | & \textbf{print\_interps} \textit{locale} + & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\ + & | & \textbf{print\_interps} \textit{name} \end{tabular} \end{center} \hrule diff -r 8dfc55999130 -r 6cc01403f78a etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Tue Nov 24 10:33:02 2009 +0100 +++ b/etc/isar-keywords-ZF.el Tue Nov 24 10:33:21 2009 +0100 @@ -19,6 +19,7 @@ "ProofGeneral\\.inform_file_processed" "ProofGeneral\\.inform_file_retracted" "ProofGeneral\\.kill_proof" + "ProofGeneral\\.pr" "ProofGeneral\\.process_pgip" "ProofGeneral\\.restart" "ProofGeneral\\.undo" @@ -271,6 +272,7 @@ (defconst isar-keywords-diag '("ML_command" "ML_val" + "ProofGeneral\\.pr" "cd" "class_deps" "commit" diff -r 8dfc55999130 -r 6cc01403f78a etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Nov 24 10:33:02 2009 +0100 +++ b/etc/isar-keywords.el Tue Nov 24 10:33:21 2009 +0100 @@ -19,6 +19,7 @@ "ProofGeneral\\.inform_file_processed" "ProofGeneral\\.inform_file_retracted" "ProofGeneral\\.kill_proof" + "ProofGeneral\\.pr" "ProofGeneral\\.process_pgip" "ProofGeneral\\.restart" "ProofGeneral\\.undo" @@ -345,6 +346,7 @@ (defconst isar-keywords-diag '("ML_command" "ML_val" + "ProofGeneral\\.pr" "atp_info" "atp_kill" "atp_messages" diff -r 8dfc55999130 -r 6cc01403f78a src/HOL/Library/Transitive_Closure_Table.thy --- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Nov 24 10:33:02 2009 +0100 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Nov 24 10:33:21 2009 +0100 @@ -185,7 +185,7 @@ by (auto simp add: rtranclp_eq_rtrancl_path) qed -declare rtranclp_eq_rtrancl_tab_nil [code_unfold] +declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del] declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] @@ -224,7 +224,11 @@ values "{x. test\<^sup>*\<^sup>* A x}" values "{x. test\<^sup>*\<^sup>* x C}" -hide const test +value "test\<^sup>*\<^sup>* A C" +value "test\<^sup>*\<^sup>* C A" + +hide type ty +hide const test A B C end diff -r 8dfc55999130 -r 6cc01403f78a src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 24 10:33:02 2009 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 24 10:33:21 2009 +0100 @@ -190,6 +190,12 @@ local structure P = OuterParse and K = OuterKeyword in +fun prP () = + OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => + if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals () + else (Toplevel.quiet := false; Toplevel.print_state true state)))); + fun undoP () = (*undo without output -- historical*) OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1))); @@ -219,7 +225,8 @@ (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt)))); fun init_outer_syntax () = List.app (fn f => f ()) - [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP]; + [prP, undoP, restartP, kill_proofP, inform_file_processedP, + inform_file_retractedP, process_pgipP]; end;