--- 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)|]