--- 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:
--- 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
--- 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).
--- 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))
->
-> ;;
--- 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[@]}"
-
--- 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
--- 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=""
--- 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"
--- 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")
--- /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"
+
--- 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)
--- 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
-----------------------------
--- 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<DIM('a). P (basis i)".
-
-* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
-to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants
-"Cart_nth" and "Cart_lambda" have been respectively renamed to
-"vec_nth" and "vec_lambda"; theorems mentioning those names have
-changed to match. Definition theorems for overloaded constants now use
-the standard "foo_vec_def" naming scheme. A few other theorems have
-been renamed as follows (INCOMPATIBILITY):
-
- Cart_eq ~> 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<DIM('a). P (basis i)".
+
+* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
+to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants
+"Cart_nth" and "Cart_lambda" have been respectively renamed to
+"vec_nth" and "vec_lambda"; theorems mentioning those names have
+changed to match. Definition theorems for overloaded constants now use
+the standard "foo_vec_def" naming scheme. A few other theorems have
+been renamed as follows (INCOMPATIBILITY):
+
+ Cart_eq ~> 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 \<bind> and \<then>
(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:
--- 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).
--- 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 {
--- 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
--- 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 \<Rightarrow> 'a::Inf"}\\
-@{const Complete_Lattice.Sup} & @{term_type_only Complete_Lattice.Sup "'a set \<Rightarrow> 'a::Sup"}\\
+@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\
+@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\
\end{tabular}
\subsubsection*{Syntax}
--- 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
--- /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")" "$@"
--- 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 \<noteq> 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 "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> 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 \<noteq> 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 \<noteq> 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 "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> 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) ==>
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
--- 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 @@
"\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
by auto
-
text {* Legacy names *}
lemma (in complete_lattice) Inf_singleton [simp]:
@@ -1142,68 +1141,9 @@
"\<Squnion>{a} = a"
by simp
-lemma (in complete_lattice) Inf_binary:
- "\<Sqinter>{a, b} = a \<sqinter> b"
- by simp
-
-lemma (in complete_lattice) Sup_binary:
- "\<Squnion>{a, b} = a \<squnion> b"
- by simp
-
-text {* Grep and put to news from here *}
-
-lemma (in complete_lattice) INF_eq:
- "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
- by (simp add: INF_def image_def)
-
-lemma (in complete_lattice) SUP_eq:
- "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
- by (simp add: SUP_def image_def)
-
-lemma (in complete_lattice) INF_subset:
- "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
- by (rule INF_superset_mono) auto
-
-lemma (in complete_lattice) INF_UNIV_range:
- "(\<Sqinter>x. f x) = \<Sqinter>range f"
- by (fact INF_def)
-
-lemma (in complete_lattice) SUP_UNIV_range:
- "(\<Squnion>x. f x) = \<Squnion>range f"
- by (fact SUP_def)
-
-lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
- by simp
-
-lemma INTER_eq_Inter_image:
- "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (fact INF_def)
-
-lemma Inter_def:
- "\<Inter>S = (\<Inter>x\<in>S. x)"
- by (simp add: INTER_eq_Inter_image image_def)
-
-lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
- by (fact INF_eq)
-
-lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
- by blast
-
-lemma UNION_eq_Union_image:
- "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
- by (fact SUP_def)
-
-lemma Union_def:
- "\<Union>S = (\<Union>x\<in>S. x)"
- by (simp add: UNION_eq_Union_image image_def)
-
lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
by blast
-lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
- by (fact SUP_eq)
-
-
text {* Finally *}
no_notation
--- 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 \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
-assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
-assumes above: "x0 \<sqsubseteq> pfp_above f x0"
+fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
begin
fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> '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) \<squnion> (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) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> 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) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
proof(induct "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
--- 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 =
--- 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 \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_above n f x0 = iter n (\<lambda>x. x0 \<squnion> f x) x0"
+abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
-lemma iter_above_pfp:
-shows "f(iter_above n f x0) \<sqsubseteq> iter_above n f x0" and "x0 \<sqsubseteq> iter_above n f x0"
-using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"]
-by(auto simp add: iter_above_def)
+lemma iter'_pfp_above:
+ "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
+using iter_pfp[of "\<lambda>x. x0 \<squnion> 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 \<noteq> Top \<Longrightarrow> \<exists>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 \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above n f x0 \<sqsubseteq> p"
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
proof-
- let ?F = "\<lambda>x. x0 \<squnion> f x"
- obtain k where "iter_above n f x0 = (?F^^k) x0"
- using iter_funpow `iter_above n f x0 \<noteq> 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 \<noteq> Top`] by blast
moreover
- { fix n have "(?F^^n) x0 \<sqsubseteq> p"
+ { fix n have "(f^^n) x0 \<sqsubseteq> p"
proof(induct n)
case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
next
@@ -81,24 +78,6 @@
} ultimately show ?thesis by simp
qed
-lemma chain: assumes "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-shows "((\<lambda>x. x0 \<squnion> f x)^^i) x0 \<sqsubseteq> ((\<lambda>x. x0 \<squnion> 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 \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
-shows "iter_above n f x0 \<sqsubseteq> x0 \<squnion> f(iter_above n f x0)"
-proof-
- let ?p = "iter_above n f x0"
- obtain k where 1: "?p = ((\<lambda>x. x0 \<squnion> f x)^^k) x0"
- using iter_funpow `?p \<noteq> 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 \<Rightarrow> 'a"
locale Abs_Int_Fun = Val_abs +
-fixes pfp_above :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
-assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
-assumes above: "x0 \<sqsubseteq> pfp_above f x0"
+fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
+assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
+assumes above: "x \<sqsubseteq> pfp f x"
begin
fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> '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) \<squnion> (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) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> 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) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
proof(induct "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
--- 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 \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
-assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
-assumes above: "x0 \<sqsubseteq> pfp_above f x0"
+fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> 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) \<squnion> AI c2 (bfilter b False S)" |
"AI (WHILE b DO c) S =
- bfilter b False (pfp_above (\<lambda>S. AI c (bfilter b True S)) S)"
+ bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> 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 (\<lambda>S. AI c (bfilter b True S)) S"
+ let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
{ fix s t
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
t <:: bfilter b False ?P"
--- 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
--- 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 \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_above m n f x =
+definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' m n f x =
(let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
-lemma iter_above_pfp:
-shows "f(iter_above m n f x0) \<sqsubseteq> iter_above m n f x0"
-and "x0 \<sqsubseteq> iter_above m n f x0"
+lemma iter'_pfp_above:
+shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
+and "x0 \<sqsubseteq> iter' m n f x0"
using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> 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)"
--- 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]:
"((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> 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]:
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> 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
--- 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
--- 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];
--- 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. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>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 "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
unfolding liminf_SUPR_INFI
by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
--- 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)) \<le> ?y"
using g_in_G
- using [[simp_trace]]
by (auto intro!: exI Sup_mono simp: SUP_def)
show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq
by (auto intro!: SUP_mono positive_integral_mono Max_ge)
--- 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]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>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 \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
+ by (induct set: finite) auto
lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
- by (induct set: finite) auto
-
-lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>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 \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
unfolding closed_def by auto
-lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> 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]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
unfolding closed_def by auto
-lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+ unfolding closed_def uminus_Inf by auto
+
+lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
by (induct set: finite) auto
-lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
- unfolding Union_def by (rule closed_UN)
+lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+ unfolding SUP_def by (rule closed_Union) auto
lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
unfolding closed_def by simp
--- 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;
--- 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)};
--- 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),
--- 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"],
--- 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 "\<lambda>i. i"] by (simp add: SUP_def)
(*Intuition: we find an (R u S)-min element of a nonempty subset A
by case distinction.
--- 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 *}
--- 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 \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
by (cases y) auto
--- 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)"
--- 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 \<or> 0 = (y::nat)" by arith
--- 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 *}
--- 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 \<noteq> 0) = (0 < w)"
proof -
--- 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 ()
--- /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 \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
+where
+ "conc Empty ys = ys"
+| "conc (Seq x xs) ys = Seq x (conc xs ys)"
+
+fun reverse :: "'a seq \<Rightarrow> '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
--- 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 *)
--- 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
--- 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
--- 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 */
--- 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 =
--- 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
--- 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 */
--- 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;
--- 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)
}
--- 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)
--- 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
}
--- 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)
+ }
}
--- 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)
--- 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;
--- 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
--- 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"
--- 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 {
--- 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)
--- 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))
}
}
}
--- 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);
--- 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}