# HG changeset patch # User paulson # Date 1250862019 -3600 # Node ID 48786f277130a3b5570fa9d505addeb981096b7f # Parent b23a4326b9bbfc745b96863bb08011838609efc7# Parent da3ca3c6ec817d84128a9bb82acaccee829fc942 merged diff -r da3ca3c6ec81 -r 48786f277130 NEWS --- 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 diff -r da3ca3c6ec81 -r 48786f277130 etc/components --- 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 diff -r da3ca3c6ec81 -r 48786f277130 lib/scripts/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 <; - 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; diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Auth/Yahalom.thy --- 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 @@ (\NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs); A \ bad; B \ bad; evs \ yahalom |] ==> \X. Says A B {|X, Crypt K (Nonce NB)|} \ 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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Code_Eval.thy --- 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 \ nibble \ char))) + in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \ nibble \ char))) (Code_Eval.term_of n)) (Code_Eval.term_of m))" by (subst term_of_anything) rule diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Predicate.thy --- 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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Quickcheck.thy --- 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 [], \u. Code_Eval.term_of (STR []))" + "random _ = Pair (STR '''', \u. Code_Eval.term_of (STR ''''))" instance .. diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Mirabelle.thy --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Tools/mirabelle.ML --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML --- /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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/etc/settings --- /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" diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/lib/Tools/mirabelle --- /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 + diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl --- /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 < + 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 = ; +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; + diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/lin_arith.ML --- 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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/quickcheck_generators.ML --- 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; diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/Tools/typecopy.ML --- 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)); diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/ex/Mirabelle.thy --- 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 diff -r da3ca3c6ec81 -r 48786f277130 src/HOL/ex/mirabelle.ML --- 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 diff -r da3ca3c6ec81 -r 48786f277130 src/Pure/Isar/class_target.ML --- 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 diff -r da3ca3c6ec81 -r 48786f277130 src/Pure/Isar/overloading.ML --- 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 diff -r da3ca3c6ec81 -r 48786f277130 src/ZF/ex/Limit.thy --- 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 \ 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 \ nat; rel(D, (\n \ 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 \ nat; m \ nat; rel(D,(\n \ nat. M`n`m1)`x,(\n \ nat. M`n`m1)`m)|] @@ -509,65 +515,72 @@ lemma isub_lemma: "[|isub(D, \n \ nat. M`n`n, y); matrix(D,M); cpo(D)|] ==> isub(D, \n \ nat. lub(D,\m \ 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 \ nat" and y: "y \ set(D)" + and rel: "\n\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 \ 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 \ nat \ 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,\n \ nat. lub(D,\m \ 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 "(\x\nat. lub(D, Lambda(nat, op `(M ` x)))) \ nat \ 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 \ 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,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) <-> - isub(D,(\n \ 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,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) <-> isub(D,(\n \ nat. M`n`n),y)" +proof + assume isub: "isub(D, \n\nat. lub(D, Lambda(nat, op `(M ` n))), y)" + hence dom: "dominate(D, \n\nat. M ` n ` n, \n\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, \n\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, \n\nat. M ` n ` n, y)" + thus "isub(D, \n\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,(\n \ nat. lub(D,\m \ nat. M`n`m))) = @@ -695,34 +708,43 @@ "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] ==> matrix(E,\x \ nat. \xa \ 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) |] - ==> (\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ 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 "(\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ cont(D, E)" +proof (rule contI) + show "(\x\set(D). lub(E, \n\nat. X ` n ` x)) \ set(D) \ 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 \ set(D)" "y \ set(D)" + hence dom: "dominate(E, \n\nat. X ` n ` x, \n\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, (\x\set(D). lub(E, \n\nat. X ` n ` x)) ` x, + (\x\set(D). lub(E, \n\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, \x\nat. lub(E, \y\nat. X ` x ` (Y ` y))) = + lub(E, \x\nat. X ` x ` (Y ` x))" + using matrix_lemma [THEN lub_matrix_diag, OF ch chDY] + by (simp add: D E) + also have "... = lub(E, \x\nat. lub(E, \n\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, \x\nat. lub(E, \n\nat. X ` x ` (Y ` n))) = + lub(E, \x\nat. lub(E, \n\nat. X ` n ` (Y ` x)))" . + thus "(\x\set(D). lub(E, \n\nat. X ` n ` x)) ` lub(D, Y) = + lub(E, \n\nat. (\x\set(D). lub(E, \n\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)|]