1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Jun 16 11:59:29 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Jun 16 13:50:35 2011 +0200
1.3 @@ -215,7 +215,7 @@
1.4 union (op =) (resolve_fact facts_offset fact_names name)
1.5 | add_fact ctxt _ _ (Inference (_, _, deps)) =
1.6 if AList.defined (op =) deps leo2_ext then
1.7 - insert (op =) (ext_name ctxt, General (* or Chained... *))
1.8 + insert (op =) (ext_name ctxt, Extensionality)
1.9 else
1.10 I
1.11 | add_fact _ _ _ _ = I
2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 16 11:59:29 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 16 13:50:35 2011 +0200
2.3 @@ -40,7 +40,9 @@
2.4 CombVar of name * typ |
2.5 CombApp of combterm * combterm
2.6
2.7 - datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
2.8 + datatype locality =
2.9 + General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
2.10 + Chained
2.11
2.12 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
2.13 datatype type_level =
2.14 @@ -534,7 +536,9 @@
2.15 |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
2.16 | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
2.17
2.18 -datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
2.19 +datatype locality =
2.20 + General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
2.21 + Chained
2.22
2.23 (* (quasi-)underapproximation of the truth *)
2.24 fun is_locality_global Local = false
2.25 @@ -1357,7 +1361,7 @@
2.26 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
2.27 (if needs_fairly_sound then typed_helper_suffix
2.28 else untyped_helper_suffix),
2.29 - General),
2.30 + Helper),
2.31 let val t = th |> prop_of in
2.32 t |> should_specialize_helper type_sys t
2.33 ? (case types of
2.34 @@ -1467,12 +1471,12 @@
2.35 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
2.36 |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
2.37
2.38 -fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
2.39 - | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
2.40 +fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
2.41 + | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
2.42 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
2.43 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
2.44 | is_var_nonmonotonic_in_formula pos phi _ name =
2.45 - formula_fold pos (var_occurs_positively_naked_in_term name) phi false
2.46 + formula_fold pos (is_var_positively_naked_in_term name) phi false
2.47
2.48 fun mk_const_aterm format type_sys x T_args args =
2.49 ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
2.50 @@ -1666,8 +1670,12 @@
2.51 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
2.52 (case level of
2.53 Noninf_Nonmono_Types =>
2.54 + (* Unlike virtually any other polymorphic fact whose type variables can
2.55 + be instantiated by a known infinite type, extensionality actually
2.56 + encodes a cardinality constraints. *)
2.57 not (is_locality_global locality) orelse
2.58 - not (is_type_surely_infinite ctxt known_infinite_types T)
2.59 + not (is_type_surely_infinite ctxt (if locality = Extensionality then []
2.60 + else known_infinite_types) T)
2.61 | Fin_Nonmono_Types => is_type_surely_finite ctxt T
2.62 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
2.63 | add_combterm_nonmonotonic_types _ _ _ _ _ = I
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 16 11:59:29 2011 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 16 13:50:35 2011 +0200
3.3 @@ -141,9 +141,11 @@
3.4 in
3.5 (ths, (0, []))
3.6 |-> fold (fn th => fn (j, rest) =>
3.7 - (j + 1, ((nth_name j,
3.8 - if member Thm.eq_thm_prop chained_ths th then Chained
3.9 - else General), th) :: rest))
3.10 + (j + 1,
3.11 + ((nth_name j,
3.12 + if member Thm.eq_thm_prop chained_ths th then Chained
3.13 + else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
3.14 + else General), th) :: rest))
3.15 |> snd
3.16 end
3.17
3.18 @@ -479,13 +481,13 @@
3.19 chained_const_irrel_weight (irrel_weight_for fudge) swap
3.20 const_tab chained_const_tab
3.21
3.22 -fun locality_bonus (_ : relevance_fudge) General = 0.0
3.23 - | locality_bonus {intro_bonus, ...} Intro = intro_bonus
3.24 +fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus
3.25 | locality_bonus {elim_bonus, ...} Elim = elim_bonus
3.26 | locality_bonus {simp_bonus, ...} Simp = simp_bonus
3.27 | locality_bonus {local_bonus, ...} Local = local_bonus
3.28 | locality_bonus {assum_bonus, ...} Assum = assum_bonus
3.29 | locality_bonus {chained_bonus, ...} Chained = chained_bonus
3.30 + | locality_bonus _ _ = 0.0
3.31
3.32 fun is_odd_const_name s =
3.33 s = abs_name orelse String.isPrefix skolem_prefix s orelse
3.34 @@ -827,7 +829,10 @@
3.35 if is_chained th then
3.36 Chained
3.37 else if global then
3.38 - Termtab.lookup clasimpset_table (prop_of th) |> the_default General
3.39 + case Termtab.lookup clasimpset_table (prop_of th) of
3.40 + SOME loc => loc
3.41 + | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
3.42 + else General
3.43 else
3.44 if is_assum th then Assum else Local
3.45 fun is_good_unnamed_local th =