--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 01 16:16:25 2011 +0900
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 01 13:18:27 2011 +0200
@@ -379,8 +379,7 @@
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I)
- #> Config.put Sledgehammer_Provers.measure_run_time true
- #> Config.put Sledgehammer_Provers.atp_sound_modulo_infiniteness false)
+ #> Config.put Sledgehammer_Provers.measure_run_time true)
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Sep 01 16:16:25 2011 +0900
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Sep 01 13:18:27 2011 +0200
@@ -21,7 +21,7 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
- datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+ datatype soundness = Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
Noninf_Nonmono_Types of soundness |
@@ -536,7 +536,7 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+datatype soundness = Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
Noninf_Nonmono_Types of soundness |
@@ -1133,11 +1133,10 @@
(* These types witness that the type classes they belong to allow infinite
models and hence that any types with these type classes is monotonic. *)
val known_infinite_types =
- [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
+ [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
- soundness <> Sound andalso
- is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
+ soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
@@ -1860,11 +1859,14 @@
end
(* We add "bool" in case the helper "True_or_False" is included later. *)
-val default_mono =
+fun default_mono level =
{maybe_finite_Ts = [@{typ bool}],
surely_finite_Ts = [@{typ bool}],
maybe_infinite_Ts = known_infinite_types,
- surely_infinite_Ts = known_infinite_types,
+ surely_infinite_Ts =
+ case level of
+ Noninf_Nonmono_Types Sound => []
+ | _ => known_infinite_types,
maybe_nonmono_Ts = [@{typ bool}]}
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
@@ -1919,7 +1921,7 @@
(add_iterm_mononotonicity_info ctxt level) iformula
fun mononotonicity_info_for_facts ctxt type_enc facts =
let val level = level_of_type_enc type_enc in
- default_mono
+ default_mono level
|> is_type_level_monotonicity_based level
? fold (add_fact_mononotonicity_info ctxt level) facts
end
--- a/src/HOL/Tools/Metis/metis_tactics.ML Thu Sep 01 16:16:25 2011 +0900
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu Sep 01 13:18:27 2011 +0200
@@ -121,7 +121,7 @@
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
- val type_enc = type_enc_from_string Unsound type_enc
+ val type_enc = type_enc_from_string Sound type_enc
val (sym_tab, axioms, old_skolems) =
prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Sep 01 16:16:25 2011 +0900
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Sep 01 13:18:27 2011 +0200
@@ -65,7 +65,6 @@
val measure_run_time : bool Config.T
val atp_lambda_translation : string Config.T
val atp_full_names : bool Config.T
- val atp_sound_modulo_infiniteness : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
val smt_weight_min_facts : int Config.T
@@ -351,9 +350,6 @@
provers (e.g., E). For these reason, short names are enabled by default. *)
val atp_full_names =
Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
-val atp_sound_modulo_infiniteness =
- Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
- (K true)
val smt_triggers =
Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
@@ -627,13 +623,7 @@
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val soundness =
- if sound then
- if Config.get ctxt atp_sound_modulo_infiniteness then
- Sound_Modulo_Infiniteness
- else
- Sound
- else
- Unsound
+ if sound then Sound else Sound_Modulo_Infiniteness
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc