--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Sep 22 15:41:47 2016 +0200
@@ -2794,6 +2794,14 @@
using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
by (metis clo closed_closedin open_openin subtopology_UNIV)
+corollary neighbourhood_extension_into_ANR:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
+ obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
+ "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ using ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf fim]
+ by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
+
lemma absolute_neighbourhood_extensor_imp_ANR:
fixes S :: "'a::euclidean_space set"
assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
@@ -3739,8 +3747,9 @@
apply (rule homeomorphic_closedin_convex [of S])
using aff_dim_le_DIM [of S] apply auto
done
- have "locally path_connected T"
- by (meson ANR_imp_absolute_neighbourhood_retract \<open>S homeomorphic T\<close> \<open>closedin (subtopology euclidean U) T\<close> \<open>convex U\<close> assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
+ then have "locally path_connected T"
+ by (meson ANR_imp_absolute_neighbourhood_retract
+ assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
then have S: "locally path_connected S"
if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Sep 22 15:41:47 2016 +0200
@@ -5420,10 +5420,6 @@
subsection\<open> General stepping result for derivative formulas.\<close>
-lemma sum_sqs_eq:
- fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
- by algebra
-
proposition Cauchy_next_derivative:
assumes "continuous_on (path_image \<gamma>) f'"
and leB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
--- a/src/HOL/Analysis/Conformal_Mappings.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Thu Sep 22 15:41:47 2016 +0200
@@ -1027,7 +1027,7 @@
using polyfun_extremal [where c=c and B="B+1", OF c]
by (auto simp: bounded_pos eventually_at_infinity_pos *)
moreover have "closed {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
- apply (rule allI continuous_closed_preimage_univ continuous_intros)+
+ apply (intro allI continuous_closed_preimage_univ continuous_intros)
using \<open>compact K\<close> compact_eq_bounded_closed by blast
ultimately show ?thesis
using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed by blast
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 22 15:41:47 2016 +0200
@@ -5554,6 +5554,31 @@
apply auto
done
+text\<open>A non-singleton connected set is perfect (i.e. has no isolated points). \<close>
+lemma connected_imp_perfect:
+ fixes a :: "'a::metric_space"
+ assumes "connected S" "a \<in> S" and S: "\<And>x. S \<noteq> {x}"
+ shows "a islimpt S"
+proof -
+ have False if "a \<in> T" "open T" "\<And>y. \<lbrakk>y \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> y = a" for T
+ proof -
+ obtain e where "e > 0" and e: "cball a e \<subseteq> T"
+ using \<open>open T\<close> \<open>a \<in> T\<close> by (auto simp: open_contains_cball)
+ have "openin (subtopology euclidean S) {a}"
+ unfolding openin_open using that \<open>a \<in> S\<close> by blast
+ moreover have "closedin (subtopology euclidean S) {a}"
+ by (simp add: assms)
+ ultimately show "False"
+ using \<open>connected S\<close> connected_clopen S by blast
+ qed
+ then show ?thesis
+ unfolding islimpt_def by blast
+qed
+
+lemma connected_imp_perfect_aff_dim:
+ "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
+ using aff_dim_sing connected_imp_perfect by blast
+
subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
lemma is_interval_1:
@@ -10406,7 +10431,7 @@
lemma collinear_3_expand:
"collinear{a,b,c} \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
-proof -
+proof -
have "collinear{a,b,c} = collinear{a,c,b}"
by (simp add: insert_commute)
also have "... = collinear {0, a - c, b - c}"
@@ -10418,6 +10443,27 @@
finally show ?thesis .
qed
+lemma collinear_aff_dim: "collinear S \<longleftrightarrow> aff_dim S \<le> 1"
+proof
+ assume "collinear S"
+ then obtain u and v :: "'a" where "aff_dim S \<le> aff_dim {u,v}"
+ by (metis \<open>collinear S\<close> aff_dim_affine_hull aff_dim_subset collinear_affine_hull)
+ then show "aff_dim S \<le> 1"
+ using order_trans by fastforce
+next
+ assume "aff_dim S \<le> 1"
+ then have le1: "aff_dim (affine hull S) \<le> 1"
+ by simp
+ obtain B where "B \<subseteq> S" and B: "\<not> affine_dependent B" "affine hull S = affine hull B"
+ using affine_basis_exists [of S] by auto
+ then have "finite B" "card B \<le> 2"
+ using B le1 by (auto simp: affine_independent_iff_card)
+ then have "collinear B"
+ by (rule collinear_small)
+ then show "collinear S"
+ by (metis \<open>affine hull S = affine hull B\<close> collinear_affine_hull_collinear)
+qed
+
lemma collinear_midpoint: "collinear{a,midpoint a b,b}"
apply (auto simp: collinear_3 collinear_lemma)
apply (drule_tac x="-1" in spec)
@@ -10443,6 +10489,35 @@
ultimately show ?thesis by blast
qed
+lemma between_imp_collinear:
+ fixes x :: "'a :: euclidean_space"
+ assumes "between (a,b) x"
+ shows "collinear {a,x,b}"
+proof (cases "x = a \<or> x = b \<or> a = b")
+ case True with assms show ?thesis
+ by (auto simp: dist_commute)
+next
+ case False with assms show ?thesis
+ apply (auto simp: collinear_3 collinear_lemma between_norm)
+ apply (drule_tac x="-(norm(b - x) / norm(x - a))" in spec)
+ apply (simp add: vector_add_divide_simps eq_vector_fraction_iff real_vector.scale_minus_right [symmetric])
+ done
+qed
+
+lemma midpoint_between:
+ fixes a b :: "'a::euclidean_space"
+ shows "b = midpoint a c \<longleftrightarrow> between (a,c) b \<and> dist a b = dist b c"
+proof (cases "a = c")
+ case True then show ?thesis
+ by (auto simp: dist_commute)
+next
+ case False
+ show ?thesis
+ apply (rule iffI)
+ apply (simp add: between_midpoint(1) dist_midpoint)
+ using False between_imp_collinear midpoint_collinear by blast
+qed
+
lemma collinear_triples:
assumes "a \<noteq> b"
shows "collinear(insert a (insert b S)) \<longleftrightarrow> (\<forall>x \<in> S. collinear{a,b,x})"
@@ -11157,7 +11232,7 @@
using assms unfolding openin_open
by (metis affine_hull_convex_Int_open hull_subset inf.orderE inf_assoc)
-corollary affine_hull_open_in:
+corollary affine_hull_openin:
fixes S :: "'a::real_normed_vector set"
assumes "openin (subtopology euclidean (affine hull T)) S" "S \<noteq> {}"
shows "affine hull S = affine hull T"
@@ -11180,6 +11255,19 @@
shows "\<lbrakk>convex S; open T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> aff_dim(S \<inter> T) = aff_dim S"
using aff_dim_convex_Int_nonempty_interior interior_eq by blast
+lemma affine_hull_Diff:
+ fixes S:: "'a::real_normed_vector set"
+ assumes ope: "openin (subtopology euclidean (affine hull S)) S" and "finite F" "F \<subset> S"
+ shows "affine hull (S - F) = affine hull S"
+proof -
+ have clo: "closedin (subtopology euclidean S) F"
+ using assms finite_imp_closedin by auto
+ moreover have "S - F \<noteq> {}"
+ using assms by auto
+ ultimately show ?thesis
+ by (metis ope closedin_def topspace_euclidean_subtopology affine_hull_openin openin_trans)
+qed
+
lemma affine_hull_halfspace_lt:
fixes a :: "'a::euclidean_space"
shows "affine hull {x. a \<bullet> x < r} = (if a = 0 \<and> r \<le> 0 then {} else UNIV)"
@@ -11963,6 +12051,44 @@
using in_convex_hull_exchange_unique assms apply blast
by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
+lemma Int_closed_segment:
+ fixes b :: "'a::euclidean_space"
+ assumes "b \<in> closed_segment a c \<or> ~collinear{a,b,c}"
+ shows "closed_segment a b \<inter> closed_segment b c = {b}"
+proof (cases "c = a")
+ case True
+ then show ?thesis
+ using assms collinear_3_eq_affine_dependent by fastforce
+next
+ case False
+ from assms show ?thesis
+ proof
+ assume "b \<in> closed_segment a c"
+ moreover have "\<not> affine_dependent {a, c}"
+ by (simp add: affine_independent_2)
+ ultimately show ?thesis
+ using False convex_hull_exchange_Int [of "{a,c}" b "{a}" "{c}"]
+ by (simp add: segment_convex_hull insert_commute)
+ next
+ assume ncoll: "\<not> collinear {a, b, c}"
+ have False if "closed_segment a b \<inter> closed_segment b c \<noteq> {b}"
+ proof -
+ have "b \<in> closed_segment a b" and "b \<in> closed_segment b c"
+ by auto
+ with that obtain d where "b \<noteq> d" "d \<in> closed_segment a b" "d \<in> closed_segment b c"
+ by force
+ then have d: "collinear {a, d, b}" "collinear {b, d, c}"
+ by (auto simp: between_mem_segment between_imp_collinear)
+ have "collinear {a, b, c}"
+ apply (rule collinear_3_trans [OF _ _ \<open>b \<noteq> d\<close>])
+ using d by (auto simp: insert_commute)
+ with ncoll show False ..
+ qed
+ then show ?thesis
+ by blast
+ qed
+qed
+
lemma affine_hull_finite_intersection_hyperplanes:
fixes s :: "'a::euclidean_space set"
obtains f where
@@ -12812,6 +12938,7 @@
finally show "aff_dim S \<le> aff_dim (f ` S)" .
qed
+
text\<open>Choosing a subspace of a given dimension\<close>
proposition choose_subspace_of_subspace:
fixes S :: "'n::euclidean_space set"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 22 15:41:47 2016 +0200
@@ -5894,7 +5894,7 @@
assumes "0 < r"
and "\<forall>x. h(g x) = x"
and "\<forall>x. g(h x) = x"
- and "\<forall>x. continuous (at x) g"
+ and contg: "\<And>x. continuous (at x) g"
and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
and "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
@@ -5947,7 +5947,7 @@
show "gauge d'"
using d(1)
unfolding gauge_def d'
- using continuous_open_preimage_univ[OF assms(4)]
+ using continuous_open_preimage_univ[OF _ contg]
by auto
fix p
assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
@@ -5985,7 +5985,7 @@
proof -
assume as: "interior k \<inter> interior k' = {}"
have "z \<in> g ` (interior k \<inter> interior k')"
- using interior_image_subset[OF assms(4) inj(1)] z
+ using interior_image_subset[OF \<open>inj g\<close> contg] z
unfolding image_Int[OF inj(1)] by blast
then show False
using as by blast
@@ -6178,20 +6178,13 @@
assumes "(f has_integral i) (cbox a b)"
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
- ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
- apply (rule has_integral_twiddle[where f=f])
- unfolding zero_less_abs_iff content_image_stretch_interval
- unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
- using assms
-proof -
- show "\<forall>y::'a. continuous (at y) (\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k))"
- apply rule
- apply (rule linear_continuous_at)
- unfolding linear_linear
- unfolding linear_iff inner_simps euclidean_eq_iff[where 'a='a]
- apply (auto simp add: field_simps)
- done
-qed auto
+ ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+apply (rule has_integral_twiddle[where f=f])
+unfolding zero_less_abs_iff content_image_stretch_interval
+unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
+using assms
+by auto
+
lemma integrable_stretch:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -6199,14 +6192,9 @@
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on
((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` cbox a b)"
- using assms
- unfolding integrable_on_def
- apply -
- apply (erule exE)
- apply (drule has_integral_stretch)
- apply assumption
- apply auto
- done
+ using assms unfolding integrable_on_def
+ by (force dest: has_integral_stretch)
+
subsection \<open>even more special cases.\<close>
--- a/src/HOL/Analysis/Norm_Arith.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Norm_Arith.thy Thu Sep 22 15:41:47 2016 +0200
@@ -8,6 +8,11 @@
imports "~~/src/HOL/Library/Sum_of_Squares"
begin
+(* FIXME: move elsewhere *)
+lemma sum_sqs_eq:
+ fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
+ by algebra
+
lemma norm_cmul_rule_thm:
fixes x :: "'a::real_normed_vector"
shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
--- a/src/HOL/Analysis/Path_Connected.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Sep 22 15:41:47 2016 +0200
@@ -4746,19 +4746,17 @@
lemma connected_equivalence_relation:
assumes "connected S"
and etc: "a \<in> S" "b \<in> S"
- and sym: "\<And>x y z. R x y \<Longrightarrow> R y x"
- and trans: "\<And>x y z. R x y \<and> R y z \<Longrightarrow> R x z"
- and opI: "\<And>a. a \<in> S
- \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
+ and sym: "\<And>x y. \<lbrakk>R x y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> R y x"
+ and trans: "\<And>x y z. \<lbrakk>R x y; R y z; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> R x z"
+ and opI: "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
shows "R a b"
proof -
have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
apply (rule connected_induction_simple [OF \<open>connected S\<close>], simp_all)
- by (meson local.sym local.trans opI)
+ by (meson local.sym local.trans opI openin_imp_subset subsetCE)
then show ?thesis by (metis etc opI)
qed
-
lemma locally_constant_imp_constant:
assumes "connected S"
and opI: "\<And>a. a \<in> S
@@ -5270,6 +5268,12 @@
apply (force simp: convex_Int convex_imp_path_connected)
done
+lemma convex_imp_locally_connected:
+ fixes S :: "'a:: real_normed_vector set"
+ shows "convex S \<Longrightarrow> locally connected S"
+ by (simp add: locally_path_connected_imp_locally_connected convex_imp_locally_path_connected)
+
+
subsection\<open>Relations between components and path components\<close>
lemma path_component_eq_connected_component:
@@ -5741,7 +5745,7 @@
done
qed
-lemma isometry_subspaces:
+corollary isometry_subspaces:
fixes S :: "'a::euclidean_space set"
and T :: "'b::euclidean_space set"
assumes S: "subspace S"
@@ -5751,6 +5755,14 @@
using isometries_subspaces [OF assms]
by metis
+corollary isomorphisms_UNIV_UNIV:
+ assumes "DIM('M) = DIM('N)"
+ obtains f::"'M::euclidean_space \<Rightarrow>'N::euclidean_space" and g
+ where "linear f" "linear g"
+ "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y"
+ "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+ using assms by (auto simp: dim_UNIV intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
+
lemma homeomorphic_subspaces:
fixes S :: "'a::euclidean_space set"
and T :: "'b::euclidean_space set"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Sep 22 15:41:47 2016 +0200
@@ -17,6 +17,7 @@
(* FIXME: move elsewhere *)
+
definition (in monoid_add) support_on :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'b set"
where
"support_on s f = {x\<in>s. f x \<noteq> 0}"
@@ -766,6 +767,11 @@
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp add: closedin_closed)
+lemma finite_imp_closedin:
+ fixes S :: "'a::t1_space set"
+ shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S"
+ by (simp add: finite_imp_closed closed_subset)
+
lemma closedin_singleton [simp]:
fixes a :: "'a::t1_space"
shows "closedin (subtopology euclidean U) {a} \<longleftrightarrow> a \<in> U"
@@ -3611,6 +3617,9 @@
unfolding bounded_def by auto
qed
+lemma bounded_closure_image: "bounded (f ` closure S) \<Longrightarrow> bounded (f ` S)"
+ by (simp add: bounded_subset closure_subset image_mono)
+
lemma bounded_cball[simp,intro]: "bounded (cball x e)"
apply (simp add: bounded_def)
apply (rule_tac x=x in exI)
@@ -3749,7 +3758,8 @@
shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
-text\<open>Some theorems on sups and infs using the notion "bounded".\<close>
+
+subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
by (simp add: bounded_iff)
@@ -6122,22 +6132,21 @@
qed
lemma continuous_open_preimage_univ:
- "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+ "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open {x. f x \<in> s}"
using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_closed_preimage_univ:
- "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s \<Longrightarrow> closed {x. f x \<in> s}"
+ "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
-lemma continuous_open_vimage: "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
+lemma continuous_open_vimage: "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` s)"
unfolding vimage_def by (rule continuous_open_preimage_univ)
-lemma continuous_closed_vimage: "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
+lemma continuous_closed_vimage: "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` s)"
unfolding vimage_def by (rule continuous_closed_preimage_univ)
lemma interior_image_subset:
- assumes "\<forall>x. continuous (at x) f"
- and "inj f"
+ assumes "inj f" "\<And>x. continuous (at x) f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
proof
fix x assume "x \<in> interior (f ` s)"
@@ -6145,7 +6154,7 @@
then have "x \<in> f ` s" by auto
then obtain y where y: "y \<in> s" "x = f y" by auto
have "open (vimage f T)"
- using assms(1) \<open>open T\<close> by (rule continuous_open_vimage)
+ using assms \<open>open T\<close> by (metis continuous_open_vimage)
moreover have "y \<in> vimage f T"
using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
moreover have "vimage f T \<subseteq> s"
@@ -6774,53 +6783,53 @@
by (auto intro!: image_eqI [where f="\<lambda>x. - x"])
lemma open_negations:
- fixes s :: "'a::real_normed_vector set"
- shows "open s \<Longrightarrow> open ((\<lambda>x. - x) ` s)"
- using open_scaling [of "- 1" s] by simp
+ fixes S :: "'a::real_normed_vector set"
+ shows "open S \<Longrightarrow> open ((\<lambda>x. - x) ` S)"
+ using open_scaling [of "- 1" S] by simp
lemma open_translation:
- fixes s :: "'a::real_normed_vector set"
- assumes "open s"
- shows "open((\<lambda>x. a + x) ` s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "open S"
+ shows "open((\<lambda>x. a + x) ` S)"
proof -
{
fix x
have "continuous (at x) (\<lambda>x. x - a)"
by (intro continuous_diff continuous_ident continuous_const)
}
- moreover have "{x. x - a \<in> s} = op + a ` s"
+ moreover have "{x. x - a \<in> S} = op + a ` S"
by force
- ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s]
- using assms by auto
+ ultimately show ?thesis
+ by (metis assms continuous_open_vimage vimage_def)
qed
lemma open_affinity:
- fixes s :: "'a::real_normed_vector set"
- assumes "open s" "c \<noteq> 0"
- shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "open S" "c \<noteq> 0"
+ shows "open ((\<lambda>x. a + c *\<^sub>R x) ` S)"
proof -
have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
unfolding o_def ..
- have "op + a ` op *\<^sub>R c ` s = (op + a \<circ> op *\<^sub>R c) ` s"
+ have "op + a ` op *\<^sub>R c ` S = (op + a \<circ> op *\<^sub>R c) ` S"
by auto
then show ?thesis
- using assms open_translation[of "op *\<^sub>R c ` s" a]
+ using assms open_translation[of "op *\<^sub>R c ` S" a]
unfolding *
by auto
qed
lemma interior_translation:
- fixes s :: "'a::real_normed_vector set"
- shows "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
+ fixes S :: "'a::real_normed_vector set"
+ shows "interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (interior S)"
proof (rule set_eqI, rule)
fix x
- assume "x \<in> interior (op + a ` s)"
- then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` s"
+ assume "x \<in> interior (op + a ` S)"
+ then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` S"
unfolding mem_interior by auto
- then have "ball (x - a) e \<subseteq> s"
+ then have "ball (x - a) e \<subseteq> S"
unfolding subset_eq Ball_def mem_ball dist_norm
by (auto simp add: diff_diff_eq)
- then show "x \<in> op + a ` interior s"
+ then show "x \<in> op + a ` interior S"
unfolding image_iff
apply (rule_tac x="x - a" in bexI)
unfolding mem_interior
@@ -6829,27 +6838,27 @@
done
next
fix x
- assume "x \<in> op + a ` interior s"
- then obtain y e where "e > 0" and e: "ball y e \<subseteq> s" and y: "x = a + y"
+ assume "x \<in> op + a ` interior S"
+ then obtain y e where "e > 0" and e: "ball y e \<subseteq> S" and y: "x = a + y"
unfolding image_iff Bex_def mem_interior by auto
{
fix z
have *: "a + y - z = y + a - z" by auto
assume "z \<in> ball x e"
- then have "z - a \<in> s"
+ then have "z - a \<in> S"
using e[unfolded subset_eq, THEN bspec[where x="z - a"]]
unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 *
by auto
- then have "z \<in> op + a ` s"
+ then have "z \<in> op + a ` S"
unfolding image_iff by (auto intro!: bexI[where x="z - a"])
}
- then have "ball x e \<subseteq> op + a ` s"
+ then have "ball x e \<subseteq> op + a ` S"
unfolding subset_eq by auto
- then show "x \<in> interior (op + a ` s)"
+ then show "x \<in> interior (op + a ` S)"
unfolding mem_interior using \<open>e > 0\<close> by auto
qed
-text \<open>Topological properties of linear functions.\<close>
+subsection \<open>Topological properties of linear functions.\<close>
lemma linear_lim_0:
assumes "bounded_linear f"
@@ -6877,6 +6886,73 @@
"bounded_linear f \<Longrightarrow> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+subsubsection\<open>Relating linear images to open/closed/interior/closure.\<close>
+
+proposition open_surjective_linear_image:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+ assumes "open A" "linear f" "surj f"
+ shows "open(f ` A)"
+unfolding open_dist
+proof clarify
+ fix x
+ assume "x \<in> A"
+ have "bounded (inv f ` Basis)"
+ by (simp add: finite_imp_bounded)
+ with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
+ by metis
+ obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
+ by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
+ define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
+ show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
+ proof (intro exI conjI)
+ show "\<delta> > 0"
+ using \<open>e > 0\<close> \<open>B > 0\<close> by (simp add: \<delta>_def divide_simps) (simp add: mult_less_0_iff)
+ have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
+ proof -
+ define u where "u \<equiv> y - f x"
+ show ?thesis
+ proof (rule image_eqI)
+ show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
+ apply (simp add: linear_add linear_setsum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
+ apply (simp add: euclidean_representation u_def)
+ done
+ have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
+ by (simp add: dist_norm setsum_norm_le)
+ also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
+ by (simp add: )
+ also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
+ by (simp add: B setsum_distrib_right setsum_mono mult_left_mono)
+ also have "... \<le> DIM('b) * dist y (f x) * B"
+ apply (rule mult_right_mono [OF setsum_bounded_above])
+ using \<open>0 < B\<close> by (auto simp add: Basis_le_norm dist_norm u_def)
+ also have "... < e"
+ by (metis mult.commute mult.left_commute that)
+ finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
+ by (rule e)
+ qed
+ qed
+ then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
+ using \<open>e > 0\<close> \<open>B > 0\<close>
+ by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
+ qed
+qed
+
+corollary open_bijective_linear_image_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "linear f" "bij f"
+ shows "open(f ` A) \<longleftrightarrow> open A"
+proof
+ assume "open(f ` A)"
+ then have "open(f -` (f ` A))"
+ using assms by (force simp add: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
+ then show "open A"
+ by (simp add: assms bij_is_inj inj_vimage_image_eq)
+next
+ assume "open A"
+ then show "open(f ` A)"
+ by (simp add: assms bij_is_surj open_surjective_linear_image)
+qed
+
text \<open>Also bilinear functions, in composition form.\<close>
lemma bilinear_continuous_at_compose:
@@ -7957,7 +8033,7 @@
then show "?L \<subseteq> ?R" ..
qed
-lemma bounded_cbox:
+lemma bounded_cbox [simp]:
fixes a :: "'a::euclidean_space"
shows "bounded (cbox a b)"
proof -
@@ -8384,11 +8460,27 @@
(\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
(\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
+lemma homeomorphismI [intro?]:
+ assumes "continuous_on S f" "continuous_on T g"
+ "f ` S \<subseteq> T" "g ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+ shows "homeomorphism S T f g"
+ using assms by (force simp: homeomorphism_def)
+
lemma homeomorphism_translation:
fixes a :: "'a :: real_normed_vector"
shows "homeomorphism (op + a ` S) S (op + (- a)) (op + a)"
unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
+lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
+ by (rule homeomorphismI) (auto simp: continuous_on_id)
+
+lemma homeomorphism_compose:
+ assumes "homeomorphism S T f g" "homeomorphism T U h k"
+ shows "homeomorphism S U (h o f) (g o k)"
+ using assms
+ unfolding homeomorphism_def
+ by (intro conjI ballI continuous_on_compose) (auto simp: image_comp [symmetric])
+
lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
by (simp add: homeomorphism_def)
@@ -8416,47 +8508,12 @@
by blast
lemma homeomorphic_trans [trans]:
- assumes "s homeomorphic t"
- and "t homeomorphic u"
- shows "s homeomorphic u"
-proof -
- obtain f1 g1 where fg1: "\<forall>x\<in>s. g1 (f1 x) = x" "f1 ` s = t"
- "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"
- using assms(1) unfolding homeomorphic_def homeomorphism_def by auto
- obtain f2 g2 where fg2: "\<forall>x\<in>t. g2 (f2 x) = x" "f2 ` t = u" "continuous_on t f2"
- "\<forall>y\<in>u. f2 (g2 y) = y" "g2 ` u = t" "continuous_on u g2"
- using assms(2) unfolding homeomorphic_def homeomorphism_def by auto
- {
- fix x
- assume "x\<in>s"
- then have "(g1 \<circ> g2) ((f2 \<circ> f1) x) = x"
- using fg1(1)[THEN bspec[where x=x]] and fg2(1)[THEN bspec[where x="f1 x"]] and fg1(2)
- by auto
- }
- moreover have "(f2 \<circ> f1) ` s = u"
- using fg1(2) fg2(2) by auto
- moreover have "continuous_on s (f2 \<circ> f1)"
- using continuous_on_compose[OF fg1(3)] and fg2(3) unfolding fg1(2) by auto
- moreover
- {
- fix y
- assume "y\<in>u"
- then have "(f2 \<circ> f1) ((g1 \<circ> g2) y) = y"
- using fg2(4)[THEN bspec[where x=y]] and fg1(4)[THEN bspec[where x="g2 y"]] and fg2(5)
- by auto
- }
- moreover have "(g1 \<circ> g2) ` u = s" using fg1(5) fg2(5) by auto
- moreover have "continuous_on u (g1 \<circ> g2)"
- using continuous_on_compose[OF fg2(6)] and fg1(6)
- unfolding fg2(5)
- by auto
- ultimately show ?thesis
- unfolding homeomorphic_def homeomorphism_def
- apply (rule_tac x="f2 \<circ> f1" in exI)
- apply (rule_tac x="g1 \<circ> g2" in exI)
- apply auto
- done
-qed
+ assumes "S homeomorphic T"
+ and "T homeomorphic U"
+ shows "S homeomorphic U"
+ using assms
+ unfolding homeomorphic_def
+by (metis homeomorphism_compose)
lemma homeomorphic_minimal:
"s homeomorphic t \<longleftrightarrow>
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Sep 22 15:41:47 2016 +0200
@@ -2863,29 +2863,6 @@
interpret_floatarith_divide interpret_floatarith_diff
by auto
-lemma interpret_floatarith_tan:
- "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs =
- tan (interpret_floatarith a vs)"
- unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
- by auto
-
-lemma interpret_floatarith_log:
- "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs =
- log (interpret_floatarith b vs) (interpret_floatarith x vs)"
- unfolding log_def interpret_floatarith.simps divide_inverse ..
-
-lemma interpret_floatarith_num:
- shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
- and "interpret_floatarith (Num (Float 1 0)) vs = 1"
- and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1"
- and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
- and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a"
- by auto
-
-lemma interpret_floatarith_ceiling:
- "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)"
- unfolding ceiling_def interpret_floatarith.simps of_int_minus ..
-
subsection "Implement approximation function"
@@ -4289,10 +4266,6 @@
subsection \<open>Implement proof method \texttt{approximation}\<close>
-lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
- interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
- interpret_floatarith_sin interpret_floatarith_ceiling
-
oracle approximation_oracle = \<open>fn (thy, t) =>
let
fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
@@ -4400,6 +4373,61 @@
lemma meta_eqE: "x \<equiv> a \<Longrightarrow> \<lbrakk> x = a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by auto
+named_theorems approximation_preproc
+
+lemma approximation_preproc_floatarith[approximation_preproc]:
+ "0 = real_of_float 0"
+ "1 = real_of_float 1"
+ "0 = Float 0 0"
+ "1 = Float 1 0"
+ "numeral a = Float (numeral a) 0"
+ "numeral a = real_of_float (numeral a)"
+ "x - y = x + - y"
+ "x / y = x * inverse y"
+ "ceiling x = - floor (- x)"
+ "log x y = ln y * inverse (ln x)"
+ "sin x = cos (pi / 2 - x)"
+ "tan x = sin x / cos x"
+ by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq)
+
+lemma approximation_preproc_int[approximation_preproc]:
+ "real_of_int 0 = real_of_float 0"
+ "real_of_int 1 = real_of_float 1"
+ "real_of_int (i + j) = real_of_int i + real_of_int j"
+ "real_of_int (- i) = - real_of_int i"
+ "real_of_int (i - j) = real_of_int i - real_of_int j"
+ "real_of_int (i * j) = real_of_int i * real_of_int j"
+ "real_of_int (i div j) = real_of_int (floor (real_of_int i / real_of_int j))"
+ "real_of_int (min i j) = min (real_of_int i) (real_of_int j)"
+ "real_of_int (max i j) = max (real_of_int i) (real_of_int j)"
+ "real_of_int (abs i) = abs (real_of_int i)"
+ "real_of_int (i ^ n) = (real_of_int i) ^ n"
+ "real_of_int (numeral a) = real_of_float (numeral a)"
+ "i mod j = i - i div j * j"
+ "i = j \<longleftrightarrow> real_of_int i = real_of_int j"
+ "i \<le> j \<longleftrightarrow> real_of_int i \<le> real_of_int j"
+ "i < j \<longleftrightarrow> real_of_int i < real_of_int j"
+ "i \<in> {j .. k} \<longleftrightarrow> real_of_int i \<in> {real_of_int j .. real_of_int k}"
+ by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality')
+
+lemma approximation_preproc_nat[approximation_preproc]:
+ "real 0 = real_of_float 0"
+ "real 1 = real_of_float 1"
+ "real (i + j) = real i + real j"
+ "real (i - j) = max (real i - real j) 0"
+ "real (i * j) = real i * real j"
+ "real (i div j) = real_of_int (floor (real i / real j))"
+ "real (min i j) = min (real i) (real j)"
+ "real (max i j) = max (real i) (real j)"
+ "real (i ^ n) = (real i) ^ n"
+ "real (numeral a) = real_of_float (numeral a)"
+ "i mod j = i - i div j * j"
+ "n = m \<longleftrightarrow> real n = real m"
+ "n \<le> m \<longleftrightarrow> real n \<le> real m"
+ "n < m \<longleftrightarrow> real n < real m"
+ "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
+ by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality')
+
ML_file "approximation.ML"
method_setup approximation = \<open>
@@ -4421,6 +4449,17 @@
section "Quickcheck Generator"
+lemma approximation_preproc_push_neg[approximation_preproc]:
+ fixes a b::real
+ shows
+ "\<not> (a < b) \<longleftrightarrow> b \<le> a"
+ "\<not> (a \<le> b) \<longleftrightarrow> b < a"
+ "\<not> (a = b) \<longleftrightarrow> b < a \<or> a < b"
+ "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
+ "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
+ "\<not> \<not> q \<longleftrightarrow> q"
+ by auto
+
ML_file "approximation_generator.ML"
setup "Approximation_Generator.setup"
--- a/src/HOL/Decision_Procs/approximation.ML Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Thu Sep 22 15:41:47 2016 +0200
@@ -4,6 +4,7 @@
signature APPROXIMATION =
sig
+ val reify_form: Proof.context -> term -> term
val approx: int -> Proof.context -> term -> term
val approximate: Proof.context -> term -> term
val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic
@@ -54,13 +55,12 @@
(Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
THEN' resolve_tac ctxt [TrueI]
-val form_equations = @{thms interpret_form_equations};
-
fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
- fun lookup_splitting (Free (name, _))
- = case AList.lookup (op =) splitting name
- of SOME s => HOLogic.mk_number @{typ nat} s
- | NONE => @{term "0 :: nat"}
+ fun lookup_splitting (Free (name, _)) =
+ (case AList.lookup (op =) splitting name
+ of SOME s => HOLogic.mk_number @{typ nat} s
+ | NONE => @{term "0 :: nat"})
+ | lookup_splitting t = raise TERM ("lookup_splitting", [t])
val vs = nth (Thm.prems_of st) (i - 1)
|> Logic.strip_imp_concl
|> HOLogic.dest_Trueprop
@@ -117,9 +117,13 @@
fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
| dest_interpret t = raise TERM ("dest_interpret", [t])
+fun dest_interpret_env (@{const "interpret_form"} $ _ $ xs) = xs
+ | dest_interpret_env (@{const "interpret_floatarith"} $ _ $ xs) = xs
+ | dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
-fun dest_float (@{const "Float"} $ m $ e) =
- (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+ | dest_float t = raise TERM ("dest_float", [t])
+
fun dest_ivl (Const (@{const_name "Some"}, _) $
(Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
@@ -138,8 +142,8 @@
let
val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
- fun frac c p 0 digits cnt = (digits, cnt, 0)
- | frac c 0 r digits cnt = (digits, cnt, r)
+ fun frac _ _ 0 digits cnt = (digits, cnt, 0)
+ | frac _ 0 r digits cnt = (digits, cnt, r)
| frac c p r digits cnt = (let
val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2)
in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
@@ -190,21 +194,52 @@
|> SINGLE tactic
|> the |> Thm.prems_of |> hd
-fun prepare_form ctxt term = apply_tactic ctxt term (
- REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
- eresolve_tac ctxt @{thms meta_eqE},
- resolve_tac ctxt @{thms impI}] 1)
- THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems 1) ctxt 1
- THEN DETERM (TRY (filter_prems_tac ctxt (K false) 1)))
+fun preproc_form_conv ctxt =
+ Simplifier.rewrite
+ (put_simpset HOL_basic_ss ctxt addsimps
+ (Named_Theorems.get ctxt @{named_theorems approximation_preproc}))
+
+fun reify_form_conv ctxt ct =
+ let
+ val thm =
+ Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps} ct
+ handle ERROR msg =>
+ cat_error ("Reification failed: " ^ msg)
+ ("Approximation does not support " ^
+ quote (Syntax.string_of_term ctxt (Thm.term_of ct)))
+ fun check_env (Free _) = ()
+ | check_env (Var _) = ()
+ | check_env t =
+ cat_error "Term not supported by approximation:" (Syntax.string_of_term ctxt t)
+ val _ = Thm.rhs_of thm |> Thm.term_of |> dest_interpret_env |> HOLogic.dest_list |> map check_env
+ in thm end
-fun reify_form ctxt term = apply_tactic ctxt term
- (Reification.tac ctxt form_equations NONE 1)
+
+fun reify_form_tac ctxt i = CONVERSION (Conv.arg_conv (reify_form_conv ctxt)) i
+
+fun prepare_form_tac ctxt i =
+ REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
+ eresolve_tac ctxt @{thms meta_eqE},
+ resolve_tac ctxt @{thms impI}] i)
+ THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i
+ THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
+ THEN CONVERSION (Conv.arg_conv (preproc_form_conv ctxt)) i
+
+fun prepare_form ctxt term = apply_tactic ctxt term (prepare_form_tac ctxt 1)
+
+fun apply_reify_form ctxt t = apply_tactic ctxt t (reify_form_tac ctxt 1)
+
+fun reify_form ctxt t = HOLogic.mk_Trueprop t
+ |> prepare_form ctxt
+ |> apply_reify_form ctxt
+ |> HOLogic.dest_Trueprop
fun approx_form prec ctxt t =
realify t
|> prepare_form ctxt
- |> (fn arith_term => reify_form ctxt arith_term
- |> HOLogic.dest_Trueprop |> dest_interpret_form
+ |> (fn arith_term => apply_reify_form ctxt arith_term
+ |> HOLogic.dest_Trueprop
+ |> dest_interpret_form
|> (fn (data, xs) =>
mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
(map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
@@ -216,7 +251,7 @@
fun approx_arith prec ctxt t = realify t
|> Thm.cterm_of ctxt
- |> Reification.conv ctxt form_equations
+ |> (preproc_form_conv ctxt then_conv reify_form_conv ctxt)
|> Thm.prop_of
|> Logic.dest_equals |> snd
|> dest_interpret |> fst
@@ -252,13 +287,9 @@
>> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
fun approximation_tac prec splitting taylor ctxt i =
- REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
- eresolve_tac ctxt @{thms meta_eqE},
- resolve_tac ctxt @{thms impI}] i)
- THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i
- THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
- THEN DETERM (Reification.tac ctxt form_equations NONE i)
+ prepare_form_tac ctxt i
+ THEN reify_form_tac ctxt i
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
THEN gen_eval_tac (approximation_conv ctxt) ctxt i
-
+
end;
--- a/src/HOL/Decision_Procs/approximation_generator.ML Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Thu Sep 22 15:41:47 2016 +0200
@@ -55,6 +55,7 @@
| mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
| mapprox_floatarith (@{term Power} $ a $ n) xs =
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
+ | mapprox_floatarith (@{term Floor} $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
| mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n)
| mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m
| mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
@@ -130,7 +131,13 @@
(map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $
@{term "[] :: nat list"}
in
- (if mapprox_form eps e (map (real_of_Float o fst) rs)
+ (if
+ mapprox_form eps e (map (real_of_Float o fst) rs)
+ handle
+ General.Overflow => false
+ | General.Domain => false
+ | General.Div => false
+ | IEEEReal.Unordered => false
then
let
val ts = map (fn x => snd x ()) rs
@@ -154,19 +161,12 @@
"a = b \<longleftrightarrow> a \<le> b \<and> b \<le> a"
"(p \<longrightarrow> q) \<longleftrightarrow> \<not>p \<or> q"
"(p \<longleftrightarrow> q) \<longleftrightarrow> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)"
- "\<not> (a < b) \<longleftrightarrow> b \<le> a"
- "\<not> (a \<le> b) \<longleftrightarrow> b < a"
- "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
- "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
- "\<not> \<not> q \<longleftrightarrow> q"
by auto}
-val form_equations = @{thms interpret_form_equations};
-
fun reify_goal ctxt t =
HOLogic.mk_not t
|> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
- |> conv_term ctxt (Reification.conv ctxt form_equations)
+ |> Approximation.reify_form ctxt
|> dest_interpret_form
||> HOLogic.dest_list
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Sep 22 15:41:47 2016 +0200
@@ -78,6 +78,10 @@
lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
by (approximation 30 splitting: x=1 taylor: x = 3)
-approximate "10"
+lemma "(n::real) \<in> {32 .. 62} \<Longrightarrow> \<lceil>log 2 (2 * (\<lfloor>n\<rfloor> div 2) + 1)\<rceil> = \<lceil>log 2 (\<lfloor>n\<rfloor> + 1)\<rceil>"
+ unfolding eq_iff
+ by (approximation 20)
+
+approximate 10
end
--- a/src/HOL/Library/Disjoint_Sets.thy Thu Sep 22 11:25:27 2016 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Thu Sep 22 15:41:47 2016 +0200
@@ -65,6 +65,26 @@
abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
+lemma disjoint_family_elem_disjnt:
+ assumes "infinite A" "finite C"
+ and df: "disjoint_family_on B A"
+ obtains x where "x \<in> A" "disjnt C (B x)"
+proof -
+ have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x"
+ proof -
+ obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x"
+ using * by metis
+ with df have "inj_on g A"
+ by (fastforce simp add: inj_on_def disjoint_family_on_def)
+ then have "infinite (g ` A)"
+ using \<open>infinite A\<close> finite_image_iff by blast
+ then show False
+ by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
+ qed
+ then show ?thesis
+ by (force simp: disjnt_iff intro: that)
+qed
+
lemma disjoint_family_onD:
"disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
by (auto simp: disjoint_family_on_def)