merged
authorwenzelm
Fri, 17 Jun 2011 14:35:24 +0200
changeset 43424 eeba70379f1a
parent 43423 717880e98e6b (diff)
parent 43420 a26e514c92b2 (current diff)
child 43425 0a5612040a8b
child 43438 a666b8d11252
merged
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Jun 17 14:31:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Jun 17 14:35:24 2011 +0200
@@ -317,6 +317,7 @@
           AConn (c, [opn pos1 phi1, opn pos2 phi2])
         end
       | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)
+      | opn _ phi = phi
   in opn (SOME (not conj)) end
 fun open_formula_line (Formula (ident, kind, phi, source, info)) =
     Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Jun 17 14:31:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Jun 17 14:35:24 2011 +0200
@@ -215,7 +215,7 @@
     union (op =) (resolve_fact facts_offset fact_names name)
   | add_fact ctxt _ _ (Inference (_, _, deps)) =
     if AList.defined (op =) deps leo2_ext then
-      insert (op =) (ext_name ctxt, General (* or Chained... *))
+      insert (op =) (ext_name ctxt, Extensionality)
     else
       I
   | add_fact _ _ _ _ = I
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 17 14:31:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 17 14:35:24 2011 +0200
@@ -40,7 +40,9 @@
     CombVar of name * typ |
     CombApp of combterm * combterm
 
-  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+  datatype locality =
+    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
+    Chained
 
   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
   datatype type_level =
@@ -534,7 +536,9 @@
     |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
-datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+datatype locality =
+  General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
+  Chained
 
 (* (quasi-)underapproximation of the truth *)
 fun is_locality_global Local = false
@@ -1357,7 +1361,7 @@
           (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
           (if needs_fairly_sound then typed_helper_suffix
            else untyped_helper_suffix),
-          General),
+          Helper),
          let val t = th |> prop_of in
            t |> should_specialize_helper type_sys t
                 ? (case types of
@@ -1467,12 +1471,12 @@
   CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
            |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
 
-fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
-  | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
+fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
+  | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
   | is_var_nonmonotonic_in_formula pos phi _ name =
-    formula_fold pos (var_occurs_positively_naked_in_term name) phi false
+    formula_fold pos (is_var_positively_naked_in_term name) phi false
 
 fun mk_const_aterm format type_sys x T_args args =
   ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
@@ -1652,11 +1656,6 @@
        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
   end
 
-(* 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"}]
-
 (* 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_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
@@ -1667,7 +1666,7 @@
      (case level of
         Noninf_Nonmono_Types =>
         not (is_locality_global locality) orelse
-        not (is_type_surely_infinite ctxt known_infinite_types T)
+        not (is_type_surely_infinite ctxt T)
       | Fin_Nonmono_Types => is_type_surely_finite ctxt T
       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
   | add_combterm_nonmonotonic_types _ _ _ _ _ = I
--- a/src/HOL/Tools/ATP/atp_util.ML	Fri Jun 17 14:31:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Jun 17 14:35:24 2011 +0200
@@ -22,7 +22,7 @@
     Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
     -> typ
   val is_type_surely_finite : Proof.context -> typ -> bool
-  val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
+  val is_type_surely_infinite : Proof.context -> typ -> bool
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val transform_elim_prop : term -> term
@@ -136,70 +136,64 @@
    0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
    cardinality 2 or more. The specified default cardinality is returned if the
    cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card assigns T =
+fun tiny_card_of_type ctxt default_card T =
   let
     val thy = Proof_Context.theory_of ctxt
     val max = 2 (* 1 would be too small for the "fun" case *)
     fun aux slack avoid T =
       if member (op =) avoid T then
         0
-      else case AList.lookup (Sign.typ_instance thy o swap) assigns T of
-        SOME k => k
-      | NONE =>
-        case T of
-          Type (@{type_name fun}, [T1, T2]) =>
-          (case (aux slack avoid T1, aux slack avoid T2) of
-             (k, 1) => if slack andalso k = 0 then 0 else 1
-           | (0, _) => 0
-           | (_, 0) => 0
-           | (k1, k2) =>
-             if k1 >= max orelse k2 >= max then max
-             else Int.min (max, Integer.pow k2 k1))
-        | @{typ prop} => 2
-        | @{typ bool} => 2 (* optimization *)
-        | @{typ nat} => 0 (* optimization *)
-        | Type ("Int.int", []) => 0 (* optimization *)
-        | Type (s, _) =>
-          (case datatype_constrs thy T of
-             constrs as _ :: _ =>
-             let
-               val constr_cards =
-                 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
-                      o snd) constrs
-             in
-               if exists (curry (op =) 0) constr_cards then 0
-               else Int.min (max, Integer.sum constr_cards)
-             end
-           | [] =>
-             case Typedef.get_info ctxt s of
-               ({abs_type, rep_type, ...}, _) :: _ =>
-               (* We cheat here by assuming that typedef types are infinite if
-                  their underlying type is infinite. This is unsound in general
-                  but it's hard to think of a realistic example where this would
-                  not be the case. We are also slack with representation types:
-                  If a representation type has the form "sigma => tau", we
-                  consider it enough to check "sigma" for infiniteness. (Look
-                  for "slack" in this function.) *)
-               (case varify_and_instantiate_type ctxt
-                         (Logic.varifyT_global abs_type) T
-                         (Logic.varifyT_global rep_type)
-                     |> aux true avoid of
-                  0 => 0
-                | 1 => 1
-                | _ => default_card)
-             | [] => default_card)
-          (* Very slightly unsound: Type variables are assumed not to be
-             constrained to cardinality 1. (In practice, the user would most
-             likely have used "unit" directly anyway.) *)
-        | TFree _ => if default_card = 1 then 2 else default_card
-          (* Schematic type variables that contain only unproblematic sorts
-             (with no finiteness axiom) can safely be considered infinite. *)
-        | TVar _ => default_card
+      else case T of
+        Type (@{type_name fun}, [T1, T2]) =>
+        (case (aux slack avoid T1, aux slack avoid T2) of
+           (k, 1) => if slack andalso k = 0 then 0 else 1
+         | (0, _) => 0
+         | (_, 0) => 0
+         | (k1, k2) =>
+           if k1 >= max orelse k2 >= max then max
+           else Int.min (max, Integer.pow k2 k1))
+      | @{typ prop} => 2
+      | @{typ bool} => 2 (* optimization *)
+      | @{typ nat} => 0 (* optimization *)
+      | Type ("Int.int", []) => 0 (* optimization *)
+      | Type (s, _) =>
+        (case datatype_constrs thy T of
+           constrs as _ :: _ =>
+           let
+             val constr_cards =
+               map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+                    o snd) constrs
+           in
+             if exists (curry (op =) 0) constr_cards then 0
+             else Int.min (max, Integer.sum constr_cards)
+           end
+         | [] =>
+           case Typedef.get_info ctxt s of
+             ({abs_type, rep_type, ...}, _) :: _ =>
+             (* We cheat here by assuming that typedef types are infinite if
+                their underlying type is infinite. This is unsound in general
+                but it's hard to think of a realistic example where this would
+                not be the case. We are also slack with representation types:
+                If a representation type has the form "sigma => tau", we
+                consider it enough to check "sigma" for infiniteness. (Look
+                for "slack" in this function.) *)
+             (case varify_and_instantiate_type ctxt
+                       (Logic.varifyT_global abs_type) T
+                       (Logic.varifyT_global rep_type)
+                   |> aux true avoid of
+                0 => 0
+              | 1 => 1
+              | _ => default_card)
+           | [] => default_card)
+        (* Very slightly unsound: Type variables are assumed not to be
+           constrained to cardinality 1. (In practice, the user would most
+           likely have used "unit" directly anyway.) *)
+      | TFree _ => if default_card = 1 then 2 else default_card
+      | TVar _ => default_card
   in Int.min (max, aux false [] T) end
 
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0
-fun is_type_surely_infinite ctxt infinite_Ts T =
-  tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
+fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
 
 fun monomorphic_term subst =
   map_types (map_type_tvar (fn v =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Jun 17 14:31:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Jun 17 14:35:24 2011 +0200
@@ -141,9 +141,11 @@
   in
     (ths, (0, []))
     |-> fold (fn th => fn (j, rest) =>
-                 (j + 1, ((nth_name j,
-                          if member Thm.eq_thm_prop chained_ths th then Chained
-                          else General), th) :: rest))
+                 (j + 1,
+                  ((nth_name j,
+                    if member Thm.eq_thm_prop chained_ths th then Chained
+                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
+                    else General), th) :: rest))
     |> snd
   end
 
@@ -479,13 +481,13 @@
                         chained_const_irrel_weight (irrel_weight_for fudge) swap
                         const_tab chained_const_tab
 
-fun locality_bonus (_ : relevance_fudge) General = 0.0
-  | locality_bonus {intro_bonus, ...} Intro = intro_bonus
+fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus
   | locality_bonus {elim_bonus, ...} Elim = elim_bonus
   | locality_bonus {simp_bonus, ...} Simp = simp_bonus
   | locality_bonus {local_bonus, ...} Local = local_bonus
   | locality_bonus {assum_bonus, ...} Assum = assum_bonus
   | locality_bonus {chained_bonus, ...} Chained = chained_bonus
+  | locality_bonus _ _ = 0.0
 
 fun is_odd_const_name s =
   s = abs_name orelse String.isPrefix skolem_prefix s orelse
@@ -827,7 +829,10 @@
       if is_chained th then
         Chained
       else if global then
-        Termtab.lookup clasimpset_table (prop_of th) |> the_default General
+        case Termtab.lookup clasimpset_table (prop_of th) of
+          SOME loc => loc
+        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
+                  else General
       else
         if is_assum th then Assum else Local
     fun is_good_unnamed_local th =