--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 01 14:43:57 2014 +0200
@@ -100,9 +100,8 @@
else Local
val may_be_induction =
- exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
- body_type T = @{typ bool}
- | _ => false)
+ exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => body_type T = @{typ bool}
+ | _ => false)
(* TODO: get rid of *)
fun normalize_vars t =
@@ -117,14 +116,12 @@
fun norm (t $ u) = norm t ##>> norm u #>> op $
| norm (Const (s, T)) = normT T #>> curry Const s
- | norm (Var (z as (_, T))) =
- normT T
+ | norm (Var (z as (_, T))) = normT T
#> (fn (T, (accumT, (known, n))) =>
- (case find_index (equal z) known of
- ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
- | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))))
- | norm (Abs (_, T, t)) =
- norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
+ (case find_index (equal z) known of
+ ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
+ | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))))
+ | norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
| norm (Bound j) = pair (Bound j)
| norm (Free (s, T)) = normT T #>> curry Free s
in fst (norm t (([], 0), ([], 0))) end
@@ -162,50 +159,43 @@
fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
- val bracket =
- map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
- |> implode
+ val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args)
fun nth_name j =
(case xref of
Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
- | Facts.Named ((name, _), NONE) =>
- make_name reserved (length ths > 1) (j + 1) name ^ bracket
+ | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>
make_name reserved true
(nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
fun add_nth th (j, rest) =
let val name = nth_name j in
- (j + 1, ((name, stature_of_thm false [] chained css name th), th)
- :: rest)
+ (j + 1, ((name, stature_of_thm false [] chained css name th), th) :: rest)
end
in
(0, []) |> fold add_nth ths |> snd
end
-(* Reject theorems with names like "List.filter.filter_list_def" or
- "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
+(* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as
+ these are definitions arising from packages. *)
fun is_package_def s =
let val ss = Long_Name.explode s in
length ss > 2 andalso not (hd ss = "local") andalso
exists (fn suf => String.isSuffix suf s)
- ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
+ ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
end
(* FIXME: put other record thms here, or declare as "no_atp" *)
fun multi_base_blacklist ctxt ho_atp =
- ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
- "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
- "weak_case_cong", "nat_of_char_simps", "nibble.simps",
+ ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps",
+ "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nat_of_char_simps", "nibble.simps",
"nibble.distinct"]
- |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ?
- append ["induct", "inducts"]
+ |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
|> map (prefix Long_Name.separator)
-(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
- 2007-10-31) was 11. *)
+(* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *)
val max_apply_depth = 18
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
@@ -216,23 +206,20 @@
(* FIXME: Ad hoc list *)
val technical_prefixes =
- ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
- "Limited_Sequence", "Meson", "Metis", "Nitpick",
- "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
+ ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", "Limited_Sequence", "Meson",
+ "Metis", "Nitpick", "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
"Random_Sequence", "Sledgehammer", "SMT"]
|> map (suffix Long_Name.separator)
-fun is_technical_const (s, _) =
- exists (fn pref => String.isPrefix pref s) technical_prefixes
+fun is_technical_const s = exists (fn pref => String.isPrefix pref s) technical_prefixes
(* FIXME: make more reliable *)
val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
-fun is_low_level_class_const (s, _) =
+fun is_low_level_class_const s =
s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
val sep_that = Long_Name.separator ^ Obtain.thatN
-
val skolem_thesis = Name.skolem Auto_Bind.thesisN
fun is_that_fact th =
@@ -258,11 +245,11 @@
| is_interesting_subterm _ = false
fun interest_of_bool t =
- if exists_Const (is_technical_const orf is_low_level_class_const orf
- type_has_top_sort o snd) t then
+ if exists_Const ((is_technical_const o fst) orf (is_low_level_class_const o fst) orf
+ type_has_top_sort o snd) t then
Deal_Breaker
else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse
- not (exists_subterm is_interesting_subterm t) then
+ not (exists_subterm is_interesting_subterm t) then
Boring
else
Interesting
@@ -280,8 +267,7 @@
val t = prop_of th
in
- (interest_of_prop [] t <> Interesting andalso
- not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
+ (interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
is_that_fact th
end
@@ -296,19 +282,18 @@
prefixes of all free variables. In the worse case scenario, where the fact
won't be resolved correctly, the user can fix it manually, e.g., by giving a
name to the offending fact. *)
-fun all_prefixes_of s =
- map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
+fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
fun close_form t =
(t, [] |> Term.add_free_names t |> maps all_prefixes_of)
|> fold (fn ((s, i), T) => fn (t', taken) =>
- let val s' = singleton (Name.variant_list taken) s in
- ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
- else Logic.all_const) T
- $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
- s' :: taken)
- end)
- (Term.add_vars t [] |> sort_wrt (fst o fst))
+ let val s' = singleton (Name.variant_list taken) s in
+ ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
+ else Logic.all_const) T
+ $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
+ s' :: taken)
+ end)
+ (Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
@@ -321,26 +306,23 @@
Termtab.empty
else
let
- fun add stature th =
- Termtab.update (normalize_vars (prop_of th), stature)
+ fun add stature th = Termtab.update (normalize_vars (prop_of th), stature)
- val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
- ctxt |> claset_of |> Classical.rep_cs
+ val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs
val intros = Item_Net.content safeIs @ Item_Net.content hazIs
(* Add once it is used:
- val elims =
- Item_Net.content safeEs @ Item_Net.content hazEs
+ val elims = Item_Net.content safeEs @ Item_Net.content hazEs
|> map Classical.classical_rule
*)
- val specs = ctxt |> Spec_Rules.get
- val (rec_defs, nonrec_defs) =
- specs |> filter (curry (op =) Spec_Rules.Equational o fst)
- |> maps (snd o snd)
- |> filter_out (member Thm.eq_thm_prop risky_defs)
- |> List.partition (is_rec_def o prop_of)
- val spec_intros =
- specs |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
- |> maps (snd o snd)
+ val specs = Spec_Rules.get ctxt
+ val (rec_defs, nonrec_defs) = specs
+ |> filter (curry (op =) Spec_Rules.Equational o fst)
+ |> maps (snd o snd)
+ |> filter_out (member Thm.eq_thm_prop risky_defs)
+ |> List.partition (is_rec_def o prop_of)
+ val spec_intros = specs
+ |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
+ |> maps (snd o snd)
in
Termtab.empty
|> fold (add Simp o snd) simps
@@ -357,7 +339,7 @@
fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 $ t2 $ t1
| normalize_eq (@{const Trueprop} $ (t as @{const Not}
- $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
+ $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
| normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) =
(if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
@@ -397,8 +379,7 @@
fun struct_induct_rule_on th =
(case Logic.strip_horn (prop_of th) of
- (prems, @{const Trueprop}
- $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
+ (prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
if not (is_TVar ind_T) andalso length prems > 1 andalso
exists (exists_subterm (curry (op aconv) p)) prems andalso
not (exists (exists_subterm (curry (op aconv) a)) prems) then
@@ -415,13 +396,14 @@
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
| varify_noninducts t = t
- val p_inst =
- concl_prop |> map_aterms varify_noninducts |> close_form
- |> lambda (Free ind_x)
- |> hackish_string_of_term ctxt
+ val p_inst = concl_prop
+ |> map_aterms varify_noninducts
+ |> close_form
+ |> lambda (Free ind_x)
+ |> hackish_string_of_term ctxt
in
- ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
- stature), th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] [])
+ ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature),
+ th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] [])
end
fun type_match thy (T1, T2) =
@@ -435,7 +417,7 @@
stmt_xs
|> filter (fn (_, T) => type_match thy (T, ind_T))
|> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
- (instantiate_induct_rule ctxt stmt p_name ax)))
+ (instantiate_induct_rule ctxt stmt p_name ax)))
end
| NONE => [ax])
@@ -450,7 +432,9 @@
(hyp_ts |> filter_out (null o external_frees), concl_t)
|> Logic.list_implies |> Object_Logic.atomize_term thy
val ind_stmt_xs = external_frees ind_stmt
- in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
+ in
+ maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
+ end
else
I
@@ -463,10 +447,8 @@
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
val is_too_complex =
- if generous orelse fact_count global_facts >= max_facts_for_complex_check then
- K false
- else
- is_too_complex
+ if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false
+ else is_too_complex
val local_facts = Proof_Context.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static true [global_facts]
val assms = Assumption.all_assms_of ctxt
@@ -478,8 +460,7 @@
val unnamed_locals =
union Thm.eq_thm_prop (Facts.props local_facts) chained
|> filter is_good_unnamed_local |> map (pair "" o single)
- val full_space =
- Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
+ val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
fun add_facts global foldx facts =
@@ -531,12 +512,12 @@
end)) ths (n, accum))
end)
in
- (* The single-theorem names go before the multiple-theorem ones (e.g.,
- "xxx" vs. "xxx(3)"), so that single names are preferred when both are
- available. *)
- `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
- |> add_facts true Facts.fold_static global_facts global_facts
- |> op @
+ (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so
+ that single names are preferred when both are available. *)
+ `I []
+ |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+ |> add_facts true Facts.fold_static global_facts global_facts
+ |> op @
end
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
@@ -544,13 +525,11 @@
[]
else
let
- val chained =
- chained
- |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
+ val chained = chained |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
- o fact_of_ref ctxt reserved chained css) add
+ o fact_of_ref ctxt reserved chained css) add
else
let
val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)