# HG changeset patch # User wenzelm # Date 1277134917 -7200 # Node ID b7821e89fb7902a8c34e4c4af67864c9760ea0aa # Parent 4de0b0c38bdfa1fb6f0ebd3fcb45f94c305776e7# Parent 7807c6b37bf494f412a80ee257232206af61ae44 merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy; diff -r 4de0b0c38bdf -r b7821e89fb79 .hgtags --- a/.hgtags Mon Jun 21 16:59:37 2010 +0200 +++ b/.hgtags Mon Jun 21 17:41:57 2010 +0200 @@ -25,5 +25,4 @@ fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1 -935c75359742ccfd4abba0c33a440241e6ef2b1e isa2009-2-test0 -d1cdbc7524b619815236e8e2e61e36809ee2d338 isa2009-2-test1 +35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2 diff -r 4de0b0c38bdf -r b7821e89fb79 Admin/CHECKLIST --- a/Admin/CHECKLIST Mon Jun 21 16:59:37 2010 +0200 +++ b/Admin/CHECKLIST Mon Jun 21 17:41:57 2010 +0200 @@ -15,7 +15,7 @@ - Admin/update-keywords; -- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS; +- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS; - diff NEWS wrt. last official release, which is read-only; diff -r 4de0b0c38bdf -r b7821e89fb79 Admin/makebundle --- a/Admin/makebundle Mon Jun 21 16:59:37 2010 +0200 +++ b/Admin/makebundle Mon Jun 21 17:41:57 2010 +0200 @@ -66,7 +66,7 @@ HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" [ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE" echo "heaps" -tar -C "$ISABELLE_HOME" -x -z -f "$HEAPS_ARCHIVE" +tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE" BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz" diff -r 4de0b0c38bdf -r b7821e89fb79 Admin/makedist --- a/Admin/makedist Mon Jun 21 16:59:37 2010 +0200 +++ b/Admin/makedist Mon Jun 21 17:41:57 2010 +0200 @@ -4,7 +4,7 @@ ## global settings -REPOS_NAME="isabelle" +REPOS_NAME="isabelle-release" REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}" DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} @@ -145,6 +145,11 @@ rm -rf doc-src mkdir -p contrib +cat >contrib/README < (nat * nat) => bool" + intrel :: "(nat * nat) => (nat * nat) => bool" where "intrel (x, y) (u, v) = (x + v = u + y)" - quotient_type int = "nat × nat" / intrel + quotient_type int = "nat * nat" / intrel by (auto simp add: equivp_def expand_fun_eq) - + quotient_definition "0::int" is "(0::nat, 0::nat)" @@ -292,6 +292,8 @@ * Theory PReal, including the type "preal" and related operations, has been removed. INCOMPATIBILITY. +* Real: new development using Cauchy Sequences. + * Split off theory "Big_Operators" containing setsum, setprod, Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. @@ -511,6 +513,17 @@ "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. - Removed "nitpick_intro" attribute. INCOMPATIBILITY. +* Method "induct" now takes instantiations of the form t, where t is not + a variable, as a shorthand for "x == t", where x is a fresh variable. + If this is not intended, t has to be enclosed in parentheses. + By default, the equalities generated by definitional instantiations + are pre-simplified, which may cause parameters of inductive cases + to disappear, or may even delete some of the inductive cases. + Use "induct (no_simp)" instead of "induct" to restore the old + behaviour. The (no_simp) option is also understood by the "cases" + and "nominal_induct" methods, which now perform pre-simplification, too. + INCOMPATIBILITY. + *** HOLCF *** @@ -683,6 +696,13 @@ See src/Tools/jEdit or "isabelle jedit" provided by the properly built component. +* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono +and Bluesky TeX fonts. It provides the usual Isabelle symbols, +similar to the default assignment of the document preparation system +(cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System +provides some operations for direct access to the font without asking +the user for manual installation. + New in Isabelle2009-1 (December 2009) @@ -3410,8 +3430,6 @@ * Real: proper support for ML code generation, including 'quickcheck'. Reals are implemented as arbitrary precision rationals. -* Real: new development using Cauchy Sequences. - * Hyperreal: Several constants that previously worked only for the reals have been generalized, so they now work over arbitrary vector spaces. Type annotations may need to be added in some cases; potential diff -r 4de0b0c38bdf -r b7821e89fb79 README --- a/README Mon Jun 21 16:59:37 2010 +0200 +++ b/README Mon Jun 21 17:41:57 2010 +0200 @@ -21,10 +21,9 @@ Installation - Binary packages are available for Isabelle/HOL etc. for several - platforms from the Isabelle web page. The system may be also built - from scratch, using the tar.gz source distribution. See file - INSTALL as distributed with Isabelle for more information. + Completely integrated bundles including the full Isabelle sources, + documentation, add-on tools and precompiled logic images for + several platforms are available from the Isabelle web page. Further background information may be found in the Isabelle System Manual, distributed with the sources (directory doc). diff -r 4de0b0c38bdf -r b7821e89fb79 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 21 16:59:37 2010 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 21 17:41:57 2010 +0200 @@ -1277,16 +1277,16 @@ ``strengthened'' inductive statements within the object-logic. \begin{rail} - 'cases' (insts * 'and') rule? + 'cases' '(no_simp)'? (insts * 'and') rule? ; - 'induct' (definsts * 'and') \\ arbitrary? taking? rule? + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule? ; 'coinduct' insts taking rule? ; rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) ; - definst: name ('==' | equiv) term | inst + definst: name ('==' | equiv) term | '(' term ')' | inst ; definsts: ( definst *) ; @@ -1320,7 +1320,9 @@ of premises of the case rule; within each premise, the \emph{prefix} of variables is instantiated. In most situations, only a single term needs to be specified; this refers to the first variable of the - last premise (it is usually the same for all cases). + last premise (it is usually the same for all cases). The @{text + "(no_simp)"} option can be used to disable pre-simplification of + cases (see the description of @{method induct} below for details). \item @{method induct}~@{text "insts R"} is analogous to the @{method cases} method, but refers to induction rules, which are @@ -1342,15 +1344,28 @@ present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example. - + Instantiations may be definitional: equations @{text "x \ t"} introduce local definitions, which are inserted into the claim and discharged after applying the induction rule. Equalities reappear in the inductive cases, but have been transformed according to the induction principle being involved here. In order to achieve practically useful induction hypotheses, some variables occurring in - @{text t} need to be fixed (see below). - + @{text t} need to be fixed (see below). Instantiations of the form + @{text t}, where @{text t} is not a variable, are taken as a + shorthand for \mbox{@{text "x \ t"}}, where @{text x} is a fresh + variable. If this is not intended, @{text t} has to be enclosed in + parentheses. By default, the equalities generated by definitional + instantiations are pre-simplified using a specific set of rules, + usually consisting of distinctness and injectivity theorems for + datatypes. This pre-simplification may cause some of the parameters + of an inductive case to disappear, or may even completely delete + some of the inductive cases, if one of the equalities occurring in + their premises can be simplified to @{text False}. The @{text + "(no_simp)"} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the @{attribute_def induct_simp} attribute. + The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' specification generalizes variables @{text "x\<^sub>1, \, x\<^sub>m"} of the original goal before applying induction. Thus diff -r 4de0b0c38bdf -r b7821e89fb79 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 21 16:59:37 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 21 17:41:57 2010 +0200 @@ -1275,16 +1275,16 @@ ``strengthened'' inductive statements within the object-logic. \begin{rail} - 'cases' (insts * 'and') rule? + 'cases' '(no_simp)'? (insts * 'and') rule? ; - 'induct' (definsts * 'and') \\ arbitrary? taking? rule? + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule? ; 'coinduct' insts taking rule? ; rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) ; - definst: name ('==' | equiv) term | inst + definst: name ('==' | equiv) term | '(' term ')' | inst ; definsts: ( definst *) ; @@ -1317,7 +1317,8 @@ of premises of the case rule; within each premise, the \emph{prefix} of variables is instantiated. In most situations, only a single term needs to be specified; this refers to the first variable of the - last premise (it is usually the same for all cases). + last premise (it is usually the same for all cases). The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of + cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details). \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are @@ -1339,15 +1340,27 @@ present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example. - + Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} introduce local definitions, which are inserted into the claim and discharged after applying the induction rule. Equalities reappear in the inductive cases, but have been transformed according to the induction principle being involved here. In order to achieve practically useful induction hypotheses, some variables occurring in - \isa{t} need to be fixed (see below). - + \isa{t} need to be fixed (see below). Instantiations of the form + \isa{t}, where \isa{t} is not a variable, are taken as a + shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh + variable. If this is not intended, \isa{t} has to be enclosed in + parentheses. By default, the equalities generated by definitional + instantiations are pre-simplified using a specific set of rules, + usually consisting of distinctness and injectivity theorems for + datatypes. This pre-simplification may cause some of the parameters + of an inductive case to disappear, or may even completely delete + some of the inductive cases, if one of the equalities occurring in + their premises can be simplified to \isa{False}. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute. + The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}'' specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus induction hypotheses may become sufficiently general to get the diff -r 4de0b0c38bdf -r b7821e89fb79 doc-src/Ref/introduction.tex --- a/doc-src/Ref/introduction.tex Mon Jun 21 16:59:37 2010 +0200 +++ b/doc-src/Ref/introduction.tex Mon Jun 21 17:41:57 2010 +0200 @@ -5,9 +5,7 @@ \index{starting up|bold}\nobreak % We assume that your local Isabelle administrator (this might be you!) has -already installed the Isabelle system together with appropriate object-logics ---- otherwise see the \texttt{README} and \texttt{INSTALL} files in the -top-level directory of the distribution on how to do this. +already installed the Isabelle system together with appropriate object-logics. \medskip Let $\langle isabellehome \rangle$ denote the location where the distribution has been installed. To run Isabelle from a the shell diff -r 4de0b0c38bdf -r b7821e89fb79 src/HOL/Nominal/Examples/CK_Machine.thy --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 21 16:59:37 2010 +0200 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 21 17:41:57 2010 +0200 @@ -491,11 +491,11 @@ and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b -proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) +proof (nominal_induct "\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_VAR y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) diff -r 4de0b0c38bdf -r b7821e89fb79 src/HOL/Nominal/Examples/Type_Preservation.thy --- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 21 16:59:37 2010 +0200 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 21 17:41:57 2010 +0200 @@ -141,11 +141,11 @@ and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b -proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) +proof (nominal_induct "\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_Var y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) diff -r 4de0b0c38bdf -r b7821e89fb79 src/HOL/Nominal/INSTALL --- a/src/HOL/Nominal/INSTALL Mon Jun 21 16:59:37 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ - -Installation Notes for the Nominal Datatype Package -=================================================== - -Although the nominal datatype package is an official -package in the development snapshot of Isabelle, we -keep a semi-official snapshot of Isabelle and Nominal -under - - http://isabelle.in.tum.de/nominal/ - -This snapshot contains the latest stable release of the -nominal datatype package. - -To install it, follow the instructions of Isabelle's INSTALL -about how a snap-shot can be set up. The building process -needs to be started inside the [ISABELLE_HOME] directory with -the command: - - ./build -m HOL-Nominal - -After the build completes, install the files with the command - - ./bin/isabelle install -p /usr/local/bin - -where /usr/local/bin needs to be replaced by an appropriate -directory, if you are not root on the system. - -The sources of the nominal datatype package can be found -in the directory - - [ISABELLE_HOME]/src/HOL/Nominal - -The examples are in - - [ISABELLE_HOME]/src/HOL/Nominal/Examples - -Starting Isabelle with the Nominal Datatype Package Preloaded -============================================================= - -Isabelle and the Proof-General interface can be started -with - - Isabelle -L HOL-Nominal <> & - -on the command-line. This automatically loads the correct -keyword file needed for the nominal datatype package. - -Problems with starting Isabelle and Proof-General usually -come from old versions of Proof-General. So make sure you -have installed at least the version ProofGeneral-3.6pre050930. - -If you have problems or comments about the installation process, -please make use of the nominal mailing list at - -https://mailmanbroy.informatik.tu-muenchen.de/pipermail/nominal-isabelle/ - diff -r 4de0b0c38bdf -r b7821e89fb79 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Mon Jun 21 16:59:37 2010 +0200 +++ b/src/Pure/General/pretty.scala Mon Jun 21 17:41:57 2010 +0200 @@ -134,7 +134,7 @@ def string_of(input: List[XML.Tree], margin: Int = margin_default, metric: String => Double = metric_default): String = - formatted(input).iterator.flatMap(XML.content).mkString + formatted(input, margin, metric).iterator.flatMap(XML.content).mkString /* unformatted output */ diff -r 4de0b0c38bdf -r b7821e89fb79 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Mon Jun 21 16:59:37 2010 +0200 +++ b/src/Pure/Isar/runtime.ML Mon Jun 21 17:41:57 2010 +0200 @@ -54,6 +54,7 @@ val detailed = ! Output.debugging; fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn + | exn_msg _ (Exn.EXCEPTIONS []) = "Exception." | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) diff -r 4de0b0c38bdf -r b7821e89fb79 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Jun 21 16:59:37 2010 +0200 +++ b/src/Pure/PIDE/command.scala Mon Jun 21 17:41:57 2010 +0200 @@ -48,8 +48,7 @@ def name: String = if (is_command) span.head.content else "" override def toString = - if (is_command) name + "(" + id + ")" - else if (is_ignored) "" else "" + id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") /* source text */ diff -r 4de0b0c38bdf -r b7821e89fb79 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Jun 21 16:59:37 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Jun 21 17:41:57 2010 +0200 @@ -12,6 +12,7 @@ BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, File, IOException} import java.awt.{GraphicsEnvironment, Font} +import java.awt.font.TextAttribute import scala.io.Source import scala.util.matching.Regex @@ -336,31 +337,23 @@ /* fonts */ val font_family = getenv_strict("ISABELLE_FONT_FAMILY") + val font_family_default = "IsabelleText" def get_font(size: Int = 1, bold: Boolean = false): Font = new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size) + def create_default_font(bold: Boolean = false): Font = + if (bold) + Font.createFont(Font.TRUETYPE_FONT, + platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf")) + else + Font.createFont(Font.TRUETYPE_FONT, + platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf")) + def install_fonts() { - def create_font(bold: Boolean): Font = - { - val name = - if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf" - else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf" - Font.createFont(Font.TRUETYPE_FONT, platform_file(name)) - } - def check_font() = get_font().getFamily == font_family - - if (!check_font()) { - val font = create_font(false) - val bold_font = create_font(true) - - val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() - ge.registerFont(font) - // workaround strange problem with Apple's Java 1.6 font manager - // FIXME does not quite work!? - if (bold_font.getFamily == font_family) ge.registerFont(bold_font) - if (!check_font()) error("Failed to install IsabelleText fonts") - } + val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() + ge.registerFont(create_default_font(bold = false)) + ge.registerFont(create_default_font(bold = true)) } } diff -r 4de0b0c38bdf -r b7821e89fb79 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 21 16:59:37 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 21 17:41:57 2010 +0200 @@ -155,9 +155,11 @@ def to: Int => Int = model.to_current(document, _) def from: Int => Int = model.from_current(document, _) + /* FIXME for (text_area <- Isabelle.jedit_text_areas(model.buffer) if Document_View(text_area).isDefined) Document_View(text_area).get.set_styles() + */ def handle_token(style: Byte, offset: Int, length: Int) = handler.handleToken(line_segment, style, offset, length, context) diff -r 4de0b0c38bdf -r b7821e89fb79 src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 21 16:59:37 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 21 17:41:57 2010 +0200 @@ -129,19 +129,18 @@ reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } } tracing.selected = show_tracing - tracing.tooltip = - "Indicate output of tracing messages
(also needs to be enabled on the prover side)" + tracing.tooltip = "Indicate output of tracing messages" private val auto_update = new CheckBox("Auto update") { reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } } auto_update.selected = follow_caret - auto_update.tooltip = "Indicate automatic update following cursor movement" + auto_update.tooltip = "Indicate automatic update following cursor movement" private val update = new Button("Update") { reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } } - update.tooltip = "Update display according to the command at cursor position" + update.tooltip = "Update display according to the command at cursor position" val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) add(controls.peer, BorderLayout.NORTH)