--- a/.hgtags Fri Dec 04 11:04:07 2009 +0100
+++ b/.hgtags Fri Dec 04 11:19:00 2009 +0100
@@ -24,6 +24,4 @@
f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
-9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
-9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
-4328de748fb2ceffe4ad5a6d5fbf3347f6aecfa6 isa2009-1-test
+6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
--- a/ANNOUNCE Fri Dec 04 11:04:07 2009 +0100
+++ b/ANNOUNCE Fri Dec 04 11:19:00 2009 +0100
@@ -26,11 +26,16 @@
* HOL: various parts of multivariate analysis.
+* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
+arithmetic, based on external semidefinite programming solvers.
+
* HOLCF: new definitional domain package.
* Revised tutorial on locales.
-* Support for Poly/ML 5.3.0, with improved reporting of compiler
+* ML: tacticals for subgoal focus.
+
+* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
errors and run-time exceptions, including detailed source positions.
* Parallel checking of nested Isar proofs, with improved scalability
--- a/Admin/MacOS/App1/script Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/MacOS/App1/script Fri Dec 04 11:19:00 2009 +0100
@@ -48,8 +48,9 @@
/Applications/Emacs.app/Contents/MacOS/Emacs \
"")"
+declare -a EMACS_OPTIONS=()
if [ -n "$PROOFGENERAL_EMACS" ]; then
- EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
+ EMACS_OPTIONS=(-p "$PROOFGENERAL_EMACS")
fi
@@ -57,7 +58,7 @@
OUTPUT="/tmp/isabelle$$.out"
-( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
+( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
RC=$?
if [ "$RC" != 0 ]; then
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/interface Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,262 @@
+#!/usr/bin/env bash
+#
+# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
+#
+# Proof General interface wrapper for Isabelle.
+
+
+## self references
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+SUPER="$(cd "$THIS/.."; pwd)"
+
+
+## diagnostics
+
+usage()
+{
+ echo
+ echo "Usage: Isabelle [OPTIONS] [FILES ...]"
+ echo
+ echo " Options are:"
+ echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
+ echo " -L NAME abbreviates -l NAME -k NAME"
+ echo " -P BOOL actually start Proof General (default true), otherwise"
+ echo " run plain tty session"
+ echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
+ echo " -X BOOL configure the X-Symbol package on startup (default true)"
+ echo " -f SIZE set X-Symbol font size (default 12)"
+ 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 enable the X-Symbol package on startup (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=""
+ISAR="true"
+START_PG="true"
+GEOMETRY=""
+KEYWORDS=""
+LOGIC="$ISABELLE_LOGIC"
+PROGNAME="emacs"
+INITFILE="true"
+WINDOWSYSTEM="true"
+XSYMBOL=""
+XSYMBOL_SETUP=true
+XSYMBOL_FONTSIZE="12"
+UNICODE=""
+
+getoptions()
+{
+ OPTIND=1
+ while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
+ do
+ case "$OPT" in
+ I)
+ ISAR="$OPTARG"
+ ;;
+ L)
+ KEYWORDS="$OPTARG"
+ LOGIC="$OPTARG"
+ ;;
+ P)
+ START_PG="$OPTARG"
+ ;;
+ U)
+ UNICODE="$OPTARG"
+ ;;
+ X)
+ XSYMBOL_SETUP="$OPTARG"
+ ;;
+ f)
+ XSYMBOL_FONTSIZE="$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)
+ XSYMBOL="$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
+
+
+## smart X11 font installation
+
+function checkfonts ()
+{
+ XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
+
+ case "$XLSFONTS" in
+ xlsfonts:*)
+ return 1
+ ;;
+ esac
+
+ return 0
+}
+
+function installfonts ()
+{
+ checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
+}
+
+
+## main
+
+# Isabelle2008 compatibility
+[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
+[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
+
+if [ "$START_PG" = false ]; then
+
+ [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
+ exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
+
+else
+
+ declare -a ARGS=()
+
+ if [ -n "$GEOMETRY" ]; then
+ ARGS["${#ARGS[@]}"]="-geometry"
+ ARGS["${#ARGS[@]}"]="$GEOMETRY"
+ fi
+
+ [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
+
+ if [ "$WINDOWSYSTEM" = false ]; then
+ ARGS["${#ARGS[@]}"]="-nw"
+ XSYMBOL=false
+ elif [ -z "$DISPLAY" ]; then
+ XSYMBOL=false
+ else
+ [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
+ fi
+
+ if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
+ then
+ if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
+ then
+ cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
+ cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
+ sleep 3
+ fi
+ fi
+
+ 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_XSYMBOL="$XSYMBOL"
+ export PROOFGENERAL_UNICODE="$UNICODE"
+
+ export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
+
+ exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
+
+fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/isar-antiq-regexp.patch Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,21 @@
+--- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200
++++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200
+@@ -252,14 +252,9 @@
+
+ ;; antiquotations
+
+-;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
+-;; incomplete antiquotations like @{text bla"} (even though it is supposed to
+-;; stop at eol anyway).
+-
+-(defconst isar-antiq-regexp
+- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
+- "Regexp matching Isabelle/Isar antiquoations.")
+-
++(defconst isar-antiq-regexp
++ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
++ "Regexp matching Isabelle/Isar antiquotations.")
+
+ ;; keyword nesting
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/menu.patch Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,30 @@
+--- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200
++++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100
+@@ -339,9 +339,12 @@
+ (error "Aborted."))
+ [(control p)])
+
+-(proof-definvisible isar-cmd-refute "refute" [r])
+ (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])
++(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)])
++(proof-definvisible isar-cmd-refute "refute" [r])
+ (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)])
++(proof-definvisible isar-cmd-atp-kill "atp_kill")
++(proof-definvisible isar-cmd-atp-info "atp_info")
+
+ (defpgdefault menu-entries
+ (append
+@@ -349,9 +352,12 @@
+ (list
+ (cons "Commands"
+ (list
+- ["refute" isar-cmd-refute t]
+ ["quickcheck" isar-cmd-quickcheck t]
++ ["nitpick" isar-cmd-nitpick t]
++ ["refute" isar-cmd-refute t]
+ ["sledgehammer" isar-cmd-sledgehammer t]
++ ["sledgehammer: kill" isar-cmd-atp-kill t]
++ ["sledgehammer: info" isar-cmd-atp-info t]
+ ["display draft" isar-cmd-display-draft t])))
+ (list
+ (cons "Show me ..."
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/progname.patch Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,89 @@
+--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
++++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100
+@@ -97,8 +97,8 @@
+ (if (or proof-rsh-command
+ (file-executable-p isa-isatool-command))
+ (let ((setting (isa-shell-command-to-string
+- (concat isa-isatool-command
+- " getenv -b " envvar))))
++ (concat "\"" isa-isatool-command
++ "\" getenv -b " envvar))))
+ (if (string-equal setting "")
+ default
+ setting))
+@@ -125,15 +125,12 @@
+ :type 'file
+ :group 'isabelle)
+
+-(defvar isabelle-prog-name nil
+- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
+-
+ (defun isa-tool-list-logics ()
+ "Generate a list of available object logics."
+ (if (isa-set-isatool-command)
+ (delete "" (split-string
+ (isa-shell-command-to-string
+- (concat isa-isatool-command " findlogics")) "[ \t]"))))
++ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
+
+ (defcustom isabelle-logics-available nil
+ "*List of logics available to use with Isabelle.
+@@ -177,7 +174,7 @@
+
+ (defun isabelle-set-prog-name (&optional filename)
+ "Make proper command line for running Isabelle.
+-This function sets `isabelle-prog-name' and `proof-prog-name'."
++This function sets `proof-prog-name' and `isar-prog-args'."
+ (let*
+ ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
+ ;; under the interface wrapper script) indicate command line
+@@ -187,21 +184,20 @@
+ (getenv "ISABELLE") ; command line override
+ (isa-getenv "ISABELLE") ; choose to match isatool
+ "isabelle")) ; to
+- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
+- (opts (concat " -PI" ;; Proof General + Isar
+- (if proof-shell-unicode " -m PGASCII" "")
+- (if (and isabelle-opts (not (equal isabelle-opts "")))
+- (concat " " isabelle-opts) "")))
++ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
++ (opts (append (list "-PI") ;; Proof General + Isar
++ (if proof-shell-unicode (list "-m" "PGASCII") nil)
++ isabelle-opts))
+ (logic (or isabelle-chosen-logic
+ (getenv "PROOFGENERAL_LOGIC")))
+ (logicarg (if (and logic (not (equal logic "")))
+- (concat " " logic) "")))
++ (list logic) nil)))
+ (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
+- (setq isabelle-prog-name (concat isabelle opts logicarg))
+- (setq proof-prog-name isabelle-prog-name)))
++ (setq isar-prog-args (append opts logicarg))
++ (setq proof-prog-name isabelle)))
+
+ (defun isabelle-choose-logic (logic)
+- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
++ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
+ (interactive
+ (list (completing-read
+ "Use logic: "
+@@ -224,9 +220,7 @@
+ (if (isa-set-isatool-command)
+ (apply 'start-process
+ "isa-view-doc" nil
+- (append (split-string
+- isa-isatool-command)
+- (list "doc" docname)))))
++ (list isa-isatool-command "doc" docname))))
+
+ (defun isa-tool-list-docs ()
+ "Generate a list of documentation files available, with descriptions.
+@@ -236,7 +230,7 @@
+ passed to isa-tool-doc-command, DOCNAME will be viewed."
+ (if (isa-set-isatool-command)
+ (let ((docs (isa-shell-command-to-string
+- (concat isa-isatool-command " doc"))))
++ (concat "\"" isa-isatool-command "\" doc"))))
+ (unless (string-equal docs "")
+ (mapcan
+ (function (lambda (docdes)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/timeout.patch Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,11 @@
+--- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200
++++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100
+@@ -1493,7 +1493,7 @@
+ :type '(choice string (const nil))
+ :group 'proof-shell)
+
+-(defcustom proof-shell-quit-timeout 4
++(defcustom proof-shell-quit-timeout 45
+ ;; FIXME could add option to quiz user before rude kill.
+ "The number of seconds to wait after sending proof-shell-quit-cmd.
+ After this timeout, the proof shell will be killed off more rudely.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/version.patch Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,20 @@
+--- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200
++++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100
+@@ -55,7 +55,7 @@
+
+ (eval-and-compile
+ ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
+- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008."
++ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009."
+ "Version string identifying Proof General release."))
+
+ (defconst proof-general-short-version
+@@ -64,7 +64,7 @@
+ (string-match "Version \\([^ ]+\\)\\." proof-general-version)
+ (match-string 1 proof-general-version))))
+
+-(defconst proof-general-version-year "2008")
++(defconst proof-general-version-year "2009")
+
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;;
--- a/Admin/isatest/settings/at-poly-5.1-para-e Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/isatest/settings/at-poly-5.1-para-e Fri Dec 04 11:19:00 2009 +0100
@@ -22,6 +22,6 @@
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 20"
+ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/makebin Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/makebin Fri Dec 04 11:19:00 2009 +0100
@@ -109,6 +109,8 @@
touch "heaps/$COMPILER/log/HOL.gz"
touch "heaps/$COMPILER/HOL-Nominal"
touch "heaps/$COMPILER/log/HOL-Nominal.gz"
+ touch "heaps/$COMPILER/HOLCF"
+ touch "heaps/$COMPILER/log/HOLCF.gz"
touch "heaps/$COMPILER/ZF"
touch "heaps/$COMPILER/log/ZF.gz"
mkdir browser_info
@@ -116,6 +118,7 @@
./build -bait
else
./build -b -m HOL-Nominal HOL
+ ./build -b HOLCF
./build -b ZF
rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
fi
@@ -133,7 +136,7 @@
gzip -f "${ISABELLE_NAME}_library.tar"
cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
else
- for IMG in HOL HOL-Nominal ZF
+ for IMG in HOL HOL-Nominal HOLCF ZF
do
tar cf "${IMG}_$PLATFORM.tar" \
"$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/makebundle Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+#
+# makebundle -- re-package with add-on components
+
+## global settings
+
+TMP="/var/tmp/isabelle-makebundle$$"
+
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG ARCHIVE COMPONENTS"
+ echo
+ echo " Re-package Isabelle distribution with add-on components."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+[ "$#" -lt 1 ] && usage
+
+ARCHIVE="$1"; shift
+
+declare -a COMPONENTS
+COMPONENTS=("$@")
+
+
+## main
+
+mkdir "$TMP" || fail "Cannot create directory $TMP"
+
+ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
+ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
+ISABELLE_HOME="$TMP/$ISABELLE_NAME"
+
+[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+tar -C "$TMP" -x -z -f "$ARCHIVE"
+
+echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
+
+for COMPONENT in "${COMPONENTS[@]}"
+do
+ tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
+ NAME="$(basename "$COMPONENT" .tar.gz)"
+ [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
+
+ if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
+ echo "component $NAME"
+ echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
+ else
+ echo "package $NAME"
+ fi
+done
+
+tar -C "$TMP" -c -z \
+ -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
+ Isabelle "$ISABELLE_NAME"
+
+
+# clean up
+cd /tmp
+rm -rf "$TMP"
--- a/Admin/makedist Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/makedist Fri Dec 04 11:19:00 2009 +0100
@@ -4,7 +4,8 @@
## global settings
-REPOS="http://isabelle.in.tum.de/repos/isabelle"
+REPOS_NAME="isabelle-release"
+REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
@@ -92,12 +93,12 @@
{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
fail "Failed to retrieve $VERSION"
-IDENT=$(echo * | sed 's/isabelle-//')
+IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
-rm -f "isabelle-$IDENT/.hg_archival.txt"
-rm -f "isabelle-$IDENT/.hgtags"
-rm -f "isabelle-$IDENT/.hgignore"
-rm -f "isabelle-$IDENT/README_REPOSITORY"
+rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
+rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
+rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
+rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
# dist name
@@ -118,7 +119,7 @@
[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
cd "$DISTBASE"
-mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
+mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
purge_tmp
cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
--- a/bin/isabelle Fri Dec 04 11:04:07 2009 +0100
+++ b/bin/isabelle Fri Dec 04 11:19:00 2009 +0100
@@ -30,7 +30,7 @@
echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
echo
echo " Available tools are:"
- for DIR in ${TOOLS[@]}
+ for DIR in "${TOOLS[@]}"
do
if [ -d "$DIR" ]; then
for TOOL in "$DIR"/*
--- a/bin/isabelle-process Fri Dec 04 11:04:07 2009 +0100
+++ b/bin/isabelle-process Fri Dec 04 11:19:00 2009 +0100
@@ -181,7 +181,9 @@
case "$OUTPUT" in
"")
- [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
+ if [ -z "$READONLY" -a -w "$INFILE" ]; then
+ perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
+ fi
;;
*/*)
OUTFILE="$OUTPUT"
--- a/doc-src/Classes/Thy/document/Classes.tex Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Fri Dec 04 11:19:00 2009 +0100
@@ -1260,7 +1260,7 @@
\hspace*{0pt}\\
\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\
+\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
\hspace*{0pt}\\
\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
\hspace*{0pt}\\
@@ -1285,7 +1285,7 @@
\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
\hspace*{0pt}\\
\hspace*{0pt}val example :~IntInf.int =\\
-\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\
+\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/Program.thy Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy Fri Dec 04 11:19:00 2009 +0100
@@ -430,5 +430,220 @@
likely to be used in such situations.
*}
+subsection {* Inductive Predicates *}
+(*<*)
+hide const append
+
+inductive append
+where
+ "append [] ys ys"
+| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+(*>*)
+text {*
+To execute inductive predicates, a special preprocessor, the predicate
+ compiler, generates code equations from the introduction rules of the predicates.
+The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+Consider the simple predicate @{const append} given by these two
+introduction rules:
+*}
+text %quote {*
+@{thm append.intros(1)[of ys]}\\
+\noindent@{thm append.intros(2)[of xs ys zs x]}
+*}
+text {*
+\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
+*}
+code_pred %quote append .
+text {*
+\noindent The @{command "code_pred"} command takes the name
+of the inductive predicate and then you put a period to discharge
+a trivial correctness proof.
+The compiler infers possible modes
+for the predicate and produces the derived code equations.
+Modes annotate which (parts of the) arguments are to be taken as input,
+and which output. Modes are similar to types, but use the notation @{text "i"}
+for input and @{text "o"} for output.
+
+For @{term "append"}, the compiler can infer the following modes:
+\begin{itemize}
+\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
+\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
+\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
+\end{itemize}
+You can compute sets of predicates using @{command_def "values"}:
+*}
+values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
+text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
+values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
+text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
+text {*
+\noindent If you are only interested in the first elements of the set
+comprehension (with respect to a depth-first search on the introduction rules), you can
+pass an argument to
+@{command "values"} to specify the number of elements you want:
+*}
+
+values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
+values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
+
+text {*
+\noindent The @{command "values"} command can only compute set
+ comprehensions for which a mode has been inferred.
+
+The code equations for a predicate are made available as theorems with
+ the suffix @{text "equation"}, and can be inspected with:
+*}
+thm %quote append.equation
+text {*
+\noindent More advanced options are described in the following subsections.
+*}
+subsubsection {* Alternative names for functions *}
+text {*
+By default, the functions generated from a predicate are named after the predicate with the
+mode mangled into the name (e.g., @{text "append_i_i_o"}).
+You can specify your own names as follows:
+*}
+code_pred %quote (modes: i => i => o => bool as concat,
+ o => o => i => bool as split,
+ i => o => i => bool as suffix) append .
+
+subsubsection {* Alternative introduction rules *}
+text {*
+Sometimes the introduction rules of an predicate are not executable because they contain
+non-executable constants or specific modes could not be inferred.
+It is also possible that the introduction rules yield a function that loops forever
+due to the execution in a depth-first search manner.
+Therefore, you can declare alternative introduction rules for predicates with the attribute
+@{attribute "code_pred_intro"}.
+For example, the transitive closure is defined by:
+*}
+text %quote {*
+@{thm tranclp.intros(1)[of r a b]}\\
+\noindent @{thm tranclp.intros(2)[of r a b c]}
+*}
+text {*
+\noindent These rules do not suit well for executing the transitive closure
+with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
+cause an infinite loop in the recursive call.
+This can be avoided using the following alternative rules which are
+declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
+*}
+lemma %quote [code_pred_intro]:
+ "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
+ "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
+by auto
+text {*
+\noindent After declaring all alternative rules for the transitive closure,
+you invoke @{command "code_pred"} as usual.
+As you have declared alternative rules for the predicate, you are urged to prove that these
+introduction rules are complete, i.e., that you can derive an elimination rule for the
+alternative rules:
+*}
+code_pred %quote tranclp
+proof -
+ case tranclp
+ from this converse_tranclpE[OF this(1)] show thesis by metis
+qed
+text {*
+\noindent Alternative rules can also be used for constants that have not
+been defined inductively. For example, the lexicographic order which
+is defined as: *}
+text %quote {*
+@{thm [display] lexord_def[of "r"]}
+*}
+text {*
+\noindent To make it executable, you can derive the following two rules and prove the
+elimination rule:
+*}
+(*<*)
+lemma append: "append xs ys zs = (xs @ ys = zs)"
+by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
+(*>*)
+lemma %quote [code_pred_intro]:
+ "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
+(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
+
+lemma %quote [code_pred_intro]:
+ "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
+ \<Longrightarrow> lexord r (xs, ys)"
+(*<*)unfolding lexord_def Collect_def append mem_def apply simp
+apply (rule disjI2) by auto
+(*>*)
+
+code_pred %quote lexord
+(*<*)
+proof -
+ fix r a1
+ assume lexord: "lexord r a1"
+ assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis"
+ assume 2: "\<And> xs ys u a v b w. a1 = (xs, ys) \<Longrightarrow> append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) \<Longrightarrow> thesis"
+ obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp
+ {
+ assume "\<exists>a v. ys = xs @ a # v"
+ from this 1 a1 have thesis
+ by (fastsimp simp add: append)
+ } moreover
+ {
+ assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
+ from this 2 a1 have thesis by (fastsimp simp add: append mem_def)
+ } moreover
+ note lexord[simplified a1]
+ ultimately show thesis
+ unfolding lexord_def
+ by (fastsimp simp add: Collect_def)
+qed
+(*>*)
+subsubsection {* Options for values *}
+text {*
+In the presence of higher-order predicates, multiple modes for some predicate could be inferred
+that are not disambiguated by the pattern of the set comprehension.
+To disambiguate the modes for the arguments of a predicate, you can state
+the modes explicitly in the @{command "values"} command.
+Consider the simple predicate @{term "succ"}:
+*}
+inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "succ 0 (Suc 0)"
+| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
+
+code_pred succ .
+
+text {*
+\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
+ @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
+The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
+modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
+is chosen. To choose another mode for the argument, you can declare the mode for the argument between
+the @{command "values"} and the number of elements.
+*}
+values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
+values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
+
+subsubsection {* Embedding into functional code within Isabelle/HOL *}
+text {*
+To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
+you have a number of options:
+\begin{itemize}
+\item You want to use the first-order predicate with the mode
+ where all arguments are input. Then you can use the predicate directly, e.g.
+\begin{quote}
+ @{text "valid_suffix ys zs = "}\\
+ @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
+\end{quote}
+\item If you know that the execution returns only one value (it is deterministic), then you can
+ use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
+ is defined with
+\begin{quote}
+ @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
+\end{quote}
+ Note that if the evaluation does not return a unique value, it raises a run-time error
+ @{term "not_unique"}.
+\end{itemize}
+*}
+subsubsection {* Further Examples *}
+text {* Further examples for compiling inductive predicates can be found in
+the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
+There are also some examples in the Archive of Formal Proofs, notably
+in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
+*}
end
-
\ No newline at end of file
--- a/doc-src/Codegen/Thy/document/Program.tex Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Fri Dec 04 11:19:00 2009 +0100
@@ -968,6 +968,458 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Inductive Predicates%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+To execute inductive predicates, a special preprocessor, the predicate
+ compiler, generates code equations from the introduction rules of the predicates.
+The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+Consider the simple predicate \isa{append} given by these two
+introduction rules:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
+\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
+of the inductive predicate and then you put a period to discharge
+a trivial correctness proof.
+The compiler infers possible modes
+for the predicate and produces the derived code equations.
+Modes annotate which (parts of the) arguments are to be taken as input,
+and which output. Modes are similar to types, but use the notation \isa{i}
+for input and \isa{o} for output.
+
+For \isa{append}, the compiler can infer the following modes:
+\begin{itemize}
+\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
+\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+\end{itemize}
+You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\noindent If you are only interested in the first elements of the set
+comprehension (with respect to a depth-first search on the introduction rules), you can
+pass an argument to
+\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\isacommand{values}\isamarkupfalse%
+\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
+ comprehensions for which a mode has been inferred.
+
+The code equations for a predicate are made available as theorems with
+ the suffix \isa{equation}, and can be inspected with:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{thm}\isamarkupfalse%
+\ append{\isachardot}equation%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent More advanced options are described in the following subsections.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Alternative names for functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+By default, the functions generated from a predicate are named after the predicate with the
+mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}).
+You can specify your own names as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline
+\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline
+\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsubsection{Alternative introduction rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Sometimes the introduction rules of an predicate are not executable because they contain
+non-executable constants or specific modes could not be inferred.
+It is also possible that the introduction rules yield a function that loops forever
+due to the execution in a depth-first search manner.
+Therefore, you can declare alternative introduction rules for predicates with the attribute
+\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}.
+For example, the transitive closure is defined by:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
+\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent These rules do not suit well for executing the transitive closure
+with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
+cause an infinite loop in the recursive call.
+This can be avoided using the following alternative rules which are
+declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline
+\isacommand{by}\isamarkupfalse%
+\ auto%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent After declaring all alternative rules for the transitive closure,
+you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
+As you have declared alternative rules for the predicate, you are urged to prove that these
+introduction rules are complete, i.e., that you can derive an elimination rule for the
+alternative rules:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ tranclp\isanewline
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ tranclp\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
+\ thesis\ \isacommand{by}\isamarkupfalse%
+\ metis\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Alternative rules can also be used for constants that have not
+been defined inductively. For example, the lexicographic order which
+is defined as:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+lexord\ r\ {\isasymequiv}\isanewline
+{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
+\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
+\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%
+\end{isabelle}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent To make it executable, you can derive the following two rules and prove the
+elimination rule:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ lexord%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsubsection{Options for values%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In the presence of higher-order predicates, multiple modes for some predicate could be inferred
+that are not disambiguated by the pattern of the set comprehension.
+To disambiguate the modes for the arguments of a predicate, you can state
+the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command.
+Consider the simple predicate \isa{succ}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive}\isamarkupfalse%
+\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ succ%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool},
+ \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
+The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple
+modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
+is chosen. To choose another mode for the argument, you can declare the mode for the argument between
+the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\isacommand{values}\isamarkupfalse%
+\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
+you have a number of options:
+\begin{itemize}
+\item You want to use the first-order predicate with the mode
+ where all arguments are input. Then you can use the predicate directly, e.g.
+\begin{quote}
+ \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
+ \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
+\end{quote}
+\item If you know that the execution returns only one value (it is deterministic), then you can
+ use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
+ is defined with
+\begin{quote}
+ \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
+\end{quote}
+ Note that if the evaluation does not return a unique value, it raises a run-time error
+ \isa{not{\isacharunderscore}unique}.
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Further Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Further examples for compiling inductive predicates can be found in
+the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
+There are also some examples in the Archive of Formal Proofs, notably
+in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
@@ -982,7 +1434,7 @@
%
\endisadelimtheory
\isanewline
-\ \end{isabellebody}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/Codegen/codegen.tex Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Codegen/codegen.tex Fri Dec 04 11:19:00 2009 +0100
@@ -13,7 +13,7 @@
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann}}
+\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
\begin{document}
--- a/doc-src/manual.bib Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/manual.bib Fri Dec 04 11:19:00 2009 +0100
@@ -172,6 +172,14 @@
title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
crossref = {tphols2001}}
+@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
+ author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
+ booktitle = {Theorem Proving in Higher Order Logics},
+ pages = {131--146},
+ title = {Turning Inductive into Equational Specifications},
+ year = {2009}
+}
+
@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
crossref = "tphols2000",
title = "Proof terms for simply typed higher order logic",
--- a/etc/settings Fri Dec 04 11:04:07 2009 +0100
+++ b/etc/settings Fri Dec 04 11:19:00 2009 +0100
@@ -208,21 +208,9 @@
## Set HOME only for tools you have installed!
# External provers
-E_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
- "$ISABELLE_HOME/../E/$ML_PLATFORM" \
- "/usr/local/E/$ML_PLATFORM" \
- "")
-VAMPIRE_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
- "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
- "/usr/local/vampire/$ML_PLATFORM" \
- "")
-SPASS_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
- "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
- "/usr/local/spass/$ML_PLATFORM" \
- "")
+#E_HOME=/usr/local/bin
+#SPASS_HOME=/usr/local/bin
+#VAMPIRE_HOME=/usr/local/bin
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
--- a/lib/Tools/findlogics Fri Dec 04 11:04:07 2009 +0100
+++ b/lib/Tools/findlogics Fri Dec 04 11:19:00 2009 +0100
@@ -39,4 +39,4 @@
done
done
-echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq)
+echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Dec 04 11:04:07 2009 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Dec 04 11:19:00 2009 +0100
@@ -537,8 +537,8 @@
fun token s =
Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
val numeral = Scan.one isnum
- val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
- val decimalfrac = Scan.repeat numeral
+ val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
+ val decimalfrac = Scan.repeat1 numeral
>> (fn s => rat_of_string(implode s) // pow10 (length s))
val decimalsig =
decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
--- a/src/Pure/Syntax/syntax.ML Fri Dec 04 11:04:07 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML Fri Dec 04 11:19:00 2009 +0100
@@ -496,7 +496,7 @@
else if ! ambiguity_is_error then error (ambiguity_msg pos)
else
(warning (cat_lines
- (("Ambiguous input " ^ Position.str_of pos ^
+ (("Ambiguous input" ^ Position.str_of pos ^
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
map show_pt (Library.take (limit, pts)))));
--- a/src/Pure/pure_setup.ML Fri Dec 04 11:04:07 2009 +0100
+++ b/src/Pure/pure_setup.ML Fri Dec 04 11:19:00 2009 +0100
@@ -39,6 +39,11 @@
then use "ML-Systems/install_pp_polyml.ML"
else ();
+if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
+ Secure.use_text ML_Parse.global_context (0, "") false
+ "PolyML.Compiler.maxInlineSize := 20"
+else ();
+
(* ML toplevel use commands *)