--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 27 14:56:28 2011 +0200
@@ -87,7 +87,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_sys
+ Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
-> bool -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -991,7 +991,8 @@
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
| should_encode_type _ _ All_Types _ = true
- | should_encode_type ctxt _ Fin_Nonmono_Types T = is_type_surely_finite ctxt T
+ | should_encode_type ctxt _ Fin_Nonmono_Types T =
+ is_type_surely_finite ctxt false T
| should_encode_type _ _ _ _ = false
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
@@ -1617,26 +1618,27 @@
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
- | add_combterm_nonmonotonic_types ctxt level locality _
+fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
+ | add_combterm_nonmonotonic_types ctxt level sound locality _
(CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
tm2)) =
(is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
(case level of
Noninf_Nonmono_Types =>
not (is_locality_global locality) orelse
- not (is_type_surely_infinite ctxt T)
- | Fin_Nonmono_Types => is_type_surely_finite ctxt T
+ not (is_type_surely_infinite ctxt sound T)
+ | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
| _ => true)) ? insert_type ctxt I (deep_freeze_type T)
- | add_combterm_nonmonotonic_types _ _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
- : translated_formula) =
+ | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
+fun add_fact_nonmonotonic_types ctxt level sound
+ ({kind, locality, combformula, ...} : translated_formula) =
formula_fold (SOME (kind <> Conjecture))
- (add_combterm_nonmonotonic_types ctxt level locality) combformula
-fun nonmonotonic_types_for_facts ctxt type_sys facts =
+ (add_combterm_nonmonotonic_types ctxt level sound locality)
+ combformula
+fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
let val level = level_of_type_sys type_sys in
if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
- [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
+ [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
(* We must add "bool" in case the helper "True_or_False" is added
later. In addition, several places in the code rely on the list of
nonmonotonic types not being empty. *)
@@ -1817,7 +1819,7 @@
val explicit_apply = NONE (* for experimental purposes *)
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
exporter readable_names preproc hyp_ts concl_t facts =
let
val (format, type_sys) = choose_format [format] type_sys
@@ -1825,7 +1827,8 @@
translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
- val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
+ val nonmono_Ts =
+ conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
val repair = repair_fact ctxt format type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab =
--- a/src/HOL/Tools/ATP/atp_util.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Mon Jun 27 14:56:28 2011 +0200
@@ -21,8 +21,8 @@
val typ_of_dtyp :
Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
-> typ
- val is_type_surely_finite : Proof.context -> typ -> bool
- val is_type_surely_infinite : Proof.context -> typ -> bool
+ val is_type_surely_finite : Proof.context -> bool -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_prop : term -> term
@@ -136,7 +136,7 @@
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card T =
+fun tiny_card_of_type ctxt sound default_card T =
let
val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
@@ -181,19 +181,20 @@
(Logic.varifyT_global abs_type) T
(Logic.varifyT_global rep_type)
|> aux true avoid of
- 0 => 0
+ 0 => if sound then default_card else 0
| 1 => 1
| _ => default_card)
| [] => default_card)
(* Very slightly unsound: Type variables are assumed not to be
constrained to cardinality 1. (In practice, the user would most
likely have used "unit" directly anyway.) *)
- | TFree _ => if default_card = 1 then 2 else default_card
+ | TFree _ =>
+ if default_card = 1 andalso not sound then 2 else default_card
| TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
-fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
+fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
+fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
fun monomorphic_term subst =
map_types (map_type_tvar (fn v =>
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 27 14:56:28 2011 +0200
@@ -196,8 +196,8 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false false
- [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
+ false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 14:56:28 2011 +0200
@@ -85,6 +85,7 @@
("overlord", "false"),
("blocking", "false"),
("type_sys", "smart"),
+ ("sound", "false"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
("max_mono_iters", "3"),
@@ -101,11 +102,12 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("non_blocking", "blocking"),
+ ("unsound", "sound"),
("no_isar_proof", "isar_proof"),
("no_slicing", "slicing")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_sys", "max_mono_iters",
+ ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
"max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
"preplay_timeout"]
@@ -122,7 +124,8 @@
ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
-(* Secret feature: "provers =" and "type_sys =" can be left out. *)
+(* "provers =" and "type_sys =" can be left out. The latter is a secret
+ feature. *)
fun check_and_repair_raw_param ctxt (name, value) =
if is_known_raw_param name then
(name, value)
@@ -267,6 +270,7 @@
else case lookup_string "type_sys" of
"smart" => NONE
| s => SOME (type_sys_from_string s)
+ val sound = mode = Auto_Try orelse lookup_bool "sound"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
@@ -285,9 +289,9 @@
provers = provers, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ sound = sound, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, slicing = slicing,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 27 14:56:28 2011 +0200
@@ -59,7 +59,7 @@
val {goal, ...} = Proof.goal state
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_sys = type_sys,
+ provers = provers, type_sys = type_sys, sound = true,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 14:56:28 2011 +0200
@@ -25,6 +25,7 @@
blocking: bool,
provers: string list,
type_sys: type_sys option,
+ sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -289,6 +290,7 @@
blocking: bool,
provers: string list,
type_sys: type_sys option,
+ sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -492,7 +494,7 @@
are omitted. *)
fun is_dangerous_prop ctxt =
transform_elim_prop
- #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
+ #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf
is_exhaustive_finite)
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
@@ -528,9 +530,9 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
- max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
- timeout, preplay_timeout, ...} : params)
+ ({debug, verbose, overlord, type_sys, sound, max_relevant,
+ max_mono_iters, max_new_mono_instances, isar_proof,
+ isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
@@ -633,8 +635,8 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_sys false (Config.get ctxt atp_readable_names) true
- hyp_ts concl_t facts
+ type_sys sound false (Config.get ctxt atp_readable_names)
+ true hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
val core =
--- a/src/HOL/ex/atp_export.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Mon Jun 27 14:56:28 2011 +0200
@@ -158,8 +158,8 @@
facts0 |> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc), prop_of th))
val (atp_problem, _, _, _, _, _, _) =
- prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
- @{prop False} facts
+ prepare_atp_problem ctxt format Axiom Axiom type_sys true true false true
+ [] @{prop False} facts
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))