--- a/bin/isabelle Wed Aug 26 10:48:12 2009 +0200
+++ b/bin/isabelle Wed Aug 26 10:48:45 2009 +0200
@@ -17,7 +17,7 @@
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-ORIG_IFS="$IFS"; IFS=":"; declare -a TOOLS=($ISABELLE_TOOLS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
## diagnostics
--- a/bin/isabelle-process Wed Aug 26 10:48:12 2009 +0200
+++ b/bin/isabelle-process Wed Aug 26 10:48:45 2009 +0200
@@ -160,7 +160,7 @@
INFILE=""
ISA_PATH=""
- ORIG_IFS="$IFS"; IFS=":"; declare -a PATHS=($ISABELLE_PATH); IFS="$ORIG_IFS"
+ splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
for DIR in "${PATHS[@]}"
do
DIR="$DIR/$ML_IDENTIFIER"
--- a/etc/components Wed Aug 26 10:48:12 2009 +0200
+++ b/etc/components Wed Aug 26 10:48:45 2009 +0200
@@ -12,5 +12,5 @@
src/Sequents
#misc components
src/HOL/Tools/ATP_Manager
+src/HOL/Tools/Mirabelle
src/HOL/Library/Sum_Of_Squares
-src/HOL/Tools/Mirabelle
--- a/etc/settings Wed Aug 26 10:48:12 2009 +0200
+++ b/etc/settings Wed Aug 26 10:48:45 2009 +0200
@@ -207,22 +207,6 @@
###
-### jEdit
-###
-
-JEDIT_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/jedit" \
- "$ISABELLE_HOME/../jedit" \
- "/usr/local/jedit" \
- "/usr/share/jedit" \
- "/opt/jedit" \
- "")
-
-JEDIT_JAVA_OPTIONS=""
-#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
-JEDIT_OPTIONS="-reuseview -noserver -nobackground"
-
-###
### External reasoning tools
###
--- a/lib/Tools/doc Wed Aug 26 10:48:12 2009 +0200
+++ b/lib/Tools/doc Wed Aug 26 10:48:45 2009 +0200
@@ -34,7 +34,7 @@
## main
-ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}")
if [ -z "$DOC" ]; then
for DIR in "${DOCS[@]}"
--- a/lib/Tools/document Wed Aug 26 10:48:12 2009 +0200
+++ b/lib/Tools/document Wed Aug 26 10:48:45 2009 +0200
@@ -53,7 +53,7 @@
OUTFORMAT="$OPTARG"
;;
t)
- ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS"
+ splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
;;
\?)
usage
--- a/lib/Tools/findlogics Wed Aug 26 10:48:12 2009 +0200
+++ b/lib/Tools/findlogics Wed Aug 26 10:48:45 2009 +0200
@@ -25,7 +25,7 @@
declare -a LOGICS=()
declare -a ISABELLE_PATHS=()
-ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS
+splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
for DIR in "${ISABELLE_PATHS[@]}"
do
@@ -34,7 +34,7 @@
do
if [ -f "$FILE" ]; then
NAME=$(basename "$FILE")
- LOGICS+=("$NAME")
+ LOGICS["${#LOGICS[@]}"]="$NAME"
fi
done
done
--- a/lib/Tools/jedit Wed Aug 26 10:48:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: Isabelle/jEdit interface wrapper
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-[ -z "$JEDIT_HOME" ] && fail "Missing Isabelle/jEdit installation (JEDIT_HOME)"
-
-INTERFACE="$JEDIT_HOME/interface"
-[ ! -x "$INTERFACE" ] && fail "Bad interface script: \"$INTERFACE\""
-
-exec "$INTERFACE" "$@"
--- a/lib/Tools/makeall Wed Aug 26 10:48:12 2009 +0200
+++ b/lib/Tools/makeall Wed Aug 26 10:48:45 2009 +0200
@@ -34,7 +34,7 @@
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_COMPONENTS"; COMPONENTS=("${SPLITARRAY[@]}")
for DIR in "${COMPONENTS[@]}"
do
--- a/lib/scripts/getsettings Wed Aug 26 10:48:12 2009 +0200
+++ b/lib/scripts/getsettings Wed Aug 26 10:48:45 2009 +0200
@@ -68,6 +68,17 @@
done
}
+#arrays
+function splitarray ()
+{
+ SPLITARRAY=()
+ local IFS="$1"; shift
+ for X in $*
+ do
+ SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
+ done
+}
+
#nested components
ISABELLE_COMPONENTS=""
function init_component ()
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Wed Aug 26 10:48:12 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Wed Aug 26 10:48:45 2009 +0200
@@ -7,11 +7,11 @@
type action
val register : string * action -> theory -> theory
+ val logfile : string Config.T
val timeout : int Config.T
val verbose : bool Config.T
val start_line : int Config.T
val end_line : int Config.T
- val set_logfile : string -> theory -> theory
val goal_thm_of : Proof.state -> thm
val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
@@ -59,10 +59,6 @@
val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
-fun set_logfile name =
- let val _ = File.write (Path.explode name) "" (* erase file content *)
- in Config.put_thy logfile name end
-
local
fun log thy s =
@@ -90,15 +86,11 @@
let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
in if in_range l r (Position.line_of pos) then f x else [] end
-fun pretty_print verbose pos name msgs =
+fun pretty_print pos name msgs =
let
- val file = the_default "unknown file" (Position.file_of pos)
-
val str0 = string_of_int o the_default 0
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
-
- val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
- val head = full_loc ^ " (" ^ name ^ "):"
+ val head = "at " ^ loc ^ " (" ^ name ^ "):"
fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
in
@@ -119,7 +111,7 @@
Actions.get thy
|> Symtab.dest
|> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
- |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
+ |> (fn [] => () | msgs => log thy (pretty_print pos name msgs))
end
end
--- a/src/HOL/Tools/Mirabelle/etc/settings Wed Aug 26 10:48:12 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/etc/settings Wed Aug 26 10:48:45 2009 +0200
@@ -6,4 +6,4 @@
MIRABELLE_TIMEOUT=30
MIRABELLE_VERBOSE=false
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Wed Aug 26 10:48:12 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Wed Aug 26 10:48:45 2009 +0200
@@ -7,15 +7,17 @@
PRG="$(basename "$0")"
-function action_names() {
+function print_action_names() {
TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
- ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'`
+ for NAME in $TOOLS
+ do
+ echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/'
+ done
}
function usage() {
out="$MIRABELLE_OUTPUT_PATH"
timeout="$MIRABELLE_TIMEOUT"
- action_names
echo
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
echo
@@ -31,14 +33,11 @@
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
- for NAME in $ACTION_NAMES
- do
- echo " $NAME"
- done
+ print_action_names
echo
- echo " FILES is a space-separated list of theory files, where each file is"
- echo " either NAME.thy or NAME.thy[START:END] and START and END are numbers"
- echo " indicating the range the given actions are to be applied."
+ echo " FILES is a list of theory files, where each file is either NAME.thy"
+ echo " or NAME.thy[START:END] and START and END are numbers indicating the"
+ echo " range the given actions are to be applied."
echo
exit 1
}
@@ -48,7 +47,7 @@
# options
-while getopts "L:T:O:vt:" OPT
+while getopts "L:T:O:vt:?" OPT
do
case "$OPT" in
L)
@@ -61,7 +60,7 @@
MIRABELLE_OUTPUT_PATH="$OPTARG"
;;
v)
- MIRABELLE_VERBOSE=true
+ MIRABELLE_VERBOSE="true"
;;
t)
MIRABELLE_TIMEOUT="$OPTARG"
@@ -81,13 +80,13 @@
# setup
-mkdir -p $MIRABELLE_OUTPUT_PATH
+mkdir -p "$MIRABELLE_OUTPUT_PATH"
## main
for FILE in "$@"
do
- perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE"
+ perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
done
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Wed Aug 26 10:48:12 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Wed Aug 26 10:48:45 2009 +0200
@@ -43,9 +43,11 @@
my $log_file = $output_path . "/" . $thy_name . ".log";
my @action_files;
+my @action_names;
foreach (split(/:/, $actions)) {
if (m/([^[]*)/) {
push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
+ push @action_names, $1;
}
}
my $tools = "";
@@ -62,7 +64,7 @@
begin
setup {*
- Mirabelle.set_logfile "$log_file" #>
+ Config.put_thy Mirabelle.logfile "$log_file" #>
Config.put_thy Mirabelle.timeout $timeout #>
Config.put_thy Mirabelle.verbose $verbose #>
Config.put_thy Mirabelle.start_line $start_line #>
@@ -99,7 +101,8 @@
my $thy_text = join("", @lines);
my $old_len = length($thy_text);
-$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm;
+$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
+$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
die "No 'imports' found" if length($thy_text) == $old_len;
open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
@@ -114,14 +117,21 @@
# run isabelle
-my $r = system "$isabelle_home/bin/isabelle-process " .
+open(LOG_FILE, ">$log_file");
+print LOG_FILE "Run of $new_thy_file with:\n";
+foreach $name (@action_names) {
+ print LOG_FILE " $name\n";
+}
+print LOG_FILE "\n\n";
+close(LOG_FILE);
+
+my $r = system "\"$ISABELLE_PROCESS\" " .
"-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
# cleanup
unlink $root_file;
-unlink $new_thy_file;
unlink $setup_file;
exit $r;
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Aug 26 10:48:12 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Aug 26 10:48:45 2009 +0200
@@ -246,8 +246,10 @@
RS eq_reflection
end;
-fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT
- | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT
+fun is_intrel_type T = T = @{typ "int => int => bool"};
+
+fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
+ | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
| is_intrel _ = false;
fun linearize_conv ctxt vs ct = case term_of ct of
--- a/src/HOL/ex/Termination.thy Wed Aug 26 10:48:12 2009 +0200
+++ b/src/HOL/ex/Termination.thy Wed Aug 26 10:48:45 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Termination.thy
- ID: $Id$
Author: Lukas Bulwahn, TU Muenchen
Author: Alexander Krauss, TU Muenchen
*)
@@ -10,12 +9,33 @@
imports Main Multiset
begin
+subsection {* Manually giving termination relations using @{text relation} and
+@{term measure} *}
+
+function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
+by pat_completeness auto
+
+termination by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
+
+function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "foo i N = (if i > N
+ then (if N = 0 then 0 else foo 0 (N - 1))
+ else i + foo (Suc i) N)"
+by pat_completeness auto
+
+termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
+
+
+subsection {* @{text lexicographic_order}: Trivial examples *}
+
text {*
- The @{text fun} command uses the method @{text lexicographic_order} by default.
+ The @{text fun} command uses the method @{text lexicographic_order} by default,
+ so it is not explicitly invoked.
*}
-subsection {* Trivial examples *}
-
fun identity :: "nat \<Rightarrow> nat"
where
"identity n = n"