--- a/NEWS Fri Nov 26 23:49:49 2010 +0100
+++ b/NEWS Fri Nov 26 23:50:14 2010 +0100
@@ -104,14 +104,13 @@
avoid confusion with finite sets. INCOMPATIBILITY.
* Quickcheck's generator for random generation is renamed from "code" to
-"random". INCOMPATIBILITY.
+"random". INCOMPATIBILITY.
* Theory Multiset provides stable quicksort implementation of sort_key.
* Quickcheck now has a configurable time limit which is set to 30 seconds
by default. This can be changed by adding [timeout = n] to the quickcheck
-command. The time limit for auto quickcheck is still set independently,
-by default to 5 seconds.
+command. The time limit for Auto Quickcheck is still set independently.
* New command 'partial_function' provides basic support for recursive
function definitions over complete partial orders. Concrete instances
@@ -357,11 +356,26 @@
(and "ms" and "min" are no longer supported)
INCOMPATIBILITY.
+* Metis and Meson now have configuration options "meson_trace", "metis_trace",
+ and "metis_verbose" that can be enabled to diagnose these tools. E.g.
+
+ using [[metis_trace = true]]
+
* Nitpick:
- Renamed options:
nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
INCOMPATIBILITY.
+ - Now requires Kodkodi 1.2.9. INCOMPATIBILITY.
+ - Added support for partial quotient types.
+ - Added local versions of the "Nitpick.register_xxx" functions.
+ - Added "whack" option.
+ - Allow registration of quotient types as codatatypes.
+ - Improved "merge_type_vars" option to merge more types.
+ - Removed unsound "fast_descrs" option.
+ - Added custom symmetry breaking for datatypes, making it possible to reach
+ higher cardinalities.
+ - Prevent the expansion of too large definitions.
* Changed SMT configuration options:
- Renamed:
@@ -650,7 +664,7 @@
Tracing is then active for all invocations of the simplifier in
subsequent goal refinement steps. Tracing may also still be enabled or
-disabled via the ProofGeneral settings menu.
+disabled via the Proof General settings menu.
* Separate commands 'hide_class', 'hide_type', 'hide_const',
'hide_fact' replace the former 'hide' KIND command. Minor
--- a/src/HOL/Tools/Meson/meson.ML Fri Nov 26 23:49:49 2010 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Nov 26 23:50:14 2010 +0100
@@ -46,7 +46,7 @@
structure Meson : MESON =
struct
-val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false)
+val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 26 23:49:49 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 26 23:50:14 2010 +0100
@@ -31,8 +31,8 @@
open Metis_Translate
-val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
-val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
+val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
fun verbose_warning ctxt msg =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 26 23:49:49 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 26 23:50:14 2010 +0100
@@ -440,7 +440,7 @@
val smt_iter_timeout_divisor = 2
val smt_monomorph_limit = 4
-fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
+fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
let
val ctxt = Proof.context_of state
fun iter timeout iter_num outcome0 msecs_so_far facts =
@@ -534,6 +534,7 @@
val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
val {outcome, used_facts, run_time_in_msecs} =
smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+ val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
val outcome = outcome |> Option.map failure_from_smt_failure
val message =
case outcome of
@@ -547,8 +548,9 @@
in
try_command_line (proof_banner auto)
(apply_on_subgoal subgoal subgoal_count ^
- command_call method (map (fst o fst) used_facts)) ^
- minimize_line minimize_command (map (fst o fst) used_facts)
+ command_call method (map fst other_lemmas)) ^
+ minimize_line minimize_command
+ (map fst (other_lemmas @ chained_lemmas))
end
| SOME failure => string_for_failure "SMT solver" failure
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 26 23:49:49 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 26 23:50:14 2010 +0100
@@ -24,7 +24,9 @@
val command_call : string -> string list -> string
val try_command_line : string -> string -> string
val minimize_line : ('a list -> string) -> 'a list -> string
- val metis_proof_text : metis_params -> text_result
+ val split_used_facts :
+ (string * locality) list
+ -> (string * locality) list * (string * locality) list
val isar_proof_text : isar_params -> metis_params -> text_result
val proof_text : bool -> isar_params -> metis_params -> text_result
end;
@@ -159,15 +161,15 @@
fun used_facts_in_tstplike_proof fact_names =
atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
-fun used_facts fact_names =
- used_facts_in_tstplike_proof fact_names
- #> List.partition (curry (op =) Chained o snd)
+val split_used_facts =
+ List.partition (curry (op =) Chained o snd)
#> pairself (sort_distinct (string_ord o pairself fst))
fun metis_proof_text (banner, full_types, minimize_command,
tstplike_proof, fact_names, goal, i) =
let
- val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
+ val (chained_lemmas, other_lemmas) =
+ split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
val n = Logic.count_prems (prop_of goal)
in
(metis_line banner full_types i n (map fst other_lemmas) ^
@@ -912,14 +914,14 @@
in do_proof end
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (other_params as (_, full_types, _, tstplike_proof,
+ (metis_params as (_, full_types, _, tstplike_proof,
fact_names, goal, i)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
val n = Logic.count_prems (prop_of goal)
- val (one_line_proof, lemma_names) = metis_proof_text other_params
+ val (one_line_proof, lemma_names) = metis_proof_text metis_params
fun isar_proof_for () =
case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
isar_shrink_factor tstplike_proof conjecture_shape fact_names
@@ -940,8 +942,8 @@
|> the_default "\nWarning: The Isar proof construction failed."
in (one_line_proof ^ isar_proof, lemma_names) end
-fun proof_text isar_proof isar_params other_params =
+fun proof_text isar_proof isar_params metis_params =
(if isar_proof then isar_proof_text isar_params else metis_proof_text)
- other_params
+ metis_params
end;
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri Nov 26 23:49:49 2010 +0100
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Fri Nov 26 23:50:14 2010 +0100
@@ -66,7 +66,7 @@
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
- by normalization rule+
+ by normalization
lemma "rev [a, b, c] = [c, b, a]" by normalization
value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
@@ -108,10 +108,13 @@
lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
value [nbe] "Suc 0 \<in> set ms"
+(* non-left-linear patterns, equality by extensionality *)
+
lemma "f = f" by normalization
lemma "f x = f x" by normalization
lemma "(f o g) x = f (g x)" by normalization
lemma "(f o id) x = f x" by normalization
+lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
value [nbe] "(\<lambda>x. x)"
(* Church numerals: *)
--- a/src/Pure/library.ML Fri Nov 26 23:49:49 2010 +0100
+++ b/src/Pure/library.ML Fri Nov 26 23:50:14 2010 +0100
@@ -546,7 +546,7 @@
fun forall2 P [] [] = true
| forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
- | forall2 P _ _ = false;
+ | forall2 P _ _ = raise UnequalLengths;
fun map_split f [] = ([], [])
| map_split f (x :: xs) =
--- a/src/Tools/nbe.ML Fri Nov 26 23:49:49 2010 +0100
+++ b/src/Tools/nbe.ML Fri Nov 26 23:50:14 2010 +0100
@@ -18,7 +18,7 @@
val apps: Univ -> Univ list -> Univ (*explicit applications*)
val abss: int -> (Univ list -> Univ) -> Univ
(*abstractions as closures*)
- val same: Univ -> Univ -> bool
+ val eq_Univ: Univ * Univ -> bool
val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
val trace: bool Unsynchronized.ref
@@ -170,11 +170,6 @@
| Abs of (int * (Univ list -> Univ)) * Univ list
(*abstractions as closures*);
-fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys
- | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
- | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys
- | same _ _ = false;
-
(* constructor functions *)
@@ -188,6 +183,28 @@
| apps (Const (name, xs)) ys = Const (name, ys @ xs)
| apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
+fun satisfy_abs (abs as ((n, f), xs)) some_k =
+ let
+ val ys = case some_k
+ of NONE => replicate n (BVar (0, []))
+ | SOME k => map_range (fn l => BVar (k + l, [])) n;
+ in (apps (Abs abs) ys, ys) end;
+
+fun maxidx (Const (_, xs)) = fold maxidx xs
+ | maxidx (DFree _) = I
+ | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
+ | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
+
+fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
+ | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
+ | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
+ | eq_Univ (x as Abs abs, y) =
+ let
+ val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
+ in eq_Univ (x, apps y ys) end
+ | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
+ | eq_Univ _ = false;
+
(** assembling and compiling ML code from terms **)
@@ -241,7 +258,7 @@
val name_const = prefix ^ "Const";
val name_abss = prefix ^ "abss";
val name_apps = prefix ^ "apps";
- val name_same = prefix ^ "same";
+ val name_eq = prefix ^ "eq_Univ";
in
val univs_cookie = (Univs.get, put_result, name_put);
@@ -267,7 +284,7 @@
fun nbe_abss 0 f = f `$` ml_list []
| nbe_abss n f = name_abss `$$` [string_of_int n, f];
-fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
+fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
end;
@@ -353,7 +370,7 @@
val (samepairs, args') = subst_nonlin_vars args;
val s_args = map assemble_arg args';
val s_rhs = if null samepairs then assemble_rhs rhs
- else ml_if (ml_and (map (uncurry nbe_same) samepairs))
+ else ml_if (ml_and (map nbe_eq samepairs))
(assemble_rhs rhs) default_rhs;
val eqns = if is_eval then
[([ml_list (rev (dicts @ s_args))], s_rhs)]