1.1 --- a/.hgtags Fri Dec 04 11:04:07 2009 +0100
1.2 +++ b/.hgtags Fri Dec 04 11:19:00 2009 +0100
1.3 @@ -24,6 +24,4 @@
1.4 f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
1.5 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
1.6 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
1.7 -9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
1.8 -9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
1.9 -4328de748fb2ceffe4ad5a6d5fbf3347f6aecfa6 isa2009-1-test
1.10 +6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
2.1 --- a/ANNOUNCE Fri Dec 04 11:04:07 2009 +0100
2.2 +++ b/ANNOUNCE Fri Dec 04 11:19:00 2009 +0100
2.3 @@ -26,11 +26,16 @@
2.4
2.5 * HOL: various parts of multivariate analysis.
2.6
2.7 +* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
2.8 +arithmetic, based on external semidefinite programming solvers.
2.9 +
2.10 * HOLCF: new definitional domain package.
2.11
2.12 * Revised tutorial on locales.
2.13
2.14 -* Support for Poly/ML 5.3.0, with improved reporting of compiler
2.15 +* ML: tacticals for subgoal focus.
2.16 +
2.17 +* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
2.18 errors and run-time exceptions, including detailed source positions.
2.19
2.20 * Parallel checking of nested Isar proofs, with improved scalability
3.1 --- a/Admin/MacOS/App1/script Fri Dec 04 11:04:07 2009 +0100
3.2 +++ b/Admin/MacOS/App1/script Fri Dec 04 11:19:00 2009 +0100
3.3 @@ -48,8 +48,9 @@
3.4 /Applications/Emacs.app/Contents/MacOS/Emacs \
3.5 "")"
3.6
3.7 +declare -a EMACS_OPTIONS=()
3.8 if [ -n "$PROOFGENERAL_EMACS" ]; then
3.9 - EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
3.10 + EMACS_OPTIONS=(-p "$PROOFGENERAL_EMACS")
3.11 fi
3.12
3.13
3.14 @@ -57,7 +58,7 @@
3.15
3.16 OUTPUT="/tmp/isabelle$$.out"
3.17
3.18 -( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
3.19 +( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
3.20 RC=$?
3.21
3.22 if [ "$RC" != 0 ]; then
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/Admin/ProofGeneral/interface Fri Dec 04 11:19:00 2009 +0100
4.3 @@ -0,0 +1,262 @@
4.4 +#!/usr/bin/env bash
4.5 +#
4.6 +# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
4.7 +#
4.8 +# Proof General interface wrapper for Isabelle.
4.9 +
4.10 +
4.11 +## self references
4.12 +
4.13 +THIS="$(cd "$(dirname "$0")"; pwd)"
4.14 +SUPER="$(cd "$THIS/.."; pwd)"
4.15 +
4.16 +
4.17 +## diagnostics
4.18 +
4.19 +usage()
4.20 +{
4.21 + echo
4.22 + echo "Usage: Isabelle [OPTIONS] [FILES ...]"
4.23 + echo
4.24 + echo " Options are:"
4.25 + echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
4.26 + echo " -L NAME abbreviates -l NAME -k NAME"
4.27 + echo " -P BOOL actually start Proof General (default true), otherwise"
4.28 + echo " run plain tty session"
4.29 + echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
4.30 + echo " -X BOOL configure the X-Symbol package on startup (default true)"
4.31 + echo " -f SIZE set X-Symbol font size (default 12)"
4.32 + echo " -g GEOMETRY specify Emacs geometry"
4.33 + echo " -k NAME use specific isar-keywords for named logic"
4.34 + echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
4.35 + echo " -m MODE add print mode for output"
4.36 + echo " -p NAME Emacs program name (default emacs)"
4.37 + echo " -u BOOL use personal .emacs file (default true)"
4.38 + echo " -w BOOL use window system (default true)"
4.39 + echo " -x BOOL enable the X-Symbol package on startup (default false)"
4.40 + echo
4.41 + echo "Starts Proof General for Isabelle with theory and proof FILES"
4.42 + echo "(default Scratch.thy)."
4.43 + echo
4.44 + echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
4.45 + echo
4.46 + exit 1
4.47 +}
4.48 +
4.49 +fail()
4.50 +{
4.51 + echo "$1" >&2
4.52 + exit 2
4.53 +}
4.54 +
4.55 +
4.56 +## process command line
4.57 +
4.58 +# options
4.59 +
4.60 +ISABELLE_OPTIONS=""
4.61 +ISAR="true"
4.62 +START_PG="true"
4.63 +GEOMETRY=""
4.64 +KEYWORDS=""
4.65 +LOGIC="$ISABELLE_LOGIC"
4.66 +PROGNAME="emacs"
4.67 +INITFILE="true"
4.68 +WINDOWSYSTEM="true"
4.69 +XSYMBOL=""
4.70 +XSYMBOL_SETUP=true
4.71 +XSYMBOL_FONTSIZE="12"
4.72 +UNICODE=""
4.73 +
4.74 +getoptions()
4.75 +{
4.76 + OPTIND=1
4.77 + while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
4.78 + do
4.79 + case "$OPT" in
4.80 + I)
4.81 + ISAR="$OPTARG"
4.82 + ;;
4.83 + L)
4.84 + KEYWORDS="$OPTARG"
4.85 + LOGIC="$OPTARG"
4.86 + ;;
4.87 + P)
4.88 + START_PG="$OPTARG"
4.89 + ;;
4.90 + U)
4.91 + UNICODE="$OPTARG"
4.92 + ;;
4.93 + X)
4.94 + XSYMBOL_SETUP="$OPTARG"
4.95 + ;;
4.96 + f)
4.97 + XSYMBOL_FONTSIZE="$OPTARG"
4.98 + ;;
4.99 + g)
4.100 + GEOMETRY="$OPTARG"
4.101 + ;;
4.102 + k)
4.103 + KEYWORDS="$OPTARG"
4.104 + ;;
4.105 + l)
4.106 + LOGIC="$OPTARG"
4.107 + ;;
4.108 + m)
4.109 + if [ -z "$ISABELLE_OPTIONS" ]; then
4.110 + ISABELLE_OPTIONS="-m $OPTARG"
4.111 + else
4.112 + ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
4.113 + fi
4.114 + ;;
4.115 + p)
4.116 + PROGNAME="$OPTARG"
4.117 + ;;
4.118 + u)
4.119 + INITFILE="$OPTARG"
4.120 + ;;
4.121 + w)
4.122 + WINDOWSYSTEM="$OPTARG"
4.123 + ;;
4.124 + x)
4.125 + XSYMBOL="$OPTARG"
4.126 + ;;
4.127 + \?)
4.128 + usage
4.129 + ;;
4.130 + esac
4.131 + done
4.132 +}
4.133 +
4.134 +eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
4.135 +getoptions "${OPTIONS[@]}"
4.136 +
4.137 +getoptions "$@"
4.138 +shift $(($OPTIND - 1))
4.139 +
4.140 +
4.141 +# args
4.142 +
4.143 +declare -a FILES=()
4.144 +
4.145 +if [ "$#" -eq 0 ]; then
4.146 + FILES["${#FILES[@]}"]="Scratch.thy"
4.147 +else
4.148 + while [ "$#" -gt 0 ]; do
4.149 + FILES["${#FILES[@]}"]="$1"
4.150 + shift
4.151 + done
4.152 +fi
4.153 +
4.154 +
4.155 +## smart X11 font installation
4.156 +
4.157 +function checkfonts ()
4.158 +{
4.159 + XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
4.160 +
4.161 + case "$XLSFONTS" in
4.162 + xlsfonts:*)
4.163 + return 1
4.164 + ;;
4.165 + esac
4.166 +
4.167 + return 0
4.168 +}
4.169 +
4.170 +function installfonts ()
4.171 +{
4.172 + checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
4.173 +}
4.174 +
4.175 +
4.176 +## main
4.177 +
4.178 +# Isabelle2008 compatibility
4.179 +[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
4.180 +[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
4.181 +
4.182 +if [ "$START_PG" = false ]; then
4.183 +
4.184 + [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
4.185 + exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
4.186 +
4.187 +else
4.188 +
4.189 + declare -a ARGS=()
4.190 +
4.191 + if [ -n "$GEOMETRY" ]; then
4.192 + ARGS["${#ARGS[@]}"]="-geometry"
4.193 + ARGS["${#ARGS[@]}"]="$GEOMETRY"
4.194 + fi
4.195 +
4.196 + [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
4.197 +
4.198 + if [ "$WINDOWSYSTEM" = false ]; then
4.199 + ARGS["${#ARGS[@]}"]="-nw"
4.200 + XSYMBOL=false
4.201 + elif [ -z "$DISPLAY" ]; then
4.202 + XSYMBOL=false
4.203 + else
4.204 + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
4.205 + fi
4.206 +
4.207 + if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
4.208 + then
4.209 + if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
4.210 + then
4.211 + cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
4.212 + cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
4.213 + sleep 3
4.214 + fi
4.215 + fi
4.216 +
4.217 + ARGS["${#ARGS[@]}"]="-l"
4.218 + ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
4.219 +
4.220 + if [ -n "$KEYWORDS" ]; then
4.221 + if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
4.222 + ARGS["${#ARGS[@]}"]="-l"
4.223 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
4.224 + elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
4.225 + ARGS["${#ARGS[@]}"]="-l"
4.226 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
4.227 + else
4.228 + fail "No isar-keywords file for '$KEYWORDS'"
4.229 + fi
4.230 + elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
4.231 + ARGS["${#ARGS[@]}"]="-l"
4.232 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
4.233 + elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
4.234 + ARGS["${#ARGS[@]}"]="-l"
4.235 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
4.236 + fi
4.237 +
4.238 + for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
4.239 + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
4.240 + do
4.241 + if [ -f "$FILE" ]; then
4.242 + ARGS["${#ARGS[@]}"]="-l"
4.243 + ARGS["${#ARGS[@]}"]="$FILE"
4.244 + fi
4.245 + done
4.246 +
4.247 + case "$LOGIC" in
4.248 + /*)
4.249 + ;;
4.250 + */*)
4.251 + LOGIC="$(pwd -P)/$LOGIC"
4.252 + ;;
4.253 + esac
4.254 +
4.255 + export PROOFGENERAL_HOME="$SUPER"
4.256 + export PROOFGENERAL_ASSISTANTS="isar"
4.257 + export PROOFGENERAL_LOGIC="$LOGIC"
4.258 + export PROOFGENERAL_XSYMBOL="$XSYMBOL"
4.259 + export PROOFGENERAL_UNICODE="$UNICODE"
4.260 +
4.261 + export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
4.262 +
4.263 + exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
4.264 +
4.265 +fi
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/Admin/ProofGeneral/isar-antiq-regexp.patch Fri Dec 04 11:19:00 2009 +0100
5.3 @@ -0,0 +1,21 @@
5.4 +--- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200
5.5 ++++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200
5.6 +@@ -252,14 +252,9 @@
5.7 +
5.8 + ;; antiquotations
5.9 +
5.10 +-;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
5.11 +-;; incomplete antiquotations like @{text bla"} (even though it is supposed to
5.12 +-;; stop at eol anyway).
5.13 +-
5.14 +-(defconst isar-antiq-regexp
5.15 +- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
5.16 +- "Regexp matching Isabelle/Isar antiquoations.")
5.17 +-
5.18 ++(defconst isar-antiq-regexp
5.19 ++ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
5.20 ++ "Regexp matching Isabelle/Isar antiquotations.")
5.21 +
5.22 + ;; keyword nesting
5.23 +
5.24 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/Admin/ProofGeneral/menu.patch Fri Dec 04 11:19:00 2009 +0100
6.3 @@ -0,0 +1,30 @@
6.4 +--- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200
6.5 ++++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100
6.6 +@@ -339,9 +339,12 @@
6.7 + (error "Aborted."))
6.8 + [(control p)])
6.9 +
6.10 +-(proof-definvisible isar-cmd-refute "refute" [r])
6.11 + (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])
6.12 ++(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)])
6.13 ++(proof-definvisible isar-cmd-refute "refute" [r])
6.14 + (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)])
6.15 ++(proof-definvisible isar-cmd-atp-kill "atp_kill")
6.16 ++(proof-definvisible isar-cmd-atp-info "atp_info")
6.17 +
6.18 + (defpgdefault menu-entries
6.19 + (append
6.20 +@@ -349,9 +352,12 @@
6.21 + (list
6.22 + (cons "Commands"
6.23 + (list
6.24 +- ["refute" isar-cmd-refute t]
6.25 + ["quickcheck" isar-cmd-quickcheck t]
6.26 ++ ["nitpick" isar-cmd-nitpick t]
6.27 ++ ["refute" isar-cmd-refute t]
6.28 + ["sledgehammer" isar-cmd-sledgehammer t]
6.29 ++ ["sledgehammer: kill" isar-cmd-atp-kill t]
6.30 ++ ["sledgehammer: info" isar-cmd-atp-info t]
6.31 + ["display draft" isar-cmd-display-draft t])))
6.32 + (list
6.33 + (cons "Show me ..."
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/Admin/ProofGeneral/progname.patch Fri Dec 04 11:19:00 2009 +0100
7.3 @@ -0,0 +1,89 @@
7.4 +--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
7.5 ++++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100
7.6 +@@ -97,8 +97,8 @@
7.7 + (if (or proof-rsh-command
7.8 + (file-executable-p isa-isatool-command))
7.9 + (let ((setting (isa-shell-command-to-string
7.10 +- (concat isa-isatool-command
7.11 +- " getenv -b " envvar))))
7.12 ++ (concat "\"" isa-isatool-command
7.13 ++ "\" getenv -b " envvar))))
7.14 + (if (string-equal setting "")
7.15 + default
7.16 + setting))
7.17 +@@ -125,15 +125,12 @@
7.18 + :type 'file
7.19 + :group 'isabelle)
7.20 +
7.21 +-(defvar isabelle-prog-name nil
7.22 +- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
7.23 +-
7.24 + (defun isa-tool-list-logics ()
7.25 + "Generate a list of available object logics."
7.26 + (if (isa-set-isatool-command)
7.27 + (delete "" (split-string
7.28 + (isa-shell-command-to-string
7.29 +- (concat isa-isatool-command " findlogics")) "[ \t]"))))
7.30 ++ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
7.31 +
7.32 + (defcustom isabelle-logics-available nil
7.33 + "*List of logics available to use with Isabelle.
7.34 +@@ -177,7 +174,7 @@
7.35 +
7.36 + (defun isabelle-set-prog-name (&optional filename)
7.37 + "Make proper command line for running Isabelle.
7.38 +-This function sets `isabelle-prog-name' and `proof-prog-name'."
7.39 ++This function sets `proof-prog-name' and `isar-prog-args'."
7.40 + (let*
7.41 + ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
7.42 + ;; under the interface wrapper script) indicate command line
7.43 +@@ -187,21 +184,20 @@
7.44 + (getenv "ISABELLE") ; command line override
7.45 + (isa-getenv "ISABELLE") ; choose to match isatool
7.46 + "isabelle")) ; to
7.47 +- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
7.48 +- (opts (concat " -PI" ;; Proof General + Isar
7.49 +- (if proof-shell-unicode " -m PGASCII" "")
7.50 +- (if (and isabelle-opts (not (equal isabelle-opts "")))
7.51 +- (concat " " isabelle-opts) "")))
7.52 ++ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
7.53 ++ (opts (append (list "-PI") ;; Proof General + Isar
7.54 ++ (if proof-shell-unicode (list "-m" "PGASCII") nil)
7.55 ++ isabelle-opts))
7.56 + (logic (or isabelle-chosen-logic
7.57 + (getenv "PROOFGENERAL_LOGIC")))
7.58 + (logicarg (if (and logic (not (equal logic "")))
7.59 +- (concat " " logic) "")))
7.60 ++ (list logic) nil)))
7.61 + (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
7.62 +- (setq isabelle-prog-name (concat isabelle opts logicarg))
7.63 +- (setq proof-prog-name isabelle-prog-name)))
7.64 ++ (setq isar-prog-args (append opts logicarg))
7.65 ++ (setq proof-prog-name isabelle)))
7.66 +
7.67 + (defun isabelle-choose-logic (logic)
7.68 +- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
7.69 ++ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
7.70 + (interactive
7.71 + (list (completing-read
7.72 + "Use logic: "
7.73 +@@ -224,9 +220,7 @@
7.74 + (if (isa-set-isatool-command)
7.75 + (apply 'start-process
7.76 + "isa-view-doc" nil
7.77 +- (append (split-string
7.78 +- isa-isatool-command)
7.79 +- (list "doc" docname)))))
7.80 ++ (list isa-isatool-command "doc" docname))))
7.81 +
7.82 + (defun isa-tool-list-docs ()
7.83 + "Generate a list of documentation files available, with descriptions.
7.84 +@@ -236,7 +230,7 @@
7.85 + passed to isa-tool-doc-command, DOCNAME will be viewed."
7.86 + (if (isa-set-isatool-command)
7.87 + (let ((docs (isa-shell-command-to-string
7.88 +- (concat isa-isatool-command " doc"))))
7.89 ++ (concat "\"" isa-isatool-command "\" doc"))))
7.90 + (unless (string-equal docs "")
7.91 + (mapcan
7.92 + (function (lambda (docdes)
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/Admin/ProofGeneral/timeout.patch Fri Dec 04 11:19:00 2009 +0100
8.3 @@ -0,0 +1,11 @@
8.4 +--- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200
8.5 ++++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100
8.6 +@@ -1493,7 +1493,7 @@
8.7 + :type '(choice string (const nil))
8.8 + :group 'proof-shell)
8.9 +
8.10 +-(defcustom proof-shell-quit-timeout 4
8.11 ++(defcustom proof-shell-quit-timeout 45
8.12 + ;; FIXME could add option to quiz user before rude kill.
8.13 + "The number of seconds to wait after sending proof-shell-quit-cmd.
8.14 + After this timeout, the proof shell will be killed off more rudely.
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/Admin/ProofGeneral/version.patch Fri Dec 04 11:19:00 2009 +0100
9.3 @@ -0,0 +1,20 @@
9.4 +--- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200
9.5 ++++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100
9.6 +@@ -55,7 +55,7 @@
9.7 +
9.8 + (eval-and-compile
9.9 + ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
9.10 +- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008."
9.11 ++ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009."
9.12 + "Version string identifying Proof General release."))
9.13 +
9.14 + (defconst proof-general-short-version
9.15 +@@ -64,7 +64,7 @@
9.16 + (string-match "Version \\([^ ]+\\)\\." proof-general-version)
9.17 + (match-string 1 proof-general-version))))
9.18 +
9.19 +-(defconst proof-general-version-year "2008")
9.20 ++(defconst proof-general-version-year "2009")
9.21 +
9.22 + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
9.23 + ;;
10.1 --- a/Admin/isatest/settings/at-poly-5.1-para-e Fri Dec 04 11:04:07 2009 +0100
10.2 +++ b/Admin/isatest/settings/at-poly-5.1-para-e Fri Dec 04 11:19:00 2009 +0100
10.3 @@ -22,6 +22,6 @@
10.4 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
10.5 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
10.6
10.7 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 20"
10.8 +ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
10.9
10.10 HOL_USEDIR_OPTIONS="-p 2 -q 0"
11.1 --- a/Admin/makebin Fri Dec 04 11:04:07 2009 +0100
11.2 +++ b/Admin/makebin Fri Dec 04 11:19:00 2009 +0100
11.3 @@ -109,6 +109,8 @@
11.4 touch "heaps/$COMPILER/log/HOL.gz"
11.5 touch "heaps/$COMPILER/HOL-Nominal"
11.6 touch "heaps/$COMPILER/log/HOL-Nominal.gz"
11.7 + touch "heaps/$COMPILER/HOLCF"
11.8 + touch "heaps/$COMPILER/log/HOLCF.gz"
11.9 touch "heaps/$COMPILER/ZF"
11.10 touch "heaps/$COMPILER/log/ZF.gz"
11.11 mkdir browser_info
11.12 @@ -116,6 +118,7 @@
11.13 ./build -bait
11.14 else
11.15 ./build -b -m HOL-Nominal HOL
11.16 + ./build -b HOLCF
11.17 ./build -b ZF
11.18 rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
11.19 fi
11.20 @@ -133,7 +136,7 @@
11.21 gzip -f "${ISABELLE_NAME}_library.tar"
11.22 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
11.23 else
11.24 - for IMG in HOL HOL-Nominal ZF
11.25 + for IMG in HOL HOL-Nominal HOLCF ZF
11.26 do
11.27 tar cf "${IMG}_$PLATFORM.tar" \
11.28 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/Admin/makebundle Fri Dec 04 11:19:00 2009 +0100
12.3 @@ -0,0 +1,75 @@
12.4 +#!/usr/bin/env bash
12.5 +#
12.6 +# makebundle -- re-package with add-on components
12.7 +
12.8 +## global settings
12.9 +
12.10 +TMP="/var/tmp/isabelle-makebundle$$"
12.11 +
12.12 +
12.13 +## diagnostics
12.14 +
12.15 +PRG=$(basename "$0")
12.16 +
12.17 +function usage()
12.18 +{
12.19 + echo
12.20 + echo "Usage: $PRG ARCHIVE COMPONENTS"
12.21 + echo
12.22 + echo " Re-package Isabelle distribution with add-on components."
12.23 + echo
12.24 + exit 1
12.25 +}
12.26 +
12.27 +function fail()
12.28 +{
12.29 + echo "$1" >&2
12.30 + exit 2
12.31 +}
12.32 +
12.33 +
12.34 +## process command line
12.35 +
12.36 +[ "$#" -lt 1 ] && usage
12.37 +
12.38 +ARCHIVE="$1"; shift
12.39 +
12.40 +declare -a COMPONENTS
12.41 +COMPONENTS=("$@")
12.42 +
12.43 +
12.44 +## main
12.45 +
12.46 +mkdir "$TMP" || fail "Cannot create directory $TMP"
12.47 +
12.48 +ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
12.49 +ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
12.50 +ISABELLE_HOME="$TMP/$ISABELLE_NAME"
12.51 +
12.52 +[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
12.53 +tar -C "$TMP" -x -z -f "$ARCHIVE"
12.54 +
12.55 +echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
12.56 +
12.57 +for COMPONENT in "${COMPONENTS[@]}"
12.58 +do
12.59 + tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
12.60 + NAME="$(basename "$COMPONENT" .tar.gz)"
12.61 + [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
12.62 +
12.63 + if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
12.64 + echo "component $NAME"
12.65 + echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
12.66 + else
12.67 + echo "package $NAME"
12.68 + fi
12.69 +done
12.70 +
12.71 +tar -C "$TMP" -c -z \
12.72 + -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
12.73 + Isabelle "$ISABELLE_NAME"
12.74 +
12.75 +
12.76 +# clean up
12.77 +cd /tmp
12.78 +rm -rf "$TMP"
13.1 --- a/Admin/makedist Fri Dec 04 11:04:07 2009 +0100
13.2 +++ b/Admin/makedist Fri Dec 04 11:19:00 2009 +0100
13.3 @@ -4,7 +4,8 @@
13.4
13.5 ## global settings
13.6
13.7 -REPOS="http://isabelle.in.tum.de/repos/isabelle"
13.8 +REPOS_NAME="isabelle-release"
13.9 +REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
13.10
13.11 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
13.12
13.13 @@ -92,12 +93,12 @@
13.14 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
13.15 fail "Failed to retrieve $VERSION"
13.16
13.17 -IDENT=$(echo * | sed 's/isabelle-//')
13.18 +IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
13.19
13.20 -rm -f "isabelle-$IDENT/.hg_archival.txt"
13.21 -rm -f "isabelle-$IDENT/.hgtags"
13.22 -rm -f "isabelle-$IDENT/.hgignore"
13.23 -rm -f "isabelle-$IDENT/README_REPOSITORY"
13.24 +rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
13.25 +rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
13.26 +rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
13.27 +rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
13.28
13.29
13.30 # dist name
13.31 @@ -118,7 +119,7 @@
13.32 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
13.33
13.34 cd "$DISTBASE"
13.35 -mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
13.36 +mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
13.37 purge_tmp
13.38
13.39 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
14.1 --- a/bin/isabelle Fri Dec 04 11:04:07 2009 +0100
14.2 +++ b/bin/isabelle Fri Dec 04 11:19:00 2009 +0100
14.3 @@ -30,7 +30,7 @@
14.4 echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
14.5 echo
14.6 echo " Available tools are:"
14.7 - for DIR in ${TOOLS[@]}
14.8 + for DIR in "${TOOLS[@]}"
14.9 do
14.10 if [ -d "$DIR" ]; then
14.11 for TOOL in "$DIR"/*
15.1 --- a/bin/isabelle-process Fri Dec 04 11:04:07 2009 +0100
15.2 +++ b/bin/isabelle-process Fri Dec 04 11:19:00 2009 +0100
15.3 @@ -181,7 +181,9 @@
15.4
15.5 case "$OUTPUT" in
15.6 "")
15.7 - [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
15.8 + if [ -z "$READONLY" -a -w "$INFILE" ]; then
15.9 + perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
15.10 + fi
15.11 ;;
15.12 */*)
15.13 OUTFILE="$OUTPUT"
16.1 --- a/doc-src/Classes/Thy/document/Classes.tex Fri Dec 04 11:04:07 2009 +0100
16.2 +++ b/doc-src/Classes/Thy/document/Classes.tex Fri Dec 04 11:19:00 2009 +0100
16.3 @@ -1260,7 +1260,7 @@
16.4 \hspace*{0pt}\\
16.5 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
16.6 \hspace*{0pt}\\
16.7 -\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\
16.8 +\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
16.9 \hspace*{0pt}\\
16.10 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
16.11 \hspace*{0pt}\\
16.12 @@ -1285,7 +1285,7 @@
16.13 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
16.14 \hspace*{0pt}\\
16.15 \hspace*{0pt}val example :~IntInf.int =\\
16.16 -\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\
16.17 +\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
16.18 \hspace*{0pt}\\
16.19 \hspace*{0pt}end;~(*struct Example*)%
16.20 \end{isamarkuptext}%
17.1 --- a/doc-src/Codegen/Thy/Program.thy Fri Dec 04 11:04:07 2009 +0100
17.2 +++ b/doc-src/Codegen/Thy/Program.thy Fri Dec 04 11:19:00 2009 +0100
17.3 @@ -430,5 +430,220 @@
17.4 likely to be used in such situations.
17.5 *}
17.6
17.7 +subsection {* Inductive Predicates *}
17.8 +(*<*)
17.9 +hide const append
17.10 +
17.11 +inductive append
17.12 +where
17.13 + "append [] ys ys"
17.14 +| "append xs ys zs ==> append (x # xs) ys (x # zs)"
17.15 +(*>*)
17.16 +text {*
17.17 +To execute inductive predicates, a special preprocessor, the predicate
17.18 + compiler, generates code equations from the introduction rules of the predicates.
17.19 +The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
17.20 +Consider the simple predicate @{const append} given by these two
17.21 +introduction rules:
17.22 +*}
17.23 +text %quote {*
17.24 +@{thm append.intros(1)[of ys]}\\
17.25 +\noindent@{thm append.intros(2)[of xs ys zs x]}
17.26 +*}
17.27 +text {*
17.28 +\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
17.29 +*}
17.30 +code_pred %quote append .
17.31 +text {*
17.32 +\noindent The @{command "code_pred"} command takes the name
17.33 +of the inductive predicate and then you put a period to discharge
17.34 +a trivial correctness proof.
17.35 +The compiler infers possible modes
17.36 +for the predicate and produces the derived code equations.
17.37 +Modes annotate which (parts of the) arguments are to be taken as input,
17.38 +and which output. Modes are similar to types, but use the notation @{text "i"}
17.39 +for input and @{text "o"} for output.
17.40 +
17.41 +For @{term "append"}, the compiler can infer the following modes:
17.42 +\begin{itemize}
17.43 +\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
17.44 +\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
17.45 +\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
17.46 +\end{itemize}
17.47 +You can compute sets of predicates using @{command_def "values"}:
17.48 +*}
17.49 +values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
17.50 +text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
17.51 +values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
17.52 +text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
17.53 +text {*
17.54 +\noindent If you are only interested in the first elements of the set
17.55 +comprehension (with respect to a depth-first search on the introduction rules), you can
17.56 +pass an argument to
17.57 +@{command "values"} to specify the number of elements you want:
17.58 +*}
17.59 +
17.60 +values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
17.61 +values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
17.62 +
17.63 +text {*
17.64 +\noindent The @{command "values"} command can only compute set
17.65 + comprehensions for which a mode has been inferred.
17.66 +
17.67 +The code equations for a predicate are made available as theorems with
17.68 + the suffix @{text "equation"}, and can be inspected with:
17.69 +*}
17.70 +thm %quote append.equation
17.71 +text {*
17.72 +\noindent More advanced options are described in the following subsections.
17.73 +*}
17.74 +subsubsection {* Alternative names for functions *}
17.75 +text {*
17.76 +By default, the functions generated from a predicate are named after the predicate with the
17.77 +mode mangled into the name (e.g., @{text "append_i_i_o"}).
17.78 +You can specify your own names as follows:
17.79 +*}
17.80 +code_pred %quote (modes: i => i => o => bool as concat,
17.81 + o => o => i => bool as split,
17.82 + i => o => i => bool as suffix) append .
17.83 +
17.84 +subsubsection {* Alternative introduction rules *}
17.85 +text {*
17.86 +Sometimes the introduction rules of an predicate are not executable because they contain
17.87 +non-executable constants or specific modes could not be inferred.
17.88 +It is also possible that the introduction rules yield a function that loops forever
17.89 +due to the execution in a depth-first search manner.
17.90 +Therefore, you can declare alternative introduction rules for predicates with the attribute
17.91 +@{attribute "code_pred_intro"}.
17.92 +For example, the transitive closure is defined by:
17.93 +*}
17.94 +text %quote {*
17.95 +@{thm tranclp.intros(1)[of r a b]}\\
17.96 +\noindent @{thm tranclp.intros(2)[of r a b c]}
17.97 +*}
17.98 +text {*
17.99 +\noindent These rules do not suit well for executing the transitive closure
17.100 +with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
17.101 +cause an infinite loop in the recursive call.
17.102 +This can be avoided using the following alternative rules which are
17.103 +declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
17.104 +*}
17.105 +lemma %quote [code_pred_intro]:
17.106 + "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
17.107 + "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
17.108 +by auto
17.109 +text {*
17.110 +\noindent After declaring all alternative rules for the transitive closure,
17.111 +you invoke @{command "code_pred"} as usual.
17.112 +As you have declared alternative rules for the predicate, you are urged to prove that these
17.113 +introduction rules are complete, i.e., that you can derive an elimination rule for the
17.114 +alternative rules:
17.115 +*}
17.116 +code_pred %quote tranclp
17.117 +proof -
17.118 + case tranclp
17.119 + from this converse_tranclpE[OF this(1)] show thesis by metis
17.120 +qed
17.121 +text {*
17.122 +\noindent Alternative rules can also be used for constants that have not
17.123 +been defined inductively. For example, the lexicographic order which
17.124 +is defined as: *}
17.125 +text %quote {*
17.126 +@{thm [display] lexord_def[of "r"]}
17.127 +*}
17.128 +text {*
17.129 +\noindent To make it executable, you can derive the following two rules and prove the
17.130 +elimination rule:
17.131 +*}
17.132 +(*<*)
17.133 +lemma append: "append xs ys zs = (xs @ ys = zs)"
17.134 +by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
17.135 +(*>*)
17.136 +lemma %quote [code_pred_intro]:
17.137 + "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
17.138 +(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
17.139 +
17.140 +lemma %quote [code_pred_intro]:
17.141 + "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
17.142 + \<Longrightarrow> lexord r (xs, ys)"
17.143 +(*<*)unfolding lexord_def Collect_def append mem_def apply simp
17.144 +apply (rule disjI2) by auto
17.145 +(*>*)
17.146 +
17.147 +code_pred %quote lexord
17.148 +(*<*)
17.149 +proof -
17.150 + fix r a1
17.151 + assume lexord: "lexord r a1"
17.152 + assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis"
17.153 + 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"
17.154 + obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp
17.155 + {
17.156 + assume "\<exists>a v. ys = xs @ a # v"
17.157 + from this 1 a1 have thesis
17.158 + by (fastsimp simp add: append)
17.159 + } moreover
17.160 + {
17.161 + assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
17.162 + from this 2 a1 have thesis by (fastsimp simp add: append mem_def)
17.163 + } moreover
17.164 + note lexord[simplified a1]
17.165 + ultimately show thesis
17.166 + unfolding lexord_def
17.167 + by (fastsimp simp add: Collect_def)
17.168 +qed
17.169 +(*>*)
17.170 +subsubsection {* Options for values *}
17.171 +text {*
17.172 +In the presence of higher-order predicates, multiple modes for some predicate could be inferred
17.173 +that are not disambiguated by the pattern of the set comprehension.
17.174 +To disambiguate the modes for the arguments of a predicate, you can state
17.175 +the modes explicitly in the @{command "values"} command.
17.176 +Consider the simple predicate @{term "succ"}:
17.177 +*}
17.178 +inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
17.179 +where
17.180 + "succ 0 (Suc 0)"
17.181 +| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
17.182 +
17.183 +code_pred succ .
17.184 +
17.185 +text {*
17.186 +\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
17.187 + @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
17.188 +The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
17.189 +modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
17.190 +is chosen. To choose another mode for the argument, you can declare the mode for the argument between
17.191 +the @{command "values"} and the number of elements.
17.192 +*}
17.193 +values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
17.194 +values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
17.195 +
17.196 +subsubsection {* Embedding into functional code within Isabelle/HOL *}
17.197 +text {*
17.198 +To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
17.199 +you have a number of options:
17.200 +\begin{itemize}
17.201 +\item You want to use the first-order predicate with the mode
17.202 + where all arguments are input. Then you can use the predicate directly, e.g.
17.203 +\begin{quote}
17.204 + @{text "valid_suffix ys zs = "}\\
17.205 + @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
17.206 +\end{quote}
17.207 +\item If you know that the execution returns only one value (it is deterministic), then you can
17.208 + use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
17.209 + is defined with
17.210 +\begin{quote}
17.211 + @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
17.212 +\end{quote}
17.213 + Note that if the evaluation does not return a unique value, it raises a run-time error
17.214 + @{term "not_unique"}.
17.215 +\end{itemize}
17.216 +*}
17.217 +subsubsection {* Further Examples *}
17.218 +text {* Further examples for compiling inductive predicates can be found in
17.219 +the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
17.220 +There are also some examples in the Archive of Formal Proofs, notably
17.221 +in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
17.222 +*}
17.223 end
17.224 -
17.225 \ No newline at end of file
18.1 --- a/doc-src/Codegen/Thy/document/Program.tex Fri Dec 04 11:04:07 2009 +0100
18.2 +++ b/doc-src/Codegen/Thy/document/Program.tex Fri Dec 04 11:19:00 2009 +0100
18.3 @@ -968,6 +968,458 @@
18.4 \end{isamarkuptext}%
18.5 \isamarkuptrue%
18.6 %
18.7 +\isamarkupsubsection{Inductive Predicates%
18.8 +}
18.9 +\isamarkuptrue%
18.10 +%
18.11 +\begin{isamarkuptext}%
18.12 +To execute inductive predicates, a special preprocessor, the predicate
18.13 + compiler, generates code equations from the introduction rules of the predicates.
18.14 +The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
18.15 +Consider the simple predicate \isa{append} given by these two
18.16 +introduction rules:%
18.17 +\end{isamarkuptext}%
18.18 +\isamarkuptrue%
18.19 +%
18.20 +\isadelimquote
18.21 +%
18.22 +\endisadelimquote
18.23 +%
18.24 +\isatagquote
18.25 +%
18.26 +\begin{isamarkuptext}%
18.27 +\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
18.28 +\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
18.29 +\end{isamarkuptext}%
18.30 +\isamarkuptrue%
18.31 +%
18.32 +\endisatagquote
18.33 +{\isafoldquote}%
18.34 +%
18.35 +\isadelimquote
18.36 +%
18.37 +\endisadelimquote
18.38 +%
18.39 +\begin{isamarkuptext}%
18.40 +\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}}}}}:%
18.41 +\end{isamarkuptext}%
18.42 +\isamarkuptrue%
18.43 +%
18.44 +\isadelimquote
18.45 +%
18.46 +\endisadelimquote
18.47 +%
18.48 +\isatagquote
18.49 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
18.50 +\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
18.51 +%
18.52 +\endisatagquote
18.53 +{\isafoldquote}%
18.54 +%
18.55 +\isadelimquote
18.56 +%
18.57 +\endisadelimquote
18.58 +%
18.59 +\begin{isamarkuptext}%
18.60 +\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
18.61 +of the inductive predicate and then you put a period to discharge
18.62 +a trivial correctness proof.
18.63 +The compiler infers possible modes
18.64 +for the predicate and produces the derived code equations.
18.65 +Modes annotate which (parts of the) arguments are to be taken as input,
18.66 +and which output. Modes are similar to types, but use the notation \isa{i}
18.67 +for input and \isa{o} for output.
18.68 +
18.69 +For \isa{append}, the compiler can infer the following modes:
18.70 +\begin{itemize}
18.71 +\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
18.72 +\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
18.73 +\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
18.74 +\end{itemize}
18.75 +You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
18.76 +\end{isamarkuptext}%
18.77 +\isamarkuptrue%
18.78 +%
18.79 +\isadelimquote
18.80 +%
18.81 +\endisadelimquote
18.82 +%
18.83 +\isatagquote
18.84 +\isacommand{values}\isamarkupfalse%
18.85 +\ {\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}%
18.86 +\endisatagquote
18.87 +{\isafoldquote}%
18.88 +%
18.89 +\isadelimquote
18.90 +%
18.91 +\endisadelimquote
18.92 +%
18.93 +\begin{isamarkuptext}%
18.94 +\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and%
18.95 +\end{isamarkuptext}%
18.96 +\isamarkuptrue%
18.97 +%
18.98 +\isadelimquote
18.99 +%
18.100 +\endisadelimquote
18.101 +%
18.102 +\isatagquote
18.103 +\isacommand{values}\isamarkupfalse%
18.104 +\ {\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}%
18.105 +\endisatagquote
18.106 +{\isafoldquote}%
18.107 +%
18.108 +\isadelimquote
18.109 +%
18.110 +\endisadelimquote
18.111 +%
18.112 +\begin{isamarkuptext}%
18.113 +\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}}.%
18.114 +\end{isamarkuptext}%
18.115 +\isamarkuptrue%
18.116 +%
18.117 +\begin{isamarkuptext}%
18.118 +\noindent If you are only interested in the first elements of the set
18.119 +comprehension (with respect to a depth-first search on the introduction rules), you can
18.120 +pass an argument to
18.121 +\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
18.122 +\end{isamarkuptext}%
18.123 +\isamarkuptrue%
18.124 +%
18.125 +\isadelimquote
18.126 +%
18.127 +\endisadelimquote
18.128 +%
18.129 +\isatagquote
18.130 +\isacommand{values}\isamarkupfalse%
18.131 +\ {\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
18.132 +\isacommand{values}\isamarkupfalse%
18.133 +\ {\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}%
18.134 +\endisatagquote
18.135 +{\isafoldquote}%
18.136 +%
18.137 +\isadelimquote
18.138 +%
18.139 +\endisadelimquote
18.140 +%
18.141 +\begin{isamarkuptext}%
18.142 +\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
18.143 + comprehensions for which a mode has been inferred.
18.144 +
18.145 +The code equations for a predicate are made available as theorems with
18.146 + the suffix \isa{equation}, and can be inspected with:%
18.147 +\end{isamarkuptext}%
18.148 +\isamarkuptrue%
18.149 +%
18.150 +\isadelimquote
18.151 +%
18.152 +\endisadelimquote
18.153 +%
18.154 +\isatagquote
18.155 +\isacommand{thm}\isamarkupfalse%
18.156 +\ append{\isachardot}equation%
18.157 +\endisatagquote
18.158 +{\isafoldquote}%
18.159 +%
18.160 +\isadelimquote
18.161 +%
18.162 +\endisadelimquote
18.163 +%
18.164 +\begin{isamarkuptext}%
18.165 +\noindent More advanced options are described in the following subsections.%
18.166 +\end{isamarkuptext}%
18.167 +\isamarkuptrue%
18.168 +%
18.169 +\isamarkupsubsubsection{Alternative names for functions%
18.170 +}
18.171 +\isamarkuptrue%
18.172 +%
18.173 +\begin{isamarkuptext}%
18.174 +By default, the functions generated from a predicate are named after the predicate with the
18.175 +mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}).
18.176 +You can specify your own names as follows:%
18.177 +\end{isamarkuptext}%
18.178 +\isamarkuptrue%
18.179 +%
18.180 +\isadelimquote
18.181 +%
18.182 +\endisadelimquote
18.183 +%
18.184 +\isatagquote
18.185 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
18.186 +\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline
18.187 +\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline
18.188 +\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
18.189 +%
18.190 +\endisatagquote
18.191 +{\isafoldquote}%
18.192 +%
18.193 +\isadelimquote
18.194 +%
18.195 +\endisadelimquote
18.196 +%
18.197 +\isamarkupsubsubsection{Alternative introduction rules%
18.198 +}
18.199 +\isamarkuptrue%
18.200 +%
18.201 +\begin{isamarkuptext}%
18.202 +Sometimes the introduction rules of an predicate are not executable because they contain
18.203 +non-executable constants or specific modes could not be inferred.
18.204 +It is also possible that the introduction rules yield a function that loops forever
18.205 +due to the execution in a depth-first search manner.
18.206 +Therefore, you can declare alternative introduction rules for predicates with the attribute
18.207 +\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}.
18.208 +For example, the transitive closure is defined by:%
18.209 +\end{isamarkuptext}%
18.210 +\isamarkuptrue%
18.211 +%
18.212 +\isadelimquote
18.213 +%
18.214 +\endisadelimquote
18.215 +%
18.216 +\isatagquote
18.217 +%
18.218 +\begin{isamarkuptext}%
18.219 +\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
18.220 +\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
18.221 +\end{isamarkuptext}%
18.222 +\isamarkuptrue%
18.223 +%
18.224 +\endisatagquote
18.225 +{\isafoldquote}%
18.226 +%
18.227 +\isadelimquote
18.228 +%
18.229 +\endisadelimquote
18.230 +%
18.231 +\begin{isamarkuptext}%
18.232 +\noindent These rules do not suit well for executing the transitive closure
18.233 +with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
18.234 +cause an infinite loop in the recursive call.
18.235 +This can be avoided using the following alternative rules which are
18.236 +declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
18.237 +\end{isamarkuptext}%
18.238 +\isamarkuptrue%
18.239 +%
18.240 +\isadelimquote
18.241 +%
18.242 +\endisadelimquote
18.243 +%
18.244 +\isatagquote
18.245 +\isacommand{lemma}\isamarkupfalse%
18.246 +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
18.247 +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline
18.248 +\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline
18.249 +\isacommand{by}\isamarkupfalse%
18.250 +\ auto%
18.251 +\endisatagquote
18.252 +{\isafoldquote}%
18.253 +%
18.254 +\isadelimquote
18.255 +%
18.256 +\endisadelimquote
18.257 +%
18.258 +\begin{isamarkuptext}%
18.259 +\noindent After declaring all alternative rules for the transitive closure,
18.260 +you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
18.261 +As you have declared alternative rules for the predicate, you are urged to prove that these
18.262 +introduction rules are complete, i.e., that you can derive an elimination rule for the
18.263 +alternative rules:%
18.264 +\end{isamarkuptext}%
18.265 +\isamarkuptrue%
18.266 +%
18.267 +\isadelimquote
18.268 +%
18.269 +\endisadelimquote
18.270 +%
18.271 +\isatagquote
18.272 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
18.273 +\ tranclp\isanewline
18.274 +\isacommand{proof}\isamarkupfalse%
18.275 +\ {\isacharminus}\isanewline
18.276 +\ \ \isacommand{case}\isamarkupfalse%
18.277 +\ tranclp\isanewline
18.278 +\ \ \isacommand{from}\isamarkupfalse%
18.279 +\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
18.280 +\ thesis\ \isacommand{by}\isamarkupfalse%
18.281 +\ metis\isanewline
18.282 +\isacommand{qed}\isamarkupfalse%
18.283 +%
18.284 +\endisatagquote
18.285 +{\isafoldquote}%
18.286 +%
18.287 +\isadelimquote
18.288 +%
18.289 +\endisadelimquote
18.290 +%
18.291 +\begin{isamarkuptext}%
18.292 +\noindent Alternative rules can also be used for constants that have not
18.293 +been defined inductively. For example, the lexicographic order which
18.294 +is defined as:%
18.295 +\end{isamarkuptext}%
18.296 +\isamarkuptrue%
18.297 +%
18.298 +\isadelimquote
18.299 +%
18.300 +\endisadelimquote
18.301 +%
18.302 +\isatagquote
18.303 +%
18.304 +\begin{isamarkuptext}%
18.305 +\begin{isabelle}%
18.306 +lexord\ r\ {\isasymequiv}\isanewline
18.307 +{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
18.308 +\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
18.309 +\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}%
18.310 +\end{isabelle}%
18.311 +\end{isamarkuptext}%
18.312 +\isamarkuptrue%
18.313 +%
18.314 +\endisatagquote
18.315 +{\isafoldquote}%
18.316 +%
18.317 +\isadelimquote
18.318 +%
18.319 +\endisadelimquote
18.320 +%
18.321 +\begin{isamarkuptext}%
18.322 +\noindent To make it executable, you can derive the following two rules and prove the
18.323 +elimination rule:%
18.324 +\end{isamarkuptext}%
18.325 +\isamarkuptrue%
18.326 +%
18.327 +\isadelimproof
18.328 +%
18.329 +\endisadelimproof
18.330 +%
18.331 +\isatagproof
18.332 +%
18.333 +\endisatagproof
18.334 +{\isafoldproof}%
18.335 +%
18.336 +\isadelimproof
18.337 +%
18.338 +\endisadelimproof
18.339 +%
18.340 +\isadelimquote
18.341 +%
18.342 +\endisadelimquote
18.343 +%
18.344 +\isatagquote
18.345 +\isacommand{lemma}\isamarkupfalse%
18.346 +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
18.347 +\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
18.348 +\isacommand{lemma}\isamarkupfalse%
18.349 +\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
18.350 +\ \ {\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
18.351 +\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
18.352 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
18.353 +\ lexord%
18.354 +\endisatagquote
18.355 +{\isafoldquote}%
18.356 +%
18.357 +\isadelimquote
18.358 +%
18.359 +\endisadelimquote
18.360 +%
18.361 +\isamarkupsubsubsection{Options for values%
18.362 +}
18.363 +\isamarkuptrue%
18.364 +%
18.365 +\begin{isamarkuptext}%
18.366 +In the presence of higher-order predicates, multiple modes for some predicate could be inferred
18.367 +that are not disambiguated by the pattern of the set comprehension.
18.368 +To disambiguate the modes for the arguments of a predicate, you can state
18.369 +the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command.
18.370 +Consider the simple predicate \isa{succ}:%
18.371 +\end{isamarkuptext}%
18.372 +\isamarkuptrue%
18.373 +\isacommand{inductive}\isamarkupfalse%
18.374 +\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
18.375 +\isakeyword{where}\isanewline
18.376 +\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
18.377 +{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
18.378 +\isanewline
18.379 +\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
18.380 +\ succ%
18.381 +\isadelimproof
18.382 +\ %
18.383 +\endisadelimproof
18.384 +%
18.385 +\isatagproof
18.386 +\isacommand{{\isachardot}}\isamarkupfalse%
18.387 +%
18.388 +\endisatagproof
18.389 +{\isafoldproof}%
18.390 +%
18.391 +\isadelimproof
18.392 +%
18.393 +\endisadelimproof
18.394 +%
18.395 +\begin{isamarkuptext}%
18.396 +\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool},
18.397 + \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
18.398 +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
18.399 +modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
18.400 +is chosen. To choose another mode for the argument, you can declare the mode for the argument between
18.401 +the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
18.402 +\end{isamarkuptext}%
18.403 +\isamarkuptrue%
18.404 +%
18.405 +\isadelimquote
18.406 +%
18.407 +\endisadelimquote
18.408 +%
18.409 +\isatagquote
18.410 +\isacommand{values}\isamarkupfalse%
18.411 +\ {\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
18.412 +\isacommand{values}\isamarkupfalse%
18.413 +\ {\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}%
18.414 +\endisatagquote
18.415 +{\isafoldquote}%
18.416 +%
18.417 +\isadelimquote
18.418 +%
18.419 +\endisadelimquote
18.420 +%
18.421 +\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
18.422 +}
18.423 +\isamarkuptrue%
18.424 +%
18.425 +\begin{isamarkuptext}%
18.426 +To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
18.427 +you have a number of options:
18.428 +\begin{itemize}
18.429 +\item You want to use the first-order predicate with the mode
18.430 + where all arguments are input. Then you can use the predicate directly, e.g.
18.431 +\begin{quote}
18.432 + \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
18.433 + \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
18.434 +\end{quote}
18.435 +\item If you know that the execution returns only one value (it is deterministic), then you can
18.436 + use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
18.437 + is defined with
18.438 +\begin{quote}
18.439 + \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
18.440 +\end{quote}
18.441 + Note that if the evaluation does not return a unique value, it raises a run-time error
18.442 + \isa{not{\isacharunderscore}unique}.
18.443 +\end{itemize}%
18.444 +\end{isamarkuptext}%
18.445 +\isamarkuptrue%
18.446 +%
18.447 +\isamarkupsubsubsection{Further Examples%
18.448 +}
18.449 +\isamarkuptrue%
18.450 +%
18.451 +\begin{isamarkuptext}%
18.452 +Further examples for compiling inductive predicates can be found in
18.453 +the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
18.454 +There are also some examples in the Archive of Formal Proofs, notably
18.455 +in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
18.456 +\end{isamarkuptext}%
18.457 +\isamarkuptrue%
18.458 +%
18.459 \isadelimtheory
18.460 %
18.461 \endisadelimtheory
18.462 @@ -982,7 +1434,7 @@
18.463 %
18.464 \endisadelimtheory
18.465 \isanewline
18.466 -\ \end{isabellebody}%
18.467 +\end{isabellebody}%
18.468 %%% Local Variables:
18.469 %%% mode: latex
18.470 %%% TeX-master: "root"
19.1 --- a/doc-src/Codegen/codegen.tex Fri Dec 04 11:04:07 2009 +0100
19.2 +++ b/doc-src/Codegen/codegen.tex Fri Dec 04 11:19:00 2009 +0100
19.3 @@ -13,7 +13,7 @@
19.4
19.5 \title{\includegraphics[scale=0.5]{isabelle_isar}
19.6 \\[4ex] Code generation from Isabelle/HOL theories}
19.7 -\author{\emph{Florian Haftmann}}
19.8 +\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
19.9
19.10 \begin{document}
19.11
20.1 --- a/doc-src/manual.bib Fri Dec 04 11:04:07 2009 +0100
20.2 +++ b/doc-src/manual.bib Fri Dec 04 11:19:00 2009 +0100
20.3 @@ -172,6 +172,14 @@
20.4 title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
20.5 crossref = {tphols2001}}
20.6
20.7 +@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
20.8 + author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
20.9 + booktitle = {Theorem Proving in Higher Order Logics},
20.10 + pages = {131--146},
20.11 + title = {Turning Inductive into Equational Specifications},
20.12 + year = {2009}
20.13 +}
20.14 +
20.15 @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
20.16 crossref = "tphols2000",
20.17 title = "Proof terms for simply typed higher order logic",
21.1 --- a/etc/settings Fri Dec 04 11:04:07 2009 +0100
21.2 +++ b/etc/settings Fri Dec 04 11:19:00 2009 +0100
21.3 @@ -208,21 +208,9 @@
21.4 ## Set HOME only for tools you have installed!
21.5
21.6 # External provers
21.7 -E_HOME=$(choosefrom \
21.8 - "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
21.9 - "$ISABELLE_HOME/../E/$ML_PLATFORM" \
21.10 - "/usr/local/E/$ML_PLATFORM" \
21.11 - "")
21.12 -VAMPIRE_HOME=$(choosefrom \
21.13 - "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
21.14 - "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
21.15 - "/usr/local/vampire/$ML_PLATFORM" \
21.16 - "")
21.17 -SPASS_HOME=$(choosefrom \
21.18 - "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
21.19 - "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
21.20 - "/usr/local/spass/$ML_PLATFORM" \
21.21 - "")
21.22 +#E_HOME=/usr/local/bin
21.23 +#SPASS_HOME=/usr/local/bin
21.24 +#VAMPIRE_HOME=/usr/local/bin
21.25
21.26 # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
21.27 #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
22.1 --- a/lib/Tools/findlogics Fri Dec 04 11:04:07 2009 +0100
22.2 +++ b/lib/Tools/findlogics Fri Dec 04 11:19:00 2009 +0100
22.3 @@ -39,4 +39,4 @@
22.4 done
22.5 done
22.6
22.7 -echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq)
22.8 +echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)
23.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Dec 04 11:04:07 2009 +0100
23.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Dec 04 11:19:00 2009 +0100
23.3 @@ -537,8 +537,8 @@
23.4 fun token s =
23.5 Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
23.6 val numeral = Scan.one isnum
23.7 - val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
23.8 - val decimalfrac = Scan.repeat numeral
23.9 + val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
23.10 + val decimalfrac = Scan.repeat1 numeral
23.11 >> (fn s => rat_of_string(implode s) // pow10 (length s))
23.12 val decimalsig =
23.13 decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
24.1 --- a/src/Pure/Syntax/syntax.ML Fri Dec 04 11:04:07 2009 +0100
24.2 +++ b/src/Pure/Syntax/syntax.ML Fri Dec 04 11:19:00 2009 +0100
24.3 @@ -496,7 +496,7 @@
24.4 else if ! ambiguity_is_error then error (ambiguity_msg pos)
24.5 else
24.6 (warning (cat_lines
24.7 - (("Ambiguous input " ^ Position.str_of pos ^
24.8 + (("Ambiguous input" ^ Position.str_of pos ^
24.9 "\nproduces " ^ string_of_int len ^ " parse trees" ^
24.10 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
24.11 map show_pt (Library.take (limit, pts)))));
25.1 --- a/src/Pure/pure_setup.ML Fri Dec 04 11:04:07 2009 +0100
25.2 +++ b/src/Pure/pure_setup.ML Fri Dec 04 11:19:00 2009 +0100
25.3 @@ -39,6 +39,11 @@
25.4 then use "ML-Systems/install_pp_polyml.ML"
25.5 else ();
25.6
25.7 +if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
25.8 + Secure.use_text ML_Parse.global_context (0, "") false
25.9 + "PolyML.Compiler.maxInlineSize := 20"
25.10 +else ();
25.11 +
25.12
25.13 (* ML toplevel use commands *)
25.14