# HG changeset patch # User huffman # Date 1316387563 25200 # Node ID 6e6e958b2d4034283c0021eace7c050b7150b4ec # Parent e7ac11643befb756fd660a084d229a7900a0fc93# Parent b36eedcd163302e1c9abc6b0b1b918ff9c916169 merged diff -r b36eedcd1633 -r 6e6e958b2d40 ANNOUNCE --- a/ANNOUNCE Thu Sep 15 10:12:36 2011 -0700 +++ b/ANNOUNCE Sun Sep 18 16:12:43 2011 -0700 @@ -3,10 +3,24 @@ Isabelle2011-1 is now available. -This version improves upon Isabelle2011, see the NEWS file in the -distribution for more details. Some important changes are: +This version significantly improves upon Isabelle2011, see the NEWS +file in the distribution for more details. Some notable changes are: + +* Significantly improved Isabelle/jEdit Prover IDE (PIDE). + +* Improved system integration with Isabelle/Scala: YXML data encoding. + +* Improved parallel performance and scalability. -* FIXME +* Improved document preparation: embedded rail-road diagrams. + +* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer, SMT/Z3 + integration. + +* Numerous HOL library improvements: main HOL, HOLCF, HOL-Library, + Multivariate_Analysis, Probability. + +* Updated and extended Isabelle/Isar reference manual. You may get Isabelle2011-1 from the following mirror sites: diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/MacOS/App1/script --- a/Admin/MacOS/App1/script Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/MacOS/App1/script Sun Sep 18 16:12:43 2011 -0700 @@ -104,7 +104,8 @@ ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1 RC=$? else - ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1 + rm -f "$OUTPUT" && touch "$OUTPUT" + "$ISABELLE_TOOL" jedit "$@" RC=$? fi diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/PLATFORMS --- a/Admin/PLATFORMS Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/PLATFORMS Sun Sep 18 16:12:43 2011 -0700 @@ -32,10 +32,14 @@ x86-linux Ubuntu 10.04 LTS x86-darwin Mac OS Leopard (macbroy30) + Mac OS Snow Leopard (macbroy2) + Mac OS Lion (macbroy6) x86-cygwin Cygwin 1.7 (vmbroy9) x86_64-linux Ubuntu 10.04 LTS x86_64-darwin Mac OS Leopard (macbroy30) + Mac OS Snow Leopard (macbroy2) + Mac OS Lion (macbroy6) All of the above platforms are 100% supported by Isabelle -- end-users should not have to care about the differences (at least in theory). diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/ProofGeneral/4.1/dif --- a/Admin/ProofGeneral/4.1/dif Thu Sep 15 10:12:36 2011 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -diff -r ProofGeneral-4.1pre101216/generic/proof-useropts.el ProofGeneral-4.1pre101216-p1/generic/proof-useropts.el -121c121 -< (defcustom proof-strict-read-only 'retract ---- -> (defcustom proof-strict-read-only t -345c345 -< (defcustom proof-full-annotation t ---- -> (defcustom proof-full-annotation nil -diff -r ProofGeneral-4.1pre101216/isar/interface ProofGeneral-4.1pre101216-p1/isar/interface -3,4d2 -< # interface,v 11.0 2010/10/10 22:57:07 da Exp -< # -23a22 -> echo " -f FONT specify Emacs font" -56a56 -> FONT="" -66c66 -< while getopts "L:U:g:k:l:m:p:u:w:x:" OPT ---- -> while getopts "L:U:f:g:k:l:m:p:u:w:x:" OPT -75a76,78 -> f) -> FONT="$OPTARG" -> ;; -135a139,143 -> if [ -n "$FONT" ]; then -> ARGS["${#ARGS[@]}"]="-fn" -> ARGS["${#ARGS[@]}"]="$FONT" -> fi -> -diff -r ProofGeneral-4.1pre101216/isar/interface-setup.el ProofGeneral-4.1pre101216-p1/isar/interface-setup.el -13a14,19 -> ;; Tool bar -> ;; -> -> (if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t)) -> -> ;; diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/ProofGeneral/4.1/interface --- a/Admin/ProofGeneral/4.1/interface Thu Sep 15 10:12:36 2011 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,203 +0,0 @@ -#!/usr/bin/env bash -# -# Proof General interface wrapper for Isabelle. - - -## self references - -THIS="$(cd "$(dirname "$0")"; pwd)" -SUPER="$(cd "$THIS/.."; pwd)" - - -## diagnostics - -usage() -{ - echo - echo "Usage: isabelle emacs [OPTIONS] [FILES ...]" - echo - echo " Options are:" - echo " -L NAME abbreviates -l NAME -k NAME" - echo " -U BOOL enable UTF-8 communication (default true)" - echo " -f FONT specify Emacs font" - echo " -g GEOMETRY specify Emacs geometry" - echo " -k NAME use specific isar-keywords for named logic" - echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)" - echo " -m MODE add print mode for output" - echo " -p NAME Emacs program name (default emacs)" - echo " -u BOOL use personal .emacs file (default true)" - echo " -w BOOL use window system (default true)" - echo " -x BOOL render Isabelle symbols via Unicode (default false)" - echo - echo "Starts Proof General for Isabelle with theory and proof FILES" - echo "(default Scratch.thy)." - echo - echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS" - echo - exit 1 -} - -fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -ISABELLE_OPTIONS="" - -KEYWORDS="" -LOGIC="$ISABELLE_LOGIC" -UNICODE="" -FONT="" -GEOMETRY="" -PROGNAME="emacs" -INITFILE="true" -WINDOWSYSTEM="true" -UNICODE_SYMBOLS="" - -getoptions() -{ - OPTIND=1 - while getopts "L:U:f:g:k:l:m:p:u:w:x:" OPT - do - case "$OPT" in - L) - KEYWORDS="$OPTARG" - LOGIC="$OPTARG" - ;; - U) - UNICODE="$OPTARG" - ;; - f) - FONT="$OPTARG" - ;; - g) - GEOMETRY="$OPTARG" - ;; - k) - KEYWORDS="$OPTARG" - ;; - l) - LOGIC="$OPTARG" - ;; - m) - if [ -z "$ISABELLE_OPTIONS" ]; then - ISABELLE_OPTIONS="-m $OPTARG" - else - ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG" - fi - ;; - p) - PROGNAME="$OPTARG" - ;; - u) - INITFILE="$OPTARG" - ;; - w) - WINDOWSYSTEM="$OPTARG" - ;; - x) - UNICODE_SYMBOLS="$OPTARG" - ;; - \?) - usage - ;; - esac - done -} - -eval "OPTIONS=($PROOFGENERAL_OPTIONS)" -getoptions "${OPTIONS[@]}" - -getoptions "$@" -shift $(($OPTIND - 1)) - - -# args - -declare -a FILES=() - -if [ "$#" -eq 0 ]; then - FILES["${#FILES[@]}"]="Scratch.thy" -else - while [ "$#" -gt 0 ]; do - FILES["${#FILES[@]}"]="$1" - shift - done -fi - - -## main - -declare -a ARGS=() - -if [ -n "$FONT" ]; then - ARGS["${#ARGS[@]}"]="-fn" - ARGS["${#ARGS[@]}"]="$FONT" -fi - -if [ -n "$GEOMETRY" ]; then - ARGS["${#ARGS[@]}"]="-geometry" - ARGS["${#ARGS[@]}"]="$GEOMETRY" -fi - -[ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" -[ "$WINDOWSYSTEM" = false ] && ARGS["${#ARGS[@]}"]="-nw" - -ARGS["${#ARGS[@]}"]="-l" -ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" - -if [ -n "$KEYWORDS" ]; then - if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" - else - fail "No isar-keywords file for '$KEYWORDS'" - fi -elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" -elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" -fi - -for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ - "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" -do - if [ -f "$FILE" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$FILE" - fi -done - -case "$LOGIC" in - /*) - ;; - */*) - LOGIC="$(pwd -P)/$LOGIC" - ;; -esac - -export PROOFGENERAL_HOME="$SUPER" -export PROOFGENERAL_ASSISTANTS="isar" -export PROOFGENERAL_LOGIC="$LOGIC" -export PROOFGENERAL_UNICODE="$UNICODE" -export PROOFGENERAL_UNICODE_SYMBOLS="$UNICODE_SYMBOLS" - -export ISABELLE_OPTIONS - -# Isabelle2008 compatibility -[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" -[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" - -exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" - diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/contributed_components --- a/Admin/contributed_components Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/contributed_components Sun Sep 18 16:12:43 2011 -0700 @@ -1,9 +1,9 @@ #contributed components contrib/cvc3-2.2 -contrib/e-1.2 +contrib/e-1.4 contrib/kodkodi-1.2.16 contrib/spass-3.7 contrib/scala-2.8.1.final contrib/vampire-1.0 contrib/yices-1.0.28 -contrib/z3-2.19 +contrib/z3-3.1 diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/isatest/isatest-makeall Sun Sep 18 16:12:43 2011 -0700 @@ -77,6 +77,11 @@ NICE="" ;; + macbroy6) + MFLAGS="-k" + NICE="" + ;; + macbroy22) MFLAGS="-k" NICE="" diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/isatest/isatest-makedist Sun Sep 18 16:12:43 2011 -0700 @@ -111,6 +111,8 @@ sleep 15 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly" sleep 15 +$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2" +sleep 15 $SSH macbroy30 "sleep 10800; $MAKEALL $HOME/settings/mac-poly-M2" sleep 15 $SSH atbroy102 "$MAKEALL $HOME/settings/cygwin-poly-e" diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/isatest/settings/at-sml-dev-e --- a/Admin/isatest/settings/at-sml-dev-e Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/isatest/settings/at-sml-dev-e Sun Sep 18 16:12:43 2011 -0700 @@ -2,7 +2,7 @@ # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj -ML_HOME="/home/smlnj/110.72/bin" +ML_HOME="/home/smlnj/110.73/bin" ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256" ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/isatest/settings/mac-poly64-M2 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly64-M2 Sun Sep 18 16:12:43 2011 -0700 @@ -0,0 +1,29 @@ +# -*- shell-script -*- :mode=shellscript: + + POLYML_HOME="/home/polyml/polyml-5.4.0" + ML_SYSTEM="polyml-5.4.0" + ML_PLATFORM="x86_64-darwin" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="--mutable 500 --immutable 500" + + +ISABELLE_HOME_USER=~/isabelle-at-mac-poly64-M2 + +# Where to look for isabelle tools (multiple dirs separated by ':'). +ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" + +# Location for temporary files (should be on a local file system). +ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" + + +# Heap input locations. ML system identifier is included in lookup. +ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" + +# Heap output location. ML system identifier is appended automatically later on. +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" + +ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2" + +init_component "$HOME/contrib_devel/kodkodi" + diff -r b36eedcd1633 -r 6e6e958b2d40 Admin/makebundle --- a/Admin/makebundle Thu Sep 15 10:12:36 2011 -0700 +++ b/Admin/makebundle Sun Sep 18 16:12:43 2011 -0700 @@ -48,17 +48,19 @@ echo "#bundled components" >> "$ISABELLE_HOME/etc/components" -for CONTRIB in "$ARCHIVE_DIR"/contrib/*.tar.gz +for CONTRIB in "$ARCHIVE_DIR/contrib/"*.tar.gz "$ARCHIVE_DIR/contrib/$PLATFORM"/*.tar.gz do - tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB" - NAME="$(basename "$CONTRIB" .tar.gz)" - [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB" + if [ -f "$CONTRIB" ]; then + tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB" + NAME="$(basename "$CONTRIB" .tar.gz)" + [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB" - if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then - echo "component $NAME" - echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components" - else - echo "package $NAME" + if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then + echo "component $NAME" + echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components" + else + echo "package $NAME" + fi fi done @@ -75,8 +77,14 @@ ) case "$PLATFORM" in + x86_64-linux) + perl -pi -e 's,^ML_PLATFORM=.*$,ML_PLATFORM="\$ISABELLE_PLATFORM64",g;' "$TMP/$ISABELLE_NAME/etc/settings" + perl -pi -e "s,^ML_OPTIONS=.*$,ML_OPTIONS=\"-H 400\",g;" "$TMP/$ISABELLE_NAME/etc/settings" + ;; *-darwin) perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \ + -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \ + -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \ "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" ;; *-cygwin) diff -r b36eedcd1633 -r 6e6e958b2d40 CONTRIBUTORS --- a/CONTRIBUTORS Thu Sep 15 10:12:36 2011 -0700 +++ b/CONTRIBUTORS Sun Sep 18 16:12:43 2011 -0700 @@ -12,30 +12,30 @@ * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM Refined theory on complete lattices. +* August 2011: Brian Huffman, Portland State University + Miscellaneous cleanup of Complex_Main and Multivariate_Analysis. + +* June 2011: Brian Huffman, Portland State University + Proof method "countable_datatype" for theory Library/Countable. + +* 2011: Jasmin Blanchette, TUM + Various improvements to Sledgehammer, notably: use of sound + translations, support for more provers (Waldmeister, LEO-II, + Satallax). Further development of Nitpick and 'try' command. + +* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology + Theory HOL/Library/Cset_Monad allows do notation for computable sets + (cset) via the generic monad ad-hoc overloading facility. + +* 2011: Johannes Hölzl, Armin Heller, TUM and + Bogdan Grechuk, University of Edinburgh + Theory HOL/Library/Extended_Reals: real numbers extended with plus + and minus infinity. + * 2011: Makarius Wenzel, Université Paris-Sud / LRI Various building blocks for Isabelle/Scala layer and Isabelle/jEdit Prover IDE. -* 2011: Jasmin Blanchette, TUM - Various improvements to Sledgehammer, notably: use of sound translations, - support for more provers (Waldmeister, LEO-II, Satallax). Further development - of Nitpick and "try". - -* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology - Theory HOL/Library/Cset_Monad allows do notation for computable - sets (cset) via the generic monad ad-hoc overloading facility. - -* 2011: Johannes Hölzl, Armin Heller, TUM, - and Bogdan Grechuk, University of Edinburgh - Theory HOL/Library/Extended_Reals: real numbers extended with - plus and minus infinity. - -* June 2011: Brian Huffman, Portland State University - Proof method 'countable_datatype' for theory Library/Countable. - -* August 2011: Brian Huffman, Portland State University - Misc cleanup of Complex_Main and Multivariate_Analysis. - Contributions to Isabelle2011 ----------------------------- diff -r b36eedcd1633 -r 6e6e958b2d40 NEWS --- a/NEWS Thu Sep 15 10:12:36 2011 -0700 +++ b/NEWS Sun Sep 18 16:12:43 2011 -0700 @@ -7,7 +7,7 @@ *** General *** * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as -"isabelle jedit" on the command line. +"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line. - Management of multiple theory files directly from the editor buffer store -- bypassing the file-system (no requirement to save @@ -49,24 +49,6 @@ Goal.parallel_proofs_threshold (default 100). See also isabelle usedir option -Q. -* Discontinued support for Poly/ML 5.2, which was the last version -without proper multithreading and TimeLimit implementation. - -* Discontinued old lib/scripts/polyml-platform, which has been -obsolete since Isabelle2009-2. - -* Various optional external tools are referenced more robustly and -uniformly by explicit Isabelle settings as follows: - - ISABELLE_CSDP (formerly CSDP_EXE) - ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) - ISABELLE_OCAML (formerly EXEC_OCAML) - ISABELLE_SWIPL (formerly EXEC_SWIPL) - ISABELLE_YAP (formerly EXEC_YAP) - -Note that automated detection from the file-system or search path has -been discontinued. INCOMPATIBILITY. - * Name space: former unsynchronized references are now proper configuration options, with more conventional names: @@ -85,23 +67,16 @@ * Attribute "case_names" has been refined: the assumptions in each case can be named now by following the case name with [name1 name2 ...]. -* Isabelle/Isar reference manual provides more formal references in -syntax diagrams. +* Isabelle/Isar reference manual has been updated and extended: + - "Synopsis" provides a catalog of main Isar language concepts. + - Formal references in syntax diagrams, via @{rail} antiquotation. + - Updated material from classic "ref" manual, notably about + "Classical Reasoner". *** HOL *** -* Theory Library/Saturated provides type of numbers with saturated -arithmetic. - -* Theory Library/Product_Lattice defines a pointwise ordering for the -product type 'a * 'b, and provides instance proofs for various order -and lattice type classes. - -* Theory Library/Countable now provides the "countable_datatype" proof -method for proving "countable" class instances for datatypes. - -* Classes bot and top require underlying partial order rather than +* Class bot and top require underlying partial order rather than preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. * Class complete_lattice: generalized a couple of lemmas from sets; @@ -115,7 +90,7 @@ Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, -INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, +INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset, UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been discarded. @@ -138,6 +113,19 @@ INCOMPATIBILITY. +* Renamed theory Complete_Lattice to Complete_Lattices. +INCOMPATIBILITY. + +* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff, +INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot, +Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, +Sup_insert are now declared as [simp]. INCOMPATIBILITY. + +* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff, +compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, +sup_inf_absob, sup_left_idem are now declared as [simp]. Minor +INCOMPATIBILITY. + * Added syntactic classes "inf" and "sup" for the respective constants. INCOMPATIBILITY: Changes in the argument order of the (mostly internal) locale predicates for some derived classes. @@ -157,193 +145,9 @@ Both use point-free characterization; interpretation proofs may need adjustment. INCOMPATIBILITY. -* Code generation: - - - Theory Library/Code_Char_ord provides native ordering of - characters in the target language. - - - Commands code_module and code_library are legacy, use export_code instead. - - - Method "evaluation" is legacy, use method "eval" instead. - - - Legacy evaluator "SML" is deactivated by default. May be - reactivated by the following theory command: - - setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} - -* Declare ext [intro] by default. Rare INCOMPATIBILITY. - -* The misleading name fastsimp has been renamed to fastforce, - but fastsimp is still available as a legacy feature. - -* Nitpick: - - Added "need" and "total_consts" options. - - Reintroduced "show_skolems" option by popular demand. - - Renamed attribute: nitpick_def ~> nitpick_unfold. - INCOMPATIBILITY. - -* Sledgehammer: - - Use quasi-sound (and efficient) translations by default. - - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK, - Waldmeister, and Z3 with TPTP syntax. - - Automatically preplay and minimize proofs before showing them if this can be - done within reasonable time. - - sledgehammer available_provers ~> sledgehammer supported_provers. - INCOMPATIBILITY. - - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters", - and "max_new_mono_instances" options. - - Removed "explicit_apply" and "full_types" options as well as "Full Types" - Proof General menu item. INCOMPATIBILITY. - -* Metis: - - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. - - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY. - -* Command 'try': - - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and - "elim:" options. INCOMPATIBILITY. - - Introduced 'try' that not only runs 'try_methods' but also - 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. - -* Quickcheck: - - - Added "eval" option to evaluate terms for the found counterexample - (currently only supported by the default (exhaustive) tester). - - - Added post-processing of terms to obtain readable counterexamples - (currently only supported by the default (exhaustive) tester). - - - New counterexample generator quickcheck[narrowing] enables - narrowing-based testing. Requires the Glasgow Haskell compiler - with its installation location defined in the Isabelle settings - environment as ISABELLE_GHC. - - - Removed quickcheck tester "SML" based on the SML code generator - (formly in HOL/Library). - -* Function package: discontinued option "tailrec". -INCOMPATIBILITY. Use 'partial_function' instead. - -* Session HOL-Probability: - - Caratheodory's extension lemma is now proved for ring_of_sets. - - Infinite products of probability measures are now available. - - Sigma closure is independent, if the generator is independent - - Use extended reals instead of positive extended - reals. INCOMPATIBILITY. - -* Theory Library/Extended_Reals replaces now the positive extended reals - found in probability theory. This file is extended by - Multivariate_Analysis/Extended_Real_Limits. - -* Old 'recdef' package has been moved to theory Library/Old_Recdef, -from where it must be imported explicitly. INCOMPATIBILITY. - -* Well-founded recursion combinator "wfrec" has been moved to theory -Library/Wfrec. INCOMPATIBILITY. - -* Theory HOL/Library/Cset_Monad allows do notation for computable - sets (cset) via the generic monad ad-hoc overloading facility. - -* Theories of common data structures are split into theories for - implementation, an invariant-ensuring type, and connection to - an abstract type. INCOMPATIBILITY. - - - RBT is split into RBT and RBT_Mapping. - - AssocList is split and renamed into AList and AList_Mapping. - - DList is split into DList_Impl, DList, and DList_Cset. - - Cset is split into Cset and List_Cset. - -* Theory Library/Nat_Infinity has been renamed to -Library/Extended_Nat, with name changes of the following types and -constants: - - type inat ~> type enat - Fin ~> enat - Infty ~> infinity (overloaded) - iSuc ~> eSuc - the_Fin ~> the_enat - -Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has -been renamed accordingly. INCOMPATIBILITY. - * Theory Limits: Type "'a net" has been renamed to "'a filter", in accordance with standard mathematical terminology. INCOMPATIBILITY. -* Session Multivariate_Analysis: The euclidean_space type class now -fixes a constant "Basis :: 'a set" consisting of the standard -orthonormal basis for the type. Users now have the option of -quantifying over this set instead of using the "basis" function, e.g. -"ALL x:Basis. P x" vs "ALL i vec_eq_iff - dist_nth_le_cart ~> dist_vec_nth_le - tendsto_vector ~> vec_tendstoI - Cauchy_vector ~> vec_CauchyI - -* Session Multivariate_Analysis: Several duplicate theorems have been -removed, and other theorems have been renamed or replaced with more -general versions. INCOMPATIBILITY. - - finite_choice ~> finite_set_choice - eventually_conjI ~> eventually_conj - eventually_and ~> eventually_conj_iff - eventually_false ~> eventually_False - setsum_norm ~> norm_setsum - Lim_sequentially ~> LIMSEQ_def - Lim_ident_at ~> LIM_ident - Lim_const ~> tendsto_const - Lim_cmul ~> tendsto_scaleR [OF tendsto_const] - Lim_neg ~> tendsto_minus - Lim_add ~> tendsto_add - Lim_sub ~> tendsto_diff - Lim_mul ~> tendsto_scaleR - Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] - Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] - Lim_linear ~> bounded_linear.tendsto - Lim_component ~> tendsto_euclidean_component - Lim_component_cart ~> tendsto_vec_nth - Lim_inner ~> tendsto_inner [OF tendsto_const] - dot_lsum ~> inner_setsum_left - dot_rsum ~> inner_setsum_right - continuous_cmul ~> continuous_scaleR [OF continuous_const] - continuous_neg ~> continuous_minus - continuous_sub ~> continuous_diff - continuous_vmul ~> continuous_scaleR [OF _ continuous_const] - continuous_mul ~> continuous_scaleR - continuous_inv ~> continuous_inverse - continuous_at_within_inv ~> continuous_at_within_inverse - continuous_at_inv ~> continuous_at_inverse - continuous_at_norm ~> continuous_norm [OF continuous_at_id] - continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] - continuous_at_component ~> continuous_component [OF continuous_at_id] - continuous_on_neg ~> continuous_on_minus - continuous_on_sub ~> continuous_on_diff - continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] - continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] - continuous_on_mul ~> continuous_on_scaleR - continuous_on_mul_real ~> continuous_on_mult - continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] - continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] - continuous_on_inverse ~> continuous_on_inv - uniformly_continuous_on_neg ~> uniformly_continuous_on_minus - uniformly_continuous_on_sub ~> uniformly_continuous_on_diff - subset_interior ~> interior_mono - subset_closure ~> closure_mono - closure_univ ~> closure_UNIV - real_arch_lt ~> reals_Archimedean2 - real_arch ~> reals_Archimedean3 - real_abs_norm ~> abs_norm_cancel - real_abs_sub_norm ~> norm_triangle_ineq3 - norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 - * Theory Complex_Main: The locale interpretations for the bounded_linear and bounded_bilinear locales have been removed, in order to reduce the number of duplicate lemmas. Users must use the @@ -423,23 +227,210 @@ bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at] -* Theory Complex_Main: The definition of infinite series was generalized. - Now it is defined on the type class {topological_space, comm_monoid_add}. - Hence it is useable also for extended real numbers. +* Theory Complex_Main: The definition of infinite series was +generalized. Now it is defined on the type class {topological_space, +comm_monoid_add}. Hence it is useable also for extended real numbers. * Theory Complex_Main: The complex exponential function "expi" is now a type-constrained abbreviation for "exp :: complex => complex"; thus several polymorphic lemmas about "exp" are now applicable to "expi". +* Code generation: + + - Theory Library/Code_Char_ord provides native ordering of + characters in the target language. + + - Commands code_module and code_library are legacy, use export_code + instead. + + - Method "evaluation" is legacy, use method "eval" instead. + + - Legacy evaluator "SML" is deactivated by default. May be + reactivated by the following theory command: + + setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} + +* Declare ext [intro] by default. Rare INCOMPATIBILITY. + +* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is +still available as a legacy feature for some time. + +* Nitpick: + - Added "need" and "total_consts" options. + - Reintroduced "show_skolems" option by popular demand. + - Renamed attribute: nitpick_def ~> nitpick_unfold. + INCOMPATIBILITY. + +* Sledgehammer: + - Use quasi-sound (and efficient) translations by default. + - Added support for the following provers: E-ToFoF, LEO-II, + Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. + - Automatically preplay and minimize proofs before showing them if + this can be done within reasonable time. + - sledgehammer available_provers ~> sledgehammer supported_provers. + INCOMPATIBILITY. + - Added "preplay_timeout", "slicing", "type_enc", "sound", + "max_mono_iters", and "max_new_mono_instances" options. + - Removed "explicit_apply" and "full_types" options as well as "Full + Types" Proof General menu item. INCOMPATIBILITY. + +* Metis: + - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. + - Obsoleted "metisFT" -- use "metis (full_types)" instead. + INCOMPATIBILITY. + +* Command 'try': + - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and + "elim:" options. INCOMPATIBILITY. + - Introduced 'try' that not only runs 'try_methods' but also + 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. + +* Quickcheck: + - Added "eval" option to evaluate terms for the found counterexample + (currently only supported by the default (exhaustive) tester). + - Added post-processing of terms to obtain readable counterexamples + (currently only supported by the default (exhaustive) tester). + - New counterexample generator quickcheck[narrowing] enables + narrowing-based testing. Requires the Glasgow Haskell compiler + with its installation location defined in the Isabelle settings + environment as ISABELLE_GHC. + - Removed quickcheck tester "SML" based on the SML code generator + (formly in HOL/Library). + +* Function package: discontinued option "tailrec". INCOMPATIBILITY, +use 'partial_function' instead. + +* Theory Library/Extended_Reals replaces now the positive extended +reals found in probability theory. This file is extended by +Multivariate_Analysis/Extended_Real_Limits. + +* Theory Library/Old_Recdef: old 'recdef' package has been moved here, +from where it must be imported explicitly if it is really required. +INCOMPATIBILITY. + +* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has +been moved here. INCOMPATIBILITY. + +* Theory Library/Saturated provides type of numbers with saturated +arithmetic. + +* Theory Library/Product_Lattice defines a pointwise ordering for the +product type 'a * 'b, and provides instance proofs for various order +and lattice type classes. + +* Theory Library/Countable now provides the "countable_datatype" proof +method for proving "countable" class instances for datatypes. + +* Theory Library/Cset_Monad allows do notation for computable sets +(cset) via the generic monad ad-hoc overloading facility. + +* Library: Theories of common data structures are split into theories +for implementation, an invariant-ensuring type, and connection to an +abstract type. INCOMPATIBILITY. + + - RBT is split into RBT and RBT_Mapping. + - AssocList is split and renamed into AList and AList_Mapping. + - DList is split into DList_Impl, DList, and DList_Cset. + - Cset is split into Cset and List_Cset. + +* Theory Library/Nat_Infinity has been renamed to +Library/Extended_Nat, with name changes of the following types and +constants: + + type inat ~> type enat + Fin ~> enat + Infty ~> infinity (overloaded) + iSuc ~> eSuc + the_Fin ~> the_enat + +Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has +been renamed accordingly. INCOMPATIBILITY. + +* Session Multivariate_Analysis: The euclidean_space type class now +fixes a constant "Basis :: 'a set" consisting of the standard +orthonormal basis for the type. Users now have the option of +quantifying over this set instead of using the "basis" function, e.g. +"ALL x:Basis. P x" vs "ALL i vec_eq_iff + dist_nth_le_cart ~> dist_vec_nth_le + tendsto_vector ~> vec_tendstoI + Cauchy_vector ~> vec_CauchyI + +* Session Multivariate_Analysis: Several duplicate theorems have been +removed, and other theorems have been renamed or replaced with more +general versions. INCOMPATIBILITY. + + finite_choice ~> finite_set_choice + eventually_conjI ~> eventually_conj + eventually_and ~> eventually_conj_iff + eventually_false ~> eventually_False + setsum_norm ~> norm_setsum + Lim_sequentially ~> LIMSEQ_def + Lim_ident_at ~> LIM_ident + Lim_const ~> tendsto_const + Lim_cmul ~> tendsto_scaleR [OF tendsto_const] + Lim_neg ~> tendsto_minus + Lim_add ~> tendsto_add + Lim_sub ~> tendsto_diff + Lim_mul ~> tendsto_scaleR + Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] + Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] + Lim_linear ~> bounded_linear.tendsto + Lim_component ~> tendsto_euclidean_component + Lim_component_cart ~> tendsto_vec_nth + Lim_inner ~> tendsto_inner [OF tendsto_const] + dot_lsum ~> inner_setsum_left + dot_rsum ~> inner_setsum_right + continuous_cmul ~> continuous_scaleR [OF continuous_const] + continuous_neg ~> continuous_minus + continuous_sub ~> continuous_diff + continuous_vmul ~> continuous_scaleR [OF _ continuous_const] + continuous_mul ~> continuous_scaleR + continuous_inv ~> continuous_inverse + continuous_at_within_inv ~> continuous_at_within_inverse + continuous_at_inv ~> continuous_at_inverse + continuous_at_norm ~> continuous_norm [OF continuous_at_id] + continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] + continuous_at_component ~> continuous_component [OF continuous_at_id] + continuous_on_neg ~> continuous_on_minus + continuous_on_sub ~> continuous_on_diff + continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] + continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] + continuous_on_mul ~> continuous_on_scaleR + continuous_on_mul_real ~> continuous_on_mult + continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] + continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] + continuous_on_inverse ~> continuous_on_inv + uniformly_continuous_on_neg ~> uniformly_continuous_on_minus + uniformly_continuous_on_sub ~> uniformly_continuous_on_diff + subset_interior ~> interior_mono + subset_closure ~> closure_mono + closure_univ ~> closure_UNIV + real_arch_lt ~> reals_Archimedean2 + real_arch ~> reals_Archimedean3 + real_abs_norm ~> abs_norm_cancel + real_abs_sub_norm ~> norm_triangle_ineq3 + norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 + +* Session HOL-Probability: + - Caratheodory's extension lemma is now proved for ring_of_sets. + - Infinite products of probability measures are now available. + - Sigma closure is independent, if the generator is independent + - Use extended reals instead of positive extended + reals. INCOMPATIBILITY. + *** Document preparation *** -* Localized \isabellestyle switch can be used within blocks or groups -like this: - - \isabellestyle{it} %preferred default - {\isabellestylett @{text "typewriter stuff"}} - * Antiquotation @{rail} layouts railroad syntax diagrams, see also isar-ref manual, both for description and actual application of the same. @@ -454,9 +445,15 @@ * Predefined LaTeX macros for Isabelle symbols \ and \ (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). -* Discontinued special treatment of hard tabulators, which are better -avoided in the first place (no universally agreed standard expansion). -Implicit tab-width is now 1. +* Localized \isabellestyle switch can be used within blocks or groups +like this: + + \isabellestyle{it} %preferred default + {\isabellestylett @{text "typewriter stuff"}} + +* Discontinued special treatment of hard tabulators. Implicit +tab-width is now defined as 1. Potential INCOMPATIBILITY for visual +layouts. *** ML *** @@ -519,14 +516,32 @@ *** System *** +* Discontinued support for Poly/ML 5.2, which was the last version +without proper multithreading and TimeLimit implementation. + +* Discontinued old lib/scripts/polyml-platform, which has been +obsolete since Isabelle2009-2. + +* Various optional external tools are referenced more robustly and +uniformly by explicit Isabelle settings as follows: + + ISABELLE_CSDP (formerly CSDP_EXE) + ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) + ISABELLE_OCAML (formerly EXEC_OCAML) + ISABELLE_SWIPL (formerly EXEC_SWIPL) + ISABELLE_YAP (formerly EXEC_YAP) + +Note that automated detection from the file-system or search path has +been discontinued. INCOMPATIBILITY. + * Scala layer provides JVM method invocation service for static methods of type (String)String, see Invoke_Scala.method in ML. For example: Invoke_Scala.method "java.lang.System.getProperty" "java.home" -Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this -allows to pass structured values between ML and Scala. +Together with YXML.string_of_body/parse_body and XML.Encode/Decode +this allows to pass structured values between ML and Scala. * The IsabelleText fonts includes some further glyphs to support the Prover IDE. Potential INCOMPATIBILITY: users who happen to have @@ -1650,26 +1665,12 @@ INTER_fold_inter ~> INFI_fold_inf UNION_fold_union ~> SUPR_fold_sup -* Theory "Complete_Lattice": - - - renamed to "Complete_Lattices". minor INCOMPATIBILITY. - - - lemmas top_def and bot_def have been replaced by the more convenient - lemmas Inf_empty and Sup_empty. Dropped lemmas Inf_insert_simp and - Sup_insert_simp, which are subsumed by Inf_insert and Sup_insert. - Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ. - Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot - respectively. INCOMPATIBILITY. - - - lemmas Inf_eq_top_iff, INF_eq_top_iff, INF_image, Inf_insert, INF_top, - Inf_top_conv, INF_top_conv, SUP_bot, Sup_bot_conv, SUP_bot_conv, - Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, Sup_insert are now declared - as [simp]. minor INCOMPATIBILITY. - -* Theory "Lattice": lemmas compl_inf_bot, compl_le_comp_iff, compl_sup_top, -inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, sup_inf_absob, -sup_left_idem are now declared as [simp]. minor INCOMPATIBILITY. - +* Theory "Complete_Lattice": lemmas top_def and bot_def have been +replaced by the more convenient lemmas Inf_empty and Sup_empty. +Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed +by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace +former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right +subsume inf_top and sup_bot respectively. INCOMPATIBILITY. * Reorganized theory Multiset: swapped notation of pointwise and multiset order: diff -r b36eedcd1633 -r 6e6e958b2d40 README --- a/README Thu Sep 15 10:12:36 2011 -0700 +++ b/README Sun Sep 18 16:12:43 2011 -0700 @@ -10,7 +10,7 @@ System requirements Isabelle requires a regular Unix-style platform (e.g. Linux, - Windows with Cygwin, Mac OS) and depends on the following main + Windows with Cygwin, Mac OS X) and depends on the following main add-on tools: * The Poly/ML compiler and runtime system (version 5.2.1 or later). diff -r b36eedcd1633 -r 6e6e958b2d40 doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Thu Sep 15 10:12:36 2011 -0700 +++ b/doc-src/Codegen/Thy/examples/Example.hs Sun Sep 18 16:12:43 2011 -0700 @@ -1,4 +1,4 @@ -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} module Example where { diff -r b36eedcd1633 -r 6e6e958b2d40 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Thu Sep 15 10:12:36 2011 -0700 +++ b/doc-src/IsarRef/isar-ref.tex Sun Sep 18 16:12:43 2011 -0700 @@ -25,15 +25,18 @@ With Contributions by Clemens Ballarin, Stefan Berghofer, \\ + Jasmin Blanchette, Timothy Bourke, + Lukas Bulwahn, \\ Lucas Dixon, - Florian Haftmann, \\ - Gerwin Klein, + Florian Haftmann, + Gerwin Klein, \\ Alexander Krauss, - Tobias Nipkow, \\ + Tobias Nipkow, + Lars Noschinski, \\ David von Oheimb, Larry Paulson, - and Sebastian Skalberg + Sebastian Skalberg } \makeindex diff -r b36eedcd1633 -r 6e6e958b2d40 doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/doc-src/Main/Docs/Main_Doc.thy Sun Sep 18 16:12:43 2011 -0700 @@ -82,8 +82,8 @@ \begin{tabular}{@ {} l @ {~::~} l @ {}} @{const Lattices.inf} & @{typeof Lattices.inf}\\ @{const Lattices.sup} & @{typeof Lattices.sup}\\ -@{const Complete_Lattice.Inf} & @{term_type_only Complete_Lattice.Inf "'a set \ 'a::Inf"}\\ -@{const Complete_Lattice.Sup} & @{term_type_only Complete_Lattice.Sup "'a set \ 'a::Sup"}\\ +@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \ 'a::Inf"}\\ +@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \ 'a::Sup"}\\ \end{tabular} \subsubsection*{Syntax} diff -r b36eedcd1633 -r 6e6e958b2d40 etc/settings --- a/etc/settings Thu Sep 15 10:12:36 2011 -0700 +++ b/etc/settings Sun Sep 18 16:12:43 2011 -0700 @@ -15,7 +15,7 @@ # not invent new ML system names unless you know what you are doing. # Only one of the sections below should be activated. -# Poly/ML 32 bit (automated settings) +# Poly/ML default (automated settings) ML_PLATFORM="$ISABELLE_PLATFORM" ML_HOME="$(choosefrom \ "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ @@ -56,8 +56,6 @@ if [ -n "$JAVA_HOME" ]; then ISABELLE_JAVA="$JAVA_HOME/bin/java" -elif [ -x /usr/libexec/java_home ]; then - ISABELLE_JAVA="$(/usr/libexec/java_home -v 1.6)"/bin/java else ISABELLE_JAVA="java" fi diff -r b36eedcd1633 -r 6e6e958b2d40 lib/Tools/scalac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/scalac Sun Sep 18 16:12:43 2011 -0700 @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: invoke Scala compiler within the Isabelle environment + +[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } + +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } + +CLASSPATH="$(jvmpath "$CLASSPATH")" +exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \ + "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@" diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Big_Operators.thy Sun Sep 18 16:12:43 2011 -0700 @@ -312,14 +312,14 @@ text{*No need to assume that @{term C} is finite. If infinite, the rhs is directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*} lemma setsum_Union_disjoint: - "[| (ALL A:C. finite A); - (ALL A:C. ALL B:C. A \ B --> A Int B = {}) |] - ==> setsum f (Union C) = setsum (setsum f) C" -apply (cases "finite C") - prefer 2 apply (force dest: finite_UnionD simp add: setsum_def) - apply (frule setsum_UN_disjoint [of C id f]) - apply (unfold Union_def id_def, assumption+) -done + assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A Int B = {}" + shows "setsum f (Union C) = setsum (setsum f) C" +proof cases + assume "finite C" + from setsum_UN_disjoint[OF this assms] + show ?thesis + by (simp add: SUP_def) +qed (force dest: finite_UnionD simp add: setsum_def) (*But we can't get rid of finite A. If infinite, although the lhs is 0, the rhs need not be, since SIGMA A B could still be finite.*) @@ -801,7 +801,7 @@ (ALL A:C. ALL B:C. A \ B --> A Int B = {}) ==> card (Union C) = setsum card C" apply (frule card_UN_disjoint [of C id]) -apply (unfold Union_def id_def, assumption+) +apply (simp_all add: SUP_def id_def) done text{*The image of a finite set can be expressed using @{term fold_image}.*} @@ -996,14 +996,14 @@ by (simp add: setprod_def fold_image_UN_disjoint) lemma setprod_Union_disjoint: - "[| (ALL A:C. finite A); - (ALL A:C. ALL B:C. A \ B --> A Int B = {}) |] - ==> setprod f (Union C) = setprod (setprod f) C" -apply (cases "finite C") - prefer 2 apply (force dest: finite_UnionD simp add: setprod_def) - apply (frule setprod_UN_disjoint [of C id f]) - apply (unfold Union_def id_def, assumption+) -done + assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A Int B = {}" + shows "setprod f (Union C) = setprod (setprod f) C" +proof cases + assume "finite C" + from setprod_UN_disjoint[OF this assms] + show ?thesis + by (simp add: SUP_def) +qed (force dest: finite_UnionD simp add: setprod_def) lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> (\x\A. (\y\ B x. f x y)) = diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Complete_Lattices.thy Sun Sep 18 16:12:43 2011 -0700 @@ -1131,7 +1131,6 @@ "\A B f. (\a\A. B (f a)) = (\x\f`A. B x)" by auto - text {* Legacy names *} lemma (in complete_lattice) Inf_singleton [simp]: @@ -1142,68 +1141,9 @@ "\{a} = a" by simp -lemma (in complete_lattice) Inf_binary: - "\{a, b} = a \ b" - by simp - -lemma (in complete_lattice) Sup_binary: - "\{a, b} = a \ b" - by simp - -text {* Grep and put to news from here *} - -lemma (in complete_lattice) INF_eq: - "(\x\A. B x) = \({Y. \x\A. Y = B x})" - by (simp add: INF_def image_def) - -lemma (in complete_lattice) SUP_eq: - "(\x\A. B x) = \({Y. \x\A. Y = B x})" - by (simp add: SUP_def image_def) - -lemma (in complete_lattice) INF_subset: - "B \ A \ INFI A f \ INFI B f" - by (rule INF_superset_mono) auto - -lemma (in complete_lattice) INF_UNIV_range: - "(\x. f x) = \range f" - by (fact INF_def) - -lemma (in complete_lattice) SUP_UNIV_range: - "(\x. f x) = \range f" - by (fact SUP_def) - -lemma Int_eq_Inter: "A \ B = \{A, B}" - by simp - -lemma INTER_eq_Inter_image: - "(\x\A. B x) = \(B`A)" - by (fact INF_def) - -lemma Inter_def: - "\S = (\x\S. x)" - by (simp add: INTER_eq_Inter_image image_def) - -lemma INT_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})" - by (fact INF_eq) - -lemma Un_eq_Union: "A \ B = \{A, B}" - by blast - -lemma UNION_eq_Union_image: - "(\x\A. B x) = \(B ` A)" - by (fact SUP_def) - -lemma Union_def: - "\S = (\x\S. x)" - by (simp add: UNION_eq_Union_image image_def) - lemma UN_singleton [simp]: "(\x\A. {x}) = A" by blast -lemma UN_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})" - by (fact SUP_eq) - - text {* Finally *} no_notation diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IMP/AbsInt0.thy --- a/src/HOL/IMP/AbsInt0.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IMP/AbsInt0.thy Sun Sep 18 16:12:43 2011 -0700 @@ -10,9 +10,9 @@ functions. *} locale Abs_Int = Val_abs + -fixes pfp_above :: "('a astate \ 'a astate) \ 'a astate \ 'a astate" -assumes pfp: "f(pfp_above f x0) \ pfp_above f x0" -assumes above: "x0 \ pfp_above f x0" +fixes pfp :: "('a astate \ 'a astate) \ 'a astate \ 'a astate" +assumes pfp: "f(pfp f x0) \ pfp f x0" +assumes above: "x0 \ pfp f x0" begin fun aval' :: "aexp \ 'a astate \ 'a" where @@ -35,7 +35,7 @@ "AI (x ::= a) S = update S x (aval' a S)" | "AI (c1;c2) S = AI c2 (AI c1 S)" | "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \ (AI c2 S)" | -"AI (WHILE b DO c) S = pfp_above (AI c) S" +"AI (WHILE b DO c) S = pfp (AI c) S" lemma AI_sound: "(c,s) \ t \ s <: S0 \ t <: AI c S0" proof(induct c arbitrary: s t S0) @@ -50,7 +50,7 @@ by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2) next case (While b c) - let ?P = "pfp_above (AI c) S0" + let ?P = "pfp (AI c) S0" { fix s t have "(WHILE b DO c,s) \ t \ s <: ?P \ t <: ?P" proof(induct "WHILE b DO c" s t rule: big_step_induct) case WhileFalse thus ?case by simp diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IMP/AbsInt0_const.thy --- a/src/HOL/IMP/AbsInt0_const.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IMP/AbsInt0_const.thy Sun Sep 18 16:12:43 2011 -0700 @@ -61,10 +61,10 @@ by(cases a1, cases a2, simp, simp, cases a2, simp, simp) qed -interpretation Abs_Int rep_cval Const plus_cval "(iter_above 3)" +interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" defines AI_const is AI and aval'_const is aval' -proof qed (auto simp: iter_above_pfp) +proof qed (auto simp: iter'_pfp_above) text{* Straight line code: *} definition "test1_const = diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IMP/AbsInt0_fun.thy --- a/src/HOL/IMP/AbsInt0_fun.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IMP/AbsInt0_fun.thy Sun Sep 18 16:12:43 2011 -0700 @@ -41,16 +41,15 @@ apply (simp) done -definition iter_above :: "nat \ ('a \ 'a) \ 'a \ 'a" where -"iter_above n f x0 = iter n (\x. x0 \ f x) x0" +abbreviation iter' :: "nat \ ('a \ 'a) \ 'a \ 'a" where +"iter' n f x0 == iter n (\x. x0 \ f x) x0" -lemma iter_above_pfp: -shows "f(iter_above n f x0) \ iter_above n f x0" and "x0 \ iter_above n f x0" -using iter_pfp[of "\x. x0 \ f x"] -by(auto simp add: iter_above_def) +lemma iter'_pfp_above: + "f(iter' n f x0) \ iter' n f x0" "x0 \ iter' n f x0" +using iter_pfp[of "\x. x0 \ f x"] by auto text{* So much for soundness. But how good an approximation of the post-fixed -point does @{const iter_above} yield? *} +point does @{const iter} yield? *} lemma iter_funpow: "iter n f x \ Top \ \k. iter n f x = (f^^k) x" apply(induct n arbitrary: x) @@ -59,19 +58,17 @@ apply(metis funpow.simps(1) id_def) by (metis funpow.simps(2) funpow_swap1 o_apply) -text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least +text{* For monotone @{text f}, @{term "iter f n x0"} yields the least post-fixed point above @{text x0}, unless it yields @{text Top}. *} lemma iter_least_pfp: -assumes mono: "!!x y. x \ y \ f x \ f y" and "iter_above n f x0 \ Top" -and "f p \ p" and "x0 \ p" shows "iter_above n f x0 \ p" +assumes mono: "\x y. x \ y \ f x \ f y" and "iter n f x0 \ Top" +and "f p \ p" and "x0 \ p" shows "iter n f x0 \ p" proof- - let ?F = "\x. x0 \ f x" - obtain k where "iter_above n f x0 = (?F^^k) x0" - using iter_funpow `iter_above n f x0 \ Top` - by(fastforce simp add: iter_above_def) + obtain k where "iter n f x0 = (f^^k) x0" + using iter_funpow[OF `iter n f x0 \ Top`] by blast moreover - { fix n have "(?F^^n) x0 \ p" + { fix n have "(f^^n) x0 \ p" proof(induct n) case 0 show ?case by(simp add: `x0 \ p`) next @@ -81,24 +78,6 @@ } ultimately show ?thesis by simp qed -lemma chain: assumes "!!x y. x \ y \ f x \ f y" -shows "((\x. x0 \ f x)^^i) x0 \ ((\x. x0 \ f x)^^(i+1)) x0" -apply(induct i) - apply simp -apply simp -by (metis assms join_ge2 le_trans) - -lemma iter_above_almost_fp: -assumes mono: "!!x y. x \ y \ f x \ f y" and "iter_above n f x0 \ Top" -shows "iter_above n f x0 \ x0 \ f(iter_above n f x0)" -proof- - let ?p = "iter_above n f x0" - obtain k where 1: "?p = ((\x. x0 \ f x)^^k) x0" - using iter_funpow `?p \ Top` - by(fastforce simp add: iter_above_def) - thus ?thesis using chain mono by simp -qed - end text{* The interface of abstract values: *} @@ -149,9 +128,9 @@ type_synonym 'a st = "name \ 'a" locale Abs_Int_Fun = Val_abs + -fixes pfp_above :: "('a st \ 'a st) \ 'a st \ 'a st" -assumes pfp: "f(pfp_above f x0) \ pfp_above f x0" -assumes above: "x0 \ pfp_above f x0" +fixes pfp :: "('a st \ 'a st) \ 'a st \ 'a st" +assumes pfp: "f(pfp f x) \ pfp f x" +assumes above: "x \ pfp f x" begin fun aval' :: "aexp \ (name \ 'a) \ 'a" where @@ -173,7 +152,7 @@ "AI (x ::= a) S = S(x := aval' a S)" | "AI (c1;c2) S = AI c2 (AI c1 S)" | "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \ (AI c2 S)" | -"AI (WHILE b DO c) S = pfp_above (AI c) S" +"AI (WHILE b DO c) S = pfp (AI c) S" lemma AI_sound: "(c,s) \ t \ s <: S0 \ t <: AI c S0" proof(induct c arbitrary: s t S0) @@ -186,7 +165,7 @@ case If thus ?case by(auto simp: in_rep_join) next case (While b c) - let ?P = "pfp_above (AI c) S0" + let ?P = "pfp (AI c) S0" { fix s t have "(WHILE b DO c,s) \ t \ s <: ?P \ t <: ?P" proof(induct "WHILE b DO c" s t rule: big_step_induct) case WhileFalse thus ?case by simp diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IMP/AbsInt1.thy --- a/src/HOL/IMP/AbsInt1.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IMP/AbsInt1.thy Sun Sep 18 16:12:43 2011 -0700 @@ -83,9 +83,9 @@ locale Abs_Int1 = Val_abs1 + -fixes pfp_above :: "('a astate up \ 'a astate up) \ 'a astate up \ 'a astate up" -assumes pfp: "f(pfp_above f x0) \ pfp_above f x0" -assumes above: "x0 \ pfp_above f x0" +fixes pfp :: "('a astate up \ 'a astate up) \ 'a astate up \ 'a astate up" +assumes pfp: "f(pfp f x0) \ pfp f x0" +assumes above: "x0 \ pfp f x0" begin (* FIXME avoid duplicating this defn *) @@ -178,7 +178,7 @@ "AI (IF b THEN c1 ELSE c2) S = AI c1 (bfilter b True S) \ AI c2 (bfilter b False S)" | "AI (WHILE b DO c) S = - bfilter b False (pfp_above (\S. AI c (bfilter b True S)) S)" + bfilter b False (pfp (\S. AI c (bfilter b True S)) S)" lemma AI_sound: "(c,s) \ t \ s <:: S \ t <:: AI c S" proof(induct c arbitrary: s t S) @@ -192,7 +192,7 @@ case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound) next case (While b c) - let ?P = "pfp_above (\S. AI c (bfilter b True S)) S" + let ?P = "pfp (\S. AI c (bfilter b True S)) S" { fix s t have "(WHILE b DO c,s) \ t \ s <:: ?P \ t <:: bfilter b False ?P" diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IMP/AbsInt1_ivl.thy --- a/src/HOL/IMP/AbsInt1_ivl.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IMP/AbsInt1_ivl.thy Sun Sep 18 16:12:43 2011 -0700 @@ -190,12 +190,12 @@ qed interpretation - Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3)" + Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3)" defines afilter_ivl is afilter and bfilter_ivl is bfilter and AI_ivl is AI and aval_ivl is aval' -proof qed (auto simp: iter_above_pfp) +proof qed (auto simp: iter'_pfp_above) fun list_up where diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IMP/AbsInt2.thy --- a/src/HOL/IMP/AbsInt2.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IMP/AbsInt2.thy Sun Sep 18 16:12:43 2011 -0700 @@ -40,15 +40,15 @@ apply (simp add: Let_def) done -definition iter_above :: "nat \ nat \ ('a \ 'a) \ 'a \ 'a" where -"iter_above m n f x = +definition iter' :: "nat \ nat \ ('a \ 'a) \ 'a \ 'a" where +"iter' m n f x = (let f' = (\y. x \ f y) in iter_down f' n (iter_up f' m x))" -lemma iter_above_pfp: -shows "f(iter_above m n f x0) \ iter_above m n f x0" -and "x0 \ iter_above m n f x0" +lemma iter'_pfp_above: +shows "f(iter' m n f x0) \ iter' m n f x0" +and "x0 \ iter' m n f x0" using iter_up_pfp[of "\x. x0 \ f x"] iter_down_pfp[of "\x. x0 \ f x"] -by(auto simp add: iter_above_def Let_def) +by(auto simp add: iter'_def Let_def) end @@ -126,12 +126,12 @@ end interpretation - Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3 2)" + Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3 2)" defines afilter_ivl' is afilter and bfilter_ivl' is bfilter and AI_ivl' is AI and aval_ivl' is aval' -proof qed (auto simp: iter_above_pfp) +proof qed (auto simp: iter'_pfp_above) value [code] "list_up(AI_ivl' test3_ivl Top)" value [code] "list_up(AI_ivl' test4_ivl Top)" diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Induct/Com.thy Sun Sep 18 16:12:43 2011 -0700 @@ -85,12 +85,12 @@ lemma [pred_set_conv]: "((\x x' y y'. ((x, x'), (y, y')) \ R) <= (\x x' y y'. ((x, x'), (y, y')) \ S)) = (R <= S)" unfolding subset_eq - by (auto simp add: le_fun_def le_bool_def) + by (auto simp add: le_fun_def) lemma [pred_set_conv]: "((\x x' y. ((x, x'), y) \ R) <= (\x x' y. ((x, x'), y) \ S)) = (R <= S)" unfolding subset_eq - by (auto simp add: le_fun_def le_bool_def) + by (auto simp add: le_fun_def) text{*Command execution is functional (deterministic) provided evaluation is*} theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" @@ -133,15 +133,14 @@ lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))" -by (rule fun_upd_same [THEN subst], fast) + by (rule fun_upd_same [THEN subst]) fast text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new version look worse than it is...*} -lemma split_lemma: - "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))" -by auto +lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))" + by auto text{*New induction rule. Note the form of the VALOF induction hypothesis*} lemma eval_induct diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/IsaMakefile Sun Sep 18 16:12:43 2011 -0700 @@ -1041,18 +1041,19 @@ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ ex/Iff_Oracle.thy ex/Induction_Schema.thy \ - ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \ - ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \ - ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ - ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \ - ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ - ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ + ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy \ + ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy \ + ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy \ + ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ + ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy \ + ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \ + ex/Quickcheck_Lattice_Examples.thy \ ex/Quickcheck_Narrowing_Examples.thy ex/Quicksort.thy ex/ROOT.ML \ ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \ ex/Set_Algebras.thy ex/SVC_Oracle.thy ex/sledgehammer_tactics.ML \ - ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy \ - ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ + ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ + ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ ex/Unification.thy ex/While_Combinator_Example.thy \ ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ ex/svc_test.thy ../Tools/interpretation_with_defs.ML diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/NSA/NSA.thy Sun Sep 18 16:12:43 2011 -0700 @@ -681,9 +681,10 @@ meta_number_of_approx_reorient); in -val approx_reorient_simproc = - Arith_Data.prep_simproc @{theory} - ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc); + +val approx_reorient_simproc = Simplifier.simproc_global @{theory} + "reorient_simproc" ["0@=x", "1@=x", "number_of w @= x"] reorient_proc; + end; Addsimprocs [approx_reorient_simproc]; diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Sun Sep 18 16:12:43 2011 -0700 @@ -1419,7 +1419,7 @@ (SUP n. \\<^isup>+ x. (INF i:{n..}. u i x) \M)" unfolding liminf_SUPR_INFI using pos u by (intro positive_integral_monotone_convergence_SUP_AE) - (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_subset) + (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono) also have "\ \ liminf (\n. integral\<^isup>P M (u n))" unfolding liminf_SUPR_INFI by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower) diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 18 16:12:43 2011 -0700 @@ -412,7 +412,6 @@ proof (rule antisym) show "(SUP i. integral\<^isup>P M (?g i)) \ ?y" using g_in_G - using [[simp_trace]] by (auto intro!: exI Sup_mono simp: SUP_def) show "?y \ (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq by (auto intro!: SUP_mono positive_integral_mono Max_ge) diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/RealVector.thy Sun Sep 18 16:12:43 2011 -0700 @@ -452,13 +452,13 @@ using open_Union [of "{S, T}"] by simp lemma open_UN [intro]: "\x\A. open (B x) \ open (\x\A. B x)" - unfolding UN_eq by (rule open_Union) auto + unfolding SUP_def by (rule open_Union) auto + +lemma open_Inter [intro]: "finite S \ \T\S. open T \ open (\S)" + by (induct set: finite) auto lemma open_INT [intro]: "finite A \ \x\A. open (B x) \ open (\x\A. B x)" - by (induct set: finite) auto - -lemma open_Inter [intro]: "finite S \ \T\S. open T \ open (\S)" - unfolding Inter_def by (rule open_INT) + unfolding INF_def by (rule open_Inter) auto lemma closed_empty [intro, simp]: "closed {}" unfolding closed_def by simp @@ -466,9 +466,6 @@ lemma closed_Un [intro]: "closed S \ closed T \ closed (S \ T)" unfolding closed_def by auto -lemma closed_Inter [intro]: "\S\K. closed S \ closed (\ K)" - unfolding closed_def Inter_def by auto - lemma closed_UNIV [intro, simp]: "closed UNIV" unfolding closed_def by simp @@ -478,11 +475,14 @@ lemma closed_INT [intro]: "\x\A. closed (B x) \ closed (\x\A. B x)" unfolding closed_def by auto -lemma closed_UN [intro]: "finite A \ \x\A. closed (B x) \ closed (\x\A. B x)" +lemma closed_Inter [intro]: "\S\K. closed S \ closed (\ K)" + unfolding closed_def uminus_Inf by auto + +lemma closed_Union [intro]: "finite S \ \T\S. closed T \ closed (\S)" by (induct set: finite) auto -lemma closed_Union [intro]: "finite S \ \T\S. closed T \ closed (\S)" - unfolding Union_def by (rule closed_UN) +lemma closed_UN [intro]: "finite A \ \x\A. closed (B x) \ closed (\x\A. B x)" + unfolding SUP_def by (rule closed_Union) auto lemma open_closed: "open S \ closed (- S)" unfolding closed_def by simp diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Tools/arith_data.ML Sun Sep 18 16:12:43 2011 -0700 @@ -21,9 +21,6 @@ val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm val simp_all_tac: thm list -> simpset -> tactic val simplify_meta_eq: thm list -> simpset -> thm -> thm - val trans_tac: thm option -> tactic - val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option) - -> simproc val setup: theory -> theory end; @@ -80,21 +77,20 @@ in Const (@{const_name Groups.uminus}, T --> T) $ t end; (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) -fun mk_sum T [] = mk_number T 0 - | mk_sum T [t,u] = mk_plus (t, u) +fun mk_sum T [] = mk_number T 0 + | mk_sum T [t, u] = mk_plus (t, u) | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); (*this version ALWAYS includes a trailing zero*) -fun long_mk_sum T [] = mk_number T 0 +fun long_mk_sum T [] = mk_number T 0 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); (*decompose additions AND subtractions as a sum*) fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (pos, u, ts)) + dest_summing (pos, t, dest_summing (pos, u, ts)) | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (not pos, u, ts)) - | dest_summing (pos, t, ts) = - if pos then t::ts else mk_minus t :: ts; + dest_summing (pos, t, dest_summing (not pos, u, ts)) + | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts; fun dest_sum t = dest_summing (true, t, []); @@ -121,10 +117,4 @@ let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end -fun trans_tac NONE = all_tac - | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); - -fun prep_simproc thy (name, pats, proc) = - Simplifier.simproc_global thy name pats proc; - end; diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Tools/lin_arith.ML Sun Sep 18 16:12:43 2011 -0700 @@ -79,8 +79,8 @@ val empty = {splits = [], inj_consts = [], discrete = []}; val extend = I; fun merge - ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1}, - {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T = + ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1}, + {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T = {splits = Thm.merge_thms (splits1, splits2), inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), discrete = Library.merge (op =) (discrete1, discrete2)}; diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sun Sep 18 16:12:43 2011 -0700 @@ -18,8 +18,7 @@ val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; val numeral_sym_ss = HOL_ss addsimps numeral_syms; -fun rename_numerals th = - simplify numeral_sym_ss (Thm.transfer @{theory} th); +val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory}; (*Utilities*) @@ -143,13 +142,13 @@ (*** Applying CancelNumeralsFun ***) structure CancelNumeralsCommon = - struct - val mk_sum = (fn T:typ => mk_sum) - val dest_sum = dest_Sucs_sum true - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first_coeff = find_first_coeff [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = (fn T : typ => mk_sum) + val dest_sum = dest_Sucs_sum true + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first_coeff = find_first_coeff [] + val trans_tac = Numeral_Simprocs.trans_tac val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac} @@ -161,12 +160,11 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); val simplify_meta_eq = simplify_meta_eq - end; - + val prove_conv = Arith_Data.prove_conv +end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT val bal_add1 = @{thm nat_eq_add_iff1} RS trans @@ -175,7 +173,6 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val bal_add1 = @{thm nat_less_add_iff1} RS trans @@ -184,7 +181,6 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT val bal_add1 = @{thm nat_le_add_iff1} RS trans @@ -193,7 +189,6 @@ structure DiffCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT val bal_add1 = @{thm nat_diff_add_eq1} RS trans @@ -202,7 +197,7 @@ val cancel_numerals = - map (Arith_Data.prep_simproc @{theory}) + map (Numeral_Simprocs.prep_simproc @{theory}) [("nateq_cancel_numerals", ["(l::nat) + m = n", "(l::nat) = m + n", "(l::nat) * m = n", "(l::nat) = m * n", @@ -228,17 +223,17 @@ (*** Applying CombineNumeralsFun ***) structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) - val dest_sum = dest_Sucs_sum false - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val left_distrib = @{thm left_add_mult_distrib} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - fun trans_tac _ = Arith_Data.trans_tac +struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = (fn T : typ => long_mk_sum) (*to work for 2*x + 3*x *) + val dest_sum = dest_Sucs_sum false + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val left_distrib = @{thm left_add_mult_distrib} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = Numeral_Simprocs.trans_tac val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac} val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} @@ -248,23 +243,23 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = simplify_meta_eq - end; + val simplify_meta_eq = simplify_meta_eq +end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); val combine_numerals = - Arith_Data.prep_simproc @{theory} + Numeral_Simprocs.prep_simproc @{theory} ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); (*** Applying CancelNumeralFactorFun ***) structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val trans_tac = Numeral_Simprocs.trans_tac val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac} @@ -275,48 +270,44 @@ val numeral_simp_ss = HOL_ss addsimps bin_simps fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = simplify_meta_eq - end + val simplify_meta_eq = simplify_meta_eq + val prove_conv = Arith_Data.prove_conv +end; structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT val cancel = @{thm nat_mult_div_cancel1} RS trans val neg_exchanges = false -) +); structure DvdCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT val cancel = @{thm nat_mult_dvd_cancel1} RS trans val neg_exchanges = false -) +); structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT val cancel = @{thm nat_mult_eq_cancel1} RS trans val neg_exchanges = false -) +); structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val cancel = @{thm nat_mult_less_cancel1} RS trans val neg_exchanges = true -) +); structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT val cancel = @{thm nat_mult_le_cancel1} RS trans @@ -324,7 +315,7 @@ ) val cancel_numeral_factors = - map (Arith_Data.prep_simproc @{theory}) + map (Numeral_Simprocs.prep_simproc @{theory}) [("nateq_cancel_numeral_factors", ["(l::nat) * m = n", "(l::nat) = m * n"], K EqCancelNumeralFactor.proc), @@ -364,45 +355,42 @@ simplify_one ss (([th, cancel_th]) MRS trans); structure CancelFactorCommon = - struct - val mk_sum = (fn T:typ => long_mk_prod) - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = (fn T : typ => long_mk_prod) + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = Numeral_Simprocs.trans_tac val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) val simplify_meta_eq = cancel_simplify_meta_eq - end; + val prove_conv = Arith_Data.prove_conv +end; structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj} ); +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT + fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} +); + structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} ); -structure LeCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT - fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} -); - structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj} @@ -410,14 +398,13 @@ structure DvdCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} ); val cancel_factor = - map (Arith_Data.prep_simproc @{theory}) + map (Numeral_Simprocs.prep_simproc @{theory}) [("nat_eq_cancel_factor", ["(l::nat) * m = n", "(l::nat) = m * n"], K EqCancelFactor.proc), diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Tools/numeral_simprocs.ML Sun Sep 18 16:12:43 2011 -0700 @@ -16,6 +16,9 @@ signature NUMERAL_SIMPROCS = sig + val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option) + -> simproc + val trans_tac: thm option -> tactic val assoc_fold_simproc: simproc val combine_numerals: simproc val cancel_numerals: simproc list @@ -30,6 +33,12 @@ structure Numeral_Simprocs : NUMERAL_SIMPROCS = struct +fun prep_simproc thy (name, pats, proc) = + Simplifier.simproc_global thy name pats proc; + +fun trans_tac NONE = all_tac + | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); + val mk_number = Arith_Data.mk_number; val mk_sum = Arith_Data.mk_sum; val long_mk_sum = Arith_Data.long_mk_sum; @@ -199,13 +208,13 @@ val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} structure CancelNumeralsCommon = - struct - val mk_sum = mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val find_first_coeff = find_first_coeff [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val find_first_coeff = find_first_coeff [] + val trans_tac = trans_tac fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -215,12 +224,11 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; - + val prove_conv = Arith_Data.prove_conv +end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT val bal_add1 = @{thm eq_add_iff1} RS trans @@ -229,7 +237,6 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val bal_add1 = @{thm less_add_iff1} RS trans @@ -238,7 +245,6 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT val bal_add1 = @{thm le_add_iff1} RS trans @@ -246,7 +252,7 @@ ); val cancel_numerals = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("inteq_cancel_numerals", ["(l::'a::number_ring) + m = n", "(l::'a::number_ring) = m + n", @@ -273,17 +279,17 @@ K LeCancelNumerals.proc)]; structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - fun trans_tac _ = Arith_Data.trans_tac +struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = trans_tac fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -293,23 +299,23 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; +end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); (*Version for fields, where coefficients can be fractions*) structure FieldCombineNumeralsData = - struct - type coeff = int * int - val iszero = (fn (p, q) => p = 0) - val add = add_frac - val mk_sum = long_mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_fcoeff - val dest_coeff = dest_fcoeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - fun trans_tac _ = Arith_Data.trans_tac +struct + type coeff = int * int + val iszero = (fn (p, q) => p = 0) + val add = add_frac + val mk_sum = long_mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_fcoeff + val dest_coeff = dest_fcoeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = trans_tac val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps fun norm_tac ss = @@ -320,18 +326,18 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) - end; +end; structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); val combine_numerals = - Arith_Data.prep_simproc @{theory} + prep_simproc @{theory} ("int_combine_numerals", ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], K CombineNumerals.proc); val field_combine_numerals = - Arith_Data.prep_simproc @{theory} + prep_simproc @{theory} ("field_combine_numerals", ["(i::'a::{field_inverse_zero, number_ring}) + j", "(i::'a::{field_inverse_zero, number_ring}) - j"], @@ -351,15 +357,15 @@ structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); val assoc_fold_simproc = - Arith_Data.prep_simproc @{theory} + prep_simproc @{theory} ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], K Semiring_Times_Assoc.proc); structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val trans_tac = trans_tac val norm_ss1 = HOL_basic_ss addsimps minus_from_mult_simps @ mult_1s val norm_ss2 = HOL_basic_ss addsimps simps @ mult_minus_simps @@ -375,12 +381,12 @@ val simplify_meta_eq = Arith_Data.simplify_meta_eq [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; - end + val prove_conv = Arith_Data.prove_conv +end (*Version for semiring_div*) structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT val cancel = @{thm div_mult_mult1} RS trans @@ -390,7 +396,6 @@ (*Version for fields*) structure DivideCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT val cancel = @{thm mult_divide_mult_cancel_left} RS trans @@ -399,7 +404,6 @@ structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT val cancel = @{thm mult_cancel_left} RS trans @@ -408,7 +412,6 @@ structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val cancel = @{thm mult_less_cancel_left} RS trans @@ -417,7 +420,6 @@ structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT val cancel = @{thm mult_le_cancel_left} RS trans @@ -425,7 +427,7 @@ ) val cancel_numeral_factors = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("ring_eq_cancel_numeral_factor", ["(l::'a::{idom,number_ring}) * m = n", "(l::'a::{idom,number_ring}) = m * n"], @@ -449,7 +451,7 @@ K DivideCancelNumeralFactor.proc)]; val field_cancel_numeral_factors = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("field_eq_cancel_numeral_factor", ["(l::'a::{field,number_ring}) * m = n", "(l::'a::{field,number_ring}) = m * n"], @@ -499,22 +501,22 @@ end structure CancelFactorCommon = - struct - val mk_sum = long_mk_prod - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = long_mk_prod + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = trans_tac val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) val simplify_meta_eq = cancel_simplify_meta_eq - end; + val prove_conv = Arith_Data.prove_conv +end; (*mult_cancel_left requires a ring with no zero divisors.*) structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT fun simp_conv _ _ = SOME @{thm mult_cancel_left} @@ -523,7 +525,6 @@ (*for ordered rings*) structure LeCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT val simp_conv = sign_conv @@ -533,7 +534,6 @@ (*for ordered rings*) structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val simp_conv = sign_conv @@ -543,7 +543,6 @@ (*for semirings with division*) structure DivCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT fun simp_conv _ _ = SOME @{thm div_mult_mult1_if} @@ -551,7 +550,6 @@ structure ModCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT fun simp_conv _ _ = SOME @{thm mod_mult_mult1} @@ -560,7 +558,6 @@ (*for idoms*) structure DvdCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} @@ -569,14 +566,13 @@ (*Version for all fields, including unordered ones (type complex).*) structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} ); val cancel_factors = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("ring_eq_cancel_factor", ["(l::'a::idom) * m = n", "(l::'a::idom) = m * n"], diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Wellfounded.thy Sun Sep 18 16:12:43 2011 -0700 @@ -305,9 +305,7 @@ "[| ALL r:R. wf r; ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} |] ==> wf(Union R)" -apply (simp add: Union_def) -apply (blast intro: wf_UN) -done + using wf_UN[of R "\i. i"] by (simp add: SUP_def) (*Intuition: we find an (R u S)-min element of a nonempty subset A by case distinction. diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Word/Bit_Int.thy --- a/src/HOL/Word/Bit_Int.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Word/Bit_Int.thy Sun Sep 18 16:12:43 2011 -0700 @@ -1,9 +1,9 @@ (* Author: Jeremy Dawson and Gerwin Klein, NICTA - definition and basic theorems for bit-wise logical operations + Definitions and basic theorems for bit-wise logical operations for integers expressed using Pls, Min, BIT, - and converting them to and from lists of bools + and converting them to and from lists of bools. *) header {* Bitwise Operations on Binary Integers *} diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Word/Bit_Representation.thy Sun Sep 18 16:12:43 2011 -0700 @@ -1,8 +1,7 @@ (* Author: Jeremy Dawson, NICTA - contains basic definition to do with integers - expressed using Pls, Min, BIT + Basic definitions to do with integers, expressed using Pls, Min, BIT. *) header {* Basic Definitions for Binary Integers *} @@ -876,8 +875,7 @@ size list = number_of k" by (auto simp: pred_def succ_def split add : split_if_asm) -lemmas ls_splits = - prod.split split_split prod.split_asm split_split_asm split_if_asm +lemmas ls_splits = prod.split prod.split_asm split_if_asm lemma not_B1_is_B0: "y \ (1::bit) \ y = (0::bit)" by (cases y) auto diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Word/Bool_List_Representation.thy Sun Sep 18 16:12:43 2011 -0700 @@ -1,7 +1,7 @@ (* Author: Jeremy Dawson, NICTA - contains theorems to do with integers, expressed using Pls, Min, BIT, + Theorems to do with integers, expressed using Pls, Min, BIT, theorems linking them to lists of booleans, and repeated splitting and concatenation. *) @@ -60,8 +60,10 @@ subsection "Arithmetic in terms of bool lists" -(* arithmetic operations in terms of the reversed bool list, - assuming input list(s) the same length, and don't extend them *) +text {* + Arithmetic operations in terms of the reversed bool list, + assuming input list(s) the same length, and don't extend them. +*} primrec rbl_succ :: "bool list => bool list" where Nil: "rbl_succ Nil = Nil" @@ -72,13 +74,13 @@ | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" primrec rbl_add :: "bool list => bool list => bool list" where - (* result is length of first arg, second arg may be longer *) + -- "result is length of first arg, second arg may be longer" Nil: "rbl_add Nil x = Nil" | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))" primrec rbl_mult :: "bool list => bool list => bool list" where - (* result is length of first arg, second arg may be longer *) + -- "result is length of first arg, second arg may be longer" Nil: "rbl_mult Nil x = Nil" | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in if y then rbl_add ws x else ws)" @@ -112,7 +114,7 @@ bin_to_bl_aux (n - 1) w (True # bl)" by (cases n) auto -(** link between bin and bool list **) +text {* Link between bin and bool list. *} lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Word/Misc_Numeric.thy --- a/src/HOL/Word/Misc_Numeric.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Word/Misc_Numeric.thy Sun Sep 18 16:12:43 2011 -0700 @@ -11,13 +11,6 @@ lemma the_elemI: "y = {x} ==> the_elem y = x" by simp -lemmas split_split = prod.split -lemmas split_split_asm = prod.split_asm -lemmas split_splits = split_split split_split_asm - -lemmas funpow_0 = funpow.simps(1) -lemmas funpow_Suc = funpow.simps(2) - lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto lemma gt_or_eq_0: "0 < y \ 0 = (y::nat)" by arith diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Word/Misc_Typedef.thy --- a/src/HOL/Word/Misc_Typedef.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Word/Misc_Typedef.thy Sun Sep 18 16:12:43 2011 -0700 @@ -1,8 +1,7 @@ (* - Author: Jeremy Dawson and Gerwin Klein, NICTA + Author: Jeremy Dawson and Gerwin Klein, NICTA - consequences of type definition theorems, - and of extended type definition theorems + Consequences of type definition theorems, and of extended type definition. theorems *) header {* Type Definition Theorems *} diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/Word/Word.thy Sun Sep 18 16:12:43 2011 -0700 @@ -4514,7 +4514,7 @@ apply (simp add: mod_nat_add word_size) done -lemma word_neq_0_conv [simp]: +lemma word_neq_0_conv: fixes w :: "'a :: len word" shows "(w \ 0) = (0 < w)" proof - diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/HOL/ex/ROOT.ML Sun Sep 18 16:12:43 2011 -0700 @@ -71,7 +71,8 @@ "Quicksort", "Birthday_Paradox", "List_to_Set_Comprehension_Examples", - "Set_Algebras" + "Set_Algebras", + "Seq" ]; if getenv "ISABELLE_GHC" = "" then () diff -r b36eedcd1633 -r 6e6e958b2d40 src/HOL/ex/Seq.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Seq.thy Sun Sep 18 16:12:43 2011 -0700 @@ -0,0 +1,35 @@ +(* Title: HOL/ex/Seq.thy + Author: Makarius +*) + +header {* Finite sequences *} + +theory Seq +imports Main +begin + +datatype 'a seq = Empty | Seq 'a "'a seq" + +fun conc :: "'a seq \ 'a seq \ 'a seq" +where + "conc Empty ys = ys" +| "conc (Seq x xs) ys = Seq x (conc xs ys)" + +fun reverse :: "'a seq \ 'a seq" +where + "reverse Empty = Empty" +| "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)" + +lemma conc_empty: "conc xs Empty = xs" + by (induct xs) simp_all + +lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)" + by (induct xs) simp_all + +lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)" + by (induct xs) (simp_all add: conc_empty conc_assoc) + +lemma reverse_reverse: "reverse (reverse xs) = xs" + by (induct xs) (simp_all add: reverse_conc) + +end diff -r b36eedcd1633 -r 6e6e958b2d40 src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Sun Sep 18 16:12:43 2011 -0700 @@ -29,7 +29,7 @@ as with < and <= but not = and div*) (*proof tools*) val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option - val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) + val trans_tac: thm option -> tactic (*applies the initial lemma*) val norm_tac: simpset -> tactic (*proves the initial lemma*) val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) @@ -72,7 +72,7 @@ in Option.map (export o Data.simplify_meta_eq ss) (Data.prove_conv - [Data.trans_tac ss reshape, rtac Data.cancel 1, + [Data.trans_tac reshape, rtac Data.cancel 1, Data.numeral_simp_tac ss] ctxt prems (t', rhs)) end (* FIXME avoid handling of generic exceptions *) diff -r b36eedcd1633 -r 6e6e958b2d40 src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Provers/Arith/cancel_numerals.ML Sun Sep 18 16:12:43 2011 -0700 @@ -36,7 +36,7 @@ val bal_add2: thm (*proof tools*) val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option - val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) + val trans_tac: thm option -> tactic (*applies the initial lemma*) val norm_tac: simpset -> tactic (*proves the initial lemma*) val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) @@ -92,12 +92,12 @@ Option.map (export o Data.simplify_meta_eq ss) (if n2 <= n1 then Data.prove_conv - [Data.trans_tac ss reshape, rtac Data.bal_add1 1, + [Data.trans_tac reshape, rtac Data.bal_add1 1, Data.numeral_simp_tac ss] ctxt prems (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2')) else Data.prove_conv - [Data.trans_tac ss reshape, rtac Data.bal_add2 1, + [Data.trans_tac reshape, rtac Data.bal_add2 1, Data.numeral_simp_tac ss] ctxt prems (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2')))) end diff -r b36eedcd1633 -r 6e6e958b2d40 src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Provers/Arith/combine_numerals.ML Sun Sep 18 16:12:43 2011 -0700 @@ -29,7 +29,7 @@ val left_distrib: thm (*proof tools*) val prove_conv: tactic list -> Proof.context -> term * term -> thm option - val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) + val trans_tac: thm option -> tactic (*applies the initial lemma*) val norm_tac: simpset -> tactic (*proves the initial lemma*) val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) @@ -83,7 +83,7 @@ in Option.map (export o Data.simplify_meta_eq ss) (Data.prove_conv - [Data.trans_tac ss reshape, rtac Data.left_distrib 1, + [Data.trans_tac reshape, rtac Data.left_distrib 1, Data.numeral_simp_tac ss] ctxt (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) end diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/General/symbol.scala Sun Sep 18 16:12:43 2011 -0700 @@ -115,6 +115,8 @@ } } + def explode(text: CharSequence): List[Symbol] = iterator(text).toList + /* decoding offsets */ diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/PIDE/command.scala Sun Sep 18 16:12:43 2011 -0700 @@ -80,7 +80,7 @@ /* dummy commands */ def unparsed(source: String): Command = - new Command(Document.no_id, Document.Node.Name("", "", ""), + new Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source))) def span(node_name: Document.Node.Name, toks: List[Token]): Command = diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/PIDE/document.ML Sun Sep 18 16:12:43 2011 -0700 @@ -15,7 +15,7 @@ val new_id: unit -> id val parse_id: string -> id val print_id: id -> string - type node_header = (string * string list * (string * bool) list) Exn.result + type node_header = ((string * string) * string list * (string * bool) list) Exn.result datatype node_edit = Clear | Edits of (command_id option * command_id option) list | @@ -58,7 +58,7 @@ (** document structure **) -type node_header = (string * string list * (string * bool) list) Exn.result; +type node_header = ((string * string) * string list * (string * bool) list) Exn.result; type perspective = (command_id -> bool) * command_id option; (*visible commands, last*) structure Entries = Linear_Set(type key = command_id val ord = int_ord); @@ -435,14 +435,11 @@ is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *) is_some (Exn.get_res (get_header (get_node nodes name))); -fun init_theory deps name node = +fun init_theory deps node = let - val (thy_name, imports, uses) = Exn.release (get_header node); - (* FIXME provide files via Scala layer *) - val (dir, files) = - if ML_System.platform_is_cygwin then (Path.current, []) - else (Path.dir (Path.explode name), map (apfst Path.explode) uses); - + (* FIXME provide files via Scala layer, not master_dir *) + val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node); + val files = map (apfst Path.explode) uses; val parents = imports |> map (fn import => (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) @@ -450,7 +447,7 @@ | NONE => get_theory (Position.file_only import) (snd (Future.join (the (AList.lookup (op =) deps import)))))); - in Thy_Load.begin_theory dir thy_name imports files parents end; + in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end; in @@ -471,7 +468,7 @@ else let val node0 = node_of old_version name; - fun init () = init_theory deps name node; + fun init () = init_theory deps node; val bad_init = not (check_theory nodes name andalso forall (check_theory nodes o #1) deps); in diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/PIDE/document.scala Sun Sep 18 16:12:43 2011 -0700 @@ -39,6 +39,17 @@ object Node { + object Name + { + val empty = Name("", "", "") + def apply(path: Path): Name = + { + val node = path.implode + val dir = path.dir.implode + val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path) + Name(node, dir, theory) + } + } sealed case class Name(node: String, dir: String, theory: String) { override def hashCode: Int = node.hashCode @@ -162,6 +173,20 @@ type Nodes = Map[Node.Name, Node] sealed case class Version(val id: Version_ID, val nodes: Nodes) + { + def topological_order: List[Node.Name] = + { + val names = nodes.map({ case (name, node) => (name.node -> name) }) + def next(x: Node.Name): List[Node.Name] = + nodes(x).header match { + case Exn.Res(header) => + for (imp <- header.imports; name <- names.get(imp)) yield(name) + case Exn.Exn(_) => Nil + } + Library.topological_order(next, + Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList)) + } + } /* changes of plain text, eventually resulting in document edits */ diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/PIDE/isar_document.ML Sun Sep 18 16:12:43 2011 -0700 @@ -47,7 +47,8 @@ fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => Document.Header - (Exn.Res (triple string (list string) (list (pair string bool)) a)), + (Exn.Res + (triple (pair string string) (list string) (list (pair string bool)) a)), fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), fn (a, []) => Document.Perspective (map int_atom a)])) end; diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/PIDE/isar_document.scala Sun Sep 18 16:12:43 2011 -0700 @@ -191,17 +191,24 @@ val edits_yxml = { import XML.Encode._ def id: T[Command] = (cmd => long(cmd.id)) - def encode: T[List[Document.Edit_Command]] = - list(pair((name => string(name.node)), - variant(List( - { case Document.Node.Clear() => (Nil, Nil) }, - { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, - { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => - (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) }, - { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, - { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })))) + def encode_edit(dir: String) + : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = + variant(List( + { case Document.Node.Clear() => (Nil, Nil) }, + { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, + { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => + (Nil, + triple(pair(string, string), list(string), list(pair(string, bool)))( + (dir, a), b, c)) }, + { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, + { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) + def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => + { + val (name, edit) = node_edit + val dir = Isabelle_System.posix_path(name.dir) + pair(string, encode_edit(dir))(name.node, edit) + }) YXML.string_of_body(encode(edits)) } - input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml) } diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/System/session.scala Sun Sep 18 16:12:43 2011 -0700 @@ -36,7 +36,7 @@ } -class Session(thy_load: Thy_Load) +class Session(thy_load: Thy_Load = new Thy_Load) { /* real time parameters */ // FIXME properties or settings (!?) @@ -107,7 +107,8 @@ private val global_state = new Volatile(Document.State.init) def current_state(): Document.State = global_state() - def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot = + def snapshot(name: Document.Node.Name = Document.Node.Name.empty, + pending_edits: List[Text.Edit] = Nil): Document.Snapshot = global_state().snapshot(name, pending_edits) diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/Thy/thy_info.scala Sun Sep 18 16:12:43 2011 -0700 @@ -47,16 +47,19 @@ Document.Node.Name(node, dir1, theory) } - type Deps = Map[Document.Node.Name, Document.Node_Header] + type Dep = (Document.Node.Name, Document.Node_Header) + private type Required = (List[Dep], Set[Document.Node.Name]) private def require_thys(initiators: List[Document.Node.Name], - deps: Deps, names: List[Document.Node.Name]): Deps = - (deps /: names)(require_thy(initiators, _, _)) + required: Required, names: List[Document.Node.Name]): Required = + (required /: names)(require_thy(initiators, _, _)) private def require_thy(initiators: List[Document.Node.Name], - deps: Deps, name: Document.Node.Name): Deps = + required: Required, name: Document.Node.Name): Required = { - if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps + val (deps, seen) = required + if (seen(name)) required + else if (thy_load.is_loaded(name.theory)) (deps, seen + name) else { try { if (initiators.contains(name)) error(cycle_msg(initiators)) @@ -68,12 +71,13 @@ quote(name.theory) + required_by(initiators)) } val imports = header.imports.map(import_name(name.dir, _)) - require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports) + val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports) + ((name, Exn.Res(header)) :: deps1, seen1) } - catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } + catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) } } } - def dependencies(names: List[Document.Node.Name]): Deps = - require_thys(Nil, Map.empty, names) + def dependencies(names: List[Document.Node.Name]): List[Dep] = + require_thys(Nil, (Nil, Set.empty), names)._1.reverse } diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/Thy/thy_load.scala Sun Sep 18 16:12:43 2011 -0700 @@ -6,11 +6,34 @@ package isabelle -abstract class Thy_Load + +import java.io.File + + + +class Thy_Load { - def register_thy(thy_name: String) - def is_loaded(thy_name: String): Boolean - def append(dir: String, path: Path): String - def check_thy(node_name: Document.Node.Name): Thy_Header + /* loaded theories provided by prover */ + + private var loaded_theories: Set[String] = Set() + + def register_thy(thy_name: String): Unit = + synchronized { loaded_theories += thy_name } + + def is_loaded(thy_name: String): Boolean = + synchronized { loaded_theories.contains(thy_name) } + + + /* file-system operations */ + + def append(dir: String, source_path: Path): String = + (Path.explode(dir) + source_path).implode + + def check_thy(name: Document.Node.Name): Thy_Header = + { + val file = new File(name.node) + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) + Thy_Header.read(file) + } } diff -r b36eedcd1633 -r 6e6e958b2d40 src/Pure/library.scala --- a/src/Pure/library.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Pure/library.scala Sun Sep 18 16:12:43 2011 -0700 @@ -139,6 +139,26 @@ } + /* graph traversal */ + + def topological_order[A](next: A => Iterable[A], starts: Iterable[A]): List[A] = + { + type Reached = (List[A], Set[A]) + def reach(reached: Reached, x: A): Reached = + { + val (rs, r_set) = reached + if (r_set(x)) reached + else { + val (rs1, r_set1) = reachs((rs, r_set + x), next(x)) + (x :: rs1, r_set1) + } + } + def reachs(reached: Reached, xs: Iterable[A]): Reached = (reached /: xs)(reach) + + reachs((Nil, Set.empty), starts)._1.reverse + } + + /* simple dialogs */ private def simple_dialog(kind: Int, default_title: String) diff -r b36eedcd1633 -r 6e6e958b2d40 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Tools/Code/code_haskell.ML Sun Sep 18 16:12:43 2011 -0700 @@ -17,13 +17,13 @@ val target = "Haskell"; val language_extensions = - ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"]; + ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"]; val language_pragma = - "{-# LANGUAGE " ^ commas language_extensions ^ " #-}"; + "{-# LANGUAGE " ^ commas language_extensions ^ " #-}"; val language_params = - space_implode " " (map (prefix "-X") language_extensions); + space_implode " " (map (prefix "-X") language_extensions); open Basic_Code_Thingol; open Code_Printer; diff -r b36eedcd1633 -r 6e6e958b2d40 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Tools/induct.ML Sun Sep 18 16:12:43 2011 -0700 @@ -746,10 +746,16 @@ |> tap (trace_rules ctxt inductN o map #2) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); - fun rule_cases ctxt rule = - let val rule' = (if simp then simplified_rule ctxt else I) - (Rule_Cases.internalize_params rule); - in Rule_Cases.make_nested (Thm.prop_of rule') (rulified_term rule') end; + fun rule_cases ctxt rule cases = + let + val rule' = Rule_Cases.internalize_params rule; + val rule'' = (if simp then simplified_rule ctxt else I) rule'; + val nonames = map (fn ((cn,_),cls) => ((cn,[]),cls)) + val cases' = + if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases + in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') + cases' + end; in (fn i => fn st => ruleq diff -r b36eedcd1633 -r 6e6e958b2d40 src/Tools/jEdit/etc/settings --- a/src/Tools/jEdit/etc/settings Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Tools/jEdit/etc/settings Sun Sep 18 16:12:43 2011 -0700 @@ -3,7 +3,7 @@ JEDIT_HOME="$COMPONENT" JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit" -JEDIT_OPTIONS="-reuseview -noserver -nobackground" +JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9" JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" #JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit" diff -r b36eedcd1633 -r 6e6e958b2d40 src/Tools/jEdit/src/jedit_thy_load.scala --- a/src/Tools/jEdit/src/jedit_thy_load.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala Sun Sep 18 16:12:43 2011 -0700 @@ -9,30 +9,16 @@ import isabelle._ -import java.io.File +import java.io.{File, IOException} import javax.swing.text.Segment -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} import org.gjt.sp.jedit.MiscUtilities +import org.gjt.sp.jedit.View class JEdit_Thy_Load extends Thy_Load { - /* loaded theories provided by prover */ - - private var loaded_theories: Set[String] = Set() - - override def register_thy(thy_name: String) - { - synchronized { loaded_theories += thy_name } - } - - override def is_loaded(thy_name: String): Boolean = - synchronized { loaded_theories.contains(thy_name) } - - - /* file-system operations */ - override def append(dir: String, source_path: Path): String = { val path = source_path.expand @@ -46,6 +32,26 @@ } } + def check_file(view: View, path: String): Boolean = + { + val vfs = VFSManager.getVFSForPath(path) + val session = vfs.createVFSSession(path, view) + + try { + session != null && { + try { + val file = vfs._getFile(session, path, view) + file != null && file.isReadable && file.getType == VFSFile.FILE + } + catch { case _: IOException => false } + } + } + finally { + try { vfs._endVFSSession(session, view) } + catch { case _: IOException => } + } + } + override def check_thy(name: Document.Node.Name): Thy_Header = { Swing_Thread.now { diff -r b36eedcd1633 -r 6e6e958b2d40 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Tools/jEdit/src/plugin.scala Sun Sep 18 16:12:43 2011 -0700 @@ -37,6 +37,9 @@ var plugin: Plugin = null var session: Session = null + val thy_load = new JEdit_Thy_Load + val thy_info = new Thy_Info(thy_load) + /* properties */ @@ -360,12 +363,11 @@ { /* theory files */ - val thy_load = new JEdit_Thy_Load - val thy_info = new Thy_Info(thy_load) - private lazy val delay_load = Swing_Thread.delay_last(Isabelle.session.load_delay) { + val view = jEdit.getActiveView() + val buffers = Isabelle.jedit_buffers().toList def loaded_buffer(name: String): Boolean = buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) @@ -373,7 +375,8 @@ val thys = for (buffer <- buffers; model <- Isabelle.document_model(buffer)) yield model.name - val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _) + val files = Isabelle.thy_info.dependencies(thys).map(_._1.node). + filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file)) if (!files.isEmpty) { val files_list = new ListView(Library.sort_strings(files)) @@ -381,15 +384,17 @@ files_list.selection.indices += i val answer = - Library.confirm_dialog(jEdit.getActiveView(), + Library.confirm_dialog(view, "Auto loading of required files", JOptionPane.YES_NO_OPTION, "The following files are required to resolve theory imports.", "Reload selected files now?", new ScrollPane(files_list)) if (answer == 0) - files_list.selection.items foreach (file => - if (!loaded_buffer(file)) jEdit.openFile(null: View, file)) + for { + file <- files + if files_list.selection.items.contains(file) + } jEdit.openFile(null: View, file) } } @@ -472,7 +477,7 @@ Isabelle.setup_tooltips() Isabelle_System.init() Isabelle_System.install_fonts() - Isabelle.session = new Session(thy_load) + Isabelle.session = new Session(Isabelle.thy_load) SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) if (ModeProvider.instance.isInstanceOf[ModeProvider]) ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) diff -r b36eedcd1633 -r 6e6e958b2d40 src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Thu Sep 15 10:12:36 2011 -0700 +++ b/src/Tools/jEdit/src/session_dockable.scala Sun Sep 18 16:12:43 2011 -0700 @@ -10,13 +10,13 @@ import isabelle._ import scala.actors.Actor._ -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, TabbedPane, Component, Swing} import scala.swing.event.{ButtonClicked, SelectionChanged} import java.lang.System -import java.awt.{BorderLayout, Graphics} -import javax.swing.{JList, DefaultListCellRenderer} +import java.awt.{BorderLayout, Graphics2D, Insets} +import javax.swing.{JList, DefaultListCellRenderer, UIManager} import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} @@ -29,7 +29,7 @@ private val readme = new HTML_Panel("SansSerif", 14) readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html")))) - val status = new ListView(Nil: List[String]) + val status = new ListView(Nil: List[Document.Node.Name]) status.peer.setLayoutOrientation(JList.VERTICAL_WRAP) status.selection.intervalMode = ListView.IntervalMode.Single @@ -86,15 +86,22 @@ private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty - val node_renderer = new DefaultListCellRenderer + private class Node_Renderer_Component extends Label { - override def paintComponent(gfx: Graphics) + xAlignment = Alignment.Leading + border = UIManager.getBorder("List.cellNoFocusBorder") + val empty_insets = new Insets(0, 0, 0, 0) + + var node_name = Document.Node.Name.empty + override def paintComponent(gfx: Graphics2D) { - nodes_status.get(Document.Node.Name(getText, "", "")) match { + nodes_status.get(node_name) match { case Some(st) if st.total > 0 => - val w = getWidth - val h = getHeight - var end = w + val size = peer.getSize() + val insets = if (border == null) empty_insets else border.getBorderInsets(this.peer) + val w = size.width - insets.left - insets.right + val h = size.height - insets.top - insets.bottom + var end = size.width - insets.right for { (n, color) <- List( (st.unprocessed, Isabelle_Markup.unprocessed1_color), @@ -103,7 +110,7 @@ { gfx.setColor(color) val v = (n * w / st.total) max (if (n > 0) 2 else 0) - gfx.fillRect(end - v, 0, v, h) + gfx.fillRect(end - v, insets.top, v, h) end -= v } case _ => @@ -112,27 +119,40 @@ } } - status.peer.setCellRenderer(node_renderer) + private class Node_Renderer extends + ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component]( + new Node_Renderer_Component) + { + def configure(list: ListView[_], isSelected: Boolean, focused: Boolean, + name: Document.Node.Name, index: Int) + { + component.opaque = false + component.background = list.background + component.foreground = list.foreground + component.node_name = name + component.text = name.theory + " " + } + } + status.renderer = new Node_Renderer private def handle_changed(changed_nodes: Set[Document.Node.Name]) { Swing_Thread.now { // FIXME correlation to changed_nodes!? - val state = Isabelle.session.current_state() - val version = state.recent_stable.version.get_finished + val snapshot = Isabelle.session.snapshot() var nodes_status1 = nodes_status for { name <- changed_nodes - node <- version.nodes.get(name) - val status = Isar_Document.node_status(state, version, node) + node <- snapshot.version.nodes.get(name) + val status = Isar_Document.node_status(snapshot.state, snapshot.version, node) } nodes_status1 += (name -> status) if (nodes_status != nodes_status1) { nodes_status = nodes_status1 status.listData = - Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList) - .map(_.node) + snapshot.version.topological_order.filter( + (name: Document.Node.Name) => nodes_status.isDefinedAt(name)) } } } diff -r b36eedcd1633 -r 6e6e958b2d40 src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/ZF/arith_data.ML Sun Sep 18 16:12:43 2011 -0700 @@ -165,7 +165,7 @@ val dest_bal = FOLogic.dest_eq val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans} val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans} - fun trans_tac _ = gen_trans_tac @{thm iff_trans} + val trans_tac = gen_trans_tac @{thm iff_trans} end; structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData); @@ -178,7 +178,7 @@ val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans} val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans} - fun trans_tac _ = gen_trans_tac @{thm iff_trans} + val trans_tac = gen_trans_tac @{thm iff_trans} end; structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData); @@ -191,7 +191,7 @@ val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT val bal_add1 = @{thm diff_add_eq} RS @{thm trans} val bal_add2 = @{thm diff_add_eq} RS @{thm trans} - fun trans_tac _ = gen_trans_tac @{thm trans} + val trans_tac = gen_trans_tac @{thm trans} end; structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData); diff -r b36eedcd1633 -r 6e6e958b2d40 src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Thu Sep 15 10:12:36 2011 -0700 +++ b/src/ZF/int_arith.ML Sun Sep 18 16:12:43 2011 -0700 @@ -156,7 +156,7 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val find_first_coeff = find_first_coeff [] - fun trans_tac _ = ArithData.gen_trans_tac @{thm iff_trans} + val trans_tac = ArithData.gen_trans_tac @{thm iff_trans} val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys @@ -234,7 +234,7 @@ val dest_coeff = dest_coeff 1 val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans} val prove_conv = prove_conv_nohyps "int_combine_numerals" - fun trans_tac _ = ArithData.gen_trans_tac @{thm trans} + val trans_tac = ArithData.gen_trans_tac @{thm trans} val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys @@ -276,7 +276,7 @@ fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans} val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" - fun trans_tac _ = ArithData.gen_trans_tac @{thm trans} + val trans_tac = ArithData.gen_trans_tac @{thm trans}