1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 27 14:56:26 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 27 14:56:28 2011 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4    val helper_table : ((string * bool) * thm list) list
     1.5    val factsN : string
     1.6    val prepare_atp_problem :
     1.7 -    Proof.context -> format -> formula_kind -> formula_kind -> type_sys
     1.8 +    Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
     1.9      -> bool -> bool -> bool -> term list -> term
    1.10      -> ((string * locality) * term) list
    1.11      -> string problem * string Symtab.table * int * int
    1.12 @@ -991,7 +991,8 @@
    1.13  fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
    1.14      exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
    1.15    | should_encode_type _ _ All_Types _ = true
    1.16 -  | should_encode_type ctxt _ Fin_Nonmono_Types T = is_type_surely_finite ctxt T
    1.17 +  | should_encode_type ctxt _ Fin_Nonmono_Types T =
    1.18 +    is_type_surely_finite ctxt false T
    1.19    | should_encode_type _ _ _ _ = false
    1.20  
    1.21  fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
    1.22 @@ -1617,26 +1618,27 @@
    1.23  
    1.24  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    1.25     out with monotonicity" paper presented at CADE 2011. *)
    1.26 -fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
    1.27 -  | add_combterm_nonmonotonic_types ctxt level locality _
    1.28 +fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
    1.29 +  | add_combterm_nonmonotonic_types ctxt level sound locality _
    1.30          (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
    1.31                             tm2)) =
    1.32      (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
    1.33       (case level of
    1.34          Noninf_Nonmono_Types =>
    1.35          not (is_locality_global locality) orelse
    1.36 -        not (is_type_surely_infinite ctxt T)
    1.37 -      | Fin_Nonmono_Types => is_type_surely_finite ctxt T
    1.38 +        not (is_type_surely_infinite ctxt sound T)
    1.39 +      | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
    1.40        | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
    1.41 -  | add_combterm_nonmonotonic_types _ _ _ _ _ = I
    1.42 -fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
    1.43 -                                            : translated_formula) =
    1.44 +  | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
    1.45 +fun add_fact_nonmonotonic_types ctxt level sound
    1.46 +        ({kind, locality, combformula, ...} : translated_formula) =
    1.47    formula_fold (SOME (kind <> Conjecture))
    1.48 -               (add_combterm_nonmonotonic_types ctxt level locality) combformula
    1.49 -fun nonmonotonic_types_for_facts ctxt type_sys facts =
    1.50 +               (add_combterm_nonmonotonic_types ctxt level sound locality)
    1.51 +               combformula
    1.52 +fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
    1.53    let val level = level_of_type_sys type_sys in
    1.54      if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
    1.55 -      [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
    1.56 +      [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
    1.57           (* We must add "bool" in case the helper "True_or_False" is added
    1.58              later. In addition, several places in the code rely on the list of
    1.59              nonmonotonic types not being empty. *)
    1.60 @@ -1817,7 +1819,7 @@
    1.61  
    1.62  val explicit_apply = NONE (* for experimental purposes *)
    1.63  
    1.64 -fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
    1.65 +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
    1.66          exporter readable_names preproc hyp_ts concl_t facts =
    1.67    let
    1.68      val (format, type_sys) = choose_format [format] type_sys
    1.69 @@ -1825,7 +1827,8 @@
    1.70        translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
    1.71                           facts
    1.72      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
    1.73 -    val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
    1.74 +    val nonmono_Ts =
    1.75 +      conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
    1.76      val repair = repair_fact ctxt format type_sys sym_tab
    1.77      val (conjs, facts) = (conjs, facts) |> pairself (map repair)
    1.78      val repaired_sym_tab =

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 27 14:56:26 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 27 14:56:28 2011 +0200
     2.3 @@ -21,8 +21,8 @@
     2.4    val typ_of_dtyp :
     2.5      Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
     2.6      -> typ
     2.7 -  val is_type_surely_finite : Proof.context -> typ -> bool
     2.8 -  val is_type_surely_infinite : Proof.context -> typ -> bool
     2.9 +  val is_type_surely_finite : Proof.context -> bool -> typ -> bool
    2.10 +  val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
    2.11    val monomorphic_term : Type.tyenv -> term -> term
    2.12    val eta_expand : typ list -> term -> int -> term
    2.13    val transform_elim_prop : term -> term
    2.14 @@ -136,7 +136,7 @@
    2.15     0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
    2.16     cardinality 2 or more. The specified default cardinality is returned if the
    2.17     cardinality of the type can't be determined. *)
    2.18 -fun tiny_card_of_type ctxt default_card T =
    2.19 +fun tiny_card_of_type ctxt sound default_card T =
    2.20    let
    2.21      val thy = Proof_Context.theory_of ctxt
    2.22      val max = 2 (* 1 would be too small for the "fun" case *)
    2.23 @@ -181,19 +181,20 @@
    2.24                         (Logic.varifyT_global abs_type) T
    2.25                         (Logic.varifyT_global rep_type)
    2.26                     |> aux true avoid of
    2.27 -                0 => 0
    2.28 +                0 => if sound then default_card else 0
    2.29                | 1 => 1
    2.30                | _ => default_card)
    2.31             | [] => default_card)
    2.32          (* Very slightly unsound: Type variables are assumed not to be
    2.33             constrained to cardinality 1. (In practice, the user would most
    2.34             likely have used "unit" directly anyway.) *)
    2.35 -      | TFree _ => if default_card = 1 then 2 else default_card
    2.36 +      | TFree _ =>
    2.37 +        if default_card = 1 andalso not sound then 2 else default_card
    2.38        | TVar _ => default_card
    2.39    in Int.min (max, aux false [] T) end
    2.40  
    2.41 -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
    2.42 -fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
    2.43 +fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
    2.44 +fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
    2.45  
    2.46  fun monomorphic_term subst =
    2.47    map_types (map_type_tvar (fn v =>

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 27 14:56:26 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 27 14:56:28 2011 +0200
     3.3 @@ -196,8 +196,8 @@
     3.4        tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     3.5      *)
     3.6      val (atp_problem, _, _, _, _, _, sym_tab) =
     3.7 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false false
     3.8 -                          [] @{prop False} props
     3.9 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
    3.10 +                          false [] @{prop False} props
    3.11      (*
    3.12      val _ = tracing ("ATP PROBLEM: " ^
    3.13                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 27 14:56:26 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 27 14:56:28 2011 +0200
     4.3 @@ -85,6 +85,7 @@
     4.4     ("overlord", "false"),
     4.5     ("blocking", "false"),
     4.6     ("type_sys", "smart"),
     4.7 +   ("sound", "false"),
     4.8     ("relevance_thresholds", "0.45 0.85"),
     4.9     ("max_relevant", "smart"),
    4.10     ("max_mono_iters", "3"),
    4.11 @@ -101,11 +102,12 @@
    4.12     ("quiet", "verbose"),
    4.13     ("no_overlord", "overlord"),
    4.14     ("non_blocking", "blocking"),
    4.15 +   ("unsound", "sound"),
    4.16     ("no_isar_proof", "isar_proof"),
    4.17     ("no_slicing", "slicing")]
    4.18  
    4.19  val params_for_minimize =
    4.20 -  ["debug", "verbose", "overlord", "type_sys", "max_mono_iters",
    4.21 +  ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
    4.22     "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    4.23     "preplay_timeout"]
    4.24  
    4.25 @@ -122,7 +124,8 @@
    4.26      ss as _ :: _ => forall (is_prover_supported ctxt) ss
    4.27    | _ => false
    4.28  
    4.29 -(* Secret feature: "provers =" and "type_sys =" can be left out. *)
    4.30 +(* "provers =" and "type_sys =" can be left out. The latter is a secret
    4.31 +   feature. *)
    4.32  fun check_and_repair_raw_param ctxt (name, value) =
    4.33    if is_known_raw_param name then
    4.34      (name, value)
    4.35 @@ -267,6 +270,7 @@
    4.36        else case lookup_string "type_sys" of
    4.37          "smart" => NONE
    4.38        | s => SOME (type_sys_from_string s)
    4.39 +    val sound = mode = Auto_Try orelse lookup_bool "sound"
    4.40      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    4.41      val max_relevant = lookup_option lookup_int "max_relevant"
    4.42      val max_mono_iters = lookup_int "max_mono_iters"
    4.43 @@ -285,9 +289,9 @@
    4.44       provers = provers, relevance_thresholds = relevance_thresholds,
    4.45       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    4.46       max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    4.47 -     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    4.48 -     slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
    4.49 -     expect = expect}
    4.50 +     sound = sound, isar_proof = isar_proof,
    4.51 +     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    4.52 +     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    4.53    end
    4.54  
    4.55  fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jun 27 14:56:26 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jun 27 14:56:28 2011 +0200
     5.3 @@ -59,7 +59,7 @@
     5.4      val {goal, ...} = Proof.goal state
     5.5      val params =
     5.6        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
     5.7 -       provers = provers, type_sys = type_sys,
     5.8 +       provers = provers, type_sys = type_sys, sound = true,
     5.9         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    5.10         max_mono_iters = max_mono_iters,
    5.11         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 14:56:26 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 14:56:28 2011 +0200
     6.3 @@ -25,6 +25,7 @@
     6.4       blocking: bool,
     6.5       provers: string list,
     6.6       type_sys: type_sys option,
     6.7 +     sound: bool,
     6.8       relevance_thresholds: real * real,
     6.9       max_relevant: int option,
    6.10       max_mono_iters: int,
    6.11 @@ -289,6 +290,7 @@
    6.12     blocking: bool,
    6.13     provers: string list,
    6.14     type_sys: type_sys option,
    6.15 +   sound: bool,
    6.16     relevance_thresholds: real * real,
    6.17     max_relevant: int option,
    6.18     max_mono_iters: int,
    6.19 @@ -492,7 +494,7 @@
    6.20     are omitted. *)
    6.21  fun is_dangerous_prop ctxt =
    6.22    transform_elim_prop
    6.23 -  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
    6.24 +  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf
    6.25        is_exhaustive_finite)
    6.26  
    6.27  fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
    6.28 @@ -528,9 +530,9 @@
    6.29  fun run_atp mode name
    6.30          ({exec, required_execs, arguments, proof_delims, known_failures,
    6.31            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    6.32 -        ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
    6.33 -          max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
    6.34 -          timeout, preplay_timeout, ...} : params)
    6.35 +        ({debug, verbose, overlord, type_sys, sound, max_relevant,
    6.36 +          max_mono_iters, max_new_mono_instances, isar_proof,
    6.37 +          isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
    6.38          minimize_command
    6.39          ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
    6.40    let
    6.41 @@ -633,8 +635,8 @@
    6.42                  val (atp_problem, pool, conjecture_offset, facts_offset,
    6.43                       fact_names, typed_helpers, sym_tab) =
    6.44                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    6.45 -                      type_sys false (Config.get ctxt atp_readable_names) true
    6.46 -                      hyp_ts concl_t facts
    6.47 +                      type_sys sound false (Config.get ctxt atp_readable_names)
    6.48 +                      true hyp_ts concl_t facts
    6.49                  fun weights () = atp_problem_weights atp_problem
    6.50                  val full_proof = debug orelse isar_proof
    6.51                  val core =

     7.1 --- a/src/HOL/ex/atp_export.ML	Mon Jun 27 14:56:26 2011 +0200
     7.2 +++ b/src/HOL/ex/atp_export.ML	Mon Jun 27 14:56:28 2011 +0200
     7.3 @@ -158,8 +158,8 @@
     7.4        facts0 |> map (fn ((_, loc), th) =>
     7.5                          ((Thm.get_name_hint th, loc), prop_of th))
     7.6      val (atp_problem, _, _, _, _, _, _) =
     7.7 -      prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
     7.8 -                          @{prop False} facts
     7.9 +      prepare_atp_problem ctxt format Axiom Axiom type_sys true true false true
    7.10 +                          [] @{prop False} facts
    7.11      val atp_problem =
    7.12        atp_problem
    7.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))