--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 30 14:55:01 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 30 16:07:30 2011 +0200
@@ -6,10 +6,10 @@
signature QUOTIENT_DEF =
sig
- val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
+ val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
local_theory -> Quotient_Info.qconsts_info * local_theory
- val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
+ val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
local_theory -> Quotient_Info.qconsts_info * local_theory
val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
@@ -43,26 +43,30 @@
quote str ^ " differs from declaration " ^ name ^ pos)
end
-fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
+fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
let
+ val (vars, ctxt) = prep_vars (the_list raw_var) lthy
+ val lhs = prep_term ctxt lhs_raw
+ val rhs = prep_term ctxt rhs_raw
+
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
val _ = if is_Const rhs then () else warning "The definiens is not a constant"
- fun sanity_test NONE _ = true
- | sanity_test (SOME bind) str =
- if Variable.check_name bind = str then true
- else error_msg bind str
+ val var =
+ (case vars of
+ [] => (Binding.name lhs_str, NoSyn)
+ | [(binding, _, mx)] =>
+ if Variable.check_name binding = lhs_str then (binding, mx)
+ else error_msg binding lhs_str
+ | _ => raise Match)
- val _ = sanity_test optbind lhs_str
-
- val qconst_bname = Binding.name lhs_str
val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'
- val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
+ val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = thm}
@@ -76,15 +80,9 @@
(qconst_data, lthy'')
end
-fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
- let
- val lhs = Syntax.read_term lthy lhs_str
- val rhs = Syntax.read_term lthy rhs_str
- val lthy' = Variable.declare_term lhs lthy
- val lthy'' = Variable.declare_term rhs lthy'
- in
- quotient_def (decl, (attr, (lhs, rhs))) lthy''
- end
+val quotient_def = gen_quotient_def Proof_Context.cert_vars Syntax.check_term
+val quotdef_cmd = gen_quotient_def Proof_Context.read_vars Syntax.read_term
+
(* a wrapper for automatically lifting a raw constant *)
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
@@ -93,14 +91,12 @@
val qty = Quotient_Term.derive_qtyp ctxt qtys rty
val lhs = Free (qconst_name, qty)
in
- quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
+ quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
end
(* parser and command *)
-val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
-
val quotdef_parser =
- Scan.optional quotdef_decl (NONE, NoSyn) --
+ Scan.option Parse_Spec.constdecl --
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
val _ =
--- a/src/HOL/Tools/lin_arith.ML Thu Jun 30 14:55:01 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Jun 30 16:07:30 2011 +0200
@@ -21,6 +21,7 @@
val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
+ val verbose: bool Config.T
val trace: bool Unsynchronized.ref
end;
@@ -101,12 +102,14 @@
val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
+val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true);
structure LA_Data =
struct
val fast_arith_neq_limit = neq_limit;
+val fast_arith_verbose = verbose;
(* Decomposition of terms *)
--- a/src/HOL/Tools/try_methods.ML Thu Jun 30 14:55:01 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML Thu Jun 30 16:07:30 2011 +0200
@@ -113,7 +113,8 @@
fun do_try_methods mode timeout_opt quad st =
let
- val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
+ val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false #>
+ Config.put Lin_Arith.verbose false)
in
if mode = Normal then
"Trying " ^ space_implode " " (Try.serial_commas "and"
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jun 30 14:55:01 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jun 30 16:07:30 2011 +0200
@@ -60,6 +60,9 @@
(*the limit on the number of ~= allowed; because each ~= is split
into two cases, this can lead to an explosion*)
val fast_arith_neq_limit: int Config.T
+
+ (*configures whether (potentially spurious) counterexamples are printed*)
+ val fast_arith_verbose: bool Config.T
end;
(*
decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
@@ -612,11 +615,10 @@
else string_of_int p ^ "/" ^ string_of_int q
in a ^ " = " ^ s end;
-fun produce_ex sds =
- curry (op ~~) sds
- #> map print_atom
- #> commas
- #> curry (op ^) "Counterexample (possibly spurious):\n";
+fun is_variable (Free _) = true
+ | is_variable (Var _) = true
+ | is_variable (Bound _) = true
+ | is_variable _ = false
fun trace_ex ctxt params atoms discr n (hist: history) =
case hist of
@@ -628,8 +630,15 @@
val start =
if v = ~1 then (hist', findex0 discr n lineqs)
else (hist, replicate n Rat.zero)
- val ex = SOME (produce_ex (map show_term atoms ~~ discr)
- (uncurry (fold (findex1 discr)) start))
+ val produce_ex =
+ map print_atom #> commas #>
+ prefix "Counterexample (possibly spurious):\n"
+ val ex = (
+ uncurry (fold (findex1 discr)) start
+ |> map2 pair (atoms ~~ discr)
+ |> filter (fn ((t, _), _) => is_variable t)
+ |> map (apfst (apfst show_term))
+ |> (fn [] => NONE | sdss => SOME (produce_ex sdss)))
handle NoEx => NONE
in
case ex of
@@ -744,7 +753,7 @@
(trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")");
refute initemss (js @ [j]))
| Failure hist =>
- (if not show_ex then ()
+ (if not show_ex orelse not (Config.get ctxt LA_Data.fast_arith_verbose) then ()
else
let
val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)