--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 20:31:22 2013 +0100
@@ -3284,7 +3284,7 @@
have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
then obtain u v where obt:"u\<in>convex hull s" "v\<in>convex hull s"
"\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull s. norm (x - y) \<le> norm (u - v)"
- using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by auto
+ using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by (auto simp: dist_norm)
thus ?thesis proof(cases "u\<notin>s \<or> v\<notin>s", erule_tac disjE)
assume "u\<notin>s" then obtain y where "y\<in>convex hull s" "norm (u - v) < norm (y - v)"
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 18 20:31:22 2013 +0100
@@ -9,7 +9,6 @@
theory Topology_Euclidean_Space
imports
Complex_Main
- "~~/src/HOL/Library/Diagonal_Subsequence"
"~~/src/HOL/Library/Countable_Set"
"~~/src/HOL/Library/Glbs"
"~~/src/HOL/Library/FuncSet"
@@ -17,9 +16,18 @@
Norm_Arith
begin
+lemma dist_0_norm:
+ fixes x :: "'a::real_normed_vector"
+ shows "dist 0 x = norm x"
+unfolding dist_norm by simp
+
lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
using dist_triangle[of y z x] by (simp add: dist_commute)
+(* LEGACY *)
+lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
+ by (rule LIMSEQ_subseq_LIMSEQ)
+
(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
apply (frule isGlb_isLb)
@@ -2223,6 +2231,9 @@
apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
by metis arith
+lemma Bseq_eq_bounded: "Bseq f \<longleftrightarrow> bounded (range f)"
+ unfolding Bseq_def bounded_pos by auto
+
lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
by (metis Int_lower1 Int_lower2 bounded_subset)
@@ -3219,88 +3230,24 @@
using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
qed
-lemma lim_subseq:
- "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
-unfolding tendsto_def eventually_sequentially o_def
-by (metis seq_suble le_trans)
-
-lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
- unfolding Ex1_def
- apply (rule_tac x="nat_rec e f" in exI)
- apply (rule conjI)+
-apply (rule def_nat_rec_0, simp)
-apply (rule allI, rule def_nat_rec_Suc, simp)
-apply (rule allI, rule impI, rule ext)
-apply (erule conjE)
-apply (induct_tac x)
-apply simp
-apply (erule_tac x="n" in allE)
-apply (simp)
-done
-
-lemma convergent_bounded_increasing: fixes s ::"nat\<Rightarrow>real"
- assumes "incseq s" and "\<forall>n. abs(s n) \<le> b"
- shows "\<exists> l. \<forall>e::real>0. \<exists> N. \<forall>n \<ge> N. abs(s n - l) < e"
-proof-
- have "isUb UNIV (range s) b" using assms(2) and abs_le_D1 unfolding isUb_def and setle_def by auto
- then obtain t where t:"isLub UNIV (range s) t" using reals_complete[of "range s" ] by auto
- { fix e::real assume "e>0" and as:"\<forall>N. \<exists>n\<ge>N. \<not> \<bar>s n - t\<bar> < e"
- { fix n::nat
- obtain N where "N\<ge>n" and n:"\<bar>s N - t\<bar> \<ge> e" using as[THEN spec[where x=n]] by auto
- have "t \<ge> s N" using isLub_isUb[OF t, unfolded isUb_def setle_def] by auto
- with n have "s N \<le> t - e" using `e>0` by auto
- hence "s n \<le> t - e" using assms(1)[unfolded incseq_def, THEN spec[where x=n], THEN spec[where x=N]] using `n\<le>N` by auto }
- hence "isUb UNIV (range s) (t - e)" unfolding isUb_def and setle_def by auto
- hence False using isLub_le_isUb[OF t, of "t - e"] and `e>0` by auto }
- thus ?thesis by blast
-qed
-
-lemma convergent_bounded_monotone: fixes s::"nat \<Rightarrow> real"
- assumes "\<forall>n. abs(s n) \<le> b" and "monoseq s"
- shows "\<exists>l. \<forall>e::real>0. \<exists>N. \<forall>n\<ge>N. abs(s n - l) < e"
- using convergent_bounded_increasing[of s b] assms using convergent_bounded_increasing[of "\<lambda>n. - s n" b]
- unfolding monoseq_def incseq_def
- apply auto unfolding minus_add_distrib[THEN sym, unfolded diff_minus[THEN sym]]
- unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto
-
-(* TODO: merge this lemma with the ones above *)
-lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real"
- assumes "bounded {s n| n::nat. True}" "\<forall>n. (s n) \<le>(s(Suc n))"
- shows "\<exists>l. (s ---> l) sequentially"
-proof-
- obtain a where a:"\<forall>n. \<bar> (s n)\<bar> \<le> a" using assms(1)[unfolded bounded_iff] by auto
- { fix m::nat
- have "\<And> n. n\<ge>m \<longrightarrow> (s m) \<le> (s n)"
- apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE)
- apply(case_tac "m \<le> na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq) }
- hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto
- then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar> (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a]
- unfolding monoseq_def by auto
- thus ?thesis unfolding LIMSEQ_def apply(rule_tac x="l" in exI)
- unfolding dist_norm by auto
-qed
-
-lemma compact_real_lemma:
- assumes "\<forall>n::nat. abs(s n) \<le> b"
- shows "\<exists>(l::real) r. subseq r \<and> ((s \<circ> r) ---> l) sequentially"
-proof-
- obtain r where r:"subseq r" "monoseq (\<lambda>n. s (r n))"
- using seq_monosub[of s] by auto
- thus ?thesis using convergent_bounded_monotone[of "\<lambda>n. s (r n)" b] and assms
- unfolding tendsto_iff dist_norm eventually_sequentially by auto
-qed
+(* TODO: is this lemma necessary? *)
+lemma bounded_increasing_convergent:
+ fixes s :: "nat \<Rightarrow> real"
+ shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s (Suc n) \<Longrightarrow> \<exists>l. s ----> l"
+ using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
+ by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
instance real :: heine_borel
proof
fix s :: "real set" and f :: "nat \<Rightarrow> real"
assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
- then obtain b where b: "\<forall>n. abs (f n) \<le> b"
- unfolding bounded_iff by auto
- obtain l :: real and r :: "nat \<Rightarrow> nat" where
- r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
- using compact_real_lemma [OF b] by auto
- thus "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
- by auto
+ obtain r where r: "subseq r" "monoseq (f \<circ> r)"
+ unfolding comp_def by (metis seq_monosub)
+ moreover
+ then have "Bseq (f \<circ> r)"
+ unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
+ ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
+ using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed
lemma compact_lemma:
@@ -3406,7 +3353,7 @@
using bounded_imp_convergent_subsequence [OF s2 f2]
unfolding o_def by fast
have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
- using lim_subseq [OF r2 l1] unfolding o_def .
+ using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially"
using tendsto_Pair [OF l1' l2] unfolding o_def by simp
have r: "subseq (r1 \<circ> r2)"
@@ -3417,10 +3364,120 @@
subsubsection{* Completeness *}
-definition
- complete :: "'a::metric_space set \<Rightarrow> bool" where
- "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f
- --> (\<exists>l \<in> s. (f ---> l) sequentially))"
+definition complete :: "'a::metric_space set \<Rightarrow> bool" where
+ "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
+
+lemma compact_imp_complete: assumes "compact s" shows "complete s"
+proof-
+ { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
+ from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) ----> l"
+ using assms unfolding compact_def by blast
+
+ note lr' = seq_suble [OF lr(2)]
+
+ { fix e::real assume "e>0"
+ from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
+ from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
+ { fix n::nat assume n:"n \<ge> max N M"
+ have "dist ((f \<circ> r) n) l < e/2" using n M by auto
+ moreover have "r n \<ge> N" using lr'[of n] n by auto
+ hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
+ ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) }
+ hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast }
+ hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto }
+ thus ?thesis unfolding complete_def by auto
+qed
+
+lemma nat_approx_posE:
+ fixes e::real
+ assumes "0 < e"
+ obtains n::nat where "1 / (Suc n) < e"
+proof atomize_elim
+ have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
+ by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
+ also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
+ by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
+ also have "\<dots> = e" by simp
+ finally show "\<exists>n. 1 / real (Suc n) < e" ..
+qed
+
+lemma compact_eq_totally_bounded:
+ "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+ (is "_ \<longleftrightarrow> ?rhs")
+proof
+ assume assms: "?rhs"
+ then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
+ by (auto simp: choice_iff')
+
+ show "compact s"
+ proof cases
+ assume "s = {}" thus "compact s" by (simp add: compact_def)
+ next
+ assume "s \<noteq> {}"
+ show ?thesis
+ unfolding compact_def
+ proof safe
+ fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+
+ def e \<equiv> "\<lambda>n. 1 / (2 * Suc n)"
+ then have [simp]: "\<And>n. 0 < e n" by auto
+ def B \<equiv> "\<lambda>n U. SOME b. infinite {n. f n \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
+ { fix n U assume "infinite {n. f n \<in> U}"
+ then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
+ using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
+ then guess a ..
+ then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
+ by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
+ from someI_ex[OF this]
+ have "infinite {i. f i \<in> B n U}" "\<exists>x. B n U \<subseteq> ball x (e n) \<inter> U"
+ unfolding B_def by auto }
+ note B = this
+
+ def F \<equiv> "nat_rec (B 0 UNIV) B"
+ { fix n have "infinite {i. f i \<in> F n}"
+ by (induct n) (auto simp: F_def B) }
+ then have F: "\<And>n. \<exists>x. F (Suc n) \<subseteq> ball x (e n) \<inter> F n"
+ using B by (simp add: F_def)
+ then have F_dec: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
+ using decseq_SucI[of F] by (auto simp: decseq_def)
+
+ obtain sel where sel: "\<And>k i. i < sel k i" "\<And>k i. f (sel k i) \<in> F k"
+ proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)
+ fix k i
+ have "infinite ({n. f n \<in> F k} - {.. i})"
+ using `infinite {n. f n \<in> F k}` by auto
+ from infinite_imp_nonempty[OF this]
+ show "\<exists>x>i. f x \<in> F k"
+ by (simp add: set_eq_iff not_le conj_commute)
+ qed
+
+ def t \<equiv> "nat_rec (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
+ have "subseq t"
+ unfolding subseq_Suc_iff by (simp add: t_def sel)
+ moreover have "\<forall>i. (f \<circ> t) i \<in> s"
+ using f by auto
+ moreover
+ { fix n have "(f \<circ> t) n \<in> F n"
+ by (cases n) (simp_all add: t_def sel) }
+ note t = this
+
+ have "Cauchy (f \<circ> t)"
+ proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
+ fix r :: real and N n m assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
+ then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
+ using F_dec t by (auto simp: e_def field_simps real_of_nat_Suc)
+ with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
+ by (auto simp: subset_eq)
+ with dist_triangle[of "(f \<circ> t) m" "(f \<circ> t) n" x] `2 * e N < r`
+ show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
+ by (simp add: dist_commute)
+ qed
+
+ ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ using assms unfolding complete_def by blast
+ qed
+ qed
+qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
proof-
@@ -3462,35 +3519,15 @@
apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
qed
-lemma seq_compact_imp_complete: assumes "seq_compact s" shows "complete s"
-proof-
- { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
- from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding seq_compact_def by blast
-
- note lr' = seq_suble [OF lr(2)]
-
- { fix e::real assume "e>0"
- from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
- from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
- { fix n::nat assume n:"n \<ge> max N M"
- have "dist ((f \<circ> r) n) l < e/2" using n M by auto
- moreover have "r n \<ge> N" using lr'[of n] n by auto
- hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
- ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) }
- hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast }
- hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto }
- thus ?thesis unfolding complete_def by auto
-qed
-
instance heine_borel < complete_space
proof
fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
hence "bounded (range f)"
by (rule cauchy_imp_bounded)
- hence "seq_compact (closure (range f))"
- using bounded_closed_imp_seq_compact [of "closure (range f)"] by auto
+ hence "compact (closure (range f))"
+ unfolding compact_eq_bounded_closed by auto
hence "complete (closure (range f))"
- by (rule seq_compact_imp_complete)
+ by (rule compact_imp_complete)
moreover have "\<forall>n. f n \<in> closure (range f)"
using closure_subset [of "range f"] by auto
ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
@@ -3543,154 +3580,6 @@
shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
-lemma nat_approx_posE:
- fixes e::real
- assumes "0 < e"
- obtains n::nat where "1 / (Suc n) < e"
-proof atomize_elim
- have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
- by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
- also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
- by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
- also have "\<dots> = e" by simp
- finally show "\<exists>n. 1 / real (Suc n) < e" ..
-qed
-
-lemma compact_eq_totally_bounded:
- "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
-proof (safe intro!: seq_compact_imp_complete[unfolded compact_eq_seq_compact_metric[symmetric]])
- fix e::real
- def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
- assume "0 < e" "compact s"
- hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
- by (simp add: compact_eq_heine_borel)
- moreover
- have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
- hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
- ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
- then guess K .. note K = this
- have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
- then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
- thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
- by (intro exI[where x="k ` K"]) (auto simp: f_def)
-next
- assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
- show "compact s"
- proof cases
- assume "s = {}" thus "compact s" by (simp add: compact_def)
- next
- assume "s \<noteq> {}"
- show ?thesis
- unfolding compact_def
- proof safe
- fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
- from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
- then obtain K where
- K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
- unfolding choice_iff by blast
- {
- fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
- assume "e > 0"
- from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
- by simp_all
- have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
- proof (rule ccontr)
- from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
- using `s \<noteq> {}`
- by auto
- moreover
- assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
- hence "\<And>r k. k \<in> K e \<Longrightarrow> subseq r \<Longrightarrow> (\<exists>i. (f o f' o r) i \<notin> ball k e)" by simp
- ultimately
- show False using f'
- proof (induct arbitrary: s f f' rule: finite_ne_induct)
- case (singleton x)
- have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
- thus ?case using singleton by (auto simp: ball_def)
- next
- case (insert x A)
- show ?case
- proof cases
- have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
- have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
- using insert by (intro infinite_super[OF _ inf_ms]) auto
- also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
- {m. (f o f') m \<in> ball x e} \<union> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by auto
- finally have "infinite \<dots>" .
- moreover assume "finite {m. (f o f') m \<in> ball x e}"
- ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
- hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
- def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
- have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
- using enumerate_mono[OF _ inf] by (simp add: r_def)
- hence "subseq r" by (simp add: subseq_def)
- have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
- using enumerate_in_set[OF inf] by (simp add: r_def)
- show False
- proof (rule insert)
- show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
- fix k s assume "k \<in> A" "subseq s"
- thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
- by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
- next
- fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
- qed
- next
- assume inf: "infinite {m. (f o f') m \<in> ball x e}"
- def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
- have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
- using enumerate_mono[OF _ inf] by (simp add: r_def)
- hence "subseq r" by (simp add: subseq_def)
- from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
- moreover
- have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
- using enumerate_in_set[OF inf] by (simp add: r_def)
- hence "(f o f') (r i) \<in> ball x e" by simp
- ultimately show False by simp
- qed
- qed
- qed
- }
- hence ex: "\<forall>f'. \<forall>e > 0. (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f o f' \<circ> r) i \<in> ball k e))" by simp
- let ?e = "\<lambda>n. 1 / real (Suc n)"
- let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
- interpret subseqs ?P using ex by unfold_locales force
- from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
- by (simp add: complete_def)
- have "\<exists>l\<in>s. (f o diagseq) ----> l"
- proof (intro limI metric_CauchyI)
- fix e::real assume "0 < e" hence "0 < e / 2" by auto
- from nat_approx_posE[OF this] guess n . note n = this
- show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
- proof (rule exI[where x="Suc n"], safe)
- fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
- let ?e = "1 / real (Suc n)"
- from reducer_reduces[of n] obtain k where
- "k\<in>K ?e" "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
- unfolding seqseq_reducer by auto
- moreover
- note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
- ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
- also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
- finally
- have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
- by (intro add_strict_mono) auto
- hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
- by (simp add: dist_commute)
- moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
- dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
- by (rule dist_triangle2)
- ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
- by simp
- qed
- next
- fix n show "(f o diagseq) n \<in> s" using f by simp
- qed
- thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
- qed
- qed
-qed
-
lemma compact_cball[simp]:
fixes x :: "'a::heine_borel"
shows "compact(cball x e)"
@@ -3872,6 +3761,10 @@
lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
using continuous_within [of x UNIV f] by simp
+lemma continuous_isCont: "isCont f x = continuous (at x) f"
+ unfolding isCont_def LIM_def
+ unfolding continuous_at Lim_at unfolding dist_nz by auto
+
lemma continuous_at_within:
assumes "continuous (at x) f" shows "continuous (at x within s) f"
using assms unfolding continuous_at continuous_within
@@ -5142,7 +5035,7 @@
apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
apply (rule_tac x="r1 \<circ> r2" in exI)
apply (rule conjI, simp add: subseq_def)
-apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
+apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
apply (drule (1) tendsto_Pair) back
apply (simp add: o_def)
done
@@ -5209,66 +5102,74 @@
text {* Hence we get the following. *}
lemma compact_sup_maxdistance:
- fixes s :: "'a::real_normed_vector set"
+ fixes s :: "'a::metric_space set"
assumes "compact s" "s \<noteq> {}"
- shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. norm(u - v) \<le> norm(x - y)"
+ shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
proof-
- have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
- then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}" "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
- using compact_differences[OF assms(1) assms(1)]
- using distance_attains_sup[where 'a="'a", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by auto
- from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
- thus ?thesis using x(2)[unfolded `x = a - b`] by blast
+ have "compact (s \<times> s)" using `compact s` by (intro compact_Times)
+ moreover have "s \<times> s \<noteq> {}" using `s \<noteq> {}` by auto
+ moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"
+ by (intro continuous_at_imp_continuous_on ballI continuous_dist
+ continuous_isCont[THEN iffD1] isCont_fst isCont_snd isCont_ident)
+ ultimately show ?thesis
+ using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
qed
text {* We can state this in terms of diameter of a set. *}
-definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
- (* TODO: generalize to class metric_space *)
+definition "diameter s = (if s = {} then 0::real else Sup {dist x y | x y. x \<in> s \<and> y \<in> s})"
+
+lemma diameter_bounded_bound:
+ fixes s :: "'a :: metric_space set"
+ assumes s: "bounded s" "x \<in> s" "y \<in> s"
+ shows "dist x y \<le> diameter s"
+proof -
+ let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
+ from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
+ unfolding bounded_def by auto
+ have "dist x y \<le> Sup ?D"
+ proof (rule Sup_upper, safe)
+ fix a b assume "a \<in> s" "b \<in> s"
+ with z[of a] z[of b] dist_triangle[of a b z]
+ show "dist a b \<le> 2 * d"
+ by (simp add: dist_commute)
+ qed (insert s, auto)
+ with `x \<in> s` show ?thesis
+ by (auto simp add: diameter_def)
+qed
+
+lemma diameter_lower_bounded:
+ fixes s :: "'a :: metric_space set"
+ assumes s: "bounded s" and d: "0 < d" "d < diameter s"
+ shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
+proof (rule ccontr)
+ let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
+ assume contr: "\<not> ?thesis"
+ moreover
+ from d have "s \<noteq> {}"
+ by (auto simp: diameter_def)
+ then have "?D \<noteq> {}" by auto
+ ultimately have "Sup ?D \<le> d"
+ by (intro Sup_least) (auto simp: not_less)
+ with `d < diameter s` `s \<noteq> {}` show False
+ by (auto simp: diameter_def)
+qed
lemma diameter_bounded:
assumes "bounded s"
- shows "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
- "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
-proof-
- let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
- obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
- { fix x y assume "x \<in> s" "y \<in> s"
- hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: field_simps) }
- note * = this
- { fix x y assume "x\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
- have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
- by simp (blast del: Sup_upper intro!: * Sup_upper) }
- moreover
- { fix d::real assume "d>0" "d < diameter s"
- hence "s\<noteq>{}" unfolding diameter_def by auto
- have "\<exists>d' \<in> ?D. d' > d"
- proof(rule ccontr)
- assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
- hence "\<forall>d'\<in>?D. d' \<le> d" by auto (metis not_leE)
- thus False using `d < diameter s` `s\<noteq>{}`
- apply (auto simp add: diameter_def)
- apply (drule Sup_real_iff [THEN [2] rev_iffD2])
- apply (auto, force)
- done
- qed
- hence "\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d" by auto }
- ultimately show "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
- "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)" by auto
-qed
-
-lemma diameter_bounded_bound:
- "bounded s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s ==> norm(x - y) \<le> diameter s"
- using diameter_bounded by blast
+ shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
+ "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
+ using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
+ by auto
lemma diameter_compact_attained:
- fixes s :: "'a::real_normed_vector set"
assumes "compact s" "s \<noteq> {}"
- shows "\<exists>x\<in>s. \<exists>y\<in>s. (norm(x - y) = diameter s)"
-proof-
+ shows "\<exists>x\<in>s. \<exists>y\<in>s. dist x y = diameter s"
+proof -
have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
- then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
- hence "diameter s \<le> norm (x - y)"
+ then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
+ using compact_sup_maxdistance[OF assms] by auto
+ hence "diameter s \<le> dist x y"
unfolding diameter_def by clarsimp (rule Sup_least, fast+)
thus ?thesis
by (metis b diameter_bounded_bound order_antisym xys)
@@ -5326,7 +5227,7 @@
obtain l' r where "l'\<in>s" and r:"subseq r" and lr:"(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
- using tendsto_diff[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
+ using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) unfolding o_def by auto
hence "l - l' \<in> t"
using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
using f(3) by auto
@@ -6320,11 +6221,6 @@
thus ?thesis unfolding complete_def by auto
qed
-lemma dist_0_norm:
- fixes x :: "'a::real_normed_vector"
- shows "dist 0 x = norm x"
-unfolding dist_norm by simp
-
lemma injective_imp_isometric: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes s:"closed s" "subspace s" and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"
@@ -6699,7 +6595,7 @@
subsection {* Edelstein fixed point theorem *}
lemma edelstein_fix:
- fixes s :: "'a::real_normed_vector set"
+ fixes s :: "'a::metric_space set"
assumes s:"compact s" "s \<noteq> {}" and gs:"(g ` s) \<subseteq> s"
and dist:"\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
shows "\<exists>! x\<in>s. g x = x"
@@ -6760,23 +6656,29 @@
unfolding o_def a_def b_def by (rule tendsto_intros)+
{ fix n::nat
- have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
- { fix x y :: 'a
- have "dist (-x) (-y) = dist x y" unfolding dist_norm
- using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
+ have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (\<bar>dist fx fy - dist a b\<bar> < dist a b - dist x y)" by auto
{ assume as:"dist a b > dist (f n x) (f n y)"
then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_numeral1)
- hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
- apply(erule_tac x="Na+Nb+n" in allE)
- apply(erule_tac x="Na+Nb+n" in allE) apply simp
- using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)"
- "-b" "- f (r (Na + Nb + n)) y"]
- unfolding ** by (auto simp add: algebra_simps dist_commute)
+ hence "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> < dist a b - dist (f n x) (f n y)"
+ apply -
+ apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
+ apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
+ apply (drule (1) add_strict_mono, simp only: real_sum_of_halves)
+ apply (erule le_less_trans [rotated])
+ apply (erule thin_rl)
+ apply (rule abs_leI)
+ apply (simp add: diff_le_iff add_assoc)
+ apply (rule order_trans [OF dist_triangle add_left_mono])
+ apply (subst add_commute, rule dist_triangle2)
+ apply (simp add: diff_le_iff add_assoc)
+ apply (rule order_trans [OF dist_triangle3 add_left_mono])
+ apply (subst add_commute, rule dist_triangle)
+ done
moreover
- have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
+ have "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> \<ge> dist a b - dist (f n x) (f n y)"
using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
using seq_suble[OF r, of "Na+Nb+n"]
using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
@@ -6797,7 +6699,10 @@
moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b"
using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto
ultimately have "dist (f (Suc n) x) (g a) + dist (f (Suc n) y) (g b) < e" using n by auto
- thus False unfolding e_def using ab_fn[of "Suc n"] by norm
+ thus False unfolding e_def using ab_fn[of "Suc n"]
+ using dist_triangle2 [of "f (Suc n) y" "g a" "g b"]
+ using dist_triangle2 [of "f (Suc n) x" "f (Suc n) y" "g a"]
+ by auto
qed
have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto
--- a/src/HOL/Probability/Projective_Limit.thy Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Fri Jan 18 20:31:22 2013 +0100
@@ -11,7 +11,7 @@
Regularity
Projective_Family
Infinite_Product_Measure
- "~~/src/HOL/Library/Countable_Set"
+ "~~/src/HOL/Library/Diagonal_Subsequence"
begin
subsection {* Sequences of Finite Maps in Compact Sets *}
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jan 18 20:31:22 2013 +0100
@@ -849,7 +849,7 @@
fun filter_type_args thy constrs type_enc s ary T_args =
let val poly = polymorphism_of_type_enc type_enc in
- if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *)
+ if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *)
T_args
else case type_enc of
Native (_, Raw_Polymorphic _, _) => T_args
@@ -1383,7 +1383,7 @@
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
- models in first-order logic (via Löwenheim-Skolem). *)
+ models in first-order logic (via Loewenheim-Skolem). *)
fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts}
@@ -1580,7 +1580,7 @@
fun add_iterm_syms conj_fact =
add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
fun add_fact_syms conj_fact =
- K (add_iterm_syms conj_fact) |> formula_fold NONE |> ifact_lift
+ ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact)))
in
((false, []), Symtab.empty)
|> fold (add_fact_syms true) conjs
@@ -2243,7 +2243,7 @@
| _ => I)
#> fold add_iterm_syms args
end
- val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
+ val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms))
fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
| add_formula_var_types (AQuant (_, xs, phi)) =
fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
@@ -2291,8 +2291,8 @@
| _ => known_infinite_types,
maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
-(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
- out with monotonicity" paper presented at CADE 2011. *)
+(* This inference is described in section 4 of Blanchette et al., "Encoding
+ monomorphic and polymorphic types", TACAS 2013. *)
fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
| add_iterm_mononotonicity_info ctxt level _
(IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
@@ -2338,8 +2338,10 @@
| add_args _ = I
and add_term tm = add_type (ityp_of tm) #> add_args tm
in formula_fold NONE (K add_term) end
+
fun add_fact_monotonic_types ctxt mono type_enc =
- add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
+ ifact_lift (add_iformula_monotonic_types ctxt mono type_enc)
+
fun monotonic_types_for_facts ctxt mono type_enc facts =
let val level = level_of_type_enc type_enc in
[] |> (is_type_enc_polymorphic type_enc andalso
@@ -2396,8 +2398,7 @@
? curry APi (map (tvar_name o dest_TVar) T_args))
end
-fun honor_conj_sym_role in_conj =
- if in_conj then (Hypothesis, I) else (Axiom, I)
+fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
fun line_for_guards_sym_decl ctxt mono type_enc n s j
(s', T_args, T, _, ary, in_conj) =
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri Jan 18 20:31:22 2013 +0100
@@ -156,12 +156,11 @@
let
val tvars = Term.add_tvar_namesT T []
val tvars' = Term.add_tvar_namesT T' []
+ val maxidx' = maxidx_of_typ T'
val T =
- if exists (member (op =) tvars') tvars then
- T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
- else
- T
- in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
+ T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1)
+ val maxidx = Integer.max (maxidx_of_typ T) maxidx'
+ in can (Sign.typ_unify thy (T, T')) (Vartab.empty, maxidx) end
val type_equiv = Sign.typ_equiv
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 18 20:31:22 2013 +0100
@@ -39,7 +39,7 @@
-> (string * string list * (string * real) list * string list) list -> unit
val relearn :
Proof.context -> bool -> (string * string list) list -> unit
- val suggest :
+ val query :
Proof.context -> bool -> bool -> int
-> string list * (string * real) list * string list -> string list
end
@@ -256,8 +256,8 @@
elide_string 1000 (space_implode " " (map #1 relearns)));
run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
-fun suggest ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
- (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
+fun query ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
+ (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
run_mash_tool ctxt overlord (learn_hints andalso not (null hints))
max_suggs ([query], str_of_query learn_hints)
(fn suggs =>
@@ -808,8 +808,8 @@
chained |> filter (is_fact_in_graph access_G snd)
|> map (nickname_of_thm o snd)
in
- (access_G, MaSh.suggest ctxt overlord learn max_facts
- (parents, feats, hints))
+ (access_G, MaSh.query ctxt overlord learn max_facts
+ (parents, feats, hints))
end)
val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
in find_mash_suggestions max_facts suggs facts chained unknown end