# HG changeset patch
# User blanchet
# Date 1327005432 -3600
# Node ID e2e52c7d25c9d7eec26f37b191ea70b8ef569351
# Parent  6ded25a6098a8fa144520d437de6559002b7b31e
renamed "sound" option to "strict"

diff -r 6ded25a6098a -r e2e52c7d25c9 NEWS
--- a/NEWS	Thu Jan 19 21:37:12 2012 +0100
+++ b/NEWS	Thu Jan 19 21:37:12 2012 +0100
@@ -275,6 +275,7 @@
 * Sledgehammer:
   - Added "lam_trans" and "minimize" options.
   - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
+  - Renamed "sound" option to "strict".
 
 * Metis:
   - Added possibility to specify lambda translations scheme as a
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/TPTP/atp_export.ML
--- a/src/HOL/TPTP/atp_export.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/TPTP/atp_export.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -169,7 +169,7 @@
 
 fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
-    val type_enc = type_enc |> type_enc_from_string Sound
+    val type_enc = type_enc |> type_enc_from_string Strict
                             |> adjust_type_enc format
     val mono = polymorphism_of_type_enc type_enc <> Polymorphic
     val path = file_name |> Path.explode
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -19,11 +19,11 @@
     General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
 
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-  datatype soundness = Sound_Modulo_Infinity | Sound
+  datatype strictness = Strict | Non_Strict
   datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
   datatype type_level =
     All_Types |
-    Noninf_Nonmono_Types of soundness * granularity |
+    Noninf_Nonmono_Types of strictness * granularity |
     Fin_Nonmono_Types of granularity |
     Const_Arg_Types |
     No_Types
@@ -88,7 +88,7 @@
   val level_of_type_enc : type_enc -> type_level
   val is_type_enc_quasi_sound : type_enc -> bool
   val is_type_enc_fairly_sound : type_enc -> bool
-  val type_enc_from_string : soundness -> string -> type_enc
+  val type_enc_from_string : strictness -> string -> type_enc
   val adjust_type_enc : atp_format -> type_enc -> type_enc
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
@@ -546,11 +546,11 @@
 
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Sound_Modulo_Infinity | Sound
+datatype strictness = Strict | Non_Strict
 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
 datatype type_level =
   All_Types |
-  Noninf_Nonmono_Types of soundness * granularity |
+  Noninf_Nonmono_Types of strictness * granularity |
   Fin_Nonmono_Types of granularity |
   Const_Arg_Types |
   No_Types
@@ -608,7 +608,7 @@
        | NONE => (constr All_Vars, s))
   | NONE => fallback s
 
-fun type_enc_from_string soundness s =
+fun type_enc_from_string strictness s =
   (case try (unprefix "poly_") s of
      SOME s => (SOME Polymorphic, s)
    | NONE =>
@@ -620,7 +620,7 @@
        | NONE => (NONE, s))
   ||> (pair All_Types
        |> try_nonmono Fin_Nonmono_Types bangs
-       |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
+       |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
   |> (fn (poly, (level, core)) =>
          case (core, (poly, level)) of
            ("simple", (SOME poly, _)) =>
@@ -1281,8 +1281,8 @@
 val known_infinite_types =
   [@{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 true cached_Ts T
+fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
+  strictness <> Strict 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
@@ -1292,12 +1292,12 @@
 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts, ...}
-                       (Noninf_Nonmono_Types (soundness, grain)) T =
+                       (Noninf_Nonmono_Types (strictness, grain)) T =
     grain = Ghost_Type_Arg_Vars orelse
     (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
      not (exists (type_instance ctxt T) surely_infinite_Ts orelse
           (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
-           is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
+           is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
                                            T)))
   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
                              maybe_nonmono_Ts, ...}
@@ -2046,7 +2046,7 @@
    maybe_infinite_Ts = known_infinite_types,
    surely_infinite_Ts =
      case level of
-       Noninf_Nonmono_Types (Sound, _) => []
+       Noninf_Nonmono_Types (Strict, _) => []
      | _ => known_infinite_types,
    maybe_nonmono_Ts = [@{typ bool}]}
 
@@ -2059,11 +2059,11 @@
                   surely_infinite_Ts, maybe_nonmono_Ts}) =
     if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
       case level of
-        Noninf_Nonmono_Types (soundness, _) =>
+        Noninf_Nonmono_Types (strictness, _) =>
         if exists (type_instance ctxt T) surely_infinite_Ts orelse
            member (type_equiv ctxt) maybe_finite_Ts T then
           mono
