1.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 30 16:33:24 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 30 17:02:06 2011 +0200
1.3 @@ -39,7 +39,6 @@
1.4 "mono_tags",
1.5 "mono_tags_uniform",
1.6 "mono_args",
1.7 - "simple",
1.8 "poly_guards?",
1.9 "poly_guards_uniform?",
1.10 "poly_tags?",
1.11 @@ -52,7 +51,6 @@
1.12 "mono_guards_uniform?",
1.13 "mono_tags?",
1.14 "mono_tags_uniform?",
1.15 - "simple?",
1.16 "poly_guards!",
1.17 "poly_guards_uniform!",
1.18 "poly_tags!",
1.19 @@ -64,8 +62,7 @@
1.20 "mono_guards!",
1.21 "mono_guards_uniform!",
1.22 "mono_tags!",
1.23 - "mono_tags_uniform!",
1.24 - "simple!"]
1.25 + "mono_tags_uniform!"]
1.26
1.27 fun metis_exhaust_tac ctxt ths =
1.28 let
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 16:33:24 2011 +0200
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 17:02:06 2011 +0200
2.3 @@ -416,11 +416,12 @@
2.4 let
2.5 val _ = if is_appropriate_prop concl_t then ()
2.6 else raise Fail "inappropriate"
2.7 + val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
2.8 val facts =
2.9 - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
2.10 - chained_ths hyp_ts concl_t
2.11 + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp
2.12 + relevance_override chained_ths hyp_ts concl_t
2.13 |> filter (is_appropriate_prop o prop_of o snd)
2.14 - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
2.15 + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
2.16 (the_default default_max_relevant max_relevant)
2.17 is_built_in_const relevance_fudge relevance_override
2.18 chained_ths hyp_ts concl_t
2.19 @@ -575,7 +576,7 @@
2.20 relevance_override
2.21 in
2.22 if !reconstructor = "sledgehammer_tac" then
2.23 - sledge_tac 0.25 ATP_Systems.z3_tptpN "simple"
2.24 + sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
2.25 ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
2.26 ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
2.27 ORELSE' Metis_Tactics.metis_tac [] ctxt thms
3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 16:33:24 2011 +0200
3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 17:02:06 2011 +0200
3.3 @@ -129,11 +129,12 @@
3.4 val relevance_override = {add = [], del = [], only = false}
3.5 val subgoal = 1
3.6 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
3.7 + val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
3.8 val facts =
3.9 - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
3.10 + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
3.11 chained_ths hyp_ts concl_t
3.12 |> filter (is_appropriate_prop o prop_of o snd)
3.13 - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
3.14 + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
3.15 (the_default default_max_relevant max_relevant)
3.16 is_built_in_const relevance_fudge relevance_override
3.17 chained_ths hyp_ts concl_t
4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 30 16:33:24 2011 +0200
4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 30 17:02:06 2011 +0200
4.3 @@ -443,27 +443,24 @@
4.4 obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
4.5 using assms unfolding islimpt_def by auto
4.6
4.7 -lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
4.8 +lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
4.9 + unfolding islimpt_def eventually_at_topological by auto
4.10 +
4.11 +lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
4.12 + unfolding islimpt_def by fast
4.13
4.14 lemma islimpt_approachable:
4.15 fixes x :: "'a::metric_space"
4.16 shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
4.17 - unfolding islimpt_def
4.18 - apply auto
4.19 - apply(erule_tac x="ball x e" in allE)
4.20 - apply auto
4.21 - apply(rule_tac x=y in bexI)
4.22 - apply (auto simp add: dist_commute)
4.23 - apply (simp add: open_dist, drule (1) bspec)
4.24 - apply (clarify, drule spec, drule (1) mp, auto)
4.25 - done
4.26 + unfolding islimpt_iff_eventually eventually_at by fast
4.27
4.28 lemma islimpt_approachable_le:
4.29 fixes x :: "'a::metric_space"
4.30 shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
4.31 unfolding islimpt_approachable
4.32 - using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
4.33 - by metis
4.34 + using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
4.35 + THEN arg_cong [where f=Not]]
4.36 + by (simp add: Bex_def conj_commute conj_left_commute)
4.37
4.38 lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
4.39 unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
4.40 @@ -1058,65 +1055,11 @@
4.41 using assms by (simp only: at_within_open)
4.42
4.43 lemma Lim_within_LIMSEQ:
4.44 - fixes a :: real and L :: "'a::metric_space"
4.45 + fixes a :: "'a::metric_space"
4.46 assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
4.47 shows "(X ---> L) (at a within T)"
4.48 -proof (rule ccontr)
4.49 - assume "\<not> (X ---> L) (at a within T)"
4.50 - 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"
4.51 - unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric])
4.52 - 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
4.53 -
4.54 - 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"
4.55 - 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"
4.56 - using r by (simp add: Bex_def)
4.57 - 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"
4.58 - by (rule someI_ex)
4.59 - hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a"
4.60 - and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
4.61 - and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
4.62 - by fast+
4.63 -
4.64 - have "?F ----> a"
4.65 - proof (rule LIMSEQ_I, unfold real_norm_def)
4.66 - fix e::real
4.67 - assume "0 < e"
4.68 - (* choose no such that inverse (real (Suc n)) < e *)
4.69 - then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
4.70 - then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
4.71 - show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
4.72 - proof (intro exI allI impI)
4.73 - fix n
4.74 - assume mlen: "m \<le> n"
4.75 - have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
4.76 - by (rule F2)
4.77 - also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
4.78 - using mlen by auto
4.79 - also from nodef have
4.80 - "inverse (real (Suc m)) < e" .
4.81 - finally show "\<bar>?F n - a\<bar> < e" .
4.82 - qed
4.83 - qed
4.84 - 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`
4.85 - ultimately have "(\<lambda>n. X (?F n)) ----> L" using F1 by simp
4.86 -
4.87 - moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
4.88 - proof -
4.89 - {
4.90 - fix no::nat
4.91 - obtain n where "n = no + 1" by simp
4.92 - then have nolen: "no \<le> n" by simp
4.93 - (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
4.94 - have "dist (X (?F n)) L \<ge> r"
4.95 - by (rule F3)
4.96 - with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
4.97 - }
4.98 - then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
4.99 - with r have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
4.100 - thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
4.101 - qed
4.102 - ultimately show False by simp
4.103 -qed
4.104 + using assms unfolding tendsto_def [where l=L]
4.105 + by (simp add: sequentially_imp_eventually_within)
4.106
4.107 lemma Lim_right_bound:
4.108 fixes f :: "real \<Rightarrow> real"
4.109 @@ -1160,21 +1103,18 @@
4.110 proof
4.111 assume ?lhs
4.112 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"
4.113 - 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
4.114 - { fix n::nat
4.115 - have "f (inverse (real n + 1)) \<in> S - {x}" using f by auto
4.116 - }
4.117 - moreover
4.118 - { fix e::real assume "e>0"
4.119 - 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
4.120 - then obtain N::nat where "inverse (real (N + 1)) < e" by auto
4.121 - 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)
4.122 - moreover have "\<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto
4.123 - 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
4.124 - }
4.125 - hence " ((\<lambda>n. f (inverse (real n + 1))) ---> x) sequentially"
4.126 - unfolding Lim_sequentially using f by auto
4.127 - ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
4.128 + unfolding islimpt_approachable
4.129 + using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
4.130 + let ?I = "\<lambda>n. inverse (real (Suc n))"
4.131 + have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
4.132 + moreover have "(\<lambda>n. f (?I n)) ----> x"
4.133 + proof (rule metric_tendsto_imp_tendsto)
4.134 + show "?I ----> 0"
4.135 + by (rule LIMSEQ_inverse_real_of_nat)
4.136 + show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
4.137 + by (simp add: norm_conv_dist [symmetric] less_imp_le f)
4.138 + qed
4.139 + ultimately show ?rhs by fast
4.140 next
4.141 assume ?rhs
4.142 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
4.143 @@ -1331,7 +1271,7 @@
4.144 shows "netlimit (at a) = a"
4.145 apply (subst within_UNIV[symmetric])
4.146 using netlimit_within[of a UNIV]
4.147 - by (simp add: trivial_limit_at within_UNIV)
4.148 + by (simp add: within_UNIV)
4.149
4.150 lemma lim_within_interior:
4.151 "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
4.152 @@ -1480,8 +1420,7 @@
4.153 lemma seq_offset:
4.154 assumes "(f ---> l) sequentially"
4.155 shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
4.156 - using assms unfolding tendsto_def
4.157 - by clarify (rule sequentially_offset, simp)
4.158 + using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
4.159
4.160 lemma seq_offset_neg:
4.161 "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
4.162 @@ -1494,21 +1433,10 @@
4.163
4.164 lemma seq_offset_rev:
4.165 "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
4.166 - apply (rule topological_tendstoI)
4.167 - apply (drule (2) topological_tendstoD)
4.168 - apply (simp only: eventually_sequentially)
4.169 - apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
4.170 - by metis arith
4.171 + by (rule LIMSEQ_offset) (* FIXME: redundant *)
4.172
4.173 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
4.174 -proof-
4.175 - { fix e::real assume "e>0"
4.176 - hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
4.177 - using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
4.178 - by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
4.179 - }
4.180 - thus ?thesis unfolding Lim_sequentially dist_norm by simp
4.181 -qed
4.182 + using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
4.183
4.184 subsection {* More properties of closed balls *}
4.185
4.186 @@ -3154,7 +3082,7 @@
4.187 lemma continuous_within_eps_delta:
4.188 "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)"
4.189 unfolding continuous_within and Lim_within
4.190 - apply auto unfolding dist_nz[THEN sym] apply(auto elim!:allE) apply(rule_tac x=d in exI) by auto
4.191 + apply auto unfolding dist_nz[THEN sym] apply(auto del: allE elim!:allE) apply(rule_tac x=d in exI) by auto
4.192
4.193 lemma continuous_at_eps_delta: "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
4.194 \<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
4.195 @@ -4408,7 +4336,7 @@
4.196 note * = this
4.197 { fix x y assume "x\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
4.198 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`
4.199 - by simp (blast intro!: Sup_upper *) }
4.200 + by simp (blast del: Sup_upper intro!: * Sup_upper) }
4.201 moreover
4.202 { fix d::real assume "d>0" "d < diameter s"
4.203 hence "s\<noteq>{}" unfolding diameter_def by auto
4.204 @@ -4667,39 +4595,26 @@
4.205 "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
4.206 unfolding interval_eq_empty[of a b] by fastsimp+
4.207
4.208 -lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
4.209 - "{a .. a} = {a}" "{a<..<a} = {}"
4.210 - apply(auto simp add: set_eq_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
4.211 - apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
4.212 +lemma interval_sing:
4.213 + fixes a :: "'a::ordered_euclidean_space"
4.214 + shows "{a .. a} = {a}" and "{a<..<a} = {}"
4.215 + unfolding set_eq_iff mem_interval eq_iff [symmetric]
4.216 + by (auto simp add: euclidean_eq[where 'a='a] eq_commute
4.217 + eucl_less[where 'a='a] eucl_le[where 'a='a])
4.218
4.219 lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
4.220 "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
4.221 "(\<forall>i<DIM('a). a$$i < c$$i \<and> d$$i < b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
4.222 "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
4.223 "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
4.224 - unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
4.225 - by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
4.226 -
4.227 -lemma interval_open_subset_closed: fixes a :: "'a::ordered_euclidean_space" shows
4.228 - "{a<..<b} \<subseteq> {a .. b}"
4.229 -proof(simp add: subset_eq, rule)
4.230 - fix x
4.231 - assume x:"x \<in>{a<..<b}"
4.232 - { fix i assume "i<DIM('a)"
4.233 - hence "a $$ i \<le> x $$ i"
4.234 - using x order_less_imp_le[of "a$$i" "x$$i"]
4.235 - by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
4.236 - }
4.237 - moreover
4.238 - { fix i assume "i<DIM('a)"
4.239 - hence "x $$ i \<le> b $$ i"
4.240 - using x order_less_imp_le[of "x$$i" "b$$i"]
4.241 - by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
4.242 - }
4.243 - ultimately
4.244 - show "a \<le> x \<and> x \<le> b"
4.245 - by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
4.246 -qed
4.247 + unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
4.248 + by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
4.249 +
4.250 +lemma interval_open_subset_closed:
4.251 + fixes a :: "'a::ordered_euclidean_space"
4.252 + shows "{a<..<b} \<subseteq> {a .. b}"
4.253 + unfolding subset_eq [unfolded Ball_def] mem_interval
4.254 + by (fast intro: less_imp_le)
4.255
4.256 lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows
4.257 "{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
4.258 @@ -4825,7 +4740,7 @@
4.259 "(x + (e / 2) *\<^sub>R basis i) $$ i \<le> b $$ i"
4.260 using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
4.261 and e[THEN spec[where x="x + (e/2) *\<^sub>R basis i"]]
4.262 - unfolding mem_interval by (auto elim!: allE[where x=i])
4.263 + unfolding mem_interval using i by blast+
4.264 hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
4.265 unfolding basis_component using `e>0` i by auto }
4.266 hence "x \<in> {a<..<b}" unfolding mem_interval by auto }
4.267 @@ -5009,9 +4924,8 @@
4.268
4.269 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
4.270 "is_interval {a<..<b}" (is ?th2) proof -
4.271 - have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
4.272 show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
4.273 - by(meson order_trans le_less_trans less_le_trans *)+ qed
4.274 + by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
4.275
4.276 lemma is_interval_empty:
4.277 "is_interval {}"
5.1 --- a/src/HOL/TPTP/atp_export.ML Tue Aug 30 16:33:24 2011 +0200
5.2 +++ b/src/HOL/TPTP/atp_export.ML Tue Aug 30 17:02:06 2011 +0200
5.3 @@ -27,8 +27,9 @@
5.4 val fact_name_of = prefix fact_prefix o ascii_of
5.5
5.6 fun facts_of thy =
5.7 - Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
5.8 - true [] []
5.9 + Sledgehammer_Filter.all_facts (Proof_Context.init_global thy)
5.10 + false(*FIXME works only for first-order*)
5.11 + Symtab.empty true [] []
5.12 |> filter (curry (op =) @{typ bool} o fastype_of
5.13 o Object_Logic.atomize_term thy o prop_of o snd)
5.14
6.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:33:24 2011 +0200
6.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 17:02:06 2011 +0200
6.3 @@ -17,16 +17,20 @@
6.4 AConn of connective * ('a, 'b, 'c) formula list |
6.5 AAtom of 'c
6.6
6.7 - datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
6.8 + datatype 'a ho_type =
6.9 + AType of 'a * 'a ho_type list |
6.10 + AFun of 'a ho_type * 'a ho_type |
6.11 + ATyAbs of 'a list * 'a ho_type
6.12
6.13 - datatype tff_flavor = Implicit | Explicit
6.14 - datatype thf_flavor = Without_Choice | With_Choice
6.15 + datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
6.16 + datatype tff_explicitness = TFF_Implicit | TFF_Explicit
6.17 + datatype thf_flavor = THF_Without_Choice | THF_With_Choice
6.18 datatype format =
6.19 CNF |
6.20 CNF_UEQ |
6.21 FOF |
6.22 - TFF of tff_flavor |
6.23 - THF of thf_flavor
6.24 + TFF of tff_polymorphism * tff_explicitness |
6.25 + THF0 of thf_flavor
6.26
6.27 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
6.28 datatype 'a problem_line =
6.29 @@ -70,6 +74,9 @@
6.30 val is_built_in_tptp_symbol : string -> bool
6.31 val is_tptp_variable : string -> bool
6.32 val is_tptp_user_symbol : string -> bool
6.33 + val atype_of_types : (string * string) ho_type
6.34 + val bool_atype : (string * string) ho_type
6.35 + val individual_atype : (string * string) ho_type
6.36 val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
6.37 val mk_aconn :
6.38 connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
6.39 @@ -117,17 +124,21 @@
6.40 AConn of connective * ('a, 'b, 'c) formula list |
6.41 AAtom of 'c
6.42
6.43 -datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
6.44 +datatype 'a ho_type =
6.45 + AType of 'a * 'a ho_type list |
6.46 + AFun of 'a ho_type * 'a ho_type |
6.47 + ATyAbs of 'a list * 'a ho_type
6.48
6.49 -datatype tff_flavor = Implicit | Explicit
6.50 -datatype thf_flavor = Without_Choice | With_Choice
6.51 +datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
6.52 +datatype tff_explicitness = TFF_Implicit | TFF_Explicit
6.53 +datatype thf_flavor = THF_Without_Choice | THF_With_Choice
6.54
6.55 datatype format =
6.56 CNF |
6.57 CNF_UEQ |
6.58 FOF |
6.59 - TFF of tff_flavor |
6.60 - THF of thf_flavor
6.61 + TFF of tff_polymorphism * tff_explicitness |
6.62 + THF0 of thf_flavor
6.63
6.64 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
6.65 datatype 'a problem_line =
6.66 @@ -211,10 +222,10 @@
6.67 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
6.68 | formula_map f (AAtom tm) = AAtom (f tm)
6.69
6.70 -fun is_format_thf (THF _) = true
6.71 +fun is_format_thf (THF0 _) = true
6.72 | is_format_thf _ = false
6.73 fun is_format_typed (TFF _) = true
6.74 - | is_format_typed (THF _) = true
6.75 + | is_format_typed (THF0 _) = true
6.76 | is_format_typed _ = false
6.77
6.78 fun string_for_kind Axiom = "axiom"
6.79 @@ -223,25 +234,38 @@
6.80 | string_for_kind Hypothesis = "hypothesis"
6.81 | string_for_kind Conjecture = "conjecture"
6.82
6.83 -fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s
6.84 - | strip_tff_type (AFun (AFun _, _)) =
6.85 +fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
6.86 + | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
6.87 + (case flatten_type ty2 of
6.88 + AFun (ty' as AType (s, tys), ty) =>
6.89 + AFun (AType (tptp_product_type,
6.90 + ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
6.91 + | _ => ty)
6.92 + | flatten_type (ty as AType _) = ty
6.93 + | flatten_type _ =
6.94 raise Fail "unexpected higher-order type in first-order format"
6.95 - | strip_tff_type (AType s) = ([], s)
6.96
6.97 -fun string_for_type (THF _) ty =
6.98 - let
6.99 - fun aux _ (AType s) = s
6.100 - | aux rhs (AFun (ty1, ty2)) =
6.101 - aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
6.102 - |> not rhs ? enclose "(" ")"
6.103 - in aux true ty end
6.104 - | string_for_type (TFF _) ty =
6.105 - (case strip_tff_type ty of
6.106 - ([], s) => s
6.107 - | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
6.108 - | (ss, s) =>
6.109 - "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^
6.110 - tptp_fun_type ^ " " ^ s)
6.111 +fun str_for_type ty =
6.112 + let
6.113 + fun str _ (AType (s, [])) = s
6.114 + | str _ (AType (s, tys)) =
6.115 + tys |> map (str false)
6.116 + |> (if s = tptp_product_type then
6.117 + space_implode (" " ^ tptp_product_type ^ " ")
6.118 + #> length tys > 1 ? enclose "(" ")"
6.119 + else
6.120 + commas #> enclose "(" ")" #> prefix s)
6.121 + | str rhs (AFun (ty1, ty2)) =
6.122 + str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
6.123 + |> not rhs ? enclose "(" ")"
6.124 + | str _ (ATyAbs (ss, ty)) =
6.125 + tptp_forall ^ "[" ^
6.126 + commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
6.127 + ss) ^ "] : " ^ str false ty
6.128 + in str true ty end
6.129 +
6.130 +fun string_for_type (THF0 _) ty = str_for_type ty
6.131 + | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
6.132 | string_for_type _ _ = raise Fail "unexpected type in untyped format"
6.133
6.134 fun string_for_quantifier AForall = tptp_forall
6.135 @@ -254,11 +278,13 @@
6.136 | string_for_connective AIff = tptp_iff
6.137
6.138 fun string_for_bound_var format (s, ty) =
6.139 - s ^ (if is_format_typed format then
6.140 - " " ^ tptp_has_type ^ " " ^
6.141 - string_for_type format (ty |> the_default (AType tptp_individual_type))
6.142 - else
6.143 - "")
6.144 + s ^
6.145 + (if is_format_typed format then
6.146 + " " ^ tptp_has_type ^ " " ^
6.147 + (ty |> the_default (AType (tptp_individual_type, []))
6.148 + |> string_for_type format)
6.149 + else
6.150 + "")
6.151
6.152 fun string_for_term _ (ATerm (s, [])) = s
6.153 | string_for_term format (ATerm (s, ts)) =
6.154 @@ -270,7 +296,7 @@
6.155 |> is_format_thf format ? enclose "(" ")"
6.156 else
6.157 (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
6.158 - s = tptp_choice andalso format = THF With_Choice, ts) of
6.159 + s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
6.160 (true, _, [AAbs ((s', ty), tm)]) =>
6.161 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
6.162 possible, to work around LEO-II 1.2.8 parser limitation. *)
6.163 @@ -291,7 +317,7 @@
6.164 else
6.165 s ^ "(" ^ commas ss ^ ")"
6.166 end)
6.167 - | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
6.168 + | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
6.169 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
6.170 string_for_term format tm ^ ")"
6.171 | string_for_term _ _ = raise Fail "unexpected term in first-order format"
6.172 @@ -324,7 +350,7 @@
6.173 | string_for_format CNF_UEQ = tptp_cnf
6.174 | string_for_format FOF = tptp_fof
6.175 | string_for_format (TFF _) = tptp_tff
6.176 - | string_for_format (THF _) = tptp_thf
6.177 + | string_for_format (THF0 _) = tptp_thf
6.178
6.179 fun string_for_problem_line format (Decl (ident, sym, ty)) =
6.180 string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
6.181 @@ -438,9 +464,9 @@
6.182 symbols (with "$i" as the type of individuals), but some provers (e.g.,
6.183 SNARK) require explicit declarations. The situation is similar for THF. *)
6.184
6.185 -val atype_of_types = AType (`I tptp_type_of_types)
6.186 -val bool_atype = AType (`I tptp_bool_type)
6.187 -val individual_atype = AType (`I tptp_individual_type)
6.188 +val atype_of_types = AType (`I tptp_type_of_types, [])
6.189 +val bool_atype = AType (`I tptp_bool_type, [])
6.190 +val individual_atype = AType (`I tptp_individual_type, [])
6.191
6.192 fun default_type pred_sym =
6.193 let
6.194 @@ -457,8 +483,10 @@
6.195 let
6.196 fun do_sym name ty =
6.197 if member (op =) declared name then I else AList.default (op =) (name, ty)
6.198 - fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
6.199 - | do_type (AType name) = do_sym name (K atype_of_types)
6.200 + fun do_type_name name = do_sym name (K atype_of_types)
6.201 + fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
6.202 + | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
6.203 + | do_type (ATyAbs (names, ty)) = fold do_type_name names #> do_type ty
6.204 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
6.205 is_tptp_user_symbol s
6.206 ? do_sym name (fn _ => default_type pred_sym (length tms))
6.207 @@ -555,8 +583,11 @@
6.208 end
6.209 in add 0 |> apsnd SOME end
6.210
6.211 -fun nice_type (AType name) = nice_name name #>> AType
6.212 +fun nice_type (AType (name, tys)) =
6.213 + nice_name name ##>> pool_map nice_type tys #>> AType
6.214 | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
6.215 + | nice_type (ATyAbs (names, ty)) =
6.216 + pool_map nice_name names ##>> nice_type ty #>> ATyAbs
6.217 fun nice_term (ATerm (name, ts)) =
6.218 nice_name name ##>> pool_map nice_term ts #>> ATerm
6.219 | nice_term (AAbs ((name, ty), tm)) =
7.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 16:33:24 2011 +0200
7.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 17:02:06 2011 +0200
7.3 @@ -37,13 +37,14 @@
7.4 val e_sym_offs_weight_base : real Config.T
7.5 val e_sym_offs_weight_span : real Config.T
7.6 val eN : string
7.7 + val e_sineN : string
7.8 + val e_tofofN : string
7.9 + val leo2N : string
7.10 + val pffN : string
7.11 + val satallaxN : string
7.12 + val snarkN : string
7.13 val spassN : string
7.14 val vampireN : string
7.15 - val leo2N : string
7.16 - val satallaxN : string
7.17 - val e_sineN : string
7.18 - val snarkN : string
7.19 - val e_tofofN : string
7.20 val waldmeisterN : string
7.21 val z3_tptpN : string
7.22 val remote_prefix : string
7.23 @@ -100,15 +101,16 @@
7.24 (* named ATPs *)
7.25
7.26 val eN = "e"
7.27 +val e_sineN = "e_sine"
7.28 +val e_tofofN = "e_tofof"
7.29 val leo2N = "leo2"
7.30 +val pffN = "pff"
7.31 val satallaxN = "satallax"
7.32 +val snarkN = "snark"
7.33 val spassN = "spass"
7.34 val vampireN = "vampire"
7.35 +val waldmeisterN = "waldmeister"
7.36 val z3_tptpN = "z3_tptp"
7.37 -val e_sineN = "e_sine"
7.38 -val snarkN = "snark"
7.39 -val e_tofofN = "e_tofof"
7.40 -val waldmeisterN = "waldmeister"
7.41 val remote_prefix = "remote_"
7.42
7.43 structure Data = Theory_Data
7.44 @@ -241,8 +243,10 @@
7.45 prem_kind = Hypothesis,
7.46 best_slices = fn ctxt =>
7.47 (* FUDGE *)
7.48 - [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
7.49 - (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
7.50 + [(0.667, (false, (150, THF0 THF_Without_Choice,
7.51 + "mono_simple_higher", sosN))),
7.52 + (0.333, (true, (50, THF0 THF_Without_Choice,
7.53 + "mono_simple_higher", no_sosN)))]
7.54 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
7.55 else I)}
7.56
7.57 @@ -262,7 +266,8 @@
7.58 conj_sym_kind = Axiom,
7.59 prem_kind = Hypothesis,
7.60 best_slices =
7.61 - K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
7.62 + K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
7.63 + (* FUDGE *)}
7.64
7.65 val satallax = (satallaxN, satallax_config)
7.66
7.67 @@ -309,6 +314,8 @@
7.68 fun is_old_vampire_version () =
7.69 string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
7.70
7.71 +val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
7.72 +
7.73 val vampire_config : atp_config =
7.74 {exec = ("VAMPIRE_HOME", "vampire"),
7.75 required_execs = [],
7.76 @@ -340,9 +347,9 @@
7.77 (0.333, (false, (500, FOF, "mono_tags?", sosN))),
7.78 (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
7.79 else
7.80 - [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
7.81 - (0.333, (false, (500, TFF Implicit, "simple", sosN))),
7.82 - (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
7.83 + [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
7.84 + (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
7.85 + (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
7.86 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
7.87 else I)}
7.88
7.89 @@ -351,6 +358,8 @@
7.90
7.91 (* Z3 with TPTP syntax *)
7.92
7.93 +val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
7.94 +
7.95 val z3_tptp_config : atp_config =
7.96 {exec = ("Z3_HOME", "z3"),
7.97 required_execs = [],
7.98 @@ -368,20 +377,37 @@
7.99 prem_kind = Hypothesis,
7.100 best_slices =
7.101 (* FUDGE *)
7.102 - K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
7.103 - (0.25, (false, (125, FOF, "mono_guards?", ""))),
7.104 - (0.125, (false, (62, TFF Implicit, "simple", ""))),
7.105 - (0.125, (false, (31, TFF Implicit, "simple", "")))]}
7.106 + K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
7.107 + (0.25, (false, (125, z3_tff, "mono_simple", ""))),
7.108 + (0.125, (false, (62, z3_tff, "mono_simple", ""))),
7.109 + (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
7.110
7.111 val z3_tptp = (z3_tptpN, z3_tptp_config)
7.112
7.113 +(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
7.114 +
7.115 +val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
7.116 +
7.117 +val pff_config : atp_config =
7.118 + {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
7.119 + required_execs = [],
7.120 + arguments = K (K (K (K (K "")))),
7.121 + proof_delims = [],
7.122 + known_failures = [(GaveUp, "SZS status Unknown")],
7.123 + conj_sym_kind = Hypothesis,
7.124 + prem_kind = Hypothesis,
7.125 + best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
7.126 +
7.127 +val pff = (pffN, pff_config)
7.128 +
7.129
7.130 (* Remote ATP invocation via SystemOnTPTP *)
7.131
7.132 val systems = Synchronized.var "atp_systems" ([] : string list)
7.133
7.134 fun get_systems () =
7.135 - case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
7.136 + case Isabelle_System.bash_output
7.137 + "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
7.138 (output, 0) => split_lines output
7.139 | (output, _) =>
7.140 error (case extract_known_failure known_perl_failures output of
7.141 @@ -449,31 +475,34 @@
7.142 (remote_prefix ^ name,
7.143 remotify_config system_name system_versions best_slice config)
7.144
7.145 +val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
7.146 +
7.147 val remote_e =
7.148 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
7.149 (K (750, FOF, "mono_tags?") (* FUDGE *))
7.150 val remote_leo2 =
7.151 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
7.152 - (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
7.153 + (K (100, THF0 THF_Without_Choice,
7.154 + "mono_simple_higher") (* FUDGE *))
7.155 val remote_satallax =
7.156 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
7.157 - (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
7.158 + (K (100, THF0 THF_With_Choice,
7.159 + "mono_simple_higher") (* FUDGE *))
7.160 val remote_vampire =
7.161 remotify_atp vampire "Vampire" ["1.8"]
7.162 - (K (250, TFF Implicit, "simple") (* FUDGE *))
7.163 + (K (250, FOF, "mono_guards?") (* FUDGE *))
7.164 val remote_z3_tptp =
7.165 - remotify_atp z3_tptp "Z3" ["3.0"]
7.166 - (K (250, TFF Implicit, "simple") (* FUDGE *))
7.167 + remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
7.168 val remote_e_sine =
7.169 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
7.170 Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
7.171 val remote_snark =
7.172 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
7.173 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
7.174 - (K (100, TFF Explicit, "simple") (* FUDGE *))
7.175 + (K (100, dumb_tff, "mono_simple") (* FUDGE *))
7.176 val remote_e_tofof =
7.177 - remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
7.178 - Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
7.179 + remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
7.180 + Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
7.181 val remote_waldmeister =
7.182 remote_atp waldmeisterN "Waldmeister" ["710"]
7.183 [("#START OF PROOF", "Proved Goals:")]
7.184 @@ -503,7 +532,7 @@
7.185 Synchronized.change systems (fn _ => get_systems ())
7.186
7.187 val atps =
7.188 - [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
7.189 + [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
7.190 remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
7.191 remote_e_tofof, remote_waldmeister]
7.192 val setup = fold add_atp atps
8.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:33:24 2011 +0200
8.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 17:02:06 2011 +0200
8.3 @@ -16,8 +16,8 @@
8.4 type 'a problem = 'a ATP_Problem.problem
8.5
8.6 datatype locality =
8.7 - General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
8.8 - Chained
8.9 + General | Helper | Induction | Extensionality | Intro | Elim | Simp |
8.10 + Local | Assum | Chained
8.11
8.12 datatype order = First_Order | Higher_Order
8.13 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
8.14 @@ -31,7 +31,7 @@
8.15 datatype type_uniformity = Uniform | Nonuniform
8.16
8.17 datatype type_enc =
8.18 - Simple_Types of order * type_level |
8.19 + Simple_Types of order * polymorphism * type_level |
8.20 Guards of polymorphism * type_level * type_uniformity |
8.21 Tags of polymorphism * type_level * type_uniformity
8.22
8.23 @@ -311,14 +311,19 @@
8.24 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
8.25
8.26 fun make_schematic_type_var (x, i) =
8.27 - tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
8.28 + tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
8.29 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
8.30
8.31 -(* "HOL.eq" is mapped to the ATP's equality. *)
8.32 -fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
8.33 - | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
8.34 - tptp_choice
8.35 - | make_fixed_const _ c = const_prefix ^ lookup_const c
8.36 +(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
8.37 +local
8.38 + val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
8.39 + fun default c = const_prefix ^ lookup_const c
8.40 +in
8.41 + fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
8.42 + | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
8.43 + if c = choice_const then tptp_choice else default c
8.44 + | make_fixed_const _ c = default c
8.45 +end
8.46
8.47 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
8.48
8.49 @@ -367,9 +372,6 @@
8.50 TConsLit of name * name * name list |
8.51 TVarLit of name * name
8.52
8.53 -fun gen_TVars 0 = []
8.54 - | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
8.55 -
8.56 val type_class = the_single @{sort type}
8.57
8.58 fun add_packed_sort tvar =
8.59 @@ -383,13 +385,12 @@
8.60 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
8.61 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
8.62 let
8.63 - val tvars = gen_TVars (length args)
8.64 + val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
8.65 val tvars_srts = ListPair.zip (tvars, args)
8.66 in
8.67 {name = name,
8.68 prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
8.69 - concl_lits = TConsLit (`make_type_class cls,
8.70 - `make_fixed_type_const tcons,
8.71 + concl_lits = TConsLit (`make_type_class cls, `make_fixed_type_const tcons,
8.72 tvars ~~ tvars)}
8.73 end
8.74
8.75 @@ -490,6 +491,15 @@
8.76 [new_skolem_const_prefix, s, string_of_int num_T_args]
8.77 |> space_implode Long_Name.separator
8.78
8.79 +fun robust_const_type thy s =
8.80 + if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
8.81 + else s |> Sign.the_const_type thy
8.82 +
8.83 +(* This function only makes sense if "T" is as general as possible. *)
8.84 +fun robust_const_typargs thy (s, T) =
8.85 + (s, T) |> Sign.const_typargs thy
8.86 + handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar
8.87 +
8.88 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
8.89 Also accumulates sort infomation. *)
8.90 fun iterm_from_term thy format bs (P $ Q) =
8.91 @@ -499,10 +509,7 @@
8.92 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
8.93 | iterm_from_term thy format _ (Const (c, T)) =
8.94 (IConst (`(make_fixed_const (SOME format)) c, T,
8.95 - if String.isPrefix old_skolem_const_prefix c then
8.96 - [] |> Term.add_tvarsT T |> map TVar
8.97 - else
8.98 - (c, T) |> Sign.const_typargs thy),
8.99 + robust_const_typargs thy (c, T)),
8.100 atyps_of T)
8.101 | iterm_from_term _ _ _ (Free (s, T)) =
8.102 (IConst (`make_fixed_var s, T,
8.103 @@ -527,8 +534,8 @@
8.104 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
8.105
8.106 datatype locality =
8.107 - General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
8.108 - Chained
8.109 + General | Helper | Induction | Extensionality | Intro | Elim | Simp |
8.110 + Local | Assum | Chained
8.111
8.112 datatype order = First_Order | Higher_Order
8.113 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
8.114 @@ -542,7 +549,7 @@
8.115 datatype type_uniformity = Uniform | Nonuniform
8.116
8.117 datatype type_enc =
8.118 - Simple_Types of order * type_level |
8.119 + Simple_Types of order * polymorphism * type_level |
8.120 Guards of polymorphism * type_level * type_uniformity |
8.121 Tags of polymorphism * type_level * type_uniformity
8.122
8.123 @@ -574,12 +581,15 @@
8.124 | NONE => (Nonuniform, s))
8.125 |> (fn (poly, (level, (uniformity, core))) =>
8.126 case (core, (poly, level, uniformity)) of
8.127 - ("simple", (NONE, _, Nonuniform)) =>
8.128 - Simple_Types (First_Order, level)
8.129 - | ("simple_higher", (NONE, _, Nonuniform)) =>
8.130 - (case level of
8.131 - Noninf_Nonmono_Types _ => raise Same.SAME
8.132 - | _ => Simple_Types (Higher_Order, level))
8.133 + ("simple", (SOME poly, _, Nonuniform)) =>
8.134 + (case poly of
8.135 + Raw_Monomorphic => raise Same.SAME
8.136 + | _ => Simple_Types (First_Order, poly, level))
8.137 + | ("simple_higher", (SOME poly, _, Nonuniform)) =>
8.138 + (case (poly, level) of
8.139 + (Raw_Monomorphic, _) => raise Same.SAME
8.140 + | (_, Noninf_Nonmono_Types _) => raise Same.SAME
8.141 + | _ => Simple_Types (Higher_Order, poly, level))
8.142 | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
8.143 | ("tags", (SOME Polymorphic, _, _)) =>
8.144 Tags (Polymorphic, level, uniformity)
8.145 @@ -591,14 +601,14 @@
8.146 | _ => raise Same.SAME)
8.147 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
8.148
8.149 -fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
8.150 +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
8.151 | is_type_enc_higher_order _ = false
8.152
8.153 -fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
8.154 +fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
8.155 | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
8.156 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
8.157
8.158 -fun level_of_type_enc (Simple_Types (_, level)) = level
8.159 +fun level_of_type_enc (Simple_Types (_, _, level)) = level
8.160 | level_of_type_enc (Guards (_, level, _)) = level
8.161 | level_of_type_enc (Tags (_, level, _)) = level
8.162
8.163 @@ -620,11 +630,15 @@
8.164 | is_type_level_monotonicity_based Fin_Nonmono_Types = true
8.165 | is_type_level_monotonicity_based _ = false
8.166
8.167 -fun adjust_type_enc (THF _) type_enc = type_enc
8.168 - | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
8.169 - Simple_Types (First_Order, level)
8.170 - | adjust_type_enc format (Simple_Types (_, level)) =
8.171 - adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
8.172 +fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
8.173 + Simple_Types (order, Mangled_Monomorphic, level)
8.174 + | adjust_type_enc (THF0 _) type_enc = type_enc
8.175 + | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
8.176 + Simple_Types (First_Order, Mangled_Monomorphic, level)
8.177 + | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
8.178 + Simple_Types (First_Order, poly, level)
8.179 + | adjust_type_enc format (Simple_Types (_, poly, level)) =
8.180 + adjust_type_enc format (Guards (poly, level, Uniform))
8.181 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
8.182 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
8.183 | adjust_type_enc _ type_enc = type_enc
8.184 @@ -678,8 +692,7 @@
8.185 Mangled_Type_Args of bool |
8.186 No_Type_Args
8.187
8.188 -fun should_drop_arg_type_args (Simple_Types _) =
8.189 - false (* since TFF doesn't support overloading *)
8.190 +fun should_drop_arg_type_args (Simple_Types _) = false
8.191 | should_drop_arg_type_args type_enc =
8.192 level_of_type_enc type_enc = All_Types andalso
8.193 uniformity_of_type_enc type_enc = Uniform
8.194 @@ -751,14 +764,28 @@
8.195 | iterm_vars (IAbs (_, tm)) = iterm_vars tm
8.196 fun close_iformula_universally phi = close_universally iterm_vars phi
8.197
8.198 -fun term_vars bounds (ATerm (name as (s, _), tms)) =
8.199 - (is_tptp_variable s andalso not (member (op =) bounds name))
8.200 - ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
8.201 - | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
8.202 -fun close_formula_universally phi = close_universally (term_vars []) phi
8.203 +fun term_vars type_enc =
8.204 + let
8.205 + fun vars bounds (ATerm (name as (s, _), tms)) =
8.206 + (if is_tptp_variable s andalso not (member (op =) bounds name) then
8.207 + (case type_enc of
8.208 + Simple_Types (_, Polymorphic, _) =>
8.209 + if String.isPrefix tvar_prefix s then SOME atype_of_types
8.210 + else NONE
8.211 + | _ => NONE)
8.212 + |> pair name |> insert (op =)
8.213 + else
8.214 + I)
8.215 + #> fold (vars bounds) tms
8.216 + | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm
8.217 + in vars end
8.218 +fun close_formula_universally type_enc =
8.219 + close_universally (term_vars type_enc [])
8.220
8.221 -val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
8.222 -val homo_infinite_type = Type (homo_infinite_type_name, [])
8.223 +val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
8.224 +val fused_infinite_type = Type (fused_infinite_type_name, [])
8.225 +
8.226 +fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
8.227
8.228 fun ho_term_from_typ format type_enc =
8.229 let
8.230 @@ -766,15 +793,14 @@
8.231 ATerm (case (is_type_enc_higher_order type_enc, s) of
8.232 (true, @{type_name bool}) => `I tptp_bool_type
8.233 | (true, @{type_name fun}) => `I tptp_fun_type
8.234 - | _ => if s = homo_infinite_type_name andalso
8.235 + | _ => if s = fused_infinite_type_name andalso
8.236 is_format_typed format then
8.237 `I tptp_individual_type
8.238 else
8.239 `make_fixed_type_const s,
8.240 map term Ts)
8.241 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
8.242 - | term (TVar ((x as (s, _)), _)) =
8.243 - ATerm ((make_schematic_type_var x, s), [])
8.244 + | term (TVar (x, _)) = ATerm (tvar_name x, [])
8.245 in term end
8.246
8.247 fun ho_term_for_type_arg format type_enc T =
8.248 @@ -792,8 +818,6 @@
8.249 fun mangled_type format type_enc =
8.250 generic_mangled_type_name fst o ho_term_from_typ format type_enc
8.251
8.252 -val bool_atype = AType (`I tptp_bool_type)
8.253 -
8.254 fun make_simple_type s =
8.255 if s = tptp_bool_type orelse s = tptp_fun_type orelse
8.256 s = tptp_individual_type then
8.257 @@ -803,9 +827,14 @@
8.258
8.259 fun ho_type_from_ho_term type_enc pred_sym ary =
8.260 let
8.261 - fun to_atype ty =
8.262 + fun to_mangled_atype ty =
8.263 AType ((make_simple_type (generic_mangled_type_name fst ty),
8.264 - generic_mangled_type_name snd ty))
8.265 + generic_mangled_type_name snd ty), [])
8.266 + fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
8.267 + | to_poly_atype _ = raise Fail "unexpected type abstraction"
8.268 + val to_atype =
8.269 + if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
8.270 + else to_mangled_atype
8.271 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
8.272 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
8.273 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
8.274 @@ -884,19 +913,17 @@
8.275 if is_tptp_equal s andalso length args = 2 then
8.276 IConst (`I tptp_equal, T, [])
8.277 else
8.278 - (* Use a proxy even for partially applied THF equality, because
8.279 - the LEO-II and Satallax parsers complain about not being
8.280 - able to infer the type of "=". *)
8.281 + (* Use a proxy even for partially applied THF0 equality,
8.282 + because the LEO-II and Satallax parsers complain about not
8.283 + being able to infer the type of "=". *)
8.284 IConst (proxy_base |>> prefix const_prefix, T, T_args)
8.285 | _ => IConst (name, T, [])
8.286 else
8.287 IConst (proxy_base |>> prefix const_prefix, T, T_args)
8.288 | NONE => if s = tptp_choice then
8.289 - (*this could be made neater by adding c_Eps as a proxy,
8.290 - but we'd need to be able to "see" Hilbert_Choice.Eps
8.291 - at this level in order to define fEps*)
8.292 tweak_ho_quant tptp_choice T args
8.293 - else IConst (name, T, T_args))
8.294 + else
8.295 + IConst (name, T, T_args))
8.296 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
8.297 | intro _ _ tm = tm
8.298 in intro true [] end
8.299 @@ -1148,14 +1175,14 @@
8.300 | _ => false)
8.301 | should_tag_with_type _ _ _ _ _ _ = false
8.302
8.303 -fun homogenized_type ctxt mono level =
8.304 +fun fused_type ctxt mono level =
8.305 let
8.306 val should_encode = should_encode_type ctxt mono level
8.307 - fun homo 0 T = if should_encode T then T else homo_infinite_type
8.308 - | homo ary (Type (@{type_name fun}, [T1, T2])) =
8.309 - homo 0 T1 --> homo (ary - 1) T2
8.310 - | homo _ _ = raise Fail "expected function type"
8.311 - in homo end
8.312 + fun fuse 0 T = if should_encode T then T else fused_infinite_type
8.313 + | fuse ary (Type (@{type_name fun}, [T1, T2])) =
8.314 + fuse 0 T1 --> fuse (ary - 1) T2
8.315 + | fuse _ _ = raise Fail "expected function type"
8.316 + in fuse end
8.317
8.318 (** predicators and application operators **)
8.319
8.320 @@ -1332,13 +1359,7 @@
8.321
8.322 fun filter_type_args _ _ _ [] = []
8.323 | filter_type_args thy s arity T_args =
8.324 - let
8.325 - (* will throw "TYPE" for pseudo-constants *)
8.326 - val U = if s = app_op_name then
8.327 - @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
8.328 - else
8.329 - s |> Sign.the_const_type thy
8.330 - in
8.331 + let val U = robust_const_type thy s in
8.332 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
8.333 [] => []
8.334 | res_U_vars =>
8.335 @@ -1444,7 +1465,7 @@
8.336 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
8.337 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
8.338 |> bound_tvars type_enc atomic_Ts
8.339 - |> close_formula_universally
8.340 + |> close_formula_universally type_enc
8.341
8.342 val type_tag = `(make_fixed_const NONE) type_tag_name
8.343
8.344 @@ -1589,8 +1610,8 @@
8.345 else make_arity_clauses thy tycons supers
8.346 val class_rel_clauses = make_class_rel_clauses thy subs supers
8.347 in
8.348 - (fact_names |> map single,
8.349 - (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
8.350 + (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
8.351 + class_rel_clauses, arity_clauses)
8.352 end
8.353
8.354 val type_guard = `(make_fixed_const NONE) type_guard_name
8.355 @@ -1659,8 +1680,7 @@
8.356 val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
8.357 val do_bound_type =
8.358 case type_enc of
8.359 - Simple_Types (_, level) =>
8.360 - homogenized_type ctxt mono level 0
8.361 + Simple_Types (_, _, level) => fused_type ctxt mono level 0
8.362 #> ho_type_from_typ format type_enc false 0 #> SOME
8.363 | _ => K NONE
8.364 fun do_out_of_bound_type pos phi universal (name, T) =
8.365 @@ -1707,7 +1727,7 @@
8.366 should_guard_var_in_formula
8.367 (if pos then SOME true else NONE)
8.368 |> bound_tvars type_enc atomic_types
8.369 - |> close_formula_universally,
8.370 + |> close_formula_universally type_enc,
8.371 NONE,
8.372 case locality of
8.373 Intro => isabelle_info introN
8.374 @@ -1716,13 +1736,13 @@
8.375 | _ => NONE)
8.376 |> Formula
8.377
8.378 -fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
8.379 - : class_rel_clause) =
8.380 - let val ty_arg = ATerm (`I "T", []) in
8.381 +fun formula_line_for_class_rel_clause type_enc
8.382 + ({name, subclass, superclass, ...} : class_rel_clause) =
8.383 + let val ty_arg = ATerm ((make_schematic_type_var ("'a", 0), "'a"), []) in
8.384 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
8.385 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
8.386 AAtom (ATerm (superclass, [ty_arg]))])
8.387 - |> close_formula_universally, isabelle_info introN, NONE)
8.388 + |> close_formula_universally type_enc, isabelle_info introN, NONE)
8.389 end
8.390
8.391 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
8.392 @@ -1730,14 +1750,14 @@
8.393 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
8.394 (false, ATerm (c, [ATerm (sort, [])]))
8.395
8.396 -fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
8.397 - : arity_clause) =
8.398 +fun formula_line_for_arity_clause type_enc
8.399 + ({name, prem_lits, concl_lits, ...} : arity_clause) =
8.400 Formula (arity_clause_prefix ^ name, Axiom,
8.401 mk_ahorn (map (formula_from_fo_literal o apfst not
8.402 o fo_literal_from_arity_literal) prem_lits)
8.403 (formula_from_fo_literal
8.404 (fo_literal_from_arity_literal concl_lits))
8.405 - |> close_formula_universally, isabelle_info introN, NONE)
8.406 + |> close_formula_universally type_enc, isabelle_info introN, NONE)
8.407
8.408 fun formula_line_for_conjecture ctxt format mono type_enc
8.409 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
8.410 @@ -1746,7 +1766,7 @@
8.411 should_guard_var_in_formula (SOME false)
8.412 (close_iformula_universally iformula)
8.413 |> bound_tvars type_enc atomic_types
8.414 - |> close_formula_universally, NONE, NONE)
8.415 + |> close_formula_universally type_enc, NONE, NONE)
8.416
8.417 fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
8.418 atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
8.419 @@ -1763,11 +1783,15 @@
8.420
8.421 (** Symbol declarations **)
8.422
8.423 -fun should_declare_sym type_enc pred_sym s =
8.424 - (case type_enc of
8.425 - Guards _ => not pred_sym
8.426 - | _ => true) andalso
8.427 - is_tptp_user_symbol s
8.428 +fun decl_line_for_class s =
8.429 + let val name as (s, _) = `make_type_class s in
8.430 + Decl (sym_decl_prefix ^ s, name, AFun (atype_of_types, bool_atype))
8.431 + end
8.432 +
8.433 +fun decl_lines_for_classes type_enc classes =
8.434 + case type_enc of
8.435 + Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
8.436 + | _ => []
8.437
8.438 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
8.439 (conjs, facts) =
8.440 @@ -1776,8 +1800,15 @@
8.441 let val (head, args) = strip_iterm_comb tm in
8.442 (case head of
8.443 IConst ((s, s'), T, T_args) =>
8.444 - let val pred_sym = is_pred_sym repaired_sym_tab s in
8.445 - if should_declare_sym type_enc pred_sym s then
8.446 + let
8.447 + val pred_sym = is_pred_sym repaired_sym_tab s
8.448 + val decl_sym =
8.449 + (case type_enc of
8.450 + Guards _ => not pred_sym
8.451 + | _ => true) andalso
8.452 + is_tptp_user_symbol s
8.453 + in
8.454 + if decl_sym then
8.455 Symtab.map_default (s, [])
8.456 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
8.457 in_conj))
8.458 @@ -1911,7 +1942,7 @@
8.459 |> formula_from_iformula ctxt format mono type_enc
8.460 (K (K (K (K true)))) (SOME true)
8.461 |> bound_tvars type_enc (atyps_of T)
8.462 - |> close_formula_universally,
8.463 + |> close_formula_universally type_enc,
8.464 isabelle_info introN, NONE)
8.465
8.466 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
8.467 @@ -1935,14 +1966,28 @@
8.468 fun decl_line_for_sym ctxt format mono type_enc s
8.469 (s', T_args, T, pred_sym, ary, _) =
8.470 let
8.471 - val (T_arg_Ts, level) =
8.472 - case type_enc of
8.473 - Simple_Types (_, level) => ([], level)
8.474 - | _ => (replicate (length T_args) homo_infinite_type, No_Types)
8.475 + val thy = Proof_Context.theory_of ctxt
8.476 + val (T, T_args) =
8.477 + if null T_args then
8.478 + (T, [])
8.479 + else case strip_prefix_and_unascii const_prefix s of
8.480 + SOME s' =>
8.481 + let
8.482 + val s' = s' |> invert_const
8.483 + val T = s' |> robust_const_type thy
8.484 + in (T, robust_const_typargs thy (s', T)) end
8.485 + | NONE =>
8.486 + case strip_prefix_and_unascii fixed_var_prefix s of
8.487 + SOME s' =>
8.488 + if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
8.489 + else raise Fail "unexpected type arguments to free variable"
8.490 + | NONE => raise Fail "unexpected type arguments"
8.491 in
8.492 Decl (sym_decl_prefix ^ s, (s, s'),
8.493 - (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
8.494 - |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
8.495 + T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
8.496 + |> ho_type_from_typ format type_enc pred_sym ary
8.497 + |> not (null T_args)
8.498 + ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
8.499 end
8.500
8.501 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
8.502 @@ -1973,7 +2018,7 @@
8.503 |> formula_from_iformula ctxt format mono type_enc
8.504 (K (K (K (K true)))) (SOME true)
8.505 |> n > 1 ? bound_tvars type_enc (atyps_of T)
8.506 - |> close_formula_universally
8.507 + |> close_formula_universally type_enc
8.508 |> maybe_negate,
8.509 isabelle_info introN, NONE)
8.510 end
8.511 @@ -2127,7 +2172,7 @@
8.512 else
8.513 error ("Unknown lambda translation method: " ^
8.514 quote lambda_trans ^ ".")
8.515 - val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
8.516 + val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
8.517 translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
8.518 hyp_ts concl_t facts
8.519 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
8.520 @@ -2142,6 +2187,7 @@
8.521 val mono_Ts =
8.522 helpers @ conjs @ facts
8.523 |> monotonic_types_for_facts ctxt mono type_enc
8.524 + val class_decl_lines = decl_lines_for_classes type_enc classes
8.525 val sym_decl_lines =
8.526 (conjs, helpers @ facts)
8.527 |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
8.528 @@ -2158,14 +2204,14 @@
8.529 (* Reordering these might confuse the proof reconstruction code or the SPASS
8.530 FLOTTER hack. *)
8.531 val problem =
8.532 - [(explicit_declsN, sym_decl_lines),
8.533 + [(explicit_declsN, class_decl_lines @ sym_decl_lines),
8.534 (factsN,
8.535 map (formula_line_for_fact ctxt format fact_prefix ascii_of
8.536 - (not exporter) (not exporter) mono
8.537 - type_enc)
8.538 + (not exporter) (not exporter) mono type_enc)
8.539 (0 upto length facts - 1 ~~ facts)),
8.540 - (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
8.541 - (aritiesN, map formula_line_for_arity_clause arity_clauses),
8.542 + (class_relsN,
8.543 + map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
8.544 + (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
8.545 (helpersN, helper_lines),
8.546 (conjsN,
8.547 map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
8.548 @@ -2175,12 +2221,10 @@
8.549 |> (case format of
8.550 CNF => ensure_cnf_problem
8.551 | CNF_UEQ => filter_cnf_ueq_problem
8.552 - | _ => I)
8.553 - |> (if is_format_typed format andalso format <> TFF Implicit then
8.554 - declare_undeclared_syms_in_atp_problem type_decl_prefix
8.555 - implicit_declsN
8.556 - else
8.557 - I)
8.558 + | FOF => I
8.559 + | TFF (_, TFF_Implicit) => I
8.560 + | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
8.561 + implicit_declsN)
8.562 val (problem, pool) = problem |> nice_atp_problem readable_names
8.563 val helpers_offset = offset_of_heading_in_problem helpersN problem 0
8.564 val typed_helpers =
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Tools/ATP/scripts/dummy_atp Tue Aug 30 17:02:06 2011 +0200
9.3 @@ -0,0 +1,1 @@
9.4 +echo "SZS status Unknown"
10.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Aug 30 16:33:24 2011 +0200
10.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Aug 30 17:02:06 2011 +0200
10.3 @@ -89,12 +89,12 @@
10.4 end
10.5 |> Meson.make_meta_clause
10.6
10.7 -fun clause_params type_enc =
10.8 +val clause_params =
10.9 {ordering = Metis_KnuthBendixOrder.default,
10.10 orderLiterals = Metis_Clause.UnsignedLiteralOrder,
10.11 orderTerms = true}
10.12 -fun active_params type_enc =
10.13 - {clause = clause_params type_enc,
10.14 +val active_params =
10.15 + {clause = clause_params,
10.16 prefactor = #prefactor Metis_Active.default,
10.17 postfactor = #postfactor Metis_Active.default}
10.18 val waiting_params =
10.19 @@ -102,8 +102,7 @@
10.20 variablesWeight = 0.0,
10.21 literalsWeight = 0.0,
10.22 models = []}
10.23 -fun resolution_params type_enc =
10.24 - {active = active_params type_enc, waiting = waiting_params}
10.25 +val resolution_params = {active = active_params, waiting = waiting_params}
10.26
10.27 (* Main function to start Metis proof and reconstruction *)
10.28 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
10.29 @@ -137,7 +136,7 @@
10.30 case filter (fn t => prop_of t aconv @{prop False}) cls of
10.31 false_th :: _ => [false_th RS @{thm FalseE}]
10.32 | [] =>
10.33 - case Metis_Resolution.new (resolution_params type_enc)
10.34 + case Metis_Resolution.new resolution_params
10.35 {axioms = thms, conjecture = []}
10.36 |> Metis_Resolution.loop of
10.37 Metis_Resolution.Contradiction mth =>
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 16:33:24 2011 +0200
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 17:02:06 2011 +0200
11.3 @@ -46,13 +46,13 @@
11.4 Proof.context -> unit Symtab.table -> thm list
11.5 -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
11.6 val all_facts :
11.7 - Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
11.8 + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
11.9 -> (((unit -> string) * locality) * thm) list
11.10 val nearly_all_facts :
11.11 - Proof.context -> relevance_override -> thm list -> term list -> term
11.12 + Proof.context -> bool -> relevance_override -> thm list -> term list -> term
11.13 -> (((unit -> string) * locality) * thm) list
11.14 val relevant_facts :
11.15 - Proof.context -> real * real -> int
11.16 + Proof.context -> bool -> real * real -> int
11.17 -> (string * typ -> term list -> bool * term list) -> relevance_fudge
11.18 -> relevance_override -> thm list -> term list -> term
11.19 -> (((unit -> string) * locality) * thm) list
11.20 @@ -586,7 +586,7 @@
11.21 facts are included. *)
11.22 val special_fact_index = 75
11.23
11.24 -fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
11.25 +fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const
11.26 (fudge as {threshold_divisor, ridiculous_threshold, ...})
11.27 ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
11.28 let
11.29 @@ -729,14 +729,15 @@
11.30 (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
11.31
11.32 (* FIXME: put other record thms here, or declare as "no_atp" *)
11.33 -fun multi_base_blacklist ctxt =
11.34 +fun multi_base_blacklist ctxt ho_atp =
11.35 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
11.36 "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
11.37 "weak_case_cong"]
11.38 - |> not (Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
11.39 + |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
11.40 + append ["induct", "inducts"]
11.41 |> map (prefix ".")
11.42
11.43 -val max_lambda_nesting = 3
11.44 +val max_lambda_nesting = 3 (*only applies if not ho_atp*)
11.45
11.46 fun term_has_too_many_lambdas max (t1 $ t2) =
11.47 exists (term_has_too_many_lambdas max) [t1, t2]
11.48 @@ -746,11 +747,12 @@
11.49
11.50 (* Don't count nested lambdas at the level of formulas, since they are
11.51 quantifiers. *)
11.52 -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
11.53 - formula_has_too_many_lambdas (T :: Ts) t
11.54 - | formula_has_too_many_lambdas Ts t =
11.55 +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
11.56 + | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
11.57 + formula_has_too_many_lambdas false (T :: Ts) t
11.58 + | formula_has_too_many_lambdas _ Ts t =
11.59 if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
11.60 - exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
11.61 + exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
11.62 else
11.63 term_has_too_many_lambdas max_lambda_nesting t
11.64
11.65 @@ -762,8 +764,8 @@
11.66 | apply_depth (Abs (_, _, t)) = apply_depth t
11.67 | apply_depth _ = 0
11.68
11.69 -fun is_formula_too_complex t =
11.70 - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
11.71 +fun is_formula_too_complex ho_atp t =
11.72 + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
11.73
11.74 (* FIXME: Extend to "Meson" and "Metis" *)
11.75 val exists_sledgehammer_const =
11.76 @@ -791,11 +793,11 @@
11.77 (**** Predicates to detect unwanted facts (prolific or likely to cause
11.78 unsoundness) ****)
11.79
11.80 -fun is_theorem_bad_for_atps exporter thm =
11.81 +fun is_theorem_bad_for_atps ho_atp exporter thm =
11.82 is_metastrange_theorem thm orelse
11.83 (not exporter andalso
11.84 let val t = prop_of thm in
11.85 - is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
11.86 + is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
11.87 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
11.88 is_that_fact thm
11.89 end)
11.90 @@ -824,7 +826,7 @@
11.91 |> add Simp normalize_simp_prop snd simps
11.92 end
11.93
11.94 -fun all_facts ctxt reserved exporter add_ths chained_ths =
11.95 +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
11.96 let
11.97 val thy = Proof_Context.theory_of ctxt
11.98 val global_facts = Global_Theory.facts_of thy
11.99 @@ -834,16 +836,18 @@
11.100 fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
11.101 val is_chained = member Thm.eq_thm_prop chained_ths
11.102 val clasimpset_table = clasimpset_rule_table_of ctxt
11.103 - fun locality_of_theorem global th =
11.104 - if is_chained th then
11.105 + fun locality_of_theorem global (name: string) th =
11.106 + if String.isSubstring ".induct" name orelse(*FIXME: use structured name*)
11.107 + String.isSubstring ".inducts" name then
11.108 + Induction
11.109 + else if is_chained th then
11.110 Chained
11.111 else if global then
11.112 case Termtab.lookup clasimpset_table (prop_of th) of
11.113 SOME loc => loc
11.114 | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
11.115 else General
11.116 - else
11.117 - if is_assum th then Assum else Local
11.118 + else if is_assum th then Assum else Local
11.119 fun is_good_unnamed_local th =
11.120 not (Thm.has_name_hint th) andalso
11.121 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
11.122 @@ -860,7 +864,7 @@
11.123 (not (Config.get ctxt ignore_no_atp) andalso
11.124 is_package_def name0) orelse
11.125 exists (fn s => String.isSuffix s name0)
11.126 - (multi_base_blacklist ctxt) orelse
11.127 + (multi_base_blacklist ctxt ho_atp) orelse
11.128 String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
11.129 I
11.130 else
11.131 @@ -877,7 +881,7 @@
11.132 #> fold (fn th => fn (j, (multis, unis)) =>
11.133 (j + 1,
11.134 if not (member Thm.eq_thm_prop add_ths th) andalso
11.135 - is_theorem_bad_for_atps exporter th then
11.136 + is_theorem_bad_for_atps ho_atp exporter th then
11.137 (multis, unis)
11.138 else
11.139 let
11.140 @@ -893,7 +897,7 @@
11.141 |> (fn SOME name =>
11.142 make_name reserved multi j name
11.143 | NONE => "")),
11.144 - locality_of_theorem global th), th)
11.145 + locality_of_theorem global name0 th), th)
11.146 in
11.147 if multi then (new :: multis, unis)
11.148 else (multis, new :: unis)
11.149 @@ -911,8 +915,8 @@
11.150 fun external_frees t =
11.151 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
11.152
11.153 -fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths
11.154 - hyp_ts concl_t =
11.155 +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
11.156 + chained_ths hyp_ts concl_t =
11.157 let
11.158 val thy = Proof_Context.theory_of ctxt
11.159 val reserved = reserved_isar_keyword_table ()
11.160 @@ -926,7 +930,7 @@
11.161 maps (map (fn ((name, loc), th) => ((K name, loc), th))
11.162 o fact_from_ref ctxt reserved chained_ths) add
11.163 else
11.164 - all_facts ctxt reserved false add_ths chained_ths)
11.165 + all_facts ctxt ho_atp reserved false add_ths chained_ths)
11.166 |> Config.get ctxt instantiate_inducts
11.167 ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
11.168 |> (not (Config.get ctxt ignore_no_atp) andalso not only)
11.169 @@ -934,7 +938,7 @@
11.170 |> uniquify
11.171 end
11.172
11.173 -fun relevant_facts ctxt (threshold0, threshold1) max_relevant
11.174 +fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant
11.175 is_built_in_const fudge (override as {only, ...}) chained_ths
11.176 hyp_ts concl_t facts =
11.177 let
11.178 @@ -950,9 +954,9 @@
11.179 max_relevant = 0 then
11.180 []
11.181 else
11.182 - relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
11.183 - fudge override facts (chained_ths |> map prop_of) hyp_ts
11.184 - (concl_t |> theory_constify fudge (Context.theory_name thy)))
11.185 + relevance_filter ctxt ho_atp threshold0 decay max_relevant
11.186 + is_built_in_const fudge override facts (chained_ths |> map prop_of)
11.187 + hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy)))
11.188 |> map (apfst (apfst (fn f => f ())))
11.189 end
11.190
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 30 16:33:24 2011 +0200
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 30 17:02:06 2011 +0200
12.3 @@ -148,8 +148,8 @@
12.4 | _ => value)
12.5 | NONE => (name, value)
12.6
12.7 -(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
12.8 - correctly. *)
12.9 +(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
12.10 + handled correctly. *)
12.11 fun implode_param [s, "?"] = s ^ "?"
12.12 | implode_param [s, "!"] = s ^ "!"
12.13 | implode_param ss = space_implode " " ss
13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 16:33:24 2011 +0200
13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 17:02:06 2011 +0200
13.3 @@ -64,7 +64,7 @@
13.4 val problem_prefix : string Config.T
13.5 val measure_run_time : bool Config.T
13.6 val atp_lambda_translation : string Config.T
13.7 - val atp_readable_names : bool Config.T
13.8 + val atp_full_names : bool Config.T
13.9 val atp_sound_modulo_infiniteness : bool Config.T
13.10 val smt_triggers : bool Config.T
13.11 val smt_weights : bool Config.T
13.12 @@ -83,6 +83,7 @@
13.13 val is_metis_prover : string -> bool
13.14 val is_atp : theory -> string -> bool
13.15 val is_smt_prover : Proof.context -> string -> bool
13.16 + val is_ho_atp: Proof.context -> string -> bool
13.17 val is_unit_equational_atp : Proof.context -> string -> bool
13.18 val is_prover_supported : Proof.context -> string -> bool
13.19 val is_prover_installed : Proof.context -> string -> bool
13.20 @@ -151,15 +152,18 @@
13.21 fun is_smt_prover ctxt name =
13.22 member (op =) (SMT_Solver.available_solvers_of ctxt) name
13.23
13.24 -fun is_unit_equational_atp ctxt name =
13.25 +fun is_atp_for_format is_format ctxt name =
13.26 let val thy = Proof_Context.theory_of ctxt in
13.27 case try (get_atp thy) name of
13.28 SOME {best_slices, ...} =>
13.29 - exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
13.30 + exists (fn (_, (_, (_, format, _, _))) => is_format format)
13.31 (best_slices ctxt)
13.32 | NONE => false
13.33 end
13.34
13.35 +val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
13.36 +val is_ho_atp = is_atp_for_format is_format_thf
13.37 +
13.38 fun is_prover_supported ctxt name =
13.39 let val thy = Proof_Context.theory_of ctxt in
13.40 is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name
13.41 @@ -329,7 +333,6 @@
13.42 type prover =
13.43 params -> (string -> minimize_command) -> prover_problem -> prover_result
13.44
13.45 -
13.46 (* configuration attributes *)
13.47
13.48 (* Empty string means create files in Isabelle's temporary files directory. *)
13.49 @@ -346,8 +349,8 @@
13.50 (* In addition to being easier to read, readable names are often much shorter,
13.51 especially if types are mangled in names. This makes a difference for some
13.52 provers (e.g., E). For these reason, short names are enabled by default. *)
13.53 -val atp_readable_names =
13.54 - Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
13.55 +val atp_full_names =
13.56 + Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
13.57 val atp_sound_modulo_infiniteness =
13.58 Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
13.59 (K true)
13.60 @@ -665,7 +668,7 @@
13.61 fact_names, typed_helpers, sym_tab) =
13.62 prepare_atp_problem ctxt format conj_sym_kind prem_kind
13.63 type_enc false (Config.get ctxt atp_lambda_translation)
13.64 - (Config.get ctxt atp_readable_names) true hyp_ts concl_t
13.65 + (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
13.66 facts
13.67 fun weights () = atp_problem_weights atp_problem
13.68 val full_proof = debug orelse isar_proof
14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 16:33:24 2011 +0200
14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 17:02:06 2011 +0200
14.3 @@ -144,6 +144,9 @@
14.4 get_prover ctxt mode name params minimize_command problem
14.5 |> minimize ctxt mode name params problem
14.6
14.7 +fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
14.8 + | is_induction_fact _ = false
14.9 +
14.10 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
14.11 timeout, expect, ...})
14.12 mode minimize_command only
14.13 @@ -160,9 +163,15 @@
14.14 fun desc () =
14.15 prover_description ctxt params name num_facts subgoal subgoal_count goal
14.16 val problem =
14.17 - {state = state, goal = goal, subgoal = subgoal,
14.18 - subgoal_count = subgoal_count, facts = facts |> take num_facts,
14.19 - smt_filter = smt_filter}
14.20 + let
14.21 + val filter_induction = filter_out is_induction_fact
14.22 + in {state = state, goal = goal, subgoal = subgoal,
14.23 + subgoal_count = subgoal_count, facts =
14.24 + ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
14.25 + facts
14.26 + |> take num_facts,
14.27 + smt_filter = smt_filter}
14.28 + end
14.29 fun really_go () =
14.30 problem
14.31 |> get_minimizing_prover ctxt mode name params minimize_command
14.32 @@ -260,8 +269,9 @@
14.33 val {facts = chained_ths, goal, ...} = Proof.goal state
14.34 val chained_ths = chained_ths |> normalize_chained_theorems
14.35 val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
14.36 - val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
14.37 - concl_t
14.38 + val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
14.39 + val facts = nearly_all_facts ctxt is_ho_atp relevance_override
14.40 + chained_ths hyp_ts concl_t
14.41 val _ = () |> not blocking ? kill_provers
14.42 val _ = case find_first (not o is_prover_supported ctxt) provers of
14.43 SOME name => error ("No such prover: " ^ name ^ ".")
14.44 @@ -313,9 +323,9 @@
14.45 |> (case is_appropriate_prop of
14.46 SOME is_app => filter (is_app o prop_of o snd)
14.47 | NONE => I)
14.48 - |> relevant_facts ctxt relevance_thresholds max_max_relevant
14.49 - is_built_in_const relevance_fudge relevance_override
14.50 - chained_ths hyp_ts concl_t
14.51 + |> relevant_facts ctxt is_ho_atp relevance_thresholds
14.52 + max_max_relevant is_built_in_const relevance_fudge
14.53 + relevance_override chained_ths hyp_ts concl_t
14.54 |> tap (fn facts =>
14.55 if debug then
14.56 label ^ plural_s (length provers) ^ ": " ^
15.1 --- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 16:33:24 2011 +0200
15.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 17:02:06 2011 +0200
15.3 @@ -37,10 +37,13 @@
15.4 val relevance_fudge =
15.5 Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
15.6 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
15.7 + val is_ho_atp =
15.8 + exists (Sledgehammer_Provers.is_ho_atp ctxt)
15.9 + provers(*FIXME: duplicated from sledgehammer_run.ML*)
15.10 val facts =
15.11 - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
15.12 - hyp_ts concl_t
15.13 - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
15.14 + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
15.15 + chained_ths hyp_ts concl_t
15.16 + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
15.17 (the_default default_max_relevant max_relevant) is_built_in_const
15.18 relevance_fudge relevance_override chained_ths hyp_ts concl_t
15.19 val problem =