summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 10 Jan 2001 20:18:55 +0100 | |

changeset 10858 | 479dad7b3b41 |

parent 10857 | 47b1f34ddd09 |

child 10859 | b88ce3ed3b1d |

tuned;

--- a/NEWS Wed Jan 10 17:21:31 2001 +0100 +++ b/NEWS Wed Jan 10 20:18:55 2001 +0100 @@ -1,22 +1,21 @@ + Isabelle NEWS -- history user-relevant changes ============================================== *** Overview of INCOMPATIBILITIES *** * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" -function; +operation; * HOL: induct renamed to lfp_induct; * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; -* HOL: infix "dvd" now has priority 50 rather than 70 - (because it is a relation) - infix ^^ has been renamed `` - infix `` has been renamed ` - "univalent" has been renamed "single_valued" +* HOL: infix "dvd" now has priority 50 rather than 70 (because it is a +relation); infix "^^" has been renamed "``"; infix "``" has been +renamed "`"; "univalent" has been renamed "single_valued"; -* HOLCF: infix ` has been renamed $ +* HOLCF: infix "`" has been renamed "$"; * Isar: 'obtain' no longer declares "that" fact as simp/intro; @@ -31,9 +30,18 @@ (should now use \isamath{...} and \isatext{...} in custom symbol definitions); +* \isabellestyle{NAME} selects version of Isabelle output (currently +available: are "it" for near math-mode best-style output, "sl" for +slanted text style, and "tt" for plain type-writer; if no +\isabellestyle command is given, output is according to slanted +type-writer); + * support sub/super scripts (for single symbols only), input syntax is like this: "A\<^sup>*" or "A\<^sup>\<star>"; +* some more standard symbols; see Appendix A of the system manual for +the complete list; + * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals state; Note that presentation of goal states does not conform to actual human-readable proof documents. Please do not include goal @@ -62,6 +70,12 @@ * Pure: ?thesis / ?this / "..." now work for pure meta-level statements as well; +* Pure: the builtin notion of 'finished' goal now includes the ==-refl +rule (as well as the assumption rule); + +* Pure: 'thm_deps' command visualizes dependencies of theorems and +lemmas, using the graph browser tool; + * HOL: improved method 'induct' --- now handles non-atomic goals (potential INCOMPATIBILITY); tuned error handling; @@ -69,6 +83,10 @@ number of facts to be consumed (0 for "type" and 1 for "set" rules); any remaining facts are inserted into the goal verbatim; +* HOL: local contexts (aka cases) may now contain term bindings as +well; the 'cases' and 'induct' methods new provide a ?case binding for +the result to be shown in each case; + * HOL: added 'recdef_tc' command; @@ -92,6 +110,7 @@ * HOL-Real, HOL-Hyperreals: improved arithmetic simplification; + *** CTT *** * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that

--- a/doc-src/IsarRef/generic.tex Wed Jan 10 17:21:31 2001 +0100 +++ b/doc-src/IsarRef/generic.tex Wed Jan 10 20:18:55 2001 +0100 @@ -43,7 +43,10 @@ classes involved. After finishing the proof, the theory will be augmented by a type signature declaration corresponding to the resulting theorem. \item [$intro_classes$] repeatedly expands all class introduction rules of - this theory. + this theory. Note that this method usually needs not be named explicitly, + as it is already included in the default proof step (of $\PROOFNAME$, + $\BYNAME$, etc.). In particular, instantiation of trivial (syntactic) + classes may be performed by a single ``$\DDOT$'' proof step. \end{descr} @@ -737,10 +740,7 @@ \begin{descr} \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} in \cite[\S11]{isabelle-ref}). The optional argument specifies a - user-supplied search bound (default 20). Note that $blast$ is the only - classical proof procedure in Isabelle that can handle actual object-logic - rules as local assumptions ($fast$ etc.\ would just ignore non-atomic - facts). + user-supplied search bound (default 20). \item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac}, \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in

