# HG changeset patch
# User blanchet
# Date 1314875907 -7200
# Node ID 2ac4ff398bc39ccc2e2b58f28d958f01d17ce2c7
# Parent  8a2fd7418435b48a067e631762630cda9f4d23b7
make "sound" sound and "unsound" more sound, based on evaluation

diff -r 8a2fd7418435 -r 2ac4ff398bc3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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"),
diff -r 8a2fd7418435 -r 2ac4ff398bc3 src/HOL/Tools/ATP/atp_translate.ML
--- 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
diff -r 8a2fd7418435 -r 2ac4ff398bc3 src/HOL/Tools/Metis/metis_tactics.ML
--- 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 =
diff -r 8a2fd7418435 -r 2ac4ff398bc3 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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