--- 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
--- 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
--- 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
--- 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 \<in> S" and "y \<in> T" and "y \<noteq> x"
using assms unfolding islimpt_def by auto
-lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
+lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
+ unfolding islimpt_def eventually_at_topological by auto
+
+lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
+ unfolding islimpt_def by fast
lemma islimpt_approachable:
fixes x :: "'a::metric_space"
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> 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 \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
unfolding islimpt_approachable
- using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
- by metis
+ using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> 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 \<longleftrightarrow> \<not> 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 "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "(X ---> L) (at a within T)"
-proof (rule ccontr)
- assume "\<not> (X ---> L) (at a within T)"
- hence "\<exists>r>0. \<forall>s>0. \<exists>x\<in>T. x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> r \<le> dist (X x) L"
- unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric])
- then obtain r where r: "r > 0" "\<And>s. s > 0 \<Longrightarrow> \<exists>x\<in>T-{a}. \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r" by blast
-
- let ?F = "\<lambda>n::nat. SOME x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
- have "\<And>n. \<exists>x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
- using r by (simp add: Bex_def)
- hence F: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
- by (rule someI_ex)
- hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a"
- and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
- and F3: "\<And>n. dist (X (?F n)) L \<ge> 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 "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
- then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
- show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
- proof (intro exI allI impI)
- fix n
- assume mlen: "m \<le> n"
- have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
- by (rule F2)
- also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
- using mlen by auto
- also from nodef have
- "inverse (real (Suc m)) < e" .
- finally show "\<bar>?F n - a\<bar> < e" .
- qed
- qed
- moreover note `\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
- ultimately have "(\<lambda>n. X (?F n)) ----> L" using F1 by simp
-
- moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
- proof -
- {
- fix no::nat
- obtain n where "n = no + 1" by simp
- then have nolen: "no \<le> n" by simp
- (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
- have "dist (X (?F n)) L \<ge> r"
- by (rule F3)
- with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
- }
- then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
- with r have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> 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 \<Rightarrow> real"
@@ -1160,21 +1103,18 @@
proof
assume ?lhs
then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
- unfolding islimpt_approachable using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
- { fix n::nat
- have "f (inverse (real n + 1)) \<in> S - {x}" using f by auto
- }
- moreover
- { fix e::real assume "e>0"
- hence "\<exists>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 "\<forall>n\<ge>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 "\<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto
- ultimately have "\<exists>N::nat. \<forall>n\<ge>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 " ((\<lambda>n. f (inverse (real n + 1))) ---> x) sequentially"
- unfolding Lim_sequentially using f by auto
- ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
+ unfolding islimpt_approachable
+ using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
+ let ?I = "\<lambda>n. inverse (real (Suc n))"
+ have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
+ moreover have "(\<lambda>n. f (?I n)) ----> x"
+ proof (rule metric_tendsto_imp_tendsto)
+ show "?I ----> 0"
+ by (rule LIMSEQ_inverse_real_of_nat)
+ show "eventually (\<lambda>n. dist (f (?I n)) x \<le> 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\<Rightarrow>'a" where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>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 \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
@@ -1480,8 +1420,7 @@
lemma seq_offset:
assumes "(f ---> l) sequentially"
shows "((\<lambda>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 ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
@@ -1494,21 +1433,10 @@
lemma seq_offset_rev:
"((\<lambda>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 "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
- by metis arith
+ by (rule LIMSEQ_offset) (* FIXME: redundant *)
lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
-proof-
- { fix e::real assume "e>0"
- hence "\<exists>N::nat. \<forall>n::nat\<ge>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 \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> 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 \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
\<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
@@ -4408,7 +4336,7 @@
note * = this
{ fix x y assume "x\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>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\<noteq>{}" unfolding diameter_def by auto
@@ -4667,39 +4595,26 @@
"{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
unfolding interval_eq_empty[of a b] by fastsimp+
-lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
- "{a .. a} = {a}" "{a<..<a} = {}"
- apply(auto simp add: set_eq_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
- apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
+lemma interval_sing:
+ fixes a :: "'a::ordered_euclidean_space"
+ shows "{a .. a} = {a}" and "{a<..<a} = {}"
+ unfolding set_eq_iff mem_interval eq_iff [symmetric]
+ by (auto simp add: euclidean_eq[where 'a='a] eq_commute
+ eucl_less[where 'a='a] eucl_le[where 'a='a])
lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
"(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
"(\<forall>i<DIM('a). a$$i < c$$i \<and> d$$i < b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
"(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
"(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
- unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
- by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
-
-lemma interval_open_subset_closed: fixes a :: "'a::ordered_euclidean_space" shows
- "{a<..<b} \<subseteq> {a .. b}"
-proof(simp add: subset_eq, rule)
- fix x
- assume x:"x \<in>{a<..<b}"
- { fix i assume "i<DIM('a)"
- hence "a $$ i \<le> 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<DIM('a)"
- hence "x $$ i \<le> 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 \<le> x \<and> x \<le> 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<..<b} \<subseteq> {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} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). c$$i \<le> d$$i) --> (\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i)" (is ?th1) and
@@ -4825,7 +4740,7 @@
"(x + (e / 2) *\<^sub>R basis i) $$ i \<le> 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 \<in> {a<..<b}" unfolding mem_interval by auto }
@@ -5009,9 +4924,8 @@
lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
"is_interval {a<..<b}" (is ?th2) proof -
- have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> 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 {}"
--- 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)
--- 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)) =
--- 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
--- 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 =
--- /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"
--- 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 =>
--- 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
--- 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
--- 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
--- 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) ^ ": " ^
--- 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 =