exploit inferred monotonicity
authorblanchet
Wed May 04 19:35:48 2011 +0200 (2011-05-04)
changeset 42680b6c27cf04fe9
parent 42679 223f01b32f17
child 42681 281cc069282c
exploit inferred monotonicity
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:48:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 19:35:48 2011 +0200
     1.3 @@ -980,7 +980,7 @@
     1.4                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
     1.5                             default_card)
     1.6  
     1.7 -(* Similar to similarly named function in "Sledgehammer_ATP_Translate". *)
     1.8 +(* Similar to "Sledgehammer_ATP_Translate.tiny_card_of_type". *)
     1.9  fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
    1.10                                 assigns T =
    1.11    let
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed May 04 18:48:25 2011 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed May 04 19:35:48 2011 +0200
     2.3 @@ -263,7 +263,7 @@
     2.4  
     2.5  val simple_string_of_typ = Refute.string_of_typ
     2.6  val is_real_constr = Refute.is_IDT_constructor
     2.7 -val typ_of_dtyp = Refute.typ_of_dtyp
     2.8 +val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
     2.9  val is_of_class_const = Refute.is_const_of_class
    2.10  val get_class_def = Refute.get_classdef
    2.11  val monomorphic_term = Sledgehammer_Util.monomorphic_term
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed May 04 18:48:25 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed May 04 19:35:48 2011 +0200
     3.3 @@ -176,8 +176,8 @@
     3.4  
     3.5  fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names =
     3.6    not o is_conjecture_referred_to_in_proof conjecture_shape andf
     3.7 -  forall (is_global_locality o snd)
     3.8 -  o used_facts_in_atp_proof type_sys facts_offset fact_names
     3.9 +  forall (is_locality_global o snd)
    3.10 +    o used_facts_in_atp_proof type_sys facts_offset fact_names
    3.11  
    3.12  (** Soft-core proof reconstruction: Metis one-liner **)
    3.13  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 18:48:25 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 19:35:48 2011 +0200
     4.3 @@ -147,17 +147,17 @@
     4.4    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
     4.5    | formula_map f (AAtom tm) = AAtom (f tm)
     4.6  
     4.7 -fun formula_fold f =
     4.8 +fun formula_fold pos f =
     4.9    let
    4.10      fun aux pos (AQuant (_, _, phi)) = aux pos phi
    4.11 -      | aux pos (AConn (ANot, [phi])) = aux (not pos) phi
    4.12 +      | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
    4.13        | aux pos (AConn (AImplies, [phi1, phi2])) =
    4.14 -        aux (not pos) phi1 #> aux pos phi2
    4.15 -      | aux pos (AConn (c, phis)) =
    4.16 -        if member (op =) [AAnd, AOr] c then fold (aux pos) phis
    4.17 -        else raise Fail "unexpected connective with unknown polarities"
    4.18 +        aux (Option.map not pos) phi1 #> aux pos phi2
    4.19 +      | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
    4.20 +      | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
    4.21 +      | aux _ (AConn (_, phis)) = fold (aux NONE) phis
    4.22        | aux pos (AAtom tm) = f pos tm
    4.23 -  in aux true end
    4.24 +  in aux (SOME pos) end
    4.25  
    4.26  type translated_formula =
    4.27    {name: string,
    4.28 @@ -483,7 +483,7 @@
    4.29        end
    4.30    in aux true end
    4.31  fun add_fact_syms_to_table explicit_apply =
    4.32 -  fact_lift (formula_fold (K (add_combterm_syms_to_table explicit_apply)))
    4.33 +  fact_lift (formula_fold true (K (add_combterm_syms_to_table explicit_apply)))
    4.34  
    4.35  val default_sym_table_entries : (string * sym_info) list =
    4.36    [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
    4.37 @@ -665,38 +665,66 @@
    4.38     unsound ATP proofs. The checks below are an (unsound) approximation of
    4.39     finiteness. *)
    4.40  
    4.41 -fun is_dtyp_finite _ (Datatype_Aux.DtTFree _) = true
    4.42 -  | is_dtyp_finite ctxt (Datatype_Aux.DtType (s, Us)) =
    4.43 -    is_type_constr_finite ctxt s andalso forall (is_dtyp_finite ctxt) Us
    4.44 -  | is_dtyp_finite _ (Datatype_Aux.DtRec _) = false
    4.45 -and is_type_finite ctxt (Type (s, Ts)) =
    4.46 -    is_type_constr_finite ctxt s andalso forall (is_type_finite ctxt) Ts
    4.47 -  | is_type_finite _ _ = false
    4.48 -and is_type_constr_finite ctxt s =
    4.49 -  let val thy = Proof_Context.theory_of ctxt in
    4.50 -    case Datatype_Data.get_info thy s of
    4.51 -      SOME {descr, ...} =>
    4.52 -      forall (fn (_, (_, _, constrs)) =>
    4.53 -                 forall (forall (is_dtyp_finite ctxt) o snd) constrs) descr
    4.54 -    | NONE =>
    4.55 -      case Typedef.get_info ctxt s of
    4.56 -        ({rep_type, ...}, _) :: _ => is_type_finite ctxt rep_type
    4.57 -      | [] => true
    4.58 -  end
    4.59 +fun datatype_constrs thy (T as Type (s, Ts)) =
    4.60 +    (case Datatype.get_info thy s of
    4.61 +       SOME {index, descr, ...} =>
    4.62 +       let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
    4.63 +         map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
    4.64 +             constrs
    4.65 +       end
    4.66 +     | NONE => [])
    4.67 +  | datatype_constrs _ _ = []
    4.68  
    4.69 -fun should_encode_type _ All_Types _ = true
    4.70 -  | should_encode_type ctxt Finite_Types T = is_type_finite ctxt T
    4.71 -  | should_encode_type _ Nonmonotonic_Types _ =
    4.72 -    error "Monotonicity inference not implemented yet."
    4.73 -  | should_encode_type _ _ _ = false
    4.74 +(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
    4.75 +   0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
    4.76 +   cardinality 2 or more. The specified default cardinality is returned if the
    4.77 +   cardinality of the type can't be determined. *)
    4.78 +fun tiny_card_of_type ctxt default_card T =
    4.79 +  let
    4.80 +    val max = 2 (* 1 would be too small for the "fun" case *)
    4.81 +    fun aux avoid T =
    4.82 +      (if member (op =) avoid T then
    4.83 +         0
    4.84 +       else case T of
    4.85 +         Type (@{type_name fun}, [T1, T2]) =>
    4.86 +         (case (aux avoid T1, aux avoid T2) of
    4.87 +            (_, 1) => 1
    4.88 +          | (0, _) => 0
    4.89 +          | (_, 0) => 0
    4.90 +          | (k1, k2) =>
    4.91 +            if k1 >= max orelse k2 >= max then max
    4.92 +            else Int.min (max, Integer.pow k2 k1))
    4.93 +       | Type _ =>
    4.94 +         (case datatype_constrs (Proof_Context.theory_of ctxt) T of
    4.95 +            [] => default_card
    4.96 +          | constrs =>
    4.97 +            let
    4.98 +              val constr_cards =
    4.99 +                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
   4.100 +                    constrs
   4.101 +            in
   4.102 +              if exists (curry (op =) 0) constr_cards then 0
   4.103 +              else Int.min (max, Integer.sum constr_cards)
   4.104 +            end)
   4.105 +       | _ => default_card)
   4.106 +  in Int.min (max, aux [] T) end
   4.107  
   4.108 -fun should_predicate_on_type ctxt (Preds (_, level)) T =
   4.109 -    should_encode_type ctxt level T
   4.110 -  | should_predicate_on_type _ _ _ = false
   4.111 +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
   4.112 +fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
   4.113  
   4.114 -fun should_tag_with_type ctxt (Tags (_, level)) T =
   4.115 -    should_encode_type ctxt level T
   4.116 -  | should_tag_with_type _ _ _ = false
   4.117 +fun should_encode_type _ _ All_Types _ = true
   4.118 +  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
   4.119 +  | should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
   4.120 +    exists (curry Type.raw_instance T) nonmono_Ts
   4.121 +  | should_encode_type _ _ _ _ = false
   4.122 +
   4.123 +fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
   4.124 +    should_encode_type ctxt nonmono_Ts level T
   4.125 +  | should_predicate_on_type _ _ _ _ = false
   4.126 +
   4.127 +fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
   4.128 +    should_encode_type ctxt nonmono_Ts level T
   4.129 +  | should_tag_with_type _ _ _ _ = false
   4.130  
   4.131  fun type_pred_combatom type_sys T tm =
   4.132    CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
   4.133 @@ -704,7 +732,7 @@
   4.134    |> impose_type_arg_policy_in_combterm type_sys
   4.135    |> AAtom
   4.136  
   4.137 -fun formula_from_combformula ctxt type_sys =
   4.138 +fun formula_from_combformula ctxt nonmono_Ts type_sys =
   4.139    let
   4.140      fun tag_with_type type_sys T tm =
   4.141        CombConst (`make_fixed_const type_tag_name, T --> T, [T])
   4.142 @@ -723,7 +751,8 @@
   4.143                            map (do_term false) args)
   4.144          val T = combtyp_of u
   4.145        in
   4.146 -        t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then
   4.147 +        t |> (if not top_level andalso
   4.148 +                should_tag_with_type ctxt nonmono_Ts type_sys T then
   4.149                  tag_with_type type_sys T
   4.150                else
   4.151                  I)
   4.152 @@ -731,7 +760,7 @@
   4.153      val do_bound_type =
   4.154        if type_sys = Many_Typed then SOME o mangled_type_name else K NONE
   4.155      fun do_out_of_bound_type (s, T) =
   4.156 -      if should_predicate_on_type ctxt type_sys T then
   4.157 +      if should_predicate_on_type ctxt nonmono_Ts type_sys T then
   4.158          type_pred_combatom type_sys T (CombVar (s, T))
   4.159          |> do_formula |> SOME
   4.160        else
   4.161 @@ -748,11 +777,11 @@
   4.162        | do_formula (AAtom tm) = AAtom (do_term true tm)
   4.163    in do_formula end
   4.164  
   4.165 -fun formula_for_fact ctxt type_sys
   4.166 +fun formula_for_fact ctxt nonmono_Ts type_sys
   4.167                       ({combformula, atomic_types, ...} : translated_formula) =
   4.168    mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
   4.169                  (atp_type_literals_for_types type_sys Axiom atomic_types))
   4.170 -           (formula_from_combformula ctxt type_sys
   4.171 +           (formula_from_combformula ctxt nonmono_Ts type_sys
   4.172                  (close_combformula_universally combformula))
   4.173    |> close_formula_universally
   4.174  
   4.175 @@ -761,13 +790,12 @@
   4.176  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   4.177     of monomorphization). The TPTP explicitly forbids name clashes, and some of
   4.178     the remote provers might care. *)
   4.179 -fun formula_line_for_fact ctxt prefix type_sys
   4.180 +fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
   4.181                            (j, formula as {name, locality, kind, ...}) =
   4.182 -  Formula (prefix ^
   4.183 -           (if polymorphism_of_type_sys type_sys = Polymorphic then ""
   4.184 -            else string_of_int j ^ "_") ^
   4.185 +  Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
   4.186 +                     else string_of_int j ^ "_") ^
   4.187             ascii_of name,
   4.188 -           kind, formula_for_fact ctxt type_sys formula, NONE,
   4.189 +           kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
   4.190             if generate_useful_info then
   4.191               case locality of
   4.192                 Intro => useful_isabelle_info "intro"
   4.193 @@ -800,10 +828,10 @@
   4.194                           (fo_literal_from_arity_literal conclLit))
   4.195             |> close_formula_universally, NONE, NONE)
   4.196  
   4.197 -fun formula_line_for_conjecture ctxt type_sys
   4.198 +fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
   4.199          ({name, kind, combformula, ...} : translated_formula) =
   4.200    Formula (conjecture_prefix ^ name, kind,
   4.201 -           formula_from_combformula ctxt type_sys
   4.202 +           formula_from_combformula ctxt nonmono_Ts type_sys
   4.203                                      (close_combformula_universally combformula)
   4.204             |> close_formula_universally, NONE, NONE)
   4.205  
   4.206 @@ -856,30 +884,34 @@
   4.207        end
   4.208    in do_term end
   4.209  fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
   4.210 -  fact_lift (formula_fold
   4.211 +  fact_lift (formula_fold true
   4.212        (K (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)))
   4.213  fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
   4.214    Symtab.empty |> is_type_sys_fairly_sound type_sys
   4.215                    ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
   4.216                           facts
   4.217  
   4.218 +
   4.219  (* FIXME: use CombVar not CombConst for bound variables? *)
   4.220  fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
   4.221      String.isPrefix bound_var_prefix s
   4.222    | is_var_or_bound_var (CombVar _) = true
   4.223    | is_var_or_bound_var _ = false
   4.224  
   4.225 -fun add_combterm_nonmonotonic_types true
   4.226 -        (CombApp (CombConst (("equal", _), Type (_, [T, _]), _),
   4.227 -                  CombApp (tm1, tm2))) =
   4.228 -    exists is_var_or_bound_var [tm1, tm2] ? insert_type I T
   4.229 -  | add_combterm_nonmonotonic_types _ _ = I
   4.230 -
   4.231 -val add_fact_nonmonotonic_types =
   4.232 -  fact_lift (formula_fold add_combterm_nonmonotonic_types)
   4.233 -fun nonmonotonic_types_for_facts type_sys facts =
   4.234 -  [] |> level_of_type_sys type_sys = Nonmonotonic_Types
   4.235 -        ? fold add_fact_nonmonotonic_types facts
   4.236 +fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
   4.237 +  | add_combterm_nonmonotonic_types ctxt _
   4.238 +        (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
   4.239 +                  tm2)) =
   4.240 +    (exists is_var_or_bound_var [tm1, tm2] andalso
   4.241 +     not (is_type_surely_infinite ctxt T)) ? insert_type I T
   4.242 +  | add_combterm_nonmonotonic_types _ _ _ = I
   4.243 +fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
   4.244 +                                      : translated_formula) =
   4.245 +  formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
   4.246 +               combformula
   4.247 +fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
   4.248 +  level_of_type_sys type_sys = Nonmonotonic_Types
   4.249 +  ? fold (add_fact_nonmonotonic_types ctxt) facts
   4.250  
   4.251  fun n_ary_strip_type 0 T = ([], T)
   4.252    | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
   4.253 @@ -896,7 +928,8 @@
   4.254  
   4.255  fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
   4.256  
   4.257 -fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) =
   4.258 +fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
   4.259 +                              (s', T_args, T, _, ary) =
   4.260    let
   4.261      val (arg_Ts, res_T) = n_ary_strip_type ary T
   4.262      val bound_names =
   4.263 @@ -913,12 +946,12 @@
   4.264               |> fold (curry (CombApp o swap)) bound_tms
   4.265               |> type_pred_combatom type_sys res_T
   4.266               |> mk_aquant AForall (bound_names ~~ bound_Ts)
   4.267 -             |> formula_from_combformula ctxt type_sys
   4.268 +             |> formula_from_combformula ctxt nonmono_Ts type_sys
   4.269               |> close_formula_universally,
   4.270               NONE, NONE)
   4.271    end
   4.272  
   4.273 -fun problem_lines_for_sym_decls ctxt type_sys (s, decls) =
   4.274 +fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) =
   4.275    if type_sys = Many_Typed then
   4.276      map (decl_line_for_sym_decl s) decls
   4.277    else
   4.278 @@ -936,15 +969,16 @@
   4.279          | _ => decls
   4.280        val n = length decls
   4.281        val decls =
   4.282 -        decls |> filter (should_predicate_on_type ctxt type_sys
   4.283 +        decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
   4.284                           o result_type_of_decl)
   4.285      in
   4.286 -      map2 (formula_line_for_sym_decl ctxt type_sys n s)
   4.287 +      map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s)
   4.288             (0 upto length decls - 1) decls
   4.289      end
   4.290  
   4.291 -fun problem_lines_for_sym_decl_table ctxt type_sys sym_decl_tab =
   4.292 -  Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt type_sys)
   4.293 +fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab =
   4.294 +  Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts
   4.295 +                                                        type_sys)
   4.296                    sym_decl_tab []
   4.297  
   4.298  fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
   4.299 @@ -985,33 +1019,35 @@
   4.300      val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
   4.301      val (conjs, facts) =
   4.302        (conjs, facts) |> pairself (map (repair_fact type_sys sym_tab))
   4.303 -    val conjs_and_facts = conjs @ facts
   4.304 -    val repaired_sym_tab = conjs_and_facts |> sym_table_for_facts false
   4.305 -    val sym_decl_lines =
   4.306 -      conjs_and_facts
   4.307 -      |> sym_decl_table_for_facts type_sys repaired_sym_tab
   4.308 -      |> problem_lines_for_sym_decl_table ctxt type_sys
   4.309 +    val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
   4.310      val helpers =
   4.311        helper_facts_for_sym_table ctxt type_sys repaired_sym_tab
   4.312        |> map (repair_fact type_sys sym_tab)
   4.313 -    val nonmonotonic_Ts =
   4.314 -      nonmonotonic_types_for_facts type_sys (helpers @ conjs_and_facts)
   4.315 +    val nonmono_Ts =
   4.316 +      [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys)
   4.317 +                 [facts, conjs, helpers]
   4.318 +    val sym_decl_lines =
   4.319 +      conjs @ facts
   4.320 +      |> sym_decl_table_for_facts type_sys repaired_sym_tab
   4.321 +      |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys
   4.322      (* Reordering these might confuse the proof reconstruction code or the SPASS
   4.323         Flotter hack. *)
   4.324      val problem =
   4.325        [(sym_declsN, sym_decl_lines),
   4.326 -       (factsN, map (formula_line_for_fact ctxt fact_prefix type_sys)
   4.327 +       (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
   4.328                      (0 upto length facts - 1 ~~ facts)),
   4.329         (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
   4.330         (aritiesN, map formula_line_for_arity_clause arity_clauses),
   4.331 -       (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys)
   4.332 +       (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
   4.333 +                                             type_sys)
   4.334                        (0 upto length helpers - 1 ~~ helpers)
   4.335                    |> (case type_sys of
   4.336                          Tags (Polymorphic, level) =>
   4.337                          member (op =) [Finite_Types, Nonmonotonic_Types] level
   4.338                          ? cons (ti_ti_helper_fact ())
   4.339                        | _ => I)),
   4.340 -       (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
   4.341 +       (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
   4.342 +                    conjs),
   4.343         (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
   4.344      val problem =
   4.345        problem
   4.346 @@ -1041,7 +1077,7 @@
   4.347    (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   4.348    #> fold (add_term_weights weight) tms
   4.349  fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
   4.350 -    formula_fold (K (add_term_weights weight)) phi
   4.351 +    formula_fold true (K (add_term_weights weight)) phi
   4.352    | add_problem_line_weights _ _ = I
   4.353  
   4.354  fun add_conjectures_weights [] = I
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 04 18:48:25 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 04 19:35:48 2011 +0200
     5.3 @@ -36,7 +36,7 @@
     5.4       only : bool}
     5.5  
     5.6    val trace : bool Config.T
     5.7 -  val is_global_locality : locality -> bool
     5.8 +  val is_locality_global : locality -> bool
     5.9    val fact_from_ref :
    5.10      Proof.context -> unit Symtab.table -> thm list
    5.11      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    5.12 @@ -70,10 +70,10 @@
    5.13  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
    5.14  
    5.15  (* (quasi-)underapproximation of the truth *)
    5.16 -fun is_global_locality Local = false
    5.17 -  | is_global_locality Assum = false
    5.18 -  | is_global_locality Chained = false
    5.19 -  | is_global_locality _ = true
    5.20 +fun is_locality_global Local = false
    5.21 +  | is_locality_global Assum = false
    5.22 +  | is_locality_global Chained = false
    5.23 +  | is_locality_global _ = true
    5.24  
    5.25  type relevance_fudge =
    5.26    {allow_ext : bool,
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed May 04 18:48:25 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed May 04 19:35:48 2011 +0200
     6.3 @@ -15,6 +15,9 @@
     6.4    val nat_subscript : int -> string
     6.5    val unyxml : string -> string
     6.6    val maybe_quote : string -> string
     6.7 +  val typ_of_dtyp :
     6.8 +    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
     6.9 +    -> typ
    6.10    val monomorphic_term : Type.tyenv -> term -> term
    6.11    val eta_expand : typ list -> term -> int -> term
    6.12    val transform_elim_term : term -> term
    6.13 @@ -80,6 +83,15 @@
    6.14             Keyword.is_keyword s) ? quote
    6.15    end
    6.16  
    6.17 +fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
    6.18 +    the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
    6.19 +  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
    6.20 +    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
    6.21 +  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
    6.22 +    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
    6.23 +      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    6.24 +    end
    6.25 +
    6.26  fun monomorphic_term subst t =
    6.27    map_types (map_type_tvar (fn v =>
    6.28        case Type.lookup subst v of
     7.1 --- a/src/HOL/Tools/refute.ML	Wed May 04 18:48:25 2011 +0200
     7.2 +++ b/src/HOL/Tools/refute.ML	Wed May 04 19:35:48 2011 +0200
     7.3 @@ -71,7 +71,6 @@
     7.4    val is_IDT_recursor : theory -> string * typ -> bool
     7.5    val is_const_of_class: theory -> string * typ -> bool
     7.6    val string_of_typ : typ -> string
     7.7 -  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
     7.8  end;
     7.9  
    7.10  structure Refute : REFUTE =
    7.11 @@ -394,17 +393,7 @@
    7.12  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
    7.13  (* ------------------------------------------------------------------------- *)
    7.14  
    7.15 -fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) =
    7.16 -      (* replace a 'DtTFree' variable by the associated type *)
    7.17 -      the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
    7.18 -  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) =
    7.19 -      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    7.20 -  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
    7.21 -      let
    7.22 -        val (s, ds, _) = the (AList.lookup (op =) descr i)
    7.23 -      in
    7.24 -        Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    7.25 -      end;
    7.26 +val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
    7.27  
    7.28  (* ------------------------------------------------------------------------- *)
    7.29  (* close_form: universal closure over schematic variables in 't'             *)