# HG changeset patch # User blanchet # Date 1309179388 -7200 # Node ID ae612a423dad4728ff9d61ef029d6479dbd7e95a # Parent 423f100f1f8528bbb4a6e9c86deb4db736043154 added "sound" option to force Sledgehammer to be pedantically sound diff -r 423f100f1f85 -r ae612a423dad src/HOL/Tools/ATP/atp_translate.ML --- 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 = diff -r 423f100f1f85 -r ae612a423dad src/HOL/Tools/ATP/atp_util.ML --- 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 => diff -r 423f100f1f85 -r ae612a423dad src/HOL/Tools/Metis/metis_translate.ML --- 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)) diff -r 423f100f1f85 -r ae612a423dad src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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) diff -r 423f100f1f85 -r ae612a423dad src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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, diff -r 423f100f1f85 -r ae612a423dad src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 = diff -r 423f100f1f85 -r ae612a423dad src/HOL/ex/atp_export.ML --- 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)))