-        else if is_type_kind_of_surely_infinite ctxt soundness
+        else if is_type_kind_of_surely_infinite ctxt strictness
                                                 surely_infinite_Ts T then
           {maybe_finite_Ts = maybe_finite_Ts,
            surely_finite_Ts = surely_finite_Ts,
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -140,7 +140,7 @@
       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
-      val type_enc = type_enc_from_string Sound type_enc
+      val type_enc = type_enc_from_string Strict type_enc
       val (sym_tab, axioms, concealed) =
         prepare_metis_problem ctxt type_enc lam_trans cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -87,7 +87,7 @@
    ("overlord", "false"),
    ("blocking", "false"),
    ("type_enc", "smart"),
-   ("sound", "false"),
+   ("strict", "false"),
    ("lam_trans", "smart"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
@@ -106,13 +106,13 @@
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("non_blocking", "blocking"),
-   ("unsound", "sound"),
+   ("non_strict", "strict"),
    ("no_isar_proof", "isar_proof"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize")]
 
 val params_for_minimize =
-  ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
+  ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    "max_mono_iters", "max_new_mono_instances", "isar_proof",
    "isar_shrink_factor", "timeout", "preplay_timeout"]
 
@@ -141,7 +141,7 @@
                             | _ => value)
     | NONE => (name, value)
 
-val any_type_enc = type_enc_from_string Sound "erased"
+val any_type_enc = type_enc_from_string Strict "erased"
 
 (* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
    this is a secret feature. *)
@@ -152,7 +152,7 @@
            (name, value)
          else if is_prover_list ctxt name andalso null value then
            ("provers", [name])
-         else if can (type_enc_from_string Sound) name andalso null value then
+         else if can (type_enc_from_string Strict) name andalso null value then
            ("type_enc", [name])
          else if can (trans_lams_from_string ctxt any_type_enc) name andalso
                  null value then
@@ -282,8 +282,8 @@
         NONE
       else case lookup_string "type_enc" of
         "smart" => NONE
-      | s => (type_enc_from_string Sound s; SOME s)
-    val sound = mode = Auto_Try orelse lookup_bool "sound"
+      | s => (type_enc_from_string Strict s; SOME s)
+    val strict = mode = Auto_Try orelse lookup_bool "strict"
     val lam_trans = lookup_option lookup_string "lam_trans"
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_option lookup_int "max_relevant"
@@ -302,7 +302,7 @@
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
-     provers = provers, type_enc = type_enc, sound = sound,
+     provers = provers, type_enc = type_enc, strict = strict,
      lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
      max_relevant = max_relevant, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -47,8 +47,8 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
-                 max_new_mono_instances, type_enc, lam_trans, isar_proof,
-                 isar_shrink_factor, preplay_timeout, ...} : params)
+                 max_new_mono_instances, type_enc, strict, lam_trans,
+                 isar_proof, isar_shrink_factor, preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
     val _ =
@@ -61,7 +61,7 @@
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
-       provers = provers, type_enc = type_enc, sound = true,
+       provers = provers, type_enc = type_enc, strict = strict,
        lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
        max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -25,7 +25,7 @@
      blocking: bool,
      provers: string list,
      type_enc: string option,
-     sound: bool,
+     strict: bool,
      lam_trans: string option,
      relevance_thresholds: real * real,
      max_relevant: int option,
@@ -289,7 +289,7 @@
    blocking: bool,
    provers: string list,
    type_enc: string option,
-   sound: bool,
+   strict: bool,
    lam_trans: string option,
    relevance_thresholds: real * real,
    max_relevant: int option,
@@ -580,7 +580,7 @@
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
-        (params as {debug, verbose, overlord, type_enc, sound, lam_trans,
+        (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     max_relevant, max_mono_iters, max_new_mono_instances,
                     isar_proof, isar_shrink_factor, slice, timeout,
                     preplay_timeout, ...})
@@ -659,7 +659,7 @@
                 val num_facts =
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
-                val soundness = if sound then Sound else Sound_Modulo_Infinity
+                val soundness = if strict then Strict else Non_Strict
                 val type_enc =
                   type_enc |> choose_type_enc soundness best_type_enc format
                 val fairly_sound = is_type_enc_fairly_sound type_enc
diff -r 6ded25a6098a -r e2e52c7d25c9 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -73,7 +73,7 @@
                            (K 5.0)
 
 fun adjust_reconstructor_params override_params
-        ({debug, verbose, overlord, blocking, provers, type_enc, sound,
+        ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
          max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
          minimize, timeout, preplay_timeout, expect} : params) =
@@ -88,7 +88,7 @@
     val lam_trans = lookup_override "lam_trans" lam_trans
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
-     provers = provers, type_enc = type_enc, sound = sound,
+     provers = provers, type_enc = type_enc, strict = strict,
      lam_trans = lam_trans, max_relevant = max_relevant,
      relevance_thresholds = relevance_thresholds,
      max_mono_iters = max_mono_iters,