--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jul 01 08:13:20 2010 +0200
@@ -59,9 +59,6 @@
lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"
unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
-lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"
- using one_le_card_finite by auto
-
lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
unfolding norm_eq_sqrt_inner by simp
@@ -1648,7 +1645,7 @@
thus "x\<in>\<Inter>g" using X[THEN bspec[where x=y]] using * f by auto
qed(auto)
thus ?thesis unfolding f using mp(3)[unfolded gh] by blast qed
-qed(insert dimindex_ge_1, auto) qed(auto)
+qed(auto) qed(auto)
lemma helly: fixes f::"('a::euclidean_space) set set"
assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
@@ -2227,8 +2224,6 @@
have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:euclidean_simps)
hence "c\<noteq>{}" using c by auto
def k \<equiv> "Max (f ` c)"
- have real_dimindex_ge_1:"real (CARD('n::finite)) \<ge> 1"
- by(metis dimindex_ge_1 real_eq_of_nat real_of_nat_1 real_of_nat_le_iff)
have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
fix z assume z:"z\<in>{x - ?d..x + ?d}"
@@ -2238,7 +2233,7 @@
using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:euclidean_simps) qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
- have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 using real_dimindex_ge_1 by auto
+ have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 by auto
hence dsube:"cball x d \<subseteq> cball x e" unfolding subset_eq Ball_def mem_cball by auto
have conv:"convex_on (cball x d) f" apply(rule convex_on_subset, rule convex_on_subset[OF assms(2)]) apply(rule e(1)) using dsube by auto
hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
@@ -2519,7 +2514,7 @@
guess a using UNIV_witness[where 'a='b] ..
let ?d = "(1 - setsum (op $$ x) {..<DIM('a)}) / real (DIM('a))"
have "Min ((op $$ x) ` {..<DIM('a)}) > 0" apply(rule Min_grI) using as(1) by auto
- moreover have"?d > 0" apply(rule divide_pos_pos) using as(2) using dimindex_ge_1 by(auto simp add: Suc_le_eq)
+ moreover have"?d > 0" apply(rule divide_pos_pos) using as(2) by(auto simp add: Suc_le_eq)
ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
apply(rule_tac x="min (Min ((op $$ x) ` {..<DIM('a)})) ?D" in exI) apply rule defer apply(rule,rule) proof-
fix y assume y:"dist x y < min (Min (op $$ x ` {..<DIM('a)})) ?d"
@@ -2528,7 +2523,7 @@
using component_le_norm[of "y - x" i]
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
thus "y $$ i \<le> x $$ i + ?d" by auto qed
- also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq)
+ also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat by(auto simp add: Suc_le_eq)
finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
proof safe fix i assume i:"i<DIM('a)"
have "norm (x - y) < x$$i" apply(rule less_le_trans)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jul 01 08:13:20 2010 +0200
@@ -88,9 +88,17 @@
"a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
unfolding has_derivative_within has_derivative_at using Lim_within_open by auto
-lemma derivative_is_linear: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" shows
+lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
+proof -
+ assume "bounded_linear f"
+ then interpret f: bounded_linear f .
+ show "linear f"
+ by (simp add: f.add f.scaleR linear_def)
+qed
+
+lemma derivative_is_linear:
"(f has_derivative f') net \<Longrightarrow> linear f'"
- unfolding has_derivative_def and linear_conv_bounded_linear by auto
+ by (rule derivative_linear [THEN bounded_linear_imp_linear])
subsection {* Combining theorems. *}
@@ -166,14 +174,21 @@
using lf
by (auto simp add: linear_def algebra_simps)
-lemma has_derivative_vmul_component: fixes c::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and v::"'c::euclidean_space"
+lemma bounded_linear_euclidean_component: "bounded_linear (\<lambda>x. x $$ k)"
+ unfolding euclidean_component_def
+ by (rule inner.bounded_linear_right)
+
+lemma has_derivative_vmul_component: fixes c::"'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" and v::"'c::real_normed_vector"
assumes "(c has_derivative c') net"
shows "((\<lambda>x. c(x)$$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$$k *\<^sub>R v)) net" proof-
have *:"\<And>y. (c y $$ k *\<^sub>R v - (c (netlimit net) $$ k *\<^sub>R v + c' (y - netlimit net) $$ k *\<^sub>R v)) =
(c y $$ k - (c (netlimit net) $$ k + c' (y - netlimit net) $$ k)) *\<^sub>R v"
unfolding scaleR_left_diff_distrib scaleR_left_distrib by auto
- show ?thesis unfolding has_derivative_def and * and linear_conv_bounded_linear[symmetric]
- apply(rule,rule linear_vmul_component[of c' k v]) defer
+ show ?thesis unfolding has_derivative_def and *
+ apply (rule conjI)
+ apply (rule bounded_linear_compose [OF scaleR.bounded_linear_left])
+ apply (rule bounded_linear_compose [OF bounded_linear_euclidean_component])
+ apply (rule derivative_linear [OF assms])
apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR apply(rule Lim_vmul)
using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
apply(rule,assumption,rule disjI2,rule,rule) proof-
@@ -192,14 +207,15 @@
using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R
(c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
qed
- qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed
+ qed
+qed
-lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real" and v::"'a::euclidean_space"
+lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real"
assumes "(c has_derivative c') (at x within s)"
shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x within s)"
using has_derivative_vmul_component[OF assms, of 0 v] by auto
-lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real" and v::"'a::euclidean_space"
+lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real"
assumes "(c has_derivative c') (at x)"
shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x)"
using has_derivative_vmul_within[where s=UNIV] and assms by(auto simp add: within_UNIV)
@@ -279,9 +295,9 @@
"f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
-lemma linear_frechet_derivative: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma linear_frechet_derivative:
shows "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)"
- unfolding frechet_derivative_works has_derivative_def unfolding linear_conv_bounded_linear by auto
+ unfolding frechet_derivative_works has_derivative_def by (auto intro: bounded_linear_imp_linear)
subsection {* Differentiability implies continuity. *}
@@ -442,13 +458,13 @@
unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z - f'a z" in exI)
apply(rule has_derivative_sub) by auto
-lemma differentiable_setsum: fixes f::"'a \<Rightarrow> ('n::euclidean_space \<Rightarrow> 'n::euclidean_space)"
+lemma differentiable_setsum:
assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net" proof-
guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
thus ?thesis unfolding differentiable_def apply- apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto qed
-lemma differentiable_setsum_numseg: fixes f::"_ \<Rightarrow> ('n::euclidean_space \<Rightarrow> 'n::euclidean_space)"
+lemma differentiable_setsum_numseg:
shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
@@ -466,7 +482,7 @@
(* The general result is a bit messy because we need approachability of the *)
(* limit point from any direction. But OK for nontrivial intervals etc. *}
-lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)"
"(\<forall>i<DIM('a). \<forall>e>0. \<exists>d. 0 < abs(d) \<and> abs(d) < e \<and> (x + d *\<^sub>R basis i) \<in> s)" shows "f' = f''" proof-
note as = assms(1,2)[unfolded has_derivative_def]
@@ -491,7 +507,7 @@
unfolding dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib using i by auto qed qed
-lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+
apply(rule,rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto
@@ -499,7 +515,7 @@
lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
unfolding continuous_at Lim_at unfolding dist_nz by auto
-lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<forall>i<DIM('a). a$$i < b$$i" "x \<in> {a..b}" (is "x\<in>?I") and
"(f has_derivative f' ) (at x within {a..b})" and
"(f has_derivative f'') (at x within {a..b})"
@@ -520,29 +536,23 @@
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
unfolding mem_interval euclidean_simps basis_component using i by(auto simp add:field_simps) qed qed
-lemma frechet_derivative_unique_within_open_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+lemma frechet_derivative_unique_within_open_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "x \<in> {a<..<b}" "(f has_derivative f' ) (at x within {a<..<b})"
"(f has_derivative f'') (at x within {a<..<b})"
- shows "f' = f''" apply(rule frechet_derivative_unique_within) apply(rule assms(2-3))+ proof(rule,rule,rule,rule)
- fix e::real and i assume "e>0" and i:"i<DIM('a)"
- note * = assms(1)[unfolded mem_interval,rule_format,OF i]
- have "a $$ i < x $$ i" using * by auto
- moreover { have "a $$ i * 2 + min (x $$ i - a $$ i) e \<le> a$$i *2 + x$$i - a$$i" by auto
- also have "\<dots> = a$$i + x$$i" by auto also have "\<dots> < 2 * x$$i" using * by auto
- finally have "a $$ i * 2 + min (x $$ i - a $$ i) e < x $$ i * 2" by auto }
- moreover have "min (x $$ i - a $$ i) e \<ge> 0" using * and `e>0` by auto
- hence "x $$ i * 2 < b $$ i * 2 + min (x $$ i - a $$ i) e" using * by auto
- ultimately show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R basis i \<in> {a<..<b}"
- apply(rule_tac x="- (min (x$$i - a$$i) e) / 2" in exI)
- using `e>0` and assms(1) unfolding mem_interval euclidean_simps apply safe unfolding basis_component
- by(auto simp add:field_simps) qed
+ shows "f' = f''"
+proof -
+ from assms(1) have *: "at x within {a<..<b} = at x"
+ by (simp add: at_within_interior interior_open open_interval)
+ from assms(2,3) [unfolded *] show "f' = f''"
+ by (rule frechet_derivative_unique_at)
+qed
-lemma frechet_derivative_at: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+lemma frechet_derivative_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))"
apply(rule frechet_derivative_unique_at[of f],assumption)
unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto
-lemma frechet_derivative_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+lemma frechet_derivative_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<forall>i<DIM('a). a$$i < b$$i" "x \<in> {a..b}" "(f has_derivative f') (at x within {a.. b})"
shows "frechet_derivative f (at x within {a.. b}) = f'"
apply(rule frechet_derivative_unique_within_closed_interval[where f=f])
@@ -622,7 +632,7 @@
subsection {* In particular if we have a mapping into @{typ "real"}. *}
lemma differential_zero_maxmin:
- fixes f::"'a\<Colon>ordered_euclidean_space \<Rightarrow> real"
+ fixes f::"'a\<Colon>euclidean_space \<Rightarrow> real"
assumes "x \<in> s" "open s"
and deriv: "(f has_derivative f') (at x)"
and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
@@ -1167,8 +1177,7 @@
subsection {* Derivative with composed bilinear function. *}
-lemma has_derivative_bilinear_within: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
- and f::"'q::euclidean_space \<Rightarrow> 'm::euclidean_space"
+lemma has_derivative_bilinear_within:
assumes "(f has_derivative f') (at x within s)" "(g has_derivative g') (at x within s)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)" proof-
have "(g ---> g x) (at x within s)" apply(rule differentiable_imp_continuous_within[unfolded continuous_within])
@@ -1200,15 +1209,17 @@
using as(3)[unfolded dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps)
finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
unfolding dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed
- have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))" unfolding linear_linear linear_def
- unfolding g'.add f'.scaleR f'.add g'.scaleR
- unfolding h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right by auto
+ have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))"
+ apply (rule bounded_linear_add)
+ apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
+ apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
+ done
thus ?thesis using Lim_add[OF * **] unfolding has_derivative_within
unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
scaleR_right_diff_distrib h.zero_right h.zero_left by(auto simp add:field_simps) qed
-lemma has_derivative_bilinear_at: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space" and f::"'p::euclidean_space \<Rightarrow> 'm::euclidean_space"
+lemma has_derivative_bilinear_at:
assumes "(f has_derivative f') (at x)" "(g has_derivative g') (at x)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
using has_derivative_bilinear_within[of f f' x UNIV g g' h] unfolding within_UNIV using assms by auto
@@ -1297,7 +1308,7 @@
using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]]
unfolding has_vector_derivative_def scaleR_right_diff_distrib by auto
-lemma has_vector_derivative_bilinear_within: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
+lemma has_vector_derivative_bilinear_within:
assumes "(f has_vector_derivative f') (at x within s)" "(g has_vector_derivative g') (at x within s)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)" proof-
interpret bounded_bilinear h using assms by auto
@@ -1305,7 +1316,7 @@
unfolding o_def has_vector_derivative_def
using assms(3) unfolding scaleR_right scaleR_left scaleR_right_distrib by auto qed
-lemma has_vector_derivative_bilinear_at: fixes h::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
+lemma has_vector_derivative_bilinear_at:
assumes "(f has_vector_derivative f') (at x)" "(g has_vector_derivative g') (at x)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
apply(rule has_vector_derivative_bilinear_within[where s=UNIV, unfolded within_UNIV]) using assms by auto
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Jul 01 08:13:20 2010 +0200
@@ -7,7 +7,7 @@
theory Euclidean_Space
imports
Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
- Infinite_Set Numeral_Type
+ Infinite_Set
Inner_Product L2_Norm Convex
uses "positivstellensatz.ML" ("normarith.ML")
begin
@@ -1582,21 +1582,13 @@
independent (basis ` {..<d}) \<and>
inj_on basis {..<d}"
-definition (in real_basis) dimension :: "'a set \<Rightarrow> nat" where
+definition (in real_basis) dimension :: "'a itself \<Rightarrow> nat" where
"dimension x =
(THE d. basis ` {d..} = {0} \<and> independent (basis ` {..<d}) \<and> inj_on basis {..<d})"
syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
-translations "DIM('t)" => "CONST dimension (CONST UNIV \<Colon> 't set)"
-
-typed_print_translation {*
-let
- fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
- Syntax.const @{syntax_const "_type_dimension"} $ Syntax.term_of_typ show_sorts T;
-in [(@{const_syntax dimension}, card_univ_tr')]
-end
-*}
+translations "DIM('t)" == "CONST dimension (TYPE('t))"
lemma (in real_basis) dimensionI:
assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0}; independent (basis ` {..<d});
@@ -1891,7 +1883,7 @@
subsection {* Linearity and Bilinearity continued *}
lemma linear_bounded:
- fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
proof-
@@ -1919,7 +1911,7 @@
qed
lemma linear_bounded_pos:
- fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
proof-
@@ -1947,7 +1939,7 @@
qed
lemma linear_conv_bounded_linear:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
shows "linear f \<longleftrightarrow> bounded_linear f"
proof
assume "linear f"
@@ -1971,14 +1963,14 @@
by (simp add: f.add f.scaleR linear_def)
qed
-lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
by(rule linearI[OF assms])
lemma bilinear_bounded:
- fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::euclidean_space"
+ fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
assumes bh: "bilinear h"
shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof-
@@ -2008,7 +2000,7 @@
qed
lemma bilinear_bounded_pos:
- fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+ fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
assumes bh: "bilinear h"
shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof-
@@ -2029,7 +2021,7 @@
qed
lemma bilinear_conv_bounded_bilinear:
- fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
proof
assume "bilinear h"
@@ -2067,7 +2059,7 @@
(** move **)
lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
- apply(subst(2) span_basis[THEN sym]) unfolding basis_range by auto
+ apply(subst span_basis[THEN sym]) unfolding basis_range by auto
lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
apply(subst card_image) using basis_inj by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 08:13:20 2010 +0200
@@ -1959,20 +1959,19 @@
show "?thesis" ..
qed
+lemma at_within_interior:
+ "x \<in> interior S \<Longrightarrow> at x within S = at x"
+ by (simp add: expand_net_eq eventually_within_interior)
+
lemma lim_within_interior:
"x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
- unfolding tendsto_def by (simp add: eventually_within_interior)
+ by (simp add: at_within_interior)
lemma netlimit_within_interior:
- fixes x :: "'a::{perfect_space, real_normed_vector}"
- (* FIXME: generalize to perfect_space *)
+ fixes x :: "'a::perfect_space"
assumes "x \<in> interior S"
- shows "netlimit(at x within S) = x" (is "?lhs = ?rhs")
-proof-
- from assms obtain e::real where e:"e>0" "ball x e \<subseteq> S" using open_interior[of S] unfolding open_contains_ball using interior_subset[of S] by auto
- hence "\<not> trivial_limit (at x within S)" using islimpt_subset[of x "ball x e" S] unfolding trivial_limit_within islimpt_ball centre_in_cball by auto
- thus ?thesis using netlimit_within by auto
-qed
+ shows "netlimit (at x within S) = x"
+using assms by (simp add: at_within_interior netlimit_at)
subsection{* Boundedness. *}
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Thu Jul 01 08:13:20 2010 +0200
@@ -337,8 +337,9 @@
extract_proof_and_outcome complete res_code proof_delims
known_failures output
in (output, msecs, proof, outcome) end
+ val readable_names = debug andalso overlord
val (pool, conjecture_offset) =
- write_tptp_file (debug andalso overlord) full_types explicit_apply
+ write_tptp_file thy readable_names full_types explicit_apply
probfile clauses
val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
val result =
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 08:13:20 2010 +0200
@@ -11,15 +11,15 @@
type name = string * string
datatype kind = Axiom | Conjecture
datatype type_literal =
- TyLitVar of string * name |
- TyLitFree of string * name
+ TyLitVar of name * name |
+ TyLitFree of name * name
datatype arLit =
- TConsLit of class * string * string list
- | TVarLit of class * string
+ TConsLit of name * name * name list |
+ TVarLit of name * name
datatype arity_clause = ArityClause of
{axiom_name: string, conclLit: arLit, premLits: arLit list}
datatype classrel_clause = ClassrelClause of
- {axiom_name: string, subclass: class, superclass: class}
+ {axiom_name: string, subclass: name, superclass: name}
datatype combtyp =
TyVar of name |
TyFree of name |
@@ -39,7 +39,7 @@
val tvar_prefix: string
val tfree_prefix: string
val const_prefix: string
- val tconst_prefix: string
+ val type_const_prefix: string
val class_prefix: string
val union_all: ''a list list -> ''a list
val invert_const: string -> string
@@ -88,7 +88,7 @@
val classrel_clause_prefix = "clsrel_";
val const_prefix = "c_";
-val tconst_prefix = "tc_";
+val type_const_prefix = "tc_";
val class_prefix = "class_";
fun union_all xss = fold (union (op =)) xss []
@@ -96,7 +96,9 @@
(* Readable names for the more common symbolic functions. Do not mess with the
last nine entries of the table unless you know what you are doing. *)
val const_trans_table =
- Symtab.make [(@{const_name "op ="}, "equal"),
+ Symtab.make [(@{type_name "*"}, "prod"),
+ (@{type_name "+"}, "sum"),
+ (@{const_name "op ="}, "equal"),
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
@@ -109,9 +111,7 @@
(@{const_name COMBS}, "COMBS"),
(@{const_name True}, "True"),
(@{const_name False}, "False"),
- (@{const_name If}, "If"),
- (@{type_name "*"}, "prod"),
- (@{type_name "+"}, "sum")]
+ (@{const_name If}, "If")]
(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
@@ -195,7 +195,7 @@
fun make_fixed_const @{const_name "op ="} = "equal"
| make_fixed_const c = const_prefix ^ lookup_const c
-fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
+fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
fun make_type_class clas = class_prefix ^ ascii_of clas;
@@ -230,8 +230,8 @@
(* The first component is the type class; the second is a TVar or TFree. *)
datatype type_literal =
- TyLitVar of string * name |
- TyLitFree of string * name
+ TyLitVar of name * name |
+ TyLitFree of name * name
exception CLAUSE of string * term;
@@ -241,8 +241,8 @@
let val sorts = sorts_on_typs_aux ((x,i), ss)
in
if s = "HOL.type" then sorts
- else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
- else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
+ else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
+ else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
end;
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
@@ -256,8 +256,9 @@
(**** Isabelle arities ****)
-datatype arLit = TConsLit of class * string * string list
- | TVarLit of class * string;
+datatype arLit =
+ TConsLit of name * name * name list |
+ TVarLit of name * name
datatype arity_clause =
ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
@@ -267,24 +268,28 @@
| gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
fun pack_sort(_,[]) = []
- | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
- | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
+ | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*)
+ | pack_sort(tvar, cls::srt) =
+ (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
(*Arity of type constructor tcon :: (arg1,...,argN)res*)
fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
- let val tvars = gen_TVars (length args)
- val tvars_srts = ListPair.zip (tvars,args)
- in
- ArityClause {axiom_name = axiom_name,
- conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
- premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
- end;
+ let
+ val tvars = gen_TVars (length args)
+ val tvars_srts = ListPair.zip (tvars, args)
+ in
+ ArityClause {axiom_name = axiom_name,
+ conclLit = TConsLit (`make_type_class cls,
+ `make_fixed_type_const tcons,
+ tvars ~~ tvars),
+ premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
+ end
(**** Isabelle class relations ****)
datatype classrel_clause =
- ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
+ ClassrelClause of {axiom_name: string, subclass: name, superclass: name}
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
fun class_pairs _ [] _ = []
@@ -298,8 +303,8 @@
fun make_classrel_clause (sub,super) =
ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
ascii_of super,
- subclass = make_type_class sub,
- superclass = make_type_class super};
+ subclass = `make_type_class sub,
+ superclass = `make_type_class super};
fun make_classrel_clauses thy subs supers =
map make_classrel_clause (class_pairs thy subs supers);
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jul 01 08:13:20 2010 +0200
@@ -124,9 +124,9 @@
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
+fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
metis_lit pos s [Metis.Term.Var s']
- | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
+ | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
metis_lit pos s [Metis.Term.Fn (s',[])]
fun default_sort _ (TVar _) = false
@@ -158,10 +158,10 @@
(* ARITY CLAUSE *)
-fun m_arity_cls (TConsLit (c,t,args)) =
- metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
- | m_arity_cls (TVarLit (c,str)) =
- metis_lit false (make_type_class c) [Metis.Term.Var str];
+fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
+ metis_lit true c [Metis.Term.Fn(t, map (Metis.Term.Var o fst) args)]
+ | m_arity_cls (TVarLit ((c, _), (s, _))) =
+ metis_lit false c [Metis.Term.Var s]
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
fun arity_cls (ArityClause {conclLit, premLits, ...}) =
@@ -170,7 +170,7 @@
(* CLASSREL CLAUSE *)
-fun m_classrel_cls subclass superclass =
+fun m_classrel_cls (subclass, _) (superclass, _) =
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
@@ -228,7 +228,7 @@
SOME w => make_tvar w
| NONE => make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
- (case strip_prefix tconst_prefix x of
+ (case strip_prefix type_const_prefix x of
SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
case strip_prefix tfree_prefix x of
@@ -279,7 +279,7 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix tconst_prefix a of
+ case strip_prefix type_const_prefix a of
SOME b =>
Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
@@ -724,7 +724,7 @@
val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn TyLitFree (s, (s', _)) =>
+ app (fn TyLitFree ((s, _), (s', _)) =>
trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 01 08:13:20 2010 +0200
@@ -214,7 +214,7 @@
fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
| type_from_node tfrees (u as StrNode (a, us)) =
let val Ts = map (type_from_node tfrees) us in
- case strip_prefix tconst_prefix a of
+ case strip_prefix type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
@@ -253,17 +253,17 @@
should allow them to be inferred.*)
fun term_from_node thy full_types tfrees =
let
- fun aux opt_T args u =
+ fun aux opt_T extra_us u =
case u of
IntLeaf _ => raise NODE [u]
| StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
- | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: args) u1
+ | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
| StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1
| StrNode (a, us) =>
if a = type_wrapper_name then
case us of
- [term_u, typ_u] =>
- aux (SOME (type_from_node tfrees typ_u)) args term_u
+ [typ_u, term_u] =>
+ aux (SOME (type_from_node tfrees typ_u)) extra_us term_u
| _ => raise NODE us
else case strip_prefix const_prefix a of
SOME "equal" =>
@@ -273,31 +273,31 @@
let
val c = invert_const b
val num_type_args = num_type_args thy c
- val actual_num_type_args = if full_types then 0 else num_type_args
- val num_term_args = length us - actual_num_type_args
- val ts = map (aux NONE []) (take num_term_args us @ args)
+ val (type_us, term_us) =
+ chop (if full_types then 0 else num_type_args) us
+ (* Extra args from "hAPP" come after any arguments given directly to
+ the constant. *)
+ val term_ts = map (aux NONE []) term_us
+ val extra_ts = map (aux NONE []) extra_us
val t =
Const (c, if full_types then
case opt_T of
- SOME T => map fastype_of ts ---> T
+ SOME T => map fastype_of term_ts ---> T
| NONE =>
if num_type_args = 0 then
Sign.const_instance thy (c, [])
else
raise Fail ("no type information for " ^ quote c)
else
- (* Extra args from "hAPP" come after any arguments
- given directly to the constant. *)
if String.isPrefix skolem_theory_name c then
- map fastype_of ts ---> HOLogic.typeT
+ map fastype_of term_ts ---> HOLogic.typeT
else
Sign.const_instance thy (c,
- map (type_from_node tfrees)
- (drop num_term_args us)))
- in list_comb (t, ts) end
+ map (type_from_node tfrees) type_us))
+ in list_comb (t, term_ts @ extra_ts) end
| NONE => (* a free or schematic variable *)
let
- val ts = map (aux NONE []) (us @ args)
+ val ts = map (aux NONE []) (us @ extra_us)
val T = map fastype_of ts ---> HOLogic.typeT
val t =
case strip_prefix fixed_var_prefix a of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Thu Jul 01 08:12:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Thu Jul 01 08:13:20 2010 +0200
@@ -12,8 +12,9 @@
type hol_clause = Metis_Clauses.hol_clause
type name_pool = string Symtab.table * string Symtab.table
+ val type_wrapper_name : string
val write_tptp_file :
- bool -> bool -> bool -> Path.T
+ theory -> bool -> bool -> bool -> Path.T
-> hol_clause list * hol_clause list * hol_clause list * hol_clause list
* classrel_clause list * arity_clause list
-> name_pool option * int
@@ -25,41 +26,57 @@
open Metis_Clauses
open Sledgehammer_Util
+
+(** ATP problem **)
+
+datatype 'a atp_term = ATerm of 'a * 'a atp_term list
+type 'a atp_literal = bool * 'a atp_term
+datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list
+type 'a problem = (string * 'a problem_line list) list
+
+fun string_for_atp_term (ATerm (s, [])) = s
+ | string_for_atp_term (ATerm (s, ts)) =
+ s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")"
+fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) =
+ string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^
+ string_for_atp_term t2
+ | string_for_atp_literal (pos, t) =
+ (if pos then "" else "~ ") ^ string_for_atp_term t
+fun string_for_problem_line (Cnf (ident, kind, lits)) =
+ "cnf(" ^ ident ^ ", " ^
+ (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^
+ " (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n"
+fun strings_for_problem problem =
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n\
+ \% " ^ timestamp () ^ "\n" ::
+ maps (fn (_, []) => []
+ | (heading, lines) =>
+ "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
+ map string_for_problem_line lines) problem
+
+
+(** Nice names **)
+
type name_pool = string Symtab.table * string Symtab.table
fun empty_name_pool readable_names =
- if readable_names then SOME (`I Symtab.empty) else NONE
+ if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
fun pool_map f xs =
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
-fun translate_first_char f s =
- String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
+ unreadable "op_1", "op_2", etc., in the problem files. *)
+val reserved_nice_names = ["equal", "op"]
fun readable_name full_name s =
- let
- val s = s |> Long_Name.base_name |> Name.desymbolize false
- val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
- val s' =
- (s' |> rev
- |> implode
- |> String.translate
- (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
- else ""))
- ^ replicate_string (String.size s - length s') "_"
- val s' =
- if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
- else s'
- (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
- ("op &", "op |", etc.). *)
- val s' = if s' = "equal" orelse s' = "op" then full_name else s'
- in
- case (Char.isLower (String.sub (full_name, 0)),
- Char.isLower (String.sub (s', 0))) of
- (true, false) => translate_first_char Char.toLower s'
- | (false, true) => translate_first_char Char.toUpper s'
- | _ => s'
- end
+ if s = full_name then
+ s
+ else
+ let
+ val s = s |> Long_Name.base_name
+ |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
+ in if member (op =) reserved_nice_names s then full_name else s end
fun nice_name (full_name, _) NONE = (full_name, NONE)
| nice_name (full_name, desired_name) (SOME the_pool) =
@@ -84,228 +101,230 @@
end
in add 0 |> apsnd SOME end
-type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+fun nice_atp_term (ATerm (name, ts)) =
+ nice_name name ##>> pool_map nice_atp_term ts #>> ATerm
+fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
+fun nice_problem_line (Cnf (ident, kind, lits)) =
+ pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
+val nice_problem =
+ pool_map (fn (heading, lines) =>
+ pool_map nice_problem_line lines #>> pair heading)
+
+
+(** Sledgehammer stuff **)
val clause_prefix = "cls_"
val arity_clause_prefix = "clsarity_"
-fun paren_pack [] = ""
- | paren_pack strings = "(" ^ commas strings ^ ")"
+fun hol_ident axiom_name clause_id =
+ clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
+
+fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
+
+fun atp_term_for_combtyp (TyVar name) = ATerm (name, [])
+ | atp_term_for_combtyp (TyFree name) = ATerm (name, [])
+ | atp_term_for_combtyp (TyConstr (name, tys)) =
+ ATerm (name, map atp_term_for_combtyp tys)
+
+fun atp_term_for_combterm full_types top_level u =
+ let
+ val (head, args) = strip_combterm_comb u
+ val (x, ty_args) =
+ case head of
+ CombConst (name, _, ty_args) =>
+ if fst name = "equal" then
+ (if top_level andalso length args = 2 then name
+ else ("c_fequal", @{const_name fequal}), [])
+ else
+ (name, if full_types then [] else ty_args)
+ | CombVar (name, _) => (name, [])
+ | CombApp _ => raise Fail "impossible \"CombApp\""
+ val t = ATerm (x, map atp_term_for_combtyp ty_args @
+ map (atp_term_for_combterm full_types false) args)
+ in
+ if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t
+ else t
+ end
+
+fun atp_literal_for_literal full_types (Literal (pos, t)) =
+ (pos, atp_term_for_combterm full_types true t)
+
+fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
+ (pos, ATerm (class, [ATerm (name, [])]))
+ | atp_literal_for_type_literal pos (TyLitFree (class, name)) =
+ (pos, ATerm (class, [ATerm (name, [])]))
+
+fun atp_literals_for_axiom full_types
+ (HOLClause {literals, ctypes_sorts, ...}) =
+ map (atp_literal_for_literal full_types) literals @
+ map (atp_literal_for_type_literal false)
+ (type_literals_for_types ctypes_sorts)
+
+fun problem_line_for_axiom full_types
+ (clause as HOLClause {axiom_name, clause_id, kind, ...}) =
+ Cnf (hol_ident axiom_name clause_id, kind,
+ atp_literals_for_axiom full_types clause)
+
+fun problem_line_for_classrel
+ (ClassrelClause {axiom_name, subclass, superclass, ...}) =
+ let val ty_arg = ATerm (("T", "T"), []) in
+ Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
+ (true, ATerm (superclass, [ty_arg]))])
+ end
+
+fun atp_literal_for_arity_literal (TConsLit (c, t, args)) =
+ (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
+ | atp_literal_for_arity_literal (TVarLit (c, sort)) =
+ (false, ATerm (c, [ATerm (sort, [])]))
+
+fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) =
+ Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+ map atp_literal_for_arity_literal (conclLit :: premLits))
+
+fun problem_line_for_conjecture full_types
+ (clause as HOLClause {axiom_name, clause_id, kind, literals, ...}) =
+ Cnf (hol_ident axiom_name clause_id, kind,
+ map (atp_literal_for_literal full_types) literals)
+
+fun atp_free_type_literals_for_conjecture (HOLClause {ctypes_sorts, ...}) =
+ map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
-fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
- | string_of_fol_type (TyFree sp) pool = nice_name sp pool
- | string_of_fol_type (TyConstr (sp, tys)) pool =
- let
- val (s, pool) = nice_name sp pool
- val (ss, pool) = pool_map string_of_fol_type tys pool
- in (s ^ paren_pack ss, pool) end
+fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
+fun problem_lines_for_free_types conjectures =
+ let
+ val litss = map atp_free_type_literals_for_conjecture conjectures
+ val lits = fold (union (op =)) litss []
+ in map problem_line_for_free_type lits end
+
+(** "hBOOL" and "hAPP" **)
+
+type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+
+fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+
+fun consider_term top_level (ATerm ((s, _), ts)) =
+ (if is_atp_variable s then
+ I
+ else
+ let val n = length ts in
+ Symtab.map_default
+ (s, {min_arity = n, max_arity = 0, sub_level = false})
+ (fn {min_arity, max_arity, sub_level} =>
+ {min_arity = Int.min (n, min_arity),
+ max_arity = Int.max (n, max_arity),
+ sub_level = sub_level orelse not top_level})
+ end)
+ #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
+fun consider_literal (_, t) = consider_term true t
+fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
+val consider_problem = fold (fold consider_problem_line o snd)
+
+fun const_table_for_problem explicit_apply problem =
+ if explicit_apply then NONE
+ else SOME (Symtab.empty |> consider_problem problem)
+
+val tc_fun = make_fixed_type_const @{type_name fun}
+
+fun min_arity_of thy full_types NONE s =
+ (if s = "equal" orelse s = type_wrapper_name orelse
+ String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s then
+ 16383 (* large number *)
+ else if full_types then
+ 0
+ else case strip_prefix const_prefix s of
+ SOME s' => num_type_args thy (invert_const s')
+ | NONE => 0)
+ | min_arity_of _ _ (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME ({min_arity, ...} : const_info) => min_arity
+ | NONE => 0
+
+fun full_type_of (ATerm ((s, _), [ty, _])) =
+ if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
+ | full_type_of _ = raise Fail "expected type wrapper"
+
+fun list_hAPP_rev _ t1 [] = t1
+ | list_hAPP_rev NONE t1 (t2 :: ts2) =
+ ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
+ | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
+ let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
+ [full_type_of t2, ty]) in
+ ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
+ end
+
+fun repair_applications_in_term thy full_types const_tab =
+ let
+ fun aux opt_ty (ATerm (name as (s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
+ | _ => raise Fail "malformed type wrapper"
+ else
+ let
+ val ts = map (aux NONE) ts
+ val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
+ in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
+ in aux NONE end
+
+fun boolify t = ATerm (`I "hBOOL", [t])
(* True if the constant ever appears outside of the top-level position in
literals, or if it appears with different arities (e.g., because of different
type instantiations). If false, the constant always receives all of its
arguments and is used as a predicate. *)
-fun needs_hBOOL NONE _ = true
- | needs_hBOOL (SOME the_const_tab) c =
- case Symtab.lookup the_const_tab c of
- SOME ({min_arity, max_arity, sub_level} : const_info) =>
- sub_level orelse min_arity < max_arity
+fun is_predicate NONE s =
+ s = "equal" orelse String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s
+ | is_predicate (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME {min_arity, max_arity, sub_level} =>
+ not sub_level andalso min_arity = max_arity
| NONE => false
-fun head_needs_hBOOL const_tab (CombConst ((c, _), _, _)) =
- needs_hBOOL const_tab c
- | head_needs_hBOOL _ _ = true
-
-fun wrap_type full_types (s, ty) pool =
- if full_types then
- let val (s', pool) = string_of_fol_type ty pool in
- (type_wrapper_name ^ paren_pack [s, s'], pool)
- end
+fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [_, t' as ATerm ((s', _), _)] =>
+ if is_predicate const_tab s' then t' else boolify t
+ | _ => raise Fail "malformed type wrapper"
else
- (s, pool)
-
-fun wrap_type_if (full_types, const_tab) (head, s, tp) =
- if head_needs_hBOOL const_tab head then wrap_type full_types (s, tp)
- else pair s
-
-fun apply ss = "hAPP" ^ paren_pack ss;
-
-fun rev_apply (v, []) = v
- | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
-
-fun string_apply (v, args) = rev_apply (v, rev args)
-
-fun min_arity_of NONE _ = 0
- | min_arity_of (SOME the_const_tab) c =
- case Symtab.lookup the_const_tab c of
- SOME ({min_arity, ...} : const_info) => min_arity
- | NONE => 0
-
-(* Apply an operator to the argument strings, using either the "apply" operator
- or direct function application. *)
-fun string_of_application (full_types, const_tab)
- (CombConst ((s, s'), _, tvars), args) pool =
- let
- val s = if s = "equal" then "c_fequal" else s
- val nargs = min_arity_of const_tab s
- val args1 = List.take (args, nargs)
- handle Subscript =>
- raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
- " but is applied to " ^ commas (map quote args))
- val args2 = List.drop (args, nargs)
- val (targs, pool) = if full_types then ([], pool)
- else pool_map string_of_fol_type tvars pool
- val (s, pool) = nice_name (s, s') pool
- in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
- | string_of_application _ (CombVar (name, _), args) pool =
- nice_name name pool |>> (fn s => string_apply (s, args))
+ t |> not (is_predicate const_tab s) ? boolify
-fun string_of_combterm params t pool =
- let
- val (head, args) = strip_combterm_comb t
- val (ss, pool) = pool_map (string_of_combterm params) args pool
- val (s, pool) = string_of_application params (head, ss) pool
- in wrap_type_if params (head, s, type_of_combterm t) pool end
-
-(*Boolean-valued terms are here converted to literals.*)
-fun boolify params c =
- string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
-
-fun string_of_predicate (params as (_, const_tab)) t =
- case #1 (strip_combterm_comb t) of
- CombConst ((s, _), _, _) =>
- (if needs_hBOOL const_tab s then boolify else string_of_combterm) params t
- | _ => boolify params t
-
-fun tptp_of_equality params pos (t1, t2) =
- pool_map (string_of_combterm params) [t1, t2]
- #>> space_implode (if pos then " = " else " != ")
-
-fun tptp_sign true s = s
- | tptp_sign false s = "~ " ^ s
+fun repair_literal thy full_types const_tab (pos, t) =
+ (pos, t |> repair_applications_in_term thy full_types const_tab
+ |> repair_predicates_in_term const_tab)
+fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
+ Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
+val repair_problem_with_const_table = map o apsnd o map ooo repair_problem_line
-fun tptp_literal params
- (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
- t2))) =
- tptp_of_equality params pos (t1, t2)
- | tptp_literal params (Literal (pos, pred)) =
- string_of_predicate params pred #>> tptp_sign pos
-
-fun tptp_of_type_literal pos (TyLitVar (s, name)) =
- nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
- | tptp_of_type_literal pos (TyLitFree (s, name)) =
- nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
-
-(* Given a clause, returns its literals paired with a list of literals
- concerning TFrees; the latter should only occur in conjecture clauses. *)
-fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
- pool =
- let
- val (lits, pool) = pool_map (tptp_literal params) literals pool
- val (tylits, pool) = pool_map (tptp_of_type_literal pos)
- (type_literals_for_types ctypes_sorts) pool
- in ((lits, tylits), pool) end
-
-fun tptp_cnf name kind formula =
- "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
+fun repair_problem thy full_types explicit_apply problem =
+ repair_problem_with_const_table thy full_types
+ (const_table_for_problem explicit_apply problem) problem
-fun tptp_raw_clause strings = "(" ^ space_implode " | " strings ^ ")"
-
-val tptp_tfree_clause =
- tptp_cnf "tfree_tcs" "negated_conjecture" o tptp_raw_clause o single
-
-fun tptp_classrel_literals sub sup =
- let val tvar = "(T)" in
- tptp_raw_clause [tptp_sign false (sub ^ tvar), tptp_sign true (sup ^ tvar)]
- end
-
-fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
- pool =
+fun write_tptp_file thy readable_names full_types explicit_apply file
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses,
+ classrel_clauses, arity_clauses) =
let
- val ((lits, tylits), pool) =
- tptp_type_literals params (kind = Conjecture) cls pool
- val name = clause_prefix ^ ascii_of axiom_name ^ "_" ^
- Int.toString clause_id
- val cnf =
- case kind of
- Axiom => tptp_cnf name "axiom" (tptp_raw_clause (tylits @ lits))
- | Conjecture => tptp_cnf name "negated_conjecture" (tptp_raw_clause lits)
- in ((cnf, tylits), pool) end
-
-fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
- ...}) =
- tptp_cnf axiom_name "axiom" (tptp_classrel_literals subclass superclass)
-
-fun tptp_of_arity_literal (TConsLit (c, t, args)) =
- tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
- | tptp_of_arity_literal (TVarLit (c, str)) =
- tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
-
-fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
- tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
- (tptp_raw_clause (map tptp_of_arity_literal (conclLit :: premLits)))
-
-(* Find the minimal arity of each function mentioned in the term. Also, note
- which uses are not at top level, to see if "hBOOL" is needed. *)
-fun count_constants_term top_level t =
- let val (head, args) = strip_combterm_comb t in
- (case head of
- CombConst ((a, _), _, _) =>
- let
- (* Predicate or function version of "equal"? *)
- val a = if a = "equal" andalso not top_level then "c_fequal" else a
- val n = length args
- in
- Symtab.map_default
- (a, {min_arity = n, max_arity = 0, sub_level = false})
- (fn {min_arity, max_arity, sub_level} =>
- {min_arity = Int.min (n, min_arity),
- max_arity = Int.max (n, max_arity),
- sub_level = sub_level orelse not top_level})
- end
- | _ => I)
- #> fold (count_constants_term false) args
- end
-fun count_constants_literal (Literal (_, t)) = count_constants_term true t
-fun count_constants_clause (HOLClause {literals, ...}) =
- fold count_constants_literal literals
-fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
- fold (fold count_constants_clause)
- [conjectures, extra_clauses, helper_clauses]
-
-fun write_tptp_file readable_names full_types explicit_apply file clauses =
- let
- fun section _ [] = []
- | section name ss =
- "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
- ")\n" :: ss
- val pool = empty_name_pool readable_names
- val (conjectures, axclauses, _, helper_clauses,
- classrel_clauses, arity_clauses) = clauses
- val const_tab = if explicit_apply then NONE
- else SOME (Symtab.empty |> count_constants clauses)
- val params = (full_types, const_tab)
- val ((conjecture_clss, tfree_litss), pool) =
- pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
- val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
- val (ax_clss, pool) =
- pool_map (apfst fst oo tptp_clause params) axclauses pool
- val classrel_clss = map tptp_classrel_clause classrel_clauses
- val arity_clss = map tptp_arity_clause arity_clauses
- val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
- helper_clauses pool
+ val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
+ val classrel_lines = map problem_line_for_classrel classrel_clauses
+ val arity_lines = map problem_line_for_arity arity_clauses
+ val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
+ val conjecture_lines =
+ map (problem_line_for_conjecture full_types) conjectures
+ val tfree_lines = problem_lines_for_free_types conjectures
+ val problem = [("Relevant facts", axiom_lines),
+ ("Class relationships", classrel_lines),
+ ("Arity declarations", arity_lines),
+ ("Helper facts", helper_lines),
+ ("Conjectures", conjecture_lines),
+ ("Type variables", tfree_lines)]
+ |> repair_problem thy full_types explicit_apply
+ val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
val conjecture_offset =
- length ax_clss + length classrel_clss + length arity_clss
- + length helper_clss
- val _ =
- File.write_list file
- ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
- section "Relevant fact" ax_clss @
- section "Class relationship" classrel_clss @
- section "Arity declaration" arity_clss @
- section "Helper fact" helper_clss @
- section "Conjecture" conjecture_clss @
- section "Type variable" tfree_clss)
+ length axiom_lines + length classrel_lines + length arity_lines
+ + length helper_lines
+ val _ = File.write_list file (strings_for_problem problem)
in (pool, conjecture_offset) end
end;