merged
authorpaulson
Fri, 21 Aug 2009 14:40:19 +0100
changeset 32405 48786f277130
parent 32388 b23a4326b9bb (diff)
parent 32404 da3ca3c6ec81 (current diff)
child 32406 9ea59bd1397a
merged
--- a/NEWS	Fri Aug 14 17:26:11 2009 +0100
+++ b/NEWS	Fri Aug 21 14:40:19 2009 +0100
@@ -18,6 +18,10 @@
 
 *** HOL ***
 
+* New testing tool "Mirabelle" for automated (proof) tools. Applies several
+tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
+in a theory. To be used in batch mode via "isabelle mirabelle".
+
 * New proof method "sos" (sum of squares) for nonlinear real arithmetic
 (originally due to John Harison). It requires Library/Sum_Of_Squares.
 It is not a complete decision procedure but works well in practice
--- a/etc/components	Fri Aug 14 17:26:11 2009 +0100
+++ b/etc/components	Fri Aug 21 14:40:19 2009 +0100
@@ -13,4 +13,4 @@
 #misc components
 src/HOL/Tools/ATP_Manager
 src/HOL/Library/Sum_Of_Squares
-
+src/HOL/Tools/Mirabelle
--- a/lib/scripts/mirabelle	Fri Aug 14 17:26:11 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-#!/usr/bin/perl -w
-
-use strict;
-use File::Basename;
-
-# Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html
-sub trim {
-    my @out = @_;
-    for (@out) {
-        s/^\s+//;
-        s/\s+$//;
-    }
-    return wantarray ? @out : $out[0];
-}
-
-sub quote {
-    my $str = pop;
-    return "\"" . $str . "\"";
-}
-
-sub print_usage_and_quit {
-    print STDERR "Usage: mirabelle actions file1.thy...\n" .
-                 "  actions: action1:...:actionN\n" .
-                 "  action: name or name[key1=value1,...,keyM=valueM]\n";
-    exit 1;
-}
-
-my $num_args = $#ARGV + 1;
-if ($num_args < 2) {
-    print_usage_and_quit();
-}
-
-my @action_names;
-my @action_settings;
-
-foreach (split(/:/, $ARGV[0])) {
-    my %settings;
-
-    $_ =~ /([^[]*)(?:\[(.*)\])?/;
-    my ($name, $settings_str) = ($1, $2 || "");
-    my @setting_strs = split(/,/, $settings_str);
-    foreach (@setting_strs) {
-        $_ =~ /(.*)=(.*)/;
-	    my $key = $1;
-	    my $value = $2;
-	    $settings{trim($key)} = trim($value);
-    }
-
-    push @action_names, trim($name);
-    push @action_settings, \%settings;
-}
-
-my $output_path = "/tmp/mirabelle"; # FIXME: generate path
-my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup";
-my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy";
-my $mirabelle_log_file = $output_path . "/mirabelle.log";
-
-mkdir $output_path, 0755;
-
-open(FILE, ">$mirabellesetup_file")
-    || die "Could not create file '$mirabellesetup_file'";
-
-my $invoke_lines;
-
-for my $i (0 .. $#action_names) { 
-    my $settings_str = "";
-    my $settings = $action_settings[$i];
-    my $key;
-    my $value;
-
-    while (($key, $value) = each(%$settings)) {
-        $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), ";
-    }
-    $settings_str =~ s/, $//;
-
-    $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" ";
-    $invoke_lines .= "[$settings_str] *}\n"
-}
-
-print FILE <<EOF;
-theory MirabelleSetup
-imports Mirabelle
-begin
-
-setup {* Mirabelle.set_logfile "$mirabelle_log_file" *}
-
-$invoke_lines
-
-end
-EOF
-
-my $root_text = "";
-my @new_thy_files;
-
-for my $i (1 .. $num_args - 1) {
-    my $old_thy_file = $ARGV[$i];
-    my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy");
-    my $new_thy_name = $base . "Mirabelle";
-    my $new_thy_file = $dir . $new_thy_name . $ext;
-
-    open(OLD_FILE, "<$old_thy_file")
-        || die "Cannot open file $old_thy_file";
-    my @lines = <OLD_FILE>;
-    close(OLD_FILE);
-
-    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 "$mirabellesetup_thy_name" /gm;
-    die "No 'imports' found" if length($thy_text) == $old_len;
-
-    open(NEW_FILE, ">$new_thy_file");
-    print NEW_FILE $thy_text;
-    close(NEW_FILE);
-
-    $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n";
-
-    push @new_thy_files, $new_thy_file;
-}
-
-my $root_file = "ROOT_mirabelle.ML";
-open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file";
-print ROOT_FILE $root_text;
-close(ROOT_FILE);
-
-system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL";
-
-# unlink $mirabellesetup_file;
-unlink $root_file;
-unlink @new_thy_files;
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 21 14:40:19 2009 +0100
@@ -633,6 +633,5 @@
          (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
-atp_minimize [atp=spass] A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz
 by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
 end
--- a/src/HOL/Code_Eval.thy	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Code_Eval.thy	Fri Aug 21 14:40:19 2009 +0100
@@ -134,7 +134,7 @@
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
     (let (n, m) = nibble_pair_of_char c
-  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   by (subst term_of_anything) rule 
 
--- a/src/HOL/Predicate.thy	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Predicate.thy	Fri Aug 21 14:40:19 2009 +0100
@@ -646,7 +646,7 @@
 @{code_datatype pred = Seq};
 @{code_datatype seq = Empty | Insert | Join};
 
-fun yield (Seq f) = next (f ())
+fun yield (@{code Seq} f) = next (f ())
 and next @{code Empty} = NONE
   | next (@{code Insert} (x, P)) = SOME (x, P)
   | next (@{code Join} (P, xq)) = (case yield P
--- a/src/HOL/Quickcheck.thy	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Aug 21 14:40:19 2009 +0100
@@ -54,7 +54,7 @@
 begin
 
 definition 
-  "random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))"
+  "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
 
 instance ..
 
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -119,7 +119,7 @@
     val tycos = map fst dataTs;
     val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
       else error ("Type constructors " ^ commas (map quote raw_tycos)
-        ^ "do not belong exhaustively to one mutual recursive datatype");
+        ^ " do not belong exhaustively to one mutual recursive datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,25 @@
+(* Title: Mirabelle.thy
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+theory Mirabelle
+imports Pure
+uses "Tools/mirabelle.ML"
+begin
+
+(* no multithreading, no parallel proofs *)
+ML {* Multithreading.max_threads := 1 *}
+ML {* Goal.parallel_proofs := 0 *}
+
+ML {* Toplevel.add_hook Mirabelle.step_hook *}
+
+setup Mirabelle.setup
+
+ML {*
+signature MIRABELLE_ACTION =
+sig
+  val invoke : (string * string) list -> theory -> theory
+end
+*}
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,193 @@
+(* Title:  mirabelle.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+signature MIRABELLE =
+sig
+  type action
+  val register : string * action -> theory -> theory
+
+  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
+  val theorems_in_proof_term : Thm.thm -> Thm.thm list
+  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
+  val get_setting : (string * string) list -> string * string -> string
+  val get_int_setting : (string * string) list -> string * int -> int
+end
+
+
+
+signature MIRABELLE_EXT =
+sig
+  include MIRABELLE
+  val setup : theory -> theory
+  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
+    unit
+end
+
+
+
+structure Mirabelle : MIRABELLE_EXT =
+struct
+
+(* Mirabelle core *)
+
+type action = {pre: Proof.state, post: Toplevel.state option} -> string option
+
+structure Actions = TheoryDataFun
+(
+  type T = action Symtab.table
+  val empty = Symtab.empty
+  val copy = I
+  val extend = I
+  fun merge _ = Symtab.merge (K true)
+)
+
+val register = Actions.map o Symtab.update_new
+
+val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
+val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
+val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
+val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
+val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
+
+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 =
+  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
+  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
+  (* FIXME: with multithreading and parallel proofs enabled, we might need to
+     encapsulate this inside a critical section *)
+
+fun verbose_msg verbose msg = if verbose then SOME msg else NONE
+
+fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
+  handle TimeLimit.TimeOut => verbose_msg verb "time out"
+       | ERROR msg => verbose_msg verb ("error: " ^ msg)
+
+fun capture_exns verb f x =
+  (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
+
+fun apply_action (c as (verb, _)) st (name, action) =
+  Option.map (pair name) (capture_exns verb (with_time_limit c action) st)
+
+fun in_range _ _ NONE = true
+  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
+
+fun only_within_range thy pos f x =
+  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 =
+  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 ^ "):"
+
+    fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
+  in
+    Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
+  end
+
+in
+
+fun basic_hook tr pre post =
+  let
+    val thy = Proof.theory_of pre
+    val pos = Toplevel.pos_of tr
+    val name = Toplevel.name_of tr
+    val verb = Config.get_thy thy verbose
+    val secs = Time.fromSeconds (Config.get_thy thy timeout)
+    val st = {pre=pre, post=post}
+  in
+    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))
+  end
+
+end
+
+fun step_hook tr pre post =
+ (* FIXME: might require wrapping into "interruptible" *)
+  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
+     not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
+  then basic_hook tr (Toplevel.proof_of pre) (SOME post)
+  else ()   (* FIXME: add theory_hook here *)
+
+
+
+(* Mirabelle utility functions *)
+
+val goal_thm_of = snd o snd o Proof.get_goal
+
+fun can_apply tac st =
+  let val (ctxt, (facts, goal)) = Proof.get_goal st
+  in
+    (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
+      SOME (thm, _) => true
+    | NONE => false)
+  end
+
+local
+
+fun fold_body_thms f =
+  let
+    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
+      fn (x, seen) =>
+        if Inttab.defined seen i then (x, seen)
+        else
+          let
+            val body' = Future.join body
+            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
+              (x, Inttab.update (i, ()) seen)
+        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
+  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
+
+in
+
+fun theorems_in_proof_term thm =
+  let
+    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
+    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
+    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
+    fun resolve_thms names = map_filter (member_of names) all_thms
+  in
+    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
+  end
+
+end
+
+fun theorems_of_sucessful_proof state =
+  (case state of
+    NONE => []
+  | SOME st =>
+      if not (Toplevel.is_proof st) then []
+      else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
+
+fun get_setting settings (key, default) =
+  the_default default (AList.lookup (op =) settings key)
+
+fun get_int_setting settings (key, default) =
+  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
+    SOME (SOME i) => i
+  | SOME NONE => error ("bad option: " ^ key)
+  | NONE => default)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,15 @@
+(* Title:  mirabelle_arith.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Arith : MIRABELLE_ACTION =
+struct
+
+fun arith_action {pre=st, ...} =
+  if Mirabelle.can_apply Arith_Data.arith_tac st
+  then SOME "succeeded"
+  else NONE
+
+fun invoke _ = Mirabelle.register ("arith", arith_action)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,24 @@
+(* Title:  mirabelle_metis.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Metis : MIRABELLE_ACTION =
+struct
+
+fun metis_action {pre, post} =
+  let
+    val thms = Mirabelle.theorems_of_sucessful_proof post
+    val names = map Thm.get_name thms
+
+    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
+
+    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
+  in
+    (if Mirabelle.can_apply metis pre then "succeeded" else "failed")
+    |> suffix (" (" ^ commas names ^ ")")
+    |> SOME
+  end
+
+fun invoke _ = Mirabelle.register ("metis", metis_action)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,19 @@
+(* Title:  mirabelle_quickcheck.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
+struct
+
+fun quickcheck_action args {pre=st, ...} =
+  let
+    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+  in
+    (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
+      NONE => SOME "no counterexample"
+    | SOME _ => SOME "counterexample found")
+  end
+
+fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,38 @@
+(* Title:  mirabelle_refute.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Refute : MIRABELLE_ACTION =
+struct
+
+
+(* FIXME:
+fun refute_action args {pre=st, ...} = 
+  let
+    val subgoal = 0
+    val thy     = Proof.theory_of st
+    val thm = goal_thm_of st
+
+    val _ = Refute.refute_subgoal thy args thm subgoal
+  in
+    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
+    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
+
+    val r =
+      if Substring.isSubstring "model found" writ_log
+      then
+        if Substring.isSubstring "spurious" warn_log
+        then SOME "potential counterexample"
+        else SOME "real counterexample (bug?)"
+      else
+        if Substring.isSubstring "time limit" writ_log
+        then SOME "no counterexample (time out)"
+        else if Substring.isSubstring "Search terminated" writ_log
+        then SOME "no counterexample (normal termination)"
+        else SOME "no counterexample (unknown)"
+  in r end
+*)
+
+fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,31 @@
+(* Title:  mirabelle_sledgehammer.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
+struct
+
+fun sledgehammer_action {pre=st, ...} =
+  let
+    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
+    val thy = Proof.theory_of st
+ 
+    val prover = the (AtpManager.get_prover prover_name thy)
+    val timeout = AtpManager.get_timeout () 
+
+    val (success, message) =
+      let
+        val (success, message, _, _, _) =
+          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
+      in (success, message) end
+      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
+           | ERROR msg => (false, "error: " ^ msg)
+  in
+    if success
+    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
+    else NONE
+  end
+
+fun invoke _ = Mirabelle.register ("sledgehammer", sledgehammer_action)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/etc/settings	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,9 @@
+MIRABELLE_HOME="$COMPONENT"
+
+MIRABELLE_LOGIC=HOL
+MIRABELLE_THEORY=Main
+MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
+MIRABELLE_TIMEOUT=30
+MIRABELLE_VERBOSE=false
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,93 @@
+#!/usr/bin/env bash
+#
+# Author: Sascha Boehme
+#
+# DESCRIPTION: testing tool for automated proof tools
+
+
+PRG="$(basename "$0")"
+
+function action_names() {
+  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
+  ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'`
+}
+
+function usage() {
+  out="$MIRABELLE_OUTPUT_PATH"
+  timeout="$MIRABELLE_TIMEOUT"
+  action_names
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
+  echo
+  echo "  Options are:"
+  echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
+  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
+  echo "    -O DIR       output directory for test data (default $out)"
+  echo "    -v           be verbose"
+  echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
+  echo
+  echo "  Apply the given actions (i.e., automated proof tools)"
+  echo "  at all proof steps in the given theory files."
+  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
+  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
+  exit 1
+}
+
+
+## process command line
+
+# options
+
+while getopts "L:T:O:vt:" OPT
+do
+  case "$OPT" in
+    L)
+      MIRABELLE_LOGIC="$OPTARG"
+      ;;
+    T)
+      MIRABELLE_THEORY="$OPTARG"
+      ;;
+    O)
+      MIRABELLE_OUTPUT_PATH="$OPTARG"
+      ;;
+    v)
+      MIRABELLE_VERBOSE=true
+      ;;
+    t)
+      MIRABELLE_TIMEOUT="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+ACTIONS="$1"
+
+shift
+
+
+# setup
+
+mkdir -p $MIRABELLE_OUTPUT_PATH
+
+
+## main
+
+for FILE in "$@"
+do
+  perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE"
+done
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 21 14:40:19 2009 +0100
@@ -0,0 +1,128 @@
+#
+# Author: Jasmin Blanchette and Sascha Boehme
+#
+# Testing tool for automated proof tools.
+#
+
+use File::Basename;
+
+# environment
+
+my $isabelle_home = $ENV{'ISABELLE_HOME'};
+my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
+my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
+my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
+my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
+my $verbose = $ENV{'MIRABELLE_VERBOSE'};
+my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
+
+my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
+
+
+# arguments
+
+my $actions = $ARGV[0];
+
+my $thy_file = $ARGV[1];
+my $start_line = "0";
+my $end_line = "~1";
+if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME
+  my $thy_file = $1;
+  my $start_line = $2;
+  my $end_line = $3;
+}
+my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
+my $new_thy_name = $thy_name . "_Mirabelle";
+my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
+
+
+# setup
+
+my $setup_thy_name = $thy_name . "_Setup";
+my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
+my $log_file = $output_path . "/" . $thy_name . ".log";
+
+my @action_files;
+foreach (split(/:/, $actions)) {
+  if (m/([^[]*)/) {
+    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
+  }
+}
+my $tools = "";
+if ($#action_files >= 0) {
+  $tools = "uses " . join(" ", @action_files);
+}
+
+open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
+
+print SETUP_FILE <<END;
+theory "$setup_thy_name"
+imports "$mirabelle_thy" "$mirabelle_theory"
+$tools
+begin
+
+setup {* 
+  Mirabelle.set_logfile "$log_file" #>
+  Config.put_thy Mirabelle.timeout $timeout #>
+  Config.put_thy Mirabelle.verbose $verbose #>
+  Config.put_thy Mirabelle.start_line $start_line #>
+  Config.put_thy Mirabelle.end_line $end_line
+*}
+
+END
+
+foreach (split(/:/, $actions)) {
+  if (m/([^[]*)(?:\[(.*)\])?/) {
+    my ($name, $settings_str) = ($1, $2 || "");
+    $name =~ s/^([a-z])/\U$1/;
+    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
+    my $sep = "";
+    foreach (split(/,/, $settings_str)) {
+      if (m/\s*(.*)\s*=\s*(.*)\s*/) {
+        print SETUP_FILE "$sep(\"$1\", \"$2\")";
+        $sep = ", ";
+      }
+    }
+    print SETUP_FILE "] *}\n";
+  }
+}
+
+print SETUP_FILE "\nend";
+close SETUP_FILE;
+
+
+# modify target theory file
+
+open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
+my @lines = <OLD_FILE>;
+close(OLD_FILE);
+
+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;
+die "No 'imports' found" if length($thy_text) == $old_len;
+
+open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
+print NEW_FILE $thy_text;
+close(NEW_FILE);
+
+my $root_file = "$output_path/ROOT_$thy_name.ML";
+open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
+print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
+close(ROOT_FILE);
+
+
+# run isabelle
+
+my $r = system "$isabelle_home/bin/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/lin_arith.ML	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -67,7 +67,7 @@
     and ct = cterm_of thy t
   in instantiate ([], [(cn, ct)]) @{thm le0} end;
 
-end;
+end;  (* LA_Logic *)
 
 
 (* arith context data *)
@@ -279,7 +279,7 @@
 
 
 (*---------------------------------------------------------------------------*)
-(* the following code performs splitting of certain constants (e.g. min,     *)
+(* the following code performs splitting of certain constants (e.g., min,    *)
 (* max) in a linear arithmetic problem; similar to what split_tac later does *)
 (* to the proof state                                                        *)
 (*---------------------------------------------------------------------------*)
@@ -342,23 +342,30 @@
   (* takes a list  [t1, ..., tn]  to the term                                *)
   (*   tn' --> ... --> t1' --> False  ,                                      *)
   (* where ti' = HOLogic.dest_Trueprop ti                                    *)
-  fun REPEAT_DETERM_etac_rev_mp terms' =
-    fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
-  val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
-  val cmap       = Splitter.cmap_of_split_thms split_thms
-  val splits     = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
+  fun REPEAT_DETERM_etac_rev_mp tms =
+    fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
+      HOLogic.false_const
+  val split_thms  = filter is_split_thm (#splits (get_arith_data ctxt))
+  val cmap        = Splitter.cmap_of_split_thms split_thms
+  val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
+  val splits      = Splitter.split_posns cmap thy Ts goal_tm
   val split_limit = Config.get ctxt split_limit
 in
-  if length splits > split_limit then
-   (tracing ("linarith_split_limit exceeded (current value is " ^
-      string_of_int split_limit ^ ")"); NONE)
-  else (
-  case splits of [] =>
+  if length splits > split_limit then (
+    tracing ("linarith_split_limit exceeded (current value is " ^
+      string_of_int split_limit ^ ")");
+    NONE
+  ) else case splits of
+    [] =>
     (* split_tac would fail: no possible split *)
     NONE
-  | ((_, _, _, split_type, split_term) :: _) => (
-    (* ignore all but the first possible split *)
-    case strip_comb split_term of
+  | (_, _::_, _, _, _) :: _ =>
+    (* disallow a split that involves non-locally bound variables (except    *)
+    (* when bound by outermost meta-quantifiers)                             *)
+    NONE
+  | (_, [], _, split_type, split_term) :: _ =>
+    (* ignore all but the first possible split                               *)
+    (case strip_comb split_term of
     (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
       (Const (@{const_name Orderings.max}, _), [t1, t2]) =>
       let
@@ -627,12 +634,11 @@
     (* out                                                                   *)
     | (t, ts) => (
       warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
-               " (with " ^ string_of_int (length ts) ^
-               " argument(s)) not implemented; proof reconstruction is likely to fail");
+        " (with " ^ string_of_int (length ts) ^
+        " argument(s)) not implemented; proof reconstruction is likely to fail");
       NONE
     ))
-  )
-end;
+end;  (* split_once_items *)
 
 (* remove terms that do not satisfy 'p'; change the order of the remaining   *)
 (* terms in the same way as filter_prems_tac does                            *)
@@ -651,29 +657,32 @@
 
 fun negated_term_occurs_positively (terms : term list) : bool =
   List.exists
-    (fn (Trueprop $ (Const ("Not", _) $ t)) => member Pattern.aeconv terms (Trueprop $ t)
-      | _                                   => false)
+    (fn (Trueprop $ (Const ("Not", _) $ t)) =>
+      member Pattern.aeconv terms (Trueprop $ t)
+      | _ => false)
     terms;
 
 fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
 let
   (* repeatedly split (including newly emerging subgoals) until no further   *)
   (* splitting is possible                                                   *)
-  fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
-    | split_loop (subgoal::subgoals)                = (
-        case split_once_items ctxt subgoal of
-          SOME new_subgoals => split_loop (new_subgoals @ subgoals)
-        | NONE              => subgoal :: split_loop subgoals
-      )
+  fun split_loop ([] : (typ list * term list) list) =
+      ([] : (typ list * term list) list)
+    | split_loop (subgoal::subgoals) =
+      (case split_once_items ctxt subgoal of
+        SOME new_subgoals => split_loop (new_subgoals @ subgoals)
+      | NONE              => subgoal :: split_loop subgoals)
   fun is_relevant t  = isSome (decomp ctxt t)
   (* filter_prems_tac is_relevant: *)
   val relevant_terms = filter_prems_tac_items is_relevant terms
   (* split_tac, NNF normalization: *)
   val split_goals    = split_loop [(Ts, relevant_terms)]
   (* necessary because split_once_tac may normalize terms: *)
-  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals
+  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
+    split_goals
   (* TRY (etac notE) THEN eq_assume_tac: *)
-  val result         = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm
+  val result         = List.filter (not o negated_term_occurs_positively o snd)
+    beta_eta_norm
 in
   result
 end;
@@ -694,7 +703,8 @@
     addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
       not_all, not_ex, not_not]
   fun prem_nnf_tac i st =
-    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
+    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset)
+      i st
 in
 
 fun split_once_tac ctxt split_thms =
@@ -706,10 +716,15 @@
         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
         val cmap = Splitter.cmap_of_split_thms split_thms
         val splits = Splitter.split_posns cmap thy Ts concl
-        val split_limit = Config.get ctxt split_limit
       in
-        if length splits > split_limit then no_tac
-        else split_tac split_thms i
+        if null splits orelse length splits > Config.get ctxt split_limit then
+          no_tac
+        else if null (#2 (hd splits)) then
+          split_tac split_thms i
+        else
+          (* disallow a split that involves non-locally bound variables      *)
+          (* (except when bound by outermost meta-quantifiers)               *)
+          no_tac
       end)
   in
     EVERY' [
@@ -726,7 +741,7 @@
 (* remove irrelevant premises, then split the i-th subgoal (and all new      *)
 (* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
 (* subgoals and finally attempt to solve them by finding an immediate        *)
-(* contradiction (i.e. a term and its negation) in their premises.           *)
+(* contradiction (i.e., a term and its negation) in their premises.          *)
 
 fun pre_tac ctxt i =
 let
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -321,24 +321,23 @@
 
 fun ensure_random_datatype config raw_tycos thy =
   let
-    val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
     val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
       Datatype.the_descr thy raw_tycos;
-    val typrep_vs = (map o apsnd)
+    val typerep_vs = (map o apsnd)
       (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
     val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
-      (DatatypeAux.interpret_construction descr typrep_vs
+      (DatatypeAux.interpret_construction descr typerep_vs
         { atyp = single, dtyp = (K o K o K) [] });
     val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
-      (DatatypeAux.interpret_construction descr typrep_vs
+      (DatatypeAux.interpret_construction descr typerep_vs
         { atyp = K [], dtyp = K o K });
     val has_inst = exists (fn tyco =>
       can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   in if has_inst then thy
-    else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
+    else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
      of SOME constrain => mk_random_datatype config descr
-          (map constrain typrep_vs) tycos prfx (names, auxnames)
+          (map constrain typerep_vs) tycos prfx (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy
   end;
--- a/src/HOL/Tools/typecopy.ML	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -91,11 +91,10 @@
 
 fun add_default_code tyco thy =
   let
-    val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
+    val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
       typ = ty_rep, ... } =  get_info thy tyco;
     val SOME { Rep_inject = proj_inject, ... } = Typedef.get_info thy tyco;
-    val constr = (constr_name, Logic.unvarifyT (Sign.the_const_type thy constr_name));
-    val vs = (map dest_TFree o snd o dest_Type) (Type (tyco, map TFree raw_vs));
+    val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
     val ty = Type (tyco, map TFree vs);
     val proj = Const (proj, ty --> ty_rep);
     val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
--- a/src/HOL/ex/Mirabelle.thy	Fri Aug 14 17:26:11 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: Mirabelle.thy
-   Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-theory Mirabelle
-imports Main
-uses "mirabelle.ML"
-begin
-
-(* FIXME: use a logfile for each theory file *)
-
-setup Mirabelle.setup
-
-end
--- a/src/HOL/ex/mirabelle.ML	Fri Aug 14 17:26:11 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,318 +0,0 @@
-(* Title:  mirabelle.ML
-   Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-signature MIRABELLE =
-sig
-  type action
-  type settings
-  val register : string -> action -> theory -> theory
-  val invoke : string -> settings -> theory -> theory
-
-  val timeout : int Config.T
-  val verbose : bool Config.T
-  val set_logfile : string -> theory -> theory
-
-  val setup : theory -> theory
-
-  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
-    unit
-
-  val goal_thm_of : Proof.state -> thm
-  val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
-  val theorems_in_proof_term : Thm.thm -> Thm.thm list
-  val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
-  val get_setting : settings -> string * string -> string
-  val get_int_setting : settings -> string * int -> int
-
-(* FIXME  val refute_action : action *)
-  val quickcheck_action : action
-  val arith_action : action
-  val sledgehammer_action : action
-  val metis_action : action
-end
-
-
-
-structure Mirabelle (*: MIRABELLE*) =
-struct
-
-(* Mirabelle core *)
-
-type settings = (string * string) list
-type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
-type action = settings -> invoked
-
-structure Registered = TheoryDataFun
-(
-  type T = action Symtab.table
-  val empty = Symtab.empty
-  val copy = I
-  val extend = I
-  fun merge _ = Symtab.merge (K true)
-)
-
-fun register name act = Registered.map (Symtab.update_new (name, act))
-
-
-structure Invoked = TheoryDataFun
-(
-  type T = (string * invoked) list
-  val empty = []
-  val copy = I
-  val extend = I
-  fun merge _ = Library.merge (K true)
-)
-
-fun invoke name sts thy = 
-  let 
-    val act = 
-      (case Symtab.lookup (Registered.get thy) name of
-        SOME act => act
-      | NONE => error ("The invoked action " ^ quote name ^ 
-          " is not registered."))
-  in Invoked.map (cons (name, act sts)) thy end
-
-val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
-val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
-val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
-val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
-val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
-
-val setup_config = 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 =
-  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
-  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
-  (* FIXME: with multithreading and parallel proofs enabled, we might need to
-     encapsulate this inside a critical section *)
-
-fun verbose_msg verbose msg = if verbose then SOME msg else NONE
-
-fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
-  handle TimeLimit.TimeOut => verbose_msg verb "time out"
-       | ERROR msg => verbose_msg verb ("error: " ^ msg)
-
-fun capture_exns verb f x =
-  (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
-
-fun apply_action (c as (verb, _)) st (name, invoked) =
-  Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
-
-fun in_range _ _ NONE = true
-  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
-
-fun only_within_range thy pos f x =
-  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 =
-  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 ^ "):"
-
-    fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
-  in
-    Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
-  end
-
-in
-
-fun basic_hook tr pre post =
-  let
-    val thy = Proof.theory_of pre
-    val pos = Toplevel.pos_of tr
-    val name = Toplevel.name_of tr
-    val verb = Config.get_thy thy verbose
-    val secs = Time.fromSeconds (Config.get_thy thy timeout)
-    val st = {pre=pre, post=post}
-  in
-    Invoked.get thy
-    |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
-    |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
-  end
-
-end
-
-fun step_hook tr pre post =
- (* FIXME: might require wrapping into "interruptible" *)
-  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
-     not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
-  then basic_hook tr (Toplevel.proof_of pre) (SOME post)
-  else ()   (* FIXME: add theory_hook here *)
-
-
-
-(* Mirabelle utility functions *)
-
-val goal_thm_of = snd o snd o Proof.get_goal
-
-fun can_apply tac st =
-  let val (ctxt, (facts, goal)) = Proof.get_goal st
-  in
-    (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
-      SOME (thm, _) => true
-    | NONE => false)
-  end
-
-local
-
-fun fold_body_thms f =
-  let
-    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
-      fn (x, seen) =>
-        if Inttab.defined seen i then (x, seen)
-        else
-          let
-            val body' = Future.join body
-            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
-              (x, Inttab.update (i, ()) seen)
-        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
-  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
-
-in
-
-fun theorems_in_proof_term thm =
-  let
-    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
-    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
-    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
-    fun resolve_thms names = map_filter (member_of names) all_thms
-  in
-    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
-  end
-
-end
-
-fun theorems_of_sucessful_proof state =
-  (case state of
-    NONE => []
-  | SOME st =>
-      if not (Toplevel.is_proof st) then []
-      else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
-
-fun get_setting settings (key, default) =
-  the_default default (AList.lookup (op =) settings key)
-
-fun get_int_setting settings (key, default) =
-  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
-    SOME (SOME i) => i
-  | SOME NONE => error ("bad option: " ^ key)
-  | NONE => default)
-
-
-
-(* Mirabelle actions *)
-
-(* FIXME
-fun refute_action settings {pre=st, ...} = 
-  let
-    val params   = [("minsize", "2") (*"maxsize", "2"*)]
-    val subgoal = 0
-    val thy     = Proof.theory_of st
-    val thm = goal_thm_of st
-
-    val _ = Refute.refute_subgoal thy parms thm subgoal
-  in
-    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
-    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
-
-    val r =
-      if Substring.isSubstring "model found" writ_log
-      then
-        if Substring.isSubstring "spurious" warn_log
-        then SOME "potential counterexample"
-        else SOME "real counterexample (bug?)"
-      else
-        if Substring.isSubstring "time limit" writ_log
-        then SOME "no counterexample (time out)"
-        else if Substring.isSubstring "Search terminated" writ_log
-        then SOME "no counterexample (normal termination)"
-        else SOME "no counterexample (unknown)"
-  in r end
-*)
-
-fun quickcheck_action settings {pre=st, ...} =
-  let
-    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
-    val args = filter has_valid_key settings
-  in
-    (case Quickcheck.quickcheck args 1 st of
-      NONE => SOME "no counterexample"
-    | SOME _ => SOME "counterexample found")
-  end
-
-
-fun arith_action _ {pre=st, ...} = 
-  if can_apply Arith_Data.arith_tac st
-  then SOME "succeeded"
-  else NONE
-
-
-fun sledgehammer_action settings {pre=st, ...} =
-  let
-    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
-    val thy = Proof.theory_of st
- 
-    val prover = the (AtpManager.get_prover prover_name thy)
-    val timeout = AtpManager.get_timeout () 
-
-    val (success, message) =
-      let
-        val (success, message, _, _, _) =
-          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
-      in (success, message) end
-      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
-           | ERROR msg => (false, "error: " ^ msg)
-  in
-    if success
-    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
-    else NONE
-  end
-
-
-fun metis_action settings {pre, post} =
-  let
-    val thms = theorems_of_sucessful_proof post
-    val names = map Thm.get_name thms
-
-    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
-
-    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
-  in
-    (if can_apply metis pre then "succeeded" else "failed")
-    |> suffix (" (" ^ commas names ^ ")")
-    |> SOME
-  end
-
-
-
-(* Mirabelle setup *)
-
-val setup =
-  setup_config #>
-(* FIXME  register "refute" refute_action #> *)
-  register "quickcheck" quickcheck_action #>
-  register "arith" arith_action #>
-  register "sledgehammer" sledgehammer_action #>
-  register "metis" metis_action (* #> FIXME:
-  Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
-
-end
-
-val _ = Toplevel.add_hook Mirabelle.step_hook
-
-(* no multithreading, no parallel proofs *)
-val _ = Multithreading.max_threads := 1
-val _ = Goal.parallel_proofs := 0
--- a/src/Pure/Isar/class_target.ML	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -513,6 +513,7 @@
       | NONE => NONE;
   in
     thy
+    |> Theory.checkpoint
     |> ProofContext.init
     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs
--- a/src/Pure/Isar/overloading.ML	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/Pure/Isar/overloading.ML	Fri Aug 21 14:40:19 2009 +0100
@@ -154,6 +154,7 @@
     val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
   in
     thy
+    |> Theory.checkpoint
     |> ProofContext.init
     |> OverloadingData.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
--- a/src/ZF/ex/Limit.thy	Fri Aug 14 17:26:11 2009 +0100
+++ b/src/ZF/ex/Limit.thy	Fri Aug 21 14:40:19 2009 +0100
@@ -488,18 +488,24 @@
       and Mfun:  "M \<in> nat->nat->set(D)"
       and cpoD:  "cpo(D)"
   shows "matrix(D,M)"
-apply (simp add: matrix_def, safe)
-apply (rule Mfun)
-apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+)
-apply (simp add: chain_rel xprem)
-apply (rule cpo_trans [OF cpoD])
-apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+)
-apply (simp_all add: chain_fun [THEN apply_type] xprem)
-done
-
-lemma lemma_rel_rel:
-     "[|m \<in> nat; rel(D, (\<lambda>n \<in> nat. M`n`n)`m, y)|] ==> rel(D,M`m`m, y)"
-by simp
+proof -
+  {
+    fix n m assume "n : nat" "m : nat"
+    with chain_rel [OF yprem]
+    have "rel(D, M ` n ` m, M ` succ(n) ` m)" by simp
+  } note rel_succ = this
+  show "matrix(D,M)"
+  proof (simp add: matrix_def Mfun rel_succ, intro conjI ballI)
+    fix n m assume n: "n : nat" and m: "m : nat"
+    thus "rel(D, M ` n ` m, M ` n ` succ(m))"
+      by (simp add: chain_rel xprem)
+  next
+    fix n m assume n: "n : nat" and m: "m : nat"
+    thus "rel(D, M ` n ` m, M ` succ(n) ` succ(m))"
+      by (rule cpo_trans [OF cpoD rel_succ], 
+          simp_all add: chain_fun [THEN apply_type] xprem)
+  qed
+qed
 
 lemma lemma2:
      "[|x \<in> nat; m \<in> nat; rel(D,(\<lambda>n \<in> nat. M`n`m1)`x,(\<lambda>n \<in> nat. M`n`m1)`m)|]
@@ -509,65 +515,72 @@
 lemma isub_lemma:
     "[|isub(D, \<lambda>n \<in> nat. M`n`n, y); matrix(D,M); cpo(D)|] 
      ==> isub(D, \<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m), y)"
-apply (unfold isub_def, safe)
-apply (simp (no_asm_simp))
-apply (frule matrix_fun [THEN apply_type], assumption)
-apply (simp (no_asm_simp))
-apply (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], assumption+)
-apply (unfold isub_def, safe)
-(*???VERY indirect proof: beta-redexes could be simplified now!*)
-apply (rename_tac k n)
-apply (case_tac "k le n")
-apply (rule cpo_trans, assumption)
-apply (rule lemma2)
-apply (rule_tac [4] lemma_rel_rel)
-prefer 5 apply blast
-apply (assumption | rule chain_rel_gen matrix_chain_right matrix_in isubD1)+
-txt{*opposite case*}
-apply (rule cpo_trans, assumption)
-apply (rule not_le_iff_lt [THEN iffD1, THEN leI, THEN chain_rel_gen])
-prefer 3 apply assumption
-apply (assumption | rule nat_into_Ord matrix_chain_left)+
-apply (rule lemma_rel_rel)
-apply (simp_all add: matrix_in)
-done
+proof (simp add: isub_def, safe)
+  fix n
+  assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \<in> nat" and y: "y \<in> set(D)" 
+     and rel: "\<forall>n\<in>nat. rel(D, M ` n ` n, y)"
+  have "rel(D, lub(D, M ` n), y)"
+  proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM)
+    show "isub(D, M ` n, y)" 
+      proof (unfold isub_def, intro conjI ballI y)
+	fix k assume k: "k \<in> nat"
+	show "rel(D, M ` n ` k, y)"
+	  proof (cases "n le k")
+	    case True 
+	    hence yy: "rel(D, M`n`k, M`k`k)" 
+	      by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right) 
+	    show "?thesis"
+	      by (rule cpo_trans [OF D yy], 
+                  simp_all add: k rel n y DM matrix_in)
+	  next
+	    case False
+	    hence le: "k le n" 
+	      by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k) 
+	    show "?thesis"
+	      by (rule cpo_trans [OF D chain_rel_gen [OF le]], 
+		  simp_all add: n y k rel DM D matrix_chain_left)
+	  qed
+	qed
+  qed
+  moreover
+  have "M ` n \<in> nat \<rightarrow> set(D)" by (blast intro: DM n matrix_fun [THEN apply_type])
+  ultimately show "rel(D, lub(D, Lambda(nat, op `(M ` n))), y)"  by simp
+qed
 
 lemma matrix_chain_lub:
     "[|matrix(D,M); cpo(D)|] ==> chain(D,\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))"
-apply (simp add: chain_def, safe)
-apply (rule lam_type)
-apply (rule islub_in)
-apply (rule cpo_lub)
-prefer 2 apply assumption
-apply (rule chainI)
-apply (rule lam_type)
-apply (simp_all add: matrix_in)
-apply (rule matrix_rel_0_1, assumption+)
-apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta])
-apply (rule dominate_islub)
-apply (rule_tac [3] cpo_lub)
-apply (rule_tac [2] cpo_lub)
-apply (simp add: dominate_def)
-apply (blast intro: matrix_rel_1_0)
-apply (simp_all add: matrix_chain_left nat_succI chain_fun)
-done
+proof (simp add: chain_def, intro conjI ballI)
+  assume "matrix(D, M)" "cpo(D)"
+  thus "(\<lambda>x\<in>nat. lub(D, Lambda(nat, op `(M ` x)))) \<in> nat \<rightarrow> set(D)"
+    by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1) 
+next
+  fix n
+  assume DD: "matrix(D, M)" "cpo(D)" "n \<in> nat"
+  hence "dominate(D, M ` n, M ` succ(n))"
+    by (force simp add: dominate_def intro: matrix_rel_1_0)
+  with DD show "rel(D, lub(D, Lambda(nat, op `(M ` n))),
+               lub(D, Lambda(nat, op `(M ` succ(n)))))"
+    by (simp add: matrix_chain_left [THEN chain_fun, THEN eta] 
+      dominate_islub cpo_lub matrix_chain_left chain_fun)
+qed
 
 lemma isub_eq:
-    "[|matrix(D,M); cpo(D)|] 
-     ==> isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) <->
-         isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
-apply (rule iffI)
-apply (rule dominate_isub)
-prefer 2 apply assumption
-apply (simp add: dominate_def)
-apply (rule ballI)
-apply (rule bexI, auto)
-apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta])
-apply (rule islub_ub)
-apply (rule cpo_lub)
-apply (simp_all add: matrix_chain_left matrix_chain_diag chain_fun 
-                     matrix_chain_lub isub_lemma)
-done
+  assumes DM: "matrix(D, M)" and D: "cpo(D)"
+  shows "isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) <-> isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
+proof
+  assume isub: "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)"
+  hence dom: "dominate(D, \<lambda>n\<in>nat. M ` n ` n, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))))" 
+    using DM D
+    by (simp add: dominate_def, intro ballI bexI,
+        simp_all add: matrix_chain_left [THEN chain_fun, THEN eta] islub_ub cpo_lub matrix_chain_left)
+  thus "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)" using DM D
+    by - (rule dominate_isub [OF dom isub], 
+          simp_all add: matrix_chain_diag chain_fun matrix_chain_lub)
+next
+  assume isub: "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)" 
+  thus "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)"  using DM D
+    by (simp add: isub_lemma)
+qed
 
 lemma lub_matrix_diag_aux1:
     "lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
@@ -695,34 +708,43 @@
     "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] 
      ==> matrix(E,\<lambda>x \<in> nat. \<lambda>xa \<in> nat. X`x`(Xa`xa))"
 apply (rule matrix_chainI, auto)
-apply (rule chainI)
-apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
-apply (blast intro: cont_mono nat_succI chain_rel cf_cont chain_in)
-apply (rule chainI)
-apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
-apply (rule rel_cf)
-apply (simp_all add: chain_in chain_rel)
+apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont cont_mono)
+apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont rel_cf)
 apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in)
 done
 
 lemma chain_cf_lub_cont:
-    "[|chain(cf(D,E),X); cpo(D); cpo(E) |] 
-     ==> (\<lambda>x \<in> set(D). lub(E, \<lambda>n \<in> nat. X ` n ` x)) \<in> cont(D, E)"
-apply (rule contI)
-apply (rule lam_type)
-apply (assumption | rule chain_cf [THEN cpo_lub, THEN islub_in])+
-apply simp
-apply (rule dominate_islub)
-apply (erule_tac [2] chain_cf [THEN cpo_lub], simp_all)+
-apply (rule dominateI, assumption, simp)
-apply (assumption | rule chain_in [THEN cf_cont, THEN cont_mono])+
-apply (assumption | rule chain_cf [THEN chain_fun])+
-apply (simp add: cpo_lub [THEN islub_in] 
-                 chain_in [THEN cf_cont, THEN cont_lub])
-apply (frule matrix_lemma [THEN lub_matrix_diag], assumption+)
-apply (simp add: chain_in [THEN beta])
-apply (drule matrix_lemma [THEN lub_matrix_diag_sym], auto)
-done
+  assumes ch: "chain(cf(D,E),X)" and D: "cpo(D)" and E: "cpo(E)"
+  shows   "(\<lambda>x \<in> set(D). lub(E, \<lambda>n \<in> nat. X ` n ` x)) \<in> cont(D, E)"
+proof (rule contI)
+  show "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) \<in> set(D) \<rightarrow> set(E)"
+    by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E) 
+next
+  fix x y
+  assume xy: "rel(D, x, y)" "x \<in> set(D)" "y \<in> set(D)"
+  hence dom: "dominate(E, \<lambda>n\<in>nat. X ` n ` x, \<lambda>n\<in>nat. X ` n ` y)"
+    by (force intro: dominateI  chain_in [OF ch, THEN cf_cont, THEN cont_mono])
+  note chE = chain_cf [OF ch] 
+  from xy show "rel(E, (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` x,
+                       (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` y)"
+    by (simp add: dominate_islub [OF dom] cpo_lub [OF chE] E chain_fun [OF chE])
+next
+  fix Y
+  assume chDY: "chain(D,Y)"
+  have "lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>y\<in>nat. X ` x ` (Y ` y))) =
+        lub(E, \<lambda>x\<in>nat. X ` x ` (Y ` x))"
+    using matrix_lemma [THEN lub_matrix_diag, OF ch chDY]
+    by (simp add: D E)
+   also have "... =  lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))"
+    using  matrix_lemma [THEN lub_matrix_diag_sym, OF ch chDY]
+    by (simp add: D E) 
+  finally have "lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` x ` (Y ` n))) =
+                lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))" .
+  thus "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` lub(D, Y) =
+        lub(E, \<lambda>n\<in>nat. (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` (Y ` n))"
+    by (simp add: cpo_lub [THEN islub_in]  D chDY
+                  chain_in [THEN cf_cont, THEN cont_lub, OF ch])
+  qed
 
 lemma islub_cf:
     "[| chain(cf(D,E),X); cpo(D); cpo(E)|]