added option to control soundness of encodings more precisely, for evaluation purposes

--- a/src/HOL/TPTP/atp_export.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -159,7 +159,7 @@
     val (atp_problem, _, _, _, _, _, _) =
       facts
       |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
-      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
+      |> prepare_atp_problem ctxt format Axiom Axiom type_enc Sound true
                              combinatorsN false true [] @{prop False}
     val atp_problem =
       atp_problem

--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -31,6 +31,8 @@
     Guards of polymorphism * type_level * type_heaviness |
     Tags of polymorphism * type_level * type_heaviness
 
+  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+
   val no_lambdasN : string
   val concealedN : string
   val liftingN : string
@@ -96,8 +98,8 @@
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
   val prepare_atp_problem :
-    Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
-    -> bool -> string -> bool -> bool -> term list -> term
+    Proof.context -> format -> formula_kind -> formula_kind -> type_enc
+    -> soundness -> bool -> string -> bool -> bool -> term list -> term
     -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
        * (string * locality) list vector * int list * int Symtab.table
@@ -622,6 +624,9 @@
                  | _ => type_enc)
      | format => (format, type_enc))
 
+(* Soundness controls how sound the "quasi-sound" encodings should be. *)
+datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+
 fun lift_lambdas ctxt type_enc =
   map (close_form o Envir.eta_contract) #> rpair ctxt
   #-> Lambda_Lifting.lift_lambdas
@@ -1770,7 +1775,7 @@
 (* 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_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
-  | add_iterm_nonmonotonic_types ctxt level sound locality _
+  | add_iterm_nonmonotonic_types ctxt level soundness locality _
         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
      (case level of
@@ -1779,22 +1784,25 @@
         (* Unlike virtually any other polymorphic fact whose type variables can
            be instantiated by a known infinite type, extensionality actually
            encodes a cardinality constraints. *)
-        not (not sound andalso
+        not (soundness <> Sound andalso
              is_type_surely_infinite ctxt
-                 (if locality = Extensionality then []
-                  else known_infinite_types) T)
+                 (if locality = Extensionality orelse
+                     soundness = Sound_Modulo_Infiniteness then
+                    []
+                  else
+                    known_infinite_types) T)
       | Fin_Nonmono_Types => is_type_surely_finite ctxt T
       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
   | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level sound
+fun add_fact_nonmonotonic_types ctxt level soundness
         ({kind, locality, iformula, ...} : translated_formula) =
   formula_fold (SOME (kind <> Conjecture))
-               (add_iterm_nonmonotonic_types ctxt level sound locality)
+               (add_iterm_nonmonotonic_types ctxt level soundness locality)
                iformula
-fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
+fun nonmonotonic_types_for_facts ctxt type_enc soundness facts =
   let val level = level_of_type_enc type_enc in
     if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
-      [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
+      [] |> fold (add_fact_nonmonotonic_types ctxt level soundness) 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. (FIXME?) *)
@@ -1972,7 +1980,7 @@
 
 val explicit_apply = NONE (* for experiments *)
 
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc soundness
         exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
     val (format, type_enc) = choose_format [format] type_enc
@@ -2008,7 +2016,7 @@
                          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_enc sound
+      conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc soundness
     val repair = repair_fact ctxt format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
     val repaired_sym_tab =

--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -196,7 +196,7 @@
       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_enc true false
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc Sound false
                           no_lambdasN false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -65,6 +65,7 @@
   val measure_run_time : bool Config.T
   val atp_lambda_translation : string Config.T
   val atp_readable_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
@@ -341,10 +342,13 @@
   Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
                              (K smartN)
 (* In addition to being easier to read, readable names are often much shorter,
-   especially if types are mangled in names. For these reason, they are enabled
-   by default. *)
+   especially if types are mangled in names. This makes a difference for some
+   provers (e.g., E). For these reason, short names are enabled by default. *)
 val atp_readable_names =
   Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
+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)
@@ -642,10 +646,18 @@
                     |> Output.urgent_message
                   else
                     ()
+                val soundness =
+                  if sound then
+                    if Config.get ctxt atp_sound_modulo_infiniteness then
+                      Sound_Modulo_Infiniteness
+                    else
+                      Sound
+                  else
+                    Unsound
                 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_enc sound false
+                      type_enc soundness false
                       (Config.get ctxt atp_lambda_translation)
                       (Config.get ctxt atp_readable_names) true hyp_ts concl_t
                       facts