--- a/doc-src/IsarRef/isar-ref.tex Wed Jan 10 17:21:31 2001 +0100 +++ b/doc-src/IsarRef/isar-ref.tex Wed Jan 10 20:18:55 2001 +0100 @@ -47,6 +47,7 @@ \newcommand{\edrv}{\mathop{\drv}\nolimits} \newcommand{\Or}{\mathrel{\;|\;}} +\renewcommand{\vec}[1]{\overline{#1}} \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

--- a/doc-src/IsarRef/pure.tex Wed Jan 10 17:21:31 2001 +0100 +++ b/doc-src/IsarRef/pure.tex Wed Jan 10 20:18:55 2001 +0100 @@ -418,7 +418,7 @@ \item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML commands from $text$. The theory context is passed in the same way as for - $\isarkeyword{use}$, but may not be changed. Note that + $\isarkeyword{use}$, but may not be changed. Note that the output of $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$. \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The @@ -543,7 +543,7 @@ \item [$proof(prove)$] means that a new goal has just been stated that is now to be \emph{proven}; the next command may refine it by some proof method, and enter a sub-proof to establish the actual result. -\item [$proof(state)$] is like an internal theory mode: the context may be +\item [$proof(state)$] is like a nested theory mode: the context may be augmented by \emph{stating} additional assumptions, intermediate results etc. \item [$proof(chain)$] is intermediate between $proof(state)$ and @@ -693,7 +693,7 @@ of facts in automated proof search. \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is equivalent to $\FROM{this}$. -\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward +\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward chaining is from earlier facts together with the current ones. \end{descr} @@ -1187,7 +1187,8 @@ \subsection{Diagnostics} -\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} +\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term} +\indexisarcmd{prop}\indexisarcmd{typ} \begin{matharray}{rcl} \isarcmd{pr}^* & : & \isarkeep{\cdot} \\ \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\ @@ -1252,18 +1253,36 @@ \indexisarcmd{print-facts}\indexisarcmd{print-binds} \indexisarcmd{print-commands}\indexisarcmd{print-syntax} \indexisarcmd{print-methods}\indexisarcmd{print-attributes} +\indexisarcmd{thms-containing}\indexisarcmd{thm-deps} +\indexisarcmd{print-theorems} \begin{matharray}{rcl} \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\ \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\ \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\ \isarcmd{print_facts}^* & : & \isarkeep{proof} \\ \isarcmd{print_binds}^* & : & \isarkeep{proof} \\ \end{matharray} -These commands print parts of the theory and proof context. Note that there -are some further ones available, such as for the set of rules declared for -simplifications. +\railalias{thmscontaining}{thms\_containing} +\railterm{thmscontaining} + +\railalias{thmdeps}{thm\_deps} +\railterm{thmdeps} + +\begin{rail} + thmscontaining (name * ) + ; + thmdeps thmrefs + ; +\end{rail} + +These commands print certain parts of the theory and proof context. Note that +there are some further ones available, such as for the set of rules declared +for simplifications. \begin{descr} \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, @@ -1272,10 +1291,20 @@ terms, depending on the current context. The output can be very verbose, including grammar tables and syntax translation rules. See \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's inner syntax. -\item [$\isarkeyword{print_methods}$] all proof methods available in the - current theory context. -\item [$\isarkeyword{print_attributes}$] all attributes available in the - current theory context. +\item [$\isarkeyword{print_methods}$] prints all proof methods available in + the current theory context. +\item [$\isarkeyword{print_attributes}$] prints all attributes available in + the current theory context. +\item [$\isarkeyword{print_theorems}$] prints theorems available in the + current theory context. In interactive mode this actually refers to the + theorems left by the last transaction; this allows to inspect the result of + advanced definitional packages, such as $\isarkeyword{datatype}$. +\item [$\isarkeyword{thms_containing}~\vec c$] retrieves theorems from the + theory context containing all of the constants $\vec c$. Note that giving + the empty list yields \emph{all} theorems of the current theory. +\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems + and lemmas, using Isabelle's graph browser tool (see also + \cite{isabelle-sys}). \item [$\isarkeyword{print_facts}$] prints any named facts of the current context, including assumptions and local results. \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in @@ -1295,7 +1324,7 @@ The Isabelle/Isar top-level maintains a two-stage history, for theory and proof state transformation. Basically, any command can be undone using $\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be -revoked via $\isarkeyword{redo}$, unless the corresponding the +revoked via $\isarkeyword{redo}$, unless the corresponding $\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The $\isarkeyword{kill}$ command aborts the current history node altogether, discontinuing a proof or even the whole theory. This operation is \emph{not}

--- a/doc-src/IsarRef/syntax.tex Wed Jan 10 17:21:31 2001 +0100 +++ b/doc-src/IsarRef/syntax.tex Wed Jan 10 20:18:55 2001 +0100 @@ -29,7 +29,7 @@ ``\texttt{;}'' (semicolon) to separate commands explicitly. This may be particularly useful in interactive shell sessions to make clear where the current command is intended to end. Otherwise, the interactive loop will -continue until end-of-command in clearly indicated from the input syntax, +continue until end-of-command is clearly indicated from the input syntax, e.g.\ encounter of the next command keyword. Advanced interfaces such as Proof~General \cite{proofgeneral} do not require