# HG changeset patch # User wenzelm # Date 1314716526 -7200 # Node ID 426834f253c80ec30fc031bf027a7eb7a676eec1 # Parent 022509c908fb6c38af1588e5fd740f36b5547687# Parent d34ff13371e025b2bcb06a481b781e0fffe2076f merged; diff -r 022509c908fb -r 426834f253c8 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 30 17:02:06 2011 +0200 @@ -39,7 +39,6 @@ "mono_tags", "mono_tags_uniform", "mono_args", - "simple", "poly_guards?", "poly_guards_uniform?", "poly_tags?", @@ -52,7 +51,6 @@ "mono_guards_uniform?", "mono_tags?", "mono_tags_uniform?", - "simple?", "poly_guards!", "poly_guards_uniform!", "poly_tags!", @@ -64,8 +62,7 @@ "mono_guards!", "mono_guards_uniform!", "mono_tags!", - "mono_tags_uniform!", - "simple!"] + "mono_tags_uniform!"] fun metis_exhaust_tac ctxt ths = let diff -r 022509c908fb -r 426834f253c8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 17:02:06 2011 +0200 @@ -416,11 +416,12 @@ let val _ = if is_appropriate_prop concl_t then () else raise Fail "inappropriate" + val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name val facts = - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override - chained_ths hyp_ts concl_t + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp + relevance_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t @@ -575,7 +576,7 @@ relevance_override in if !reconstructor = "sledgehammer_tac" then - sledge_tac 0.25 ATP_Systems.z3_tptpN "simple" + sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple" ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?" ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform" ORELSE' Metis_Tactics.metis_tac [] ctxt thms diff -r 022509c908fb -r 426834f253c8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 17:02:06 2011 +0200 @@ -129,11 +129,12 @@ val relevance_override = {add = [], del = [], only = false} val subgoal = 1 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal + val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val facts = - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r 022509c908fb -r 426834f253c8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 30 17:02:06 2011 +0200 @@ -443,27 +443,24 @@ obtains y where "y \ S" and "y \ T" and "y \ x" using assms unfolding islimpt_def by auto -lemma islimpt_subset: "x islimpt S \ S \ T ==> x islimpt T" by (auto simp add: islimpt_def) +lemma islimpt_iff_eventually: "x islimpt S \ \ eventually (\y. y \ S) (at x)" + unfolding islimpt_def eventually_at_topological by auto + +lemma islimpt_subset: "\x islimpt S; S \ T\ \ x islimpt T" + unfolding islimpt_def by fast lemma islimpt_approachable: fixes x :: "'a::metric_space" shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" - unfolding islimpt_def - apply auto - apply(erule_tac x="ball x e" in allE) - apply auto - apply(rule_tac x=y in bexI) - apply (auto simp add: dist_commute) - apply (simp add: open_dist, drule (1) bspec) - apply (clarify, drule spec, drule (1) mp, auto) - done + unfolding islimpt_iff_eventually eventually_at by fast lemma islimpt_approachable_le: fixes x :: "'a::metric_space" shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x <= e)" unfolding islimpt_approachable - using approachable_lt_le[where f="\x'. dist x' x" and P="\x'. \ (x'\S \ x'\x)"] - by metis + using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", + THEN arg_cong [where f=Not]] + by (simp add: Bex_def conj_commute conj_left_commute) lemma islimpt_UNIV_iff: "x islimpt UNIV \ \ open {x}" unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) @@ -1058,65 +1055,11 @@ using assms by (simp only: at_within_open) lemma Lim_within_LIMSEQ: - fixes a :: real and L :: "'a::metric_space" + fixes a :: "'a::metric_space" assumes "\S. (\n. S n \ a \ S n \ T) \ S ----> a \ (\n. X (S n)) ----> L" shows "(X ---> L) (at a within T)" -proof (rule ccontr) - assume "\ (X ---> L) (at a within T)" - hence "\r>0. \s>0. \x\T. x \ a \ \x - a\ < s \ r \ dist (X x) L" - unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric]) - then obtain r where r: "r > 0" "\s. s > 0 \ \x\T-{a}. \x - a\ < s \ dist (X x) L \ r" by blast - - let ?F = "\n::nat. SOME x. x \ T \ x \ a \ \x - a\ < inverse (real (Suc n)) \ dist (X x) L \ r" - have "\n. \x. x \ T \ x \ a \ \x - a\ < inverse (real (Suc n)) \ dist (X x) L \ r" - using r by (simp add: Bex_def) - hence F: "\n. ?F n \ T \ ?F n \ a \ \?F n - a\ < inverse (real (Suc n)) \ dist (X (?F n)) L \ r" - by (rule someI_ex) - hence F1: "\n. ?F n \ T \ ?F n \ a" - and F2: "\n. \?F n - a\ < inverse (real (Suc n))" - and F3: "\n. dist (X (?F n)) L \ r" - by fast+ - - have "?F ----> a" - proof (rule LIMSEQ_I, unfold real_norm_def) - fix e::real - assume "0 < e" - (* choose no such that inverse (real (Suc n)) < e *) - then have "\no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) - then obtain m where nodef: "inverse (real (Suc m)) < e" by auto - show "\no. \n. no \ n --> \?F n - a\ < e" - proof (intro exI allI impI) - fix n - assume mlen: "m \ n" - have "\?F n - a\ < inverse (real (Suc n))" - by (rule F2) - also have "inverse (real (Suc n)) \ inverse (real (Suc m))" - using mlen by auto - also from nodef have - "inverse (real (Suc m)) < e" . - finally show "\?F n - a\ < e" . - qed - qed - moreover note `\S. (\n. S n \ a \ S n \ T) \ S ----> a \ (\n. X (S n)) ----> L` - ultimately have "(\n. X (?F n)) ----> L" using F1 by simp - - moreover have "\ ((\n. X (?F n)) ----> L)" - proof - - { - fix no::nat - obtain n where "n = no + 1" by simp - then have nolen: "no \ n" by simp - (* We prove this by showing that for any m there is an n\m such that |X (?F n) - L| \ r *) - have "dist (X (?F n)) L \ r" - by (rule F3) - with nolen have "\n. no \ n \ dist (X (?F n)) L \ r" by fast - } - then have "(\no. \n. no \ n \ dist (X (?F n)) L \ r)" by simp - with r have "\e>0. (\no. \n. no \ n \ dist (X (?F n)) L \ e)" by auto - thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less) - qed - ultimately show False by simp -qed + using assms unfolding tendsto_def [where l=L] + by (simp add: sequentially_imp_eventually_within) lemma Lim_right_bound: fixes f :: "real \ real" @@ -1160,21 +1103,18 @@ proof assume ?lhs then obtain f where f:"\y. y>0 \ f y \ S \ f y \ x \ dist (f y) x < y" - unfolding islimpt_approachable using choice[of "\e y. e>0 \ y\S \ y\x \ dist y x < e"] by auto - { fix n::nat - have "f (inverse (real n + 1)) \ S - {x}" using f by auto - } - moreover - { fix e::real assume "e>0" - hence "\N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n - 1" in exI) by auto - then obtain N::nat where "inverse (real (N + 1)) < e" by auto - hence "\n\N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero) - moreover have "\n\N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto - ultimately have "\N::nat. \n\N. dist (f (inverse (real n + 1))) x < e" apply(rule_tac x=N in exI) apply auto apply(erule_tac x=n in allE)+ by auto - } - hence " ((\n. f (inverse (real n + 1))) ---> x) sequentially" - unfolding Lim_sequentially using f by auto - ultimately show ?rhs apply (rule_tac x="(\n::nat. f (inverse (real n + 1)))" in exI) by auto + unfolding islimpt_approachable + using choice[of "\e y. e>0 \ y\S \ y\x \ dist y x < e"] by auto + let ?I = "\n. inverse (real (Suc n))" + have "\n. f (?I n) \ S - {x}" using f by simp + moreover have "(\n. f (?I n)) ----> x" + proof (rule metric_tendsto_imp_tendsto) + show "?I ----> 0" + by (rule LIMSEQ_inverse_real_of_nat) + show "eventually (\n. dist (f (?I n)) x \ dist (?I n) 0) sequentially" + by (simp add: norm_conv_dist [symmetric] less_imp_le f) + qed + ultimately show ?rhs by fast next assume ?rhs then obtain f::"nat\'a" where f:"(\n. f n \ S - {x})" "(\e>0. \N. \n\N. dist (f n) x < e)" unfolding Lim_sequentially by auto @@ -1331,7 +1271,7 @@ shows "netlimit (at a) = a" apply (subst within_UNIV[symmetric]) using netlimit_within[of a UNIV] - by (simp add: trivial_limit_at within_UNIV) + by (simp add: within_UNIV) lemma lim_within_interior: "x \ interior S \ (f ---> l) (at x within S) \ (f ---> l) (at x)" @@ -1480,8 +1420,7 @@ lemma seq_offset: assumes "(f ---> l) sequentially" shows "((\i. f (i + k)) ---> l) sequentially" - using assms unfolding tendsto_def - by clarify (rule sequentially_offset, simp) + using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *) lemma seq_offset_neg: "(f ---> l) sequentially ==> ((\i. f(i - k)) ---> l) sequentially" @@ -1494,21 +1433,10 @@ lemma seq_offset_rev: "((\i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially" - apply (rule topological_tendstoI) - apply (drule (2) topological_tendstoD) - apply (simp only: eventually_sequentially) - apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k \ (n - k) + k = n") - by metis arith + by (rule LIMSEQ_offset) (* FIXME: redundant *) lemma seq_harmonic: "((\n. inverse (real n)) ---> 0) sequentially" -proof- - { fix e::real assume "e>0" - hence "\N::nat. \n::nat\N. inverse (real n) < e" - using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI) - by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7)) - } - thus ?thesis unfolding Lim_sequentially dist_norm by simp -qed + using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) subsection {* More properties of closed balls *} @@ -3154,7 +3082,7 @@ lemma continuous_within_eps_delta: "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" unfolding continuous_within and Lim_within - apply auto unfolding dist_nz[THEN sym] apply(auto elim!:allE) apply(rule_tac x=d in exI) by auto + apply auto unfolding dist_nz[THEN sym] apply(auto del: allE elim!:allE) apply(rule_tac x=d in exI) by auto lemma continuous_at_eps_delta: "continuous (at x) f \ (\e>0. \d>0. \x'. dist x' x < d --> dist(f x')(f x) < e)" @@ -4408,7 +4336,7 @@ note * = this { fix x y assume "x\s" "y\s" hence "s \ {}" by auto have "norm(x - y) \ diameter s" unfolding diameter_def using `s\{}` *[OF `x\s` `y\s`] `x\s` `y\s` - by simp (blast intro!: Sup_upper *) } + by simp (blast del: Sup_upper intro!: * Sup_upper) } moreover { fix d::real assume "d>0" "d < diameter s" hence "s\{}" unfolding diameter_def by auto @@ -4667,39 +4595,26 @@ "{a <..< b} \ {} \ (\ii c$$i \ d$$i \ b$$i) \ {c .. d} \ {a .. b}" and "(\i d$$i < b$$i) \ {c .. d} \ {a<..i c$$i \ d$$i \ b$$i) \ {c<.. {a .. b}" and "(\i c$$i \ d$$i \ b$$i) \ {c<.. {a<.. {a .. b}" -proof(simp add: subset_eq, rule) - fix x - assume x:"x \{a<.. x $$ i" - using x order_less_imp_le[of "a$$i" "x$$i"] - by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) - } - moreover - { fix i assume "i b $$ i" - using x order_less_imp_le[of "x$$i" "b$$i"] - by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) - } - ultimately - show "a \ x \ x \ b" - by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) -qed + unfolding subset_eq[unfolded Ball_def] unfolding mem_interval + by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+ + +lemma interval_open_subset_closed: + fixes a :: "'a::ordered_euclidean_space" + shows "{a<.. {a .. b}" + unfolding subset_eq [unfolded Ball_def] mem_interval + by (fast intro: less_imp_le) lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows "{c .. d} \ {a .. b} \ (\i d$$i) --> (\i c$$i \ d$$i \ b$$i)" (is ?th1) and @@ -4825,7 +4740,7 @@ "(x + (e / 2) *\<^sub>R basis i) $$ i \ b $$ i" using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]] and e[THEN spec[where x="x + (e/2) *\<^sub>R basis i"]] - unfolding mem_interval by (auto elim!: allE[where x=i]) + unfolding mem_interval using i by blast+ hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps unfolding basis_component using `e>0` i by auto } hence "x \ {a<..x y z::real. x < y \ y < z \ x < z" by auto show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff - by(meson order_trans le_less_trans less_le_trans *)+ qed + by(meson order_trans le_less_trans less_le_trans less_trans)+ qed lemma is_interval_empty: "is_interval {}" diff -r 022509c908fb -r 426834f253c8 src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/TPTP/atp_export.ML Tue Aug 30 17:02:06 2011 +0200 @@ -27,8 +27,9 @@ val fact_name_of = prefix fact_prefix o ascii_of fun facts_of thy = - Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty - true [] [] + Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) + false(*FIXME works only for first-order*) + Symtab.empty true [] [] |> filter (curry (op =) @{typ bool} o fastype_of o Object_Logic.atomize_term thy o prop_of o snd) diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 17:02:06 2011 +0200 @@ -17,16 +17,20 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c - datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type + datatype 'a ho_type = + AType of 'a * 'a ho_type list | + AFun of 'a ho_type * 'a ho_type | + ATyAbs of 'a list * 'a ho_type - datatype tff_flavor = Implicit | Explicit - datatype thf_flavor = Without_Choice | With_Choice + datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic + datatype tff_explicitness = TFF_Implicit | TFF_Explicit + datatype thf_flavor = THF_Without_Choice | THF_With_Choice datatype format = CNF | CNF_UEQ | FOF | - TFF of tff_flavor | - THF of thf_flavor + TFF of tff_polymorphism * tff_explicitness | + THF0 of thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -70,6 +74,9 @@ val is_built_in_tptp_symbol : string -> bool val is_tptp_variable : string -> bool val is_tptp_user_symbol : string -> bool + val atype_of_types : (string * string) ho_type + val bool_atype : (string * string) ho_type + val individual_atype : (string * string) ho_type val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula val mk_aconn : connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula @@ -117,17 +124,21 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c -datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type +datatype 'a ho_type = + AType of 'a * 'a ho_type list | + AFun of 'a ho_type * 'a ho_type | + ATyAbs of 'a list * 'a ho_type -datatype tff_flavor = Implicit | Explicit -datatype thf_flavor = Without_Choice | With_Choice +datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic +datatype tff_explicitness = TFF_Implicit | TFF_Explicit +datatype thf_flavor = THF_Without_Choice | THF_With_Choice datatype format = CNF | CNF_UEQ | FOF | - TFF of tff_flavor | - THF of thf_flavor + TFF of tff_polymorphism * tff_explicitness | + THF0 of thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -211,10 +222,10 @@ | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) -fun is_format_thf (THF _) = true +fun is_format_thf (THF0 _) = true | is_format_thf _ = false fun is_format_typed (TFF _) = true - | is_format_typed (THF _) = true + | is_format_typed (THF0 _) = true | is_format_typed _ = false fun string_for_kind Axiom = "axiom" @@ -223,25 +234,38 @@ | string_for_kind Hypothesis = "hypothesis" | string_for_kind Conjecture = "conjecture" -fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s - | strip_tff_type (AFun (AFun _, _)) = +fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty) + | flatten_type (ty as AFun (ty1 as AType _, ty2)) = + (case flatten_type ty2 of + AFun (ty' as AType (s, tys), ty) => + AFun (AType (tptp_product_type, + ty1 :: (if s = tptp_product_type then tys else [ty'])), ty) + | _ => ty) + | flatten_type (ty as AType _) = ty + | flatten_type _ = raise Fail "unexpected higher-order type in first-order format" - | strip_tff_type (AType s) = ([], s) -fun string_for_type (THF _) ty = - let - fun aux _ (AType s) = s - | aux rhs (AFun (ty1, ty2)) = - aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2 - |> not rhs ? enclose "(" ")" - in aux true ty end - | string_for_type (TFF _) ty = - (case strip_tff_type ty of - ([], s) => s - | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s - | (ss, s) => - "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^ - tptp_fun_type ^ " " ^ s) +fun str_for_type ty = + let + fun str _ (AType (s, [])) = s + | str _ (AType (s, tys)) = + tys |> map (str false) + |> (if s = tptp_product_type then + space_implode (" " ^ tptp_product_type ^ " ") + #> length tys > 1 ? enclose "(" ")" + else + commas #> enclose "(" ")" #> prefix s) + | str rhs (AFun (ty1, ty2)) = + str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2 + |> not rhs ? enclose "(" ")" + | str _ (ATyAbs (ss, ty)) = + tptp_forall ^ "[" ^ + commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)) + ss) ^ "] : " ^ str false ty + in str true ty end + +fun string_for_type (THF0 _) ty = str_for_type ty + | string_for_type (TFF _) ty = str_for_type (flatten_type ty) | string_for_type _ _ = raise Fail "unexpected type in untyped format" fun string_for_quantifier AForall = tptp_forall @@ -254,11 +278,13 @@ | string_for_connective AIff = tptp_iff fun string_for_bound_var format (s, ty) = - s ^ (if is_format_typed format then - " " ^ tptp_has_type ^ " " ^ - string_for_type format (ty |> the_default (AType tptp_individual_type)) - else - "") + s ^ + (if is_format_typed format then + " " ^ tptp_has_type ^ " " ^ + (ty |> the_default (AType (tptp_individual_type, [])) + |> string_for_type format) + else + "") fun string_for_term _ (ATerm (s, [])) = s | string_for_term format (ATerm (s, ts)) = @@ -270,7 +296,7 @@ |> is_format_thf format ? enclose "(" ")" else (case (s = tptp_ho_forall orelse s = tptp_ho_exists, - s = tptp_choice andalso format = THF With_Choice, ts) of + s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of (true, _, [AAbs ((s', ty), tm)]) => (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work around LEO-II 1.2.8 parser limitation. *) @@ -291,7 +317,7 @@ else s ^ "(" ^ commas ss ^ ")" end) - | string_for_term (format as THF _) (AAbs ((s, ty), tm)) = + | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) = "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^ string_for_term format tm ^ ")" | string_for_term _ _ = raise Fail "unexpected term in first-order format" @@ -324,7 +350,7 @@ | string_for_format CNF_UEQ = tptp_cnf | string_for_format FOF = tptp_fof | string_for_format (TFF _) = tptp_tff - | string_for_format (THF _) = tptp_thf + | string_for_format (THF0 _) = tptp_thf fun string_for_problem_line format (Decl (ident, sym, ty)) = string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ @@ -438,9 +464,9 @@ symbols (with "$i" as the type of individuals), but some provers (e.g., SNARK) require explicit declarations. The situation is similar for THF. *) -val atype_of_types = AType (`I tptp_type_of_types) -val bool_atype = AType (`I tptp_bool_type) -val individual_atype = AType (`I tptp_individual_type) +val atype_of_types = AType (`I tptp_type_of_types, []) +val bool_atype = AType (`I tptp_bool_type, []) +val individual_atype = AType (`I tptp_individual_type, []) fun default_type pred_sym = let @@ -457,8 +483,10 @@ let fun do_sym name ty = if member (op =) declared name then I else AList.default (op =) (name, ty) - fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2] - | do_type (AType name) = do_sym name (K atype_of_types) + fun do_type_name name = do_sym name (K atype_of_types) + fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys + | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 + | do_type (ATyAbs (names, ty)) = fold do_type_name names #> do_type ty fun do_term pred_sym (ATerm (name as (s, _), tms)) = is_tptp_user_symbol s ? do_sym name (fn _ => default_type pred_sym (length tms)) @@ -555,8 +583,11 @@ end in add 0 |> apsnd SOME end -fun nice_type (AType name) = nice_name name #>> AType +fun nice_type (AType (name, tys)) = + nice_name name ##>> pool_map nice_type tys #>> AType | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun + | nice_type (ATyAbs (names, ty)) = + pool_map nice_name names ##>> nice_type ty #>> ATyAbs fun nice_term (ATerm (name, ts)) = nice_name name ##>> pool_map nice_term ts #>> ATerm | nice_term (AAbs ((name, ty), tm)) = diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 17:02:06 2011 +0200 @@ -37,13 +37,14 @@ val e_sym_offs_weight_base : real Config.T val e_sym_offs_weight_span : real Config.T val eN : string + val e_sineN : string + val e_tofofN : string + val leo2N : string + val pffN : string + val satallaxN : string + val snarkN : string val spassN : string val vampireN : string - val leo2N : string - val satallaxN : string - val e_sineN : string - val snarkN : string - val e_tofofN : string val waldmeisterN : string val z3_tptpN : string val remote_prefix : string @@ -100,15 +101,16 @@ (* named ATPs *) val eN = "e" +val e_sineN = "e_sine" +val e_tofofN = "e_tofof" val leo2N = "leo2" +val pffN = "pff" val satallaxN = "satallax" +val snarkN = "snark" val spassN = "spass" val vampireN = "vampire" +val waldmeisterN = "waldmeister" val z3_tptpN = "z3_tptp" -val e_sineN = "e_sine" -val snarkN = "snark" -val e_tofofN = "e_tofof" -val waldmeisterN = "waldmeister" val remote_prefix = "remote_" structure Data = Theory_Data @@ -241,8 +243,10 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))), - (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))] + [(0.667, (false, (150, THF0 THF_Without_Choice, + "mono_simple_higher", sosN))), + (0.333, (true, (50, THF0 THF_Without_Choice, + "mono_simple_higher", no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -262,7 +266,8 @@ conj_sym_kind = Axiom, prem_kind = Hypothesis, best_slices = - K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)} + K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))] + (* FUDGE *)} val satallax = (satallaxN, satallax_config) @@ -309,6 +314,8 @@ fun is_old_vampire_version () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER +val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit) + val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], @@ -340,9 +347,9 @@ (0.333, (false, (500, FOF, "mono_tags?", sosN))), (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))] else - [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))), - (0.333, (false, (500, TFF Implicit, "simple", sosN))), - (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))]) + [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))), + (0.333, (false, (500, vampire_tff, "mono_simple", sosN))), + (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -351,6 +358,8 @@ (* Z3 with TPTP syntax *) +val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit) + val z3_tptp_config : atp_config = {exec = ("Z3_HOME", "z3"), required_execs = [], @@ -368,20 +377,37 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, (250, FOF, "mono_guards?", ""))), - (0.25, (false, (125, FOF, "mono_guards?", ""))), - (0.125, (false, (62, TFF Implicit, "simple", ""))), - (0.125, (false, (31, TFF Implicit, "simple", "")))]} + K [(0.5, (false, (250, z3_tff, "mono_simple", ""))), + (0.25, (false, (125, z3_tff, "mono_simple", ""))), + (0.125, (false, (62, z3_tff, "mono_simple", ""))), + (0.125, (false, (31, z3_tff, "mono_simple", "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) +(* Not really a prover: Experimental PFF (Polymorphic TFF) output *) + +val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit) + +val pff_config : atp_config = + {exec = ("ISABELLE_ATP", "scripts/dummy_atp"), + required_execs = [], + arguments = K (K (K (K (K "")))), + proof_delims = [], + known_failures = [(GaveUp, "SZS status Unknown")], + conj_sym_kind = Hypothesis, + prem_kind = Hypothesis, + best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]} + +val pff = (pffN, pff_config) + (* Remote ATP invocation via SystemOnTPTP *) val systems = Synchronized.var "atp_systems" ([] : string list) fun get_systems () = - case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of + case Isabelle_System.bash_output + "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of (output, 0) => split_lines output | (output, _) => error (case extract_known_failure known_perl_failures output of @@ -449,31 +475,34 @@ (remote_prefix ^ name, remotify_config system_name system_versions best_slice config) +val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit) + val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] (K (750, FOF, "mono_tags?") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, THF Without_Choice, "simple_higher") (* FUDGE *)) + (K (100, THF0 THF_Without_Choice, + "mono_simple_higher") (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, THF With_Choice, "simple_higher") (* FUDGE *)) + (K (100, THF0 THF_With_Choice, + "mono_simple_higher") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] - (K (250, TFF Implicit, "simple") (* FUDGE *)) + (K (250, FOF, "mono_guards?") (* FUDGE *)) val remote_z3_tptp = - remotify_atp z3_tptp "Z3" ["3.0"] - (K (250, TFF Implicit, "simple") (* FUDGE *)) + remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, TFF Explicit, "simple") (* FUDGE *)) + (K (100, dumb_tff, "mono_simple") (* FUDGE *)) val remote_e_tofof = - remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *)) + remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom + Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] @@ -503,7 +532,7 @@ Synchronized.change systems (fn _ => get_systems ()) val atps = - [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, + [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark, remote_e_tofof, remote_waldmeister] val setup = fold add_atp atps diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 17:02:06 2011 +0200 @@ -16,8 +16,8 @@ type 'a problem = 'a ATP_Problem.problem datatype locality = - General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | - Chained + General | Helper | Induction | Extensionality | Intro | Elim | Simp | + Local | Assum | Chained datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic @@ -31,7 +31,7 @@ datatype type_uniformity = Uniform | Nonuniform datatype type_enc = - Simple_Types of order * type_level | + Simple_Types of order * polymorphism * type_level | Guards of polymorphism * type_level * type_uniformity | Tags of polymorphism * type_level * type_uniformity @@ -311,14 +311,19 @@ fun make_fixed_var x = fixed_var_prefix ^ ascii_of x fun make_schematic_type_var (x, i) = - tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) + tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) -(* "HOL.eq" is mapped to the ATP's equality. *) -fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal - | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) = - tptp_choice - | make_fixed_const _ c = const_prefix ^ lookup_const c +(* "HOL.eq" and Choice are mapped to the ATP's equivalents *) +local + val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT + fun default c = const_prefix ^ lookup_const c +in + fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal + | make_fixed_const (SOME (THF0 THF_With_Choice)) c = + if c = choice_const then tptp_choice else default c + | make_fixed_const _ c = default c +end fun make_fixed_type_const c = type_const_prefix ^ lookup_const c @@ -367,9 +372,6 @@ TConsLit of name * name * name list | TVarLit of name * name -fun gen_TVars 0 = [] - | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1) - val type_class = the_single @{sort type} fun add_packed_sort tvar = @@ -383,13 +385,12 @@ (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *) fun make_axiom_arity_clause (tcons, name, (cls, args)) = let - val tvars = gen_TVars (length args) + val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args) val tvars_srts = ListPair.zip (tvars, args) in {name = name, prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit, - concl_lits = TConsLit (`make_type_class cls, - `make_fixed_type_const tcons, + concl_lits = TConsLit (`make_type_class cls, `make_fixed_type_const tcons, tvars ~~ tvars)} end @@ -490,6 +491,15 @@ [new_skolem_const_prefix, s, string_of_int num_T_args] |> space_implode Long_Name.separator +fun robust_const_type thy s = + if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"} + else s |> Sign.the_const_type thy + +(* This function only makes sense if "T" is as general as possible. *) +fun robust_const_typargs thy (s, T) = + (s, T) |> Sign.const_typargs thy + handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar + (* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort infomation. *) fun iterm_from_term thy format bs (P $ Q) = @@ -499,10 +509,7 @@ in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end | iterm_from_term thy format _ (Const (c, T)) = (IConst (`(make_fixed_const (SOME format)) c, T, - if String.isPrefix old_skolem_const_prefix c then - [] |> Term.add_tvarsT T |> map TVar - else - (c, T) |> Sign.const_typargs thy), + robust_const_typargs thy (c, T)), atyps_of T) | iterm_from_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, @@ -527,8 +534,8 @@ in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end datatype locality = - General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | - Chained + General | Helper | Induction | Extensionality | Intro | Elim | Simp | + Local | Assum | Chained datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic @@ -542,7 +549,7 @@ datatype type_uniformity = Uniform | Nonuniform datatype type_enc = - Simple_Types of order * type_level | + Simple_Types of order * polymorphism * type_level | Guards of polymorphism * type_level * type_uniformity | Tags of polymorphism * type_level * type_uniformity @@ -574,12 +581,15 @@ | NONE => (Nonuniform, s)) |> (fn (poly, (level, (uniformity, core))) => case (core, (poly, level, uniformity)) of - ("simple", (NONE, _, Nonuniform)) => - Simple_Types (First_Order, level) - | ("simple_higher", (NONE, _, Nonuniform)) => - (case level of - Noninf_Nonmono_Types _ => raise Same.SAME - | _ => Simple_Types (Higher_Order, level)) + ("simple", (SOME poly, _, Nonuniform)) => + (case poly of + Raw_Monomorphic => raise Same.SAME + | _ => Simple_Types (First_Order, poly, level)) + | ("simple_higher", (SOME poly, _, Nonuniform)) => + (case (poly, level) of + (Raw_Monomorphic, _) => raise Same.SAME + | (_, Noninf_Nonmono_Types _) => raise Same.SAME + | _ => Simple_Types (Higher_Order, poly, level)) | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity) | ("tags", (SOME Polymorphic, _, _)) => Tags (Polymorphic, level, uniformity) @@ -591,14 +601,14 @@ | _ => raise Same.SAME) handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") -fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true | is_type_enc_higher_order _ = false -fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic +fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly | polymorphism_of_type_enc (Guards (poly, _, _)) = poly | polymorphism_of_type_enc (Tags (poly, _, _)) = poly -fun level_of_type_enc (Simple_Types (_, level)) = level +fun level_of_type_enc (Simple_Types (_, _, level)) = level | level_of_type_enc (Guards (_, level, _)) = level | level_of_type_enc (Tags (_, level, _)) = level @@ -620,11 +630,15 @@ | is_type_level_monotonicity_based Fin_Nonmono_Types = true | is_type_level_monotonicity_based _ = false -fun adjust_type_enc (THF _) type_enc = type_enc - | adjust_type_enc (TFF _) (Simple_Types (_, level)) = - Simple_Types (First_Order, level) - | adjust_type_enc format (Simple_Types (_, level)) = - adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform)) +fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) = + Simple_Types (order, Mangled_Monomorphic, level) + | adjust_type_enc (THF0 _) type_enc = type_enc + | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) = + Simple_Types (First_Order, Mangled_Monomorphic, level) + | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) = + Simple_Types (First_Order, poly, level) + | adjust_type_enc format (Simple_Types (_, poly, level)) = + adjust_type_enc format (Guards (poly, level, Uniform)) | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff | adjust_type_enc _ type_enc = type_enc @@ -678,8 +692,7 @@ Mangled_Type_Args of bool | No_Type_Args -fun should_drop_arg_type_args (Simple_Types _) = - false (* since TFF doesn't support overloading *) +fun should_drop_arg_type_args (Simple_Types _) = false | should_drop_arg_type_args type_enc = level_of_type_enc type_enc = All_Types andalso uniformity_of_type_enc type_enc = Uniform @@ -751,14 +764,28 @@ | iterm_vars (IAbs (_, tm)) = iterm_vars tm fun close_iformula_universally phi = close_universally iterm_vars phi -fun term_vars bounds (ATerm (name as (s, _), tms)) = - (is_tptp_variable s andalso not (member (op =) bounds name)) - ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms - | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm -fun close_formula_universally phi = close_universally (term_vars []) phi +fun term_vars type_enc = + let + fun vars bounds (ATerm (name as (s, _), tms)) = + (if is_tptp_variable s andalso not (member (op =) bounds name) then + (case type_enc of + Simple_Types (_, Polymorphic, _) => + if String.isPrefix tvar_prefix s then SOME atype_of_types + else NONE + | _ => NONE) + |> pair name |> insert (op =) + else + I) + #> fold (vars bounds) tms + | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm + in vars end +fun close_formula_universally type_enc = + close_universally (term_vars type_enc []) -val homo_infinite_type_name = @{type_name ind} (* any infinite type *) -val homo_infinite_type = Type (homo_infinite_type_name, []) +val fused_infinite_type_name = @{type_name ind} (* any infinite type *) +val fused_infinite_type = Type (fused_infinite_type_name, []) + +fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s) fun ho_term_from_typ format type_enc = let @@ -766,15 +793,14 @@ ATerm (case (is_type_enc_higher_order type_enc, s) of (true, @{type_name bool}) => `I tptp_bool_type | (true, @{type_name fun}) => `I tptp_fun_type - | _ => if s = homo_infinite_type_name andalso + | _ => if s = fused_infinite_type_name andalso is_format_typed format then `I tptp_individual_type else `make_fixed_type_const s, map term Ts) | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) - | term (TVar ((x as (s, _)), _)) = - ATerm ((make_schematic_type_var x, s), []) + | term (TVar (x, _)) = ATerm (tvar_name x, []) in term end fun ho_term_for_type_arg format type_enc T = @@ -792,8 +818,6 @@ fun mangled_type format type_enc = generic_mangled_type_name fst o ho_term_from_typ format type_enc -val bool_atype = AType (`I tptp_bool_type) - fun make_simple_type s = if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then @@ -803,9 +827,14 @@ fun ho_type_from_ho_term type_enc pred_sym ary = let - fun to_atype ty = + fun to_mangled_atype ty = AType ((make_simple_type (generic_mangled_type_name fst ty), - generic_mangled_type_name snd ty)) + generic_mangled_type_name snd ty), []) + fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys) + | to_poly_atype _ = raise Fail "unexpected type abstraction" + val to_atype = + if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype + else to_mangled_atype fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys @@ -884,19 +913,17 @@ if is_tptp_equal s andalso length args = 2 then IConst (`I tptp_equal, T, []) else - (* Use a proxy even for partially applied THF equality, because - the LEO-II and Satallax parsers complain about not being - able to infer the type of "=". *) + (* Use a proxy even for partially applied THF0 equality, + because the LEO-II and Satallax parsers complain about not + being able to infer the type of "=". *) IConst (proxy_base |>> prefix const_prefix, T, T_args) | _ => IConst (name, T, []) else IConst (proxy_base |>> prefix const_prefix, T, T_args) | NONE => if s = tptp_choice then - (*this could be made neater by adding c_Eps as a proxy, - but we'd need to be able to "see" Hilbert_Choice.Eps - at this level in order to define fEps*) tweak_ho_quant tptp_choice T args - else IConst (name, T, T_args)) + else + IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end @@ -1148,14 +1175,14 @@ | _ => false) | should_tag_with_type _ _ _ _ _ _ = false -fun homogenized_type ctxt mono level = +fun fused_type ctxt mono level = let val should_encode = should_encode_type ctxt mono level - fun homo 0 T = if should_encode T then T else homo_infinite_type - | homo ary (Type (@{type_name fun}, [T1, T2])) = - homo 0 T1 --> homo (ary - 1) T2 - | homo _ _ = raise Fail "expected function type" - in homo end + fun fuse 0 T = if should_encode T then T else fused_infinite_type + | fuse ary (Type (@{type_name fun}, [T1, T2])) = + fuse 0 T1 --> fuse (ary - 1) T2 + | fuse _ _ = raise Fail "expected function type" + in fuse end (** predicators and application operators **) @@ -1332,13 +1359,7 @@ fun filter_type_args _ _ _ [] = [] | filter_type_args thy s arity T_args = - let - (* will throw "TYPE" for pseudo-constants *) - val U = if s = app_op_name then - @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global - else - s |> Sign.the_const_type thy - in + let val U = robust_const_type thy s in case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of [] => [] | res_U_vars => @@ -1444,7 +1465,7 @@ (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) else AAtom (ATerm (`I tptp_equal, [tm1, tm2]))) |> bound_tvars type_enc atomic_Ts - |> close_formula_universally + |> close_formula_universally type_enc val type_tag = `(make_fixed_const NONE) type_tag_name @@ -1589,8 +1610,8 @@ else make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers in - (fact_names |> map single, - (conjs, facts @ lambdas, class_rel_clauses, arity_clauses)) + (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas, + class_rel_clauses, arity_clauses) end val type_guard = `(make_fixed_const NONE) type_guard_name @@ -1659,8 +1680,7 @@ val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level val do_bound_type = case type_enc of - Simple_Types (_, level) => - homogenized_type ctxt mono level 0 + Simple_Types (_, _, level) => fused_type ctxt mono level 0 #> ho_type_from_typ format type_enc false 0 #> SOME | _ => K NONE fun do_out_of_bound_type pos phi universal (name, T) = @@ -1707,7 +1727,7 @@ should_guard_var_in_formula (if pos then SOME true else NONE) |> bound_tvars type_enc atomic_types - |> close_formula_universally, + |> close_formula_universally type_enc, NONE, case locality of Intro => isabelle_info introN @@ -1716,13 +1736,13 @@ | _ => NONE) |> Formula -fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...} - : class_rel_clause) = - let val ty_arg = ATerm (`I "T", []) in +fun formula_line_for_class_rel_clause type_enc + ({name, subclass, superclass, ...} : class_rel_clause) = + let val ty_arg = ATerm ((make_schematic_type_var ("'a", 0), "'a"), []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), AAtom (ATerm (superclass, [ty_arg]))]) - |> close_formula_universally, isabelle_info introN, NONE) + |> close_formula_universally type_enc, isabelle_info introN, NONE) end fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = @@ -1730,14 +1750,14 @@ | fo_literal_from_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...} - : arity_clause) = +fun formula_line_for_arity_clause type_enc + ({name, prem_lits, concl_lits, ...} : arity_clause) = Formula (arity_clause_prefix ^ name, Axiom, mk_ahorn (map (formula_from_fo_literal o apfst not o fo_literal_from_arity_literal) prem_lits) (formula_from_fo_literal (fo_literal_from_arity_literal concl_lits)) - |> close_formula_universally, isabelle_info introN, NONE) + |> close_formula_universally type_enc, isabelle_info introN, NONE) fun formula_line_for_conjecture ctxt format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -1746,7 +1766,7 @@ should_guard_var_in_formula (SOME false) (close_iformula_universally iformula) |> bound_tvars type_enc atomic_types - |> close_formula_universally, NONE, NONE) + |> close_formula_universally type_enc, NONE, NONE) fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) = atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree @@ -1763,11 +1783,15 @@ (** Symbol declarations **) -fun should_declare_sym type_enc pred_sym s = - (case type_enc of - Guards _ => not pred_sym - | _ => true) andalso - is_tptp_user_symbol s +fun decl_line_for_class s = + let val name as (s, _) = `make_type_class s in + Decl (sym_decl_prefix ^ s, name, AFun (atype_of_types, bool_atype)) + end + +fun decl_lines_for_classes type_enc classes = + case type_enc of + Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes + | _ => [] fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab (conjs, facts) = @@ -1776,8 +1800,15 @@ let val (head, args) = strip_iterm_comb tm in (case head of IConst ((s, s'), T, T_args) => - let val pred_sym = is_pred_sym repaired_sym_tab s in - if should_declare_sym type_enc pred_sym s then + let + val pred_sym = is_pred_sym repaired_sym_tab s + val decl_sym = + (case type_enc of + Guards _ => not pred_sym + | _ => true) andalso + is_tptp_user_symbol s + in + if decl_sym then Symtab.map_default (s, []) (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, in_conj)) @@ -1911,7 +1942,7 @@ |> formula_from_iformula ctxt format mono type_enc (K (K (K (K true)))) (SOME true) |> bound_tvars type_enc (atyps_of T) - |> close_formula_universally, + |> close_formula_universally type_enc, isabelle_info introN, NONE) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = @@ -1935,14 +1966,28 @@ fun decl_line_for_sym ctxt format mono type_enc s (s', T_args, T, pred_sym, ary, _) = let - val (T_arg_Ts, level) = - case type_enc of - Simple_Types (_, level) => ([], level) - | _ => (replicate (length T_args) homo_infinite_type, No_Types) + val thy = Proof_Context.theory_of ctxt + val (T, T_args) = + if null T_args then + (T, []) + else case strip_prefix_and_unascii const_prefix s of + SOME s' => + let + val s' = s' |> invert_const + val T = s' |> robust_const_type thy + in (T, robust_const_typargs thy (s', T)) end + | NONE => + case strip_prefix_and_unascii fixed_var_prefix s of + SOME s' => + if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a]) + else raise Fail "unexpected type arguments to free variable" + | NONE => raise Fail "unexpected type arguments" in Decl (sym_decl_prefix ^ s, (s, s'), - (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary)) - |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary)) + T |> fused_type ctxt mono (level_of_type_enc type_enc) ary + |> ho_type_from_typ format type_enc pred_sym ary + |> not (null T_args) + ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args)) end fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s @@ -1973,7 +2018,7 @@ |> formula_from_iformula ctxt format mono type_enc (K (K (K (K true)))) (SOME true) |> n > 1 ? bound_tvars type_enc (atyps_of T) - |> close_formula_universally + |> close_formula_universally type_enc |> maybe_negate, isabelle_info introN, NONE) end @@ -2127,7 +2172,7 @@ else error ("Unknown lambda translation method: " ^ quote lambda_trans ^ ".") - val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = + val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) = translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply @@ -2142,6 +2187,7 @@ val mono_Ts = helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc + val class_decl_lines = decl_lines_for_classes type_enc classes val sym_decl_lines = (conjs, helpers @ facts) |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab @@ -2158,14 +2204,14 @@ (* Reordering these might confuse the proof reconstruction code or the SPASS FLOTTER hack. *) val problem = - [(explicit_declsN, sym_decl_lines), + [(explicit_declsN, class_decl_lines @ sym_decl_lines), (factsN, map (formula_line_for_fact ctxt format fact_prefix ascii_of - (not exporter) (not exporter) mono - type_enc) + (not exporter) (not exporter) mono type_enc) (0 upto length facts - 1 ~~ facts)), - (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), - (aritiesN, map formula_line_for_arity_clause arity_clauses), + (class_relsN, + map (formula_line_for_class_rel_clause type_enc) class_rel_clauses), + (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses), (helpersN, helper_lines), (conjsN, map (formula_line_for_conjecture ctxt format mono type_enc) conjs), @@ -2175,12 +2221,10 @@ |> (case format of CNF => ensure_cnf_problem | CNF_UEQ => filter_cnf_ueq_problem - | _ => I) - |> (if is_format_typed format andalso format <> TFF Implicit then - declare_undeclared_syms_in_atp_problem type_decl_prefix - implicit_declsN - else - I) + | FOF => I + | TFF (_, TFF_Implicit) => I + | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix + implicit_declsN) val (problem, pool) = problem |> nice_atp_problem readable_names val helpers_offset = offset_of_heading_in_problem helpersN problem 0 val typed_helpers = diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/ATP/scripts/dummy_atp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/scripts/dummy_atp Tue Aug 30 17:02:06 2011 +0200 @@ -0,0 +1,1 @@ +echo "SZS status Unknown" diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Aug 30 17:02:06 2011 +0200 @@ -89,12 +89,12 @@ end |> Meson.make_meta_clause -fun clause_params type_enc = +val clause_params = {ordering = Metis_KnuthBendixOrder.default, orderLiterals = Metis_Clause.UnsignedLiteralOrder, orderTerms = true} -fun active_params type_enc = - {clause = clause_params type_enc, +val active_params = + {clause = clause_params, prefactor = #prefactor Metis_Active.default, postfactor = #postfactor Metis_Active.default} val waiting_params = @@ -102,8 +102,7 @@ variablesWeight = 0.0, literalsWeight = 0.0, models = []} -fun resolution_params type_enc = - {active = active_params type_enc, waiting = waiting_params} +val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = @@ -137,7 +136,7 @@ case filter (fn t => prop_of t aconv @{prop False}) cls of false_th :: _ => [false_th RS @{thm FalseE}] | [] => - case Metis_Resolution.new (resolution_params type_enc) + case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} |> Metis_Resolution.loop of Metis_Resolution.Contradiction mth => diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 17:02:06 2011 +0200 @@ -46,13 +46,13 @@ Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list val all_facts : - Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list -> (((unit -> string) * locality) * thm) list val nearly_all_facts : - Proof.context -> relevance_override -> thm list -> term list -> term + Proof.context -> bool -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * locality) * thm) list val relevant_facts : - Proof.context -> real * real -> int + Proof.context -> bool -> real * real -> int -> (string * typ -> term list -> bool * term list) -> relevance_fudge -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * locality) * thm) list @@ -586,7 +586,7 @@ facts are included. *) val special_fact_index = 75 -fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const +fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const (fudge as {threshold_divisor, ridiculous_threshold, ...}) ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t = let @@ -729,14 +729,15 @@ (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] (* FIXME: put other record thms here, or declare as "no_atp" *) -fun multi_base_blacklist ctxt = +fun multi_base_blacklist ctxt ho_atp = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", "weak_case_cong"] - |> not (Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"] + |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? + append ["induct", "inducts"] |> map (prefix ".") -val max_lambda_nesting = 3 +val max_lambda_nesting = 3 (*only applies if not ho_atp*) fun term_has_too_many_lambdas max (t1 $ t2) = exists (term_has_too_many_lambdas max) [t1, t2] @@ -746,11 +747,12 @@ (* Don't count nested lambdas at the level of formulas, since they are quantifiers. *) -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = - formula_has_too_many_lambdas (T :: Ts) t - | formula_has_too_many_lambdas Ts t = +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) + | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = + formula_has_too_many_lambdas false (T :: Ts) t + | formula_has_too_many_lambdas _ Ts t = if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then - exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) + exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) else term_has_too_many_lambdas max_lambda_nesting t @@ -762,8 +764,8 @@ | apply_depth (Abs (_, _, t)) = apply_depth t | apply_depth _ = 0 -fun is_formula_too_complex t = - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t +fun is_formula_too_complex ho_atp t = + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t (* FIXME: Extend to "Meson" and "Metis" *) val exists_sledgehammer_const = @@ -791,11 +793,11 @@ (**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) -fun is_theorem_bad_for_atps exporter thm = +fun is_theorem_bad_for_atps ho_atp exporter thm = is_metastrange_theorem thm orelse (not exporter andalso let val t = prop_of thm in - is_formula_too_complex t orelse exists_type type_has_top_sort t orelse + is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse exists_low_level_class_const t orelse is_that_fact thm end) @@ -824,7 +826,7 @@ |> add Simp normalize_simp_prop snd simps end -fun all_facts ctxt reserved exporter add_ths chained_ths = +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -834,16 +836,18 @@ fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms val is_chained = member Thm.eq_thm_prop chained_ths val clasimpset_table = clasimpset_rule_table_of ctxt - fun locality_of_theorem global th = - if is_chained th then + fun locality_of_theorem global (name: string) th = + if String.isSubstring ".induct" name orelse(*FIXME: use structured name*) + String.isSubstring ".inducts" name then + Induction + else if is_chained th then Chained else if global then 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 + else if is_assum th then Assum else Local fun is_good_unnamed_local th = not (Thm.has_name_hint th) andalso forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals @@ -860,7 +864,7 @@ (not (Config.get ctxt ignore_no_atp) andalso is_package_def name0) orelse exists (fn s => String.isSuffix s name0) - (multi_base_blacklist ctxt) orelse + (multi_base_blacklist ctxt ho_atp) orelse String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then I else @@ -877,7 +881,7 @@ #> fold (fn th => fn (j, (multis, unis)) => (j + 1, if not (member Thm.eq_thm_prop add_ths th) andalso - is_theorem_bad_for_atps exporter th then + is_theorem_bad_for_atps ho_atp exporter th then (multis, unis) else let @@ -893,7 +897,7 @@ |> (fn SOME name => make_name reserved multi j name | NONE => "")), - locality_of_theorem global th), th) + locality_of_theorem global name0 th), th) in if multi then (new :: multis, unis) else (multis, new :: unis) @@ -911,8 +915,8 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) -fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths - hyp_ts concl_t = +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) + chained_ths hyp_ts concl_t = let val thy = Proof_Context.theory_of ctxt val reserved = reserved_isar_keyword_table () @@ -926,7 +930,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), th)) o fact_from_ref ctxt reserved chained_ths) add else - all_facts ctxt reserved false add_ths chained_ths) + all_facts ctxt ho_atp reserved false add_ths chained_ths) |> Config.get ctxt instantiate_inducts ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |> (not (Config.get ctxt ignore_no_atp) andalso not only) @@ -934,7 +938,7 @@ |> uniquify end -fun relevant_facts ctxt (threshold0, threshold1) max_relevant +fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant is_built_in_const fudge (override as {only, ...}) chained_ths hyp_ts concl_t facts = let @@ -950,9 +954,9 @@ max_relevant = 0 then [] else - relevance_filter ctxt threshold0 decay max_relevant is_built_in_const - fudge override facts (chained_ths |> map prop_of) hyp_ts - (concl_t |> theory_constify fudge (Context.theory_name thy))) + relevance_filter ctxt ho_atp threshold0 decay max_relevant + is_built_in_const fudge override facts (chained_ths |> map prop_of) + hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy))) |> map (apfst (apfst (fn f => f ()))) end diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 30 17:02:06 2011 +0200 @@ -148,8 +148,8 @@ | _ => value) | NONE => (name, value) -(* Ensure that type systems such as "simple!" and "mono_guards?" are handled - correctly. *) +(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are + handled correctly. *) fun implode_param [s, "?"] = s ^ "?" | implode_param [s, "!"] = s ^ "!" | implode_param ss = space_implode " " ss diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 17:02:06 2011 +0200 @@ -64,7 +64,7 @@ val problem_prefix : string Config.T val measure_run_time : bool Config.T val atp_lambda_translation : string Config.T - val atp_readable_names : bool Config.T + val atp_full_names : bool Config.T val atp_sound_modulo_infiniteness : bool Config.T val smt_triggers : bool Config.T val smt_weights : bool Config.T @@ -83,6 +83,7 @@ val is_metis_prover : string -> bool val is_atp : theory -> string -> bool val is_smt_prover : Proof.context -> string -> bool + val is_ho_atp: Proof.context -> string -> bool val is_unit_equational_atp : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool @@ -151,15 +152,18 @@ fun is_smt_prover ctxt name = member (op =) (SMT_Solver.available_solvers_of ctxt) name -fun is_unit_equational_atp ctxt name = +fun is_atp_for_format is_format ctxt name = let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of SOME {best_slices, ...} => - exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ) + exists (fn (_, (_, (_, format, _, _))) => is_format format) (best_slices ctxt) | NONE => false end +val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ) +val is_ho_atp = is_atp_for_format is_format_thf + fun is_prover_supported ctxt name = let val thy = Proof_Context.theory_of ctxt in is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name @@ -329,7 +333,6 @@ type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result - (* configuration attributes *) (* Empty string means create files in Isabelle's temporary files directory. *) @@ -346,8 +349,8 @@ (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) -val atp_readable_names = - Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) +val atp_full_names = + Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false) val atp_sound_modulo_infiniteness = Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness} (K true) @@ -665,7 +668,7 @@ fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc false (Config.get ctxt atp_lambda_translation) - (Config.get ctxt atp_readable_names) true hyp_ts concl_t + (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem val full_proof = debug orelse isar_proof diff -r 022509c908fb -r 426834f253c8 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 17:02:06 2011 +0200 @@ -144,6 +144,9 @@ get_prover ctxt mode name params minimize_command problem |> minimize ctxt mode name params problem +fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true + | is_induction_fact _ = false + fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing, timeout, expect, ...}) mode minimize_command only @@ -160,9 +163,15 @@ fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = - {state = state, goal = goal, subgoal = subgoal, - subgoal_count = subgoal_count, facts = facts |> take num_facts, - smt_filter = smt_filter} + let + val filter_induction = filter_out is_induction_fact + in {state = state, goal = goal, subgoal = subgoal, + subgoal_count = subgoal_count, facts = + ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction) + facts + |> take num_facts, + smt_filter = smt_filter} + end fun really_go () = problem |> get_minimizing_prover ctxt mode name params minimize_command @@ -260,8 +269,9 @@ val {facts = chained_ths, goal, ...} = Proof.goal state val chained_ths = chained_ths |> normalize_chained_theorems val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i - val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts - concl_t + val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers + val facts = nearly_all_facts ctxt is_ho_atp relevance_override + chained_ths hyp_ts concl_t val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -313,9 +323,9 @@ |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I) - |> relevant_facts ctxt relevance_thresholds max_max_relevant - is_built_in_const relevance_fudge relevance_override - chained_ths hyp_ts concl_t + |> relevant_facts ctxt is_ho_atp relevance_thresholds + max_max_relevant is_built_in_const relevance_fudge + relevance_override chained_ths hyp_ts concl_t |> tap (fn facts => if debug then label ^ plural_s (length provers) ^ ": " ^ diff -r 022509c908fb -r 426834f253c8 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 16:33:24 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 17:02:06 2011 +0200 @@ -37,10 +37,13 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i + val is_ho_atp = + exists (Sledgehammer_Provers.is_ho_atp ctxt) + provers(*FIXME: duplicated from sledgehammer_run.ML*) val facts = - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths - hyp_ts concl_t - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override + chained_ths hyp_ts concl_t + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem =