--- a/src/HOL/Analysis/Abstract_Topology.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Fri Mar 22 22:37:30 2019 +0100
@@ -2761,6 +2761,11 @@
definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
"connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
+lemma connected_spaceD:
+ "\<lbrakk>connected_space X;
+ openin X U; openin X V; topspace X \<subseteq> U \<union> V; U \<inter> V = {}; U \<noteq> {}; V \<noteq> {}\<rbrakk> \<Longrightarrow> False"
+ by (auto simp: connected_space_def)
+
lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
by (simp add: connectedin_def)
--- a/src/HOL/Analysis/Analysis.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy Fri Mar 22 22:37:30 2019 +0100
@@ -6,6 +6,7 @@
(* Topology *)
Connected
Abstract_Limits
+ Locally
(* Functional Analysis *)
Elementary_Normed_Spaces
Norm_Arith
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Mar 22 22:37:30 2019 +0100
@@ -84,7 +84,7 @@
done
qed
-lemma retraction_imp_quotient_map:
+lemma retraction_openin_vimage_iff:
"openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
if retraction: "retraction S T r" and "U \<subseteq> T"
using retraction apply (rule retractionE)
@@ -110,13 +110,13 @@
assumes "locally connected T" "S retract_of T"
shows "locally connected S"
using assms
- by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image retract_ofE)
+ by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
lemma retract_of_locally_path_connected:
assumes "locally path_connected T" "S retract_of T"
shows "locally path_connected S"
using assms
- by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image retract_ofE)
+ by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
text \<open>A few simple lemmas about deformation retracts\<close>
--- a/src/HOL/Analysis/Function_Topology.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Fri Mar 22 22:37:30 2019 +0100
@@ -3,7 +3,7 @@
*)
theory Function_Topology
-imports Topology_Euclidean_Space
+imports Topology_Euclidean_Space Abstract_Limits
begin
@@ -1480,6 +1480,8 @@
"k \<in> I \<Longrightarrow> continuous_map (product_topology X I) (X k) (\<lambda>x. x k)"
using continuous_map_componentwise [of "product_topology X I" X I id] by simp
+declare continuous_map_from_subtopology [OF continuous_map_product_projection, continuous_intros]
+
proposition open_map_product_projection:
assumes "i \<in> I"
shows "open_map (product_topology Y I) (Y i) (\<lambda>f. f i)"
@@ -1752,4 +1754,245 @@
apply (auto simp: image_iff inj_on_def)
done
+subsection\<open>Relationship with connected spaces, paths, etc.\<close>
+
+proposition connected_space_product_topology:
+ "connected_space(product_topology X I) \<longleftrightarrow>
+ (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
+ (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
+proof (cases ?eq)
+ case False
+ moreover have "?lhs = ?rhs"
+ proof
+ assume ?lhs
+ moreover
+ have "connectedin(X i) (topspace(X i))"
+ if "i \<in> I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i
+ proof -
+ have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
+ by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
+ show ?thesis
+ using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
+ by (simp add: False image_projection_PiE)
+ qed
+ ultimately show ?rhs
+ by (meson connectedin_topspace)
+ next
+ assume cs [rule_format]: ?rhs
+ have False
+ if disj: "U \<inter> V = {}" and subUV: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U \<union> V"
+ and U: "openin (product_topology X I) U"
+ and V: "openin (product_topology X I) V"
+ and "U \<noteq> {}" "V \<noteq> {}"
+ for U V
+ proof -
+ obtain f where "f \<in> U"
+ using \<open>U \<noteq> {}\<close> by blast
+ then have f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ using U openin_subset by fastforce
+ have "U \<subseteq> topspace(product_topology X I)" "V \<subseteq> topspace(product_topology X I)"
+ using U V openin_subset by blast+
+ moreover have "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U"
+ proof -
+ obtain C where "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
+ (\<Pi>\<^sub>E i\<in>I. topspace (X i))) C" "C \<subseteq> U" "f \<in> C"
+ using U \<open>f \<in> U\<close> unfolding openin_product_topology union_of_def by auto
+ then obtain \<T> where "finite \<T>"
+ and t: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i u. (i \<in> I \<and> openin (X i) u) \<and> C = {x. x i \<in> u}"
+ and subU: "topspace (product_topology X I) \<inter> \<Inter>\<T> \<subseteq> U"
+ and ftop: "f \<in> topspace (product_topology X I)"
+ and fint: "f \<in> \<Inter> \<T>"
+ by (fastforce simp: relative_to_def intersection_of_def subset_iff)
+ let ?L = "\<Union>C\<in>\<T>. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
+ obtain L where "finite L"
+ and L: "\<And>i U. \<lbrakk>i \<in> I; openin (X i) U; U \<subset> topspace(X i); {x. x i \<in> U} \<in> \<T>\<rbrakk> \<Longrightarrow> i \<in> L"
+ proof
+ show "finite ?L"
+ proof (rule finite_Union)
+ fix M
+ assume "M \<in> (\<lambda>C. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}) ` \<T>"
+ then obtain C where "C \<in> \<T>" and C: "M = {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
+ by blast
+ then obtain j V where "j \<in> I" and ope: "openin (X j) V" and Ceq: "C = {x. x j \<in> V}"
+ using t by meson
+ then have "f j \<in> V"
+ using \<open>C \<in> \<T>\<close> fint by force
+ then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
+ using that
+ apply (clarsimp simp add: set_eq_iff)
+ apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
+ done
+ then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
+ using Ceq by auto
+ then show "finite M"
+ using C finite_subset by fastforce
+ qed (use \<open>finite \<T>\<close> in blast)
+ next
+ fix i U
+ assume "i \<in> I" and ope: "openin (X i) U" and psub: "U \<subset> topspace (X i)" and int: "{x. x i \<in> U} \<in> \<T>"
+ then show "i \<in> ?L"
+ by (rule_tac a="{x. x i \<in> U}" in UN_I) (force+)
+ qed
+ show ?thesis
+ proof
+ fix h
+ assume h: "h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ define g where "g \<equiv> \<lambda>i. if i \<in> L then f i else h i"
+ have gin: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ unfolding g_def using f h by auto
+ moreover have "g \<in> X" if "X \<in> \<T>" for X
+ using fint openin_subset t [OF that] L g_def h that by fastforce
+ ultimately have "g \<in> U"
+ using subU by auto
+ have "h \<in> U" if "finite M" "h \<in> PiE I (topspace \<circ> X)" "{i \<in> I. h i \<noteq> g i} \<subseteq> M" for M h
+ using that
+ proof (induction arbitrary: h)
+ case empty
+ then show ?case
+ using PiE_ext \<open>g \<in> U\<close> gin by force
+ next
+ case (insert i M)
+ define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
+ have fin: "f \<in> PiE I (topspace \<circ> X)"
+ unfolding f_def using gin insert.prems(1) by auto
+ have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
+ unfolding f_def using insert.prems(2) by auto
+ have "f \<in> U"
+ using insert.IH [OF fin subM] .
+ show ?case
+ proof (cases "h \<in> V")
+ case True
+ show ?thesis
+ proof (cases "i \<in> I")
+ case True
+ let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
+ let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
+ have False
+ proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
+ have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
+ using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
+ then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
+ using \<open>i \<in> I\<close> insert.prems(1)
+ by (auto simp: continuous_map_componentwise extensional_def)
+ show "openin (X i) ?U"
+ by (rule openin_continuous_map_preimage [OF cm U])
+ show "openin (X i) ?V"
+ by (rule openin_continuous_map_preimage [OF cm V])
+ show "topspace (X i) \<subseteq> ?U \<union> ?V"
+ proof clarsimp
+ fix x
+ assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
+ with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
+ show "(\<lambda>j. if j = i then x else h j) \<in> U"
+ by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
+ qed
+ show "?U \<inter> ?V = {}"
+ using disj by blast
+ show "?U \<noteq> {}"
+ using \<open>U \<noteq> {}\<close> f_def
+ proof -
+ have "(\<lambda>j. if j = i then g i else h j) \<in> U"
+ using \<open>f \<in> U\<close> f_def by blast
+ moreover have "f i \<in> topspace (X i)"
+ by (metis PiE_iff True comp_apply fin)
+ ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
+ using f_def by auto
+ then show ?thesis
+ by blast
+ qed
+ have "(\<lambda>j. if j = i then h i else h j) = h"
+ by force
+ moreover have "h i \<in> topspace (X i)"
+ using True insert.prems(1) by auto
+ ultimately show "?V \<noteq> {}"
+ using \<open>h \<in> V\<close> by force
+ qed
+ then show ?thesis ..
+ next
+ case False
+ show ?thesis
+ proof (cases "h = f")
+ case True
+ show ?thesis
+ by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
+ next
+ case False
+ then show ?thesis
+ using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
+ qed
+ qed
+ next
+ case False
+ then show ?thesis
+ using subUV insert.prems(1) by auto
+ qed
+ qed
+ then show "h \<in> U"
+ unfolding g_def using PiE_iff \<open>finite L\<close> h by fastforce
+ qed
+ qed
+ ultimately show ?thesis
+ using disj inf_absorb2 \<open>V \<noteq> {}\<close> by fastforce
+ qed
+ then show ?lhs
+ unfolding connected_space_def
+ by auto
+ qed
+ ultimately show ?thesis
+ by simp
+qed (simp add: connected_space_topspace_empty)
+
+
+lemma connectedin_PiE:
+ "connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
+ PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
+ by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff
+ topspace_subtopology_subset)
+
+lemma path_connected_space_product_topology:
+ "path_connected_space(product_topology X I) \<longleftrightarrow>
+ topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. path_connected_space(X i))"
+ (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
+proof (cases ?eq)
+ case False
+ moreover have "?lhs = ?rhs"
+ proof
+ assume L: ?lhs
+ show ?rhs
+ proof (clarsimp simp flip: path_connectedin_topspace)
+ fix i :: "'a"
+ assume "i \<in> I"
+ have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
+ by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
+ show "path_connectedin (X i) (topspace (X i))"
+ using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]]
+ by (metis \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
+ qed
+ next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ unfolding path_connected_space_def topspace_product_topology
+ proof clarify
+ fix x y
+ assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and y: "y \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ have "\<forall>i. \<exists>g. i \<in> I \<longrightarrow> pathin (X i) g \<and> g 0 = x i \<and> g 1 = y i"
+ using PiE_mem R path_connected_space_def x y by force
+ then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> pathin (X i) (g i) \<and> g i 0 = x i \<and> g i 1 = y i"
+ by metis
+ with x y show "\<exists>g. pathin (product_topology X I) g \<and> g 0 = x \<and> g 1 = y"
+ apply (rule_tac x="\<lambda>a. \<lambda>i \<in> I. g i a" in exI)
+ apply (force simp: pathin_def continuous_map_componentwise)
+ done
+ qed
+ qed
+ ultimately show ?thesis
+ by simp
+qed (simp add: path_connected_space_topspace_empty)
+
+lemma path_connectedin_PiE:
+ "path_connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
+ PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
+ by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
+
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Locally.thy Fri Mar 22 22:37:30 2019 +0100
@@ -0,0 +1,449 @@
+section \<open>Neigbourhood bases and Locally path-connected spaces\<close>
+
+theory Locally
+ imports
+ Path_Connected Function_Topology
+begin
+
+subsection\<open>Neigbourhood bases (useful for "local" properties of various kinds)\<close>
+
+definition neighbourhood_base_at where
+ "neighbourhood_base_at x P X \<equiv>
+ \<forall>W. openin X W \<and> x \<in> W
+ \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
+
+definition neighbourhood_base_of where
+ "neighbourhood_base_of P X \<equiv>
+ \<forall>x \<in> topspace X. neighbourhood_base_at x P X"
+
+lemma neighbourhood_base_of:
+ "neighbourhood_base_of P X \<longleftrightarrow>
+ (\<forall>W x. openin X W \<and> x \<in> W
+ \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
+ unfolding neighbourhood_base_at_def neighbourhood_base_of_def
+ using openin_subset by blast
+
+lemma neighbourhood_base_at_mono:
+ "\<lbrakk>neighbourhood_base_at x P X; \<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_at x Q X"
+ unfolding neighbourhood_base_at_def
+ by (meson subset_eq)
+
+lemma neighbourhood_base_of_mono:
+ "\<lbrakk>neighbourhood_base_of P X; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_of Q X"
+ unfolding neighbourhood_base_of_def
+ using neighbourhood_base_at_mono by force
+
+lemma open_neighbourhood_base_at:
+ "(\<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> openin X S)
+ \<Longrightarrow> neighbourhood_base_at x P X \<longleftrightarrow> (\<forall>W. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))"
+ unfolding neighbourhood_base_at_def
+ by (meson subsetD)
+
+lemma open_neighbourhood_base_of:
+ "(\<forall>S. P S \<longrightarrow> openin X S)
+ \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow> (\<forall>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))"
+ apply (simp add: neighbourhood_base_of, safe, blast)
+ by meson
+
+lemma neighbourhood_base_of_open_subset:
+ "\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk>
+ \<Longrightarrow> neighbourhood_base_of P (subtopology X S)"
+ apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def)
+ apply (rename_tac x V)
+ apply (drule_tac x="S \<inter> V" in spec)
+ apply (simp add: Int_ac)
+ by (metis IntI le_infI1 openin_Int)
+
+lemma neighbourhood_base_of_topology_base:
+ "openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>)
+ \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow>
+ (\<forall>W x. W \<in> \<B> \<and> x \<in> W \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
+ apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
+ by (meson subset_trans)
+
+lemma neighbourhood_base_at_unlocalized:
+ assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T"
+ shows "neighbourhood_base_at x P X
+ \<longleftrightarrow> (x \<in> topspace X \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> topspace X))"
+ (is "?lhs = ?rhs")
+proof
+ assume R: ?rhs show ?lhs
+ unfolding neighbourhood_base_at_def
+ proof clarify
+ fix W
+ assume "openin X W" "x \<in> W"
+ then have "x \<in> topspace X"
+ using openin_subset by blast
+ with R obtain U V where "openin X U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> topspace X"
+ by blast
+ then show "\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+ by (metis IntI \<open>openin X W\<close> \<open>x \<in> W\<close> assms inf_le1 inf_le2 openin_Int)
+ qed
+qed (simp add: neighbourhood_base_at_def)
+
+lemma neighbourhood_base_at_with_subset:
+ "\<lbrakk>openin X U; x \<in> U\<rbrakk>
+ \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)"
+ apply (simp add: neighbourhood_base_at_def)
+ apply (metis IntI Int_subset_iff openin_Int)
+ done
+
+lemma neighbourhood_base_of_with_subset:
+ "neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X"
+ using neighbourhood_base_at_with_subset
+ by (fastforce simp add: neighbourhood_base_of_def)
+
+subsection\<open>Locally path-connected spaces\<close>
+
+definition weakly_locally_path_connected_at
+ where "weakly_locally_path_connected_at x X \<equiv> neighbourhood_base_at x (path_connectedin X) X"
+
+definition locally_path_connected_at
+ where "locally_path_connected_at x X \<equiv>
+ neighbourhood_base_at x (\<lambda>U. openin X U \<and> path_connectedin X U) X"
+
+definition locally_path_connected_space
+ where "locally_path_connected_space X \<equiv> neighbourhood_base_of (path_connectedin X) X"
+
+lemma locally_path_connected_space_alt:
+ "locally_path_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> path_connectedin X U) X"
+ (is "?P = ?Q")
+ and locally_path_connected_space_eq_open_path_component_of:
+ "locally_path_connected_space X \<longleftrightarrow>
+ (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (Collect (path_component_of (subtopology X U) x)))"
+ (is "?P = ?R")
+proof -
+ have ?P if ?Q
+ using locally_path_connected_space_def neighbourhood_base_of_mono that by auto
+ moreover have ?R if P: ?P
+ proof -
+ show ?thesis
+ proof clarify
+ fix U y
+ assume "openin X U" "y \<in> U"
+ have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> Collect (path_component_of (subtopology X U) y)"
+ if "path_component_of (subtopology X U) y x" for x
+
+ proof -
+ have "x \<in> U"
+ using path_component_of_equiv that topspace_subtopology by fastforce
+ then have "\<exists>Ua. openin X Ua \<and> (\<exists>V. path_connectedin X V \<and> x \<in> Ua \<and> Ua \<subseteq> V \<and> V \<subseteq> U)"
+ using P
+ by (simp add: \<open>openin X U\<close> locally_path_connected_space_def neighbourhood_base_of)
+ then show ?thesis
+ by (metis dual_order.trans path_component_of_equiv path_component_of_maximal path_connectedin_subtopology subset_iff that)
+ qed
+ then show "openin X (Collect (path_component_of (subtopology X U) y))"
+ using openin_subopen by force
+ qed
+ qed
+ moreover have ?Q if ?R
+ using that
+ apply (simp add: open_neighbourhood_base_of)
+ by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
+ ultimately show "?P = ?Q" "?P = ?R"
+ by blast+
+qed
+
+lemma locally_path_connected_space:
+ "locally_path_connected_space X
+ \<longleftrightarrow> (\<forall>V x. openin X V \<and> x \<in> V \<longrightarrow> (\<exists>U. openin X U \<and> path_connectedin X U \<and> x \<in> U \<and> U \<subseteq> V))"
+ by (simp add: locally_path_connected_space_alt open_neighbourhood_base_of)
+
+lemma locally_path_connected_space_open_path_components:
+ "locally_path_connected_space X \<longleftrightarrow>
+ (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
+ apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology)
+ by (metis imageI inf.absorb_iff2 openin_closedin_eq)
+
+lemma openin_path_component_of_locally_path_connected_space:
+ "locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))"
+ apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
+ by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace)
+
+lemma openin_path_components_of_locally_path_connected_space:
+ "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c"
+ apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
+ by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace)
+
+lemma closedin_path_components_of_locally_path_connected_space:
+ "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c"
+ by (simp add: closedin_def complement_path_components_of_Union openin_path_components_of_locally_path_connected_space openin_clauses(3) path_components_of_subset)
+
+lemma closedin_path_component_of_locally_path_connected_space:
+ assumes "locally_path_connected_space X"
+ shows "closedin X (Collect (path_component_of X x))"
+proof (cases "x \<in> topspace X")
+ case True
+ then show ?thesis
+ by (simp add: assms closedin_path_components_of_locally_path_connected_space path_component_in_path_components_of)
+next
+ case False
+ then show ?thesis
+ by (metis closedin_empty path_component_of_eq_empty)
+qed
+
+lemma weakly_locally_path_connected_at:
+ "weakly_locally_path_connected_at x X \<longleftrightarrow>
+ (\<forall>V. openin X V \<and> x \<in> V
+ \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
+ (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def)
+ by (meson order_trans subsetD)
+next
+ have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W"
+ if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)"
+ for W U
+ proof (intro exI conjI)
+ let ?V = "(Collect (path_component_of (subtopology X W) x))"
+ show "path_connectedin X (Collect (path_component_of (subtopology X W) x))"
+ by (meson path_connectedin_path_component_of path_connectedin_subtopology)
+ show "U \<subseteq> ?V"
+ by (auto simp: path_component_of path_connectedin_subtopology that)
+ show "?V \<subseteq> W"
+ by (meson path_connectedin_path_component_of path_connectedin_subtopology)
+ qed
+ assume ?rhs
+ then show ?lhs
+ unfolding weakly_locally_path_connected_at_def neighbourhood_base_at_def by (metis "*")
+qed
+
+lemma locally_path_connected_space_im_kleinen:
+ "locally_path_connected_space X \<longleftrightarrow>
+ (\<forall>V x. openin X V \<and> x \<in> V
+ \<longrightarrow> (\<exists>U. openin X U \<and>
+ x \<in> U \<and> U \<subseteq> V \<and>
+ (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and>
+ c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))"
+ apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def)
+ apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def)
+ using openin_subset apply force
+ done
+
+lemma locally_path_connected_space_open_subset:
+ "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk>
+ \<Longrightarrow> locally_path_connected_space (subtopology X s)"
+ apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology)
+ by (meson order_trans)
+
+lemma locally_path_connected_space_quotient_map_image:
+ assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X"
+ shows "locally_path_connected_space Y"
+ unfolding locally_path_connected_space_open_path_components
+proof clarify
+ fix V C
+ assume V: "openin Y V" and c: "C \<in> path_components_of (subtopology Y V)"
+ then have sub: "C \<subseteq> topspace Y"
+ using path_connectedin_path_components_of path_connectedin_subset_topspace path_connectedin_subtopology by blast
+ have "openin X {x \<in> topspace X. f x \<in> C}"
+ proof (subst openin_subopen, clarify)
+ fix x
+ assume x: "x \<in> topspace X" and "f x \<in> C"
+ let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)"
+ show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
+ proof (intro exI conjI)
+ have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
+ proof (intro exI conjI)
+ show "openin X ({z \<in> topspace X. f z \<in> V})"
+ using V f openin_subset quotient_map_def by fastforce
+ show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
+ \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
+ by (metis (no_types, lifting) Int_iff \<open>f x \<in> C\<close> c mem_Collect_eq path_component_in_path_components_of path_components_of_subset topspace_subtopology topspace_subtopology_subset x)
+ qed
+ with X show "openin X ?T"
+ using locally_path_connected_space_open_path_components by blast
+ show x: "x \<in> ?T"
+ using V \<open>f x \<in> C\<close> c openin_subset path_component_of_equiv path_components_of_subset topspace_subtopology topspace_subtopology_subset x
+ by fastforce
+ have "f ` ?T \<subseteq> C"
+ proof (rule path_components_of_maximal)
+ show "C \<in> path_components_of (subtopology Y V)"
+ by (simp add: c)
+ show "path_connectedin (subtopology Y V) (f ` ?T)"
+ proof -
+ have "quotient_map (subtopology X {a \<in> topspace X. f a \<in> V}) (subtopology Y V) f"
+ by (simp add: V f quotient_map_restriction)
+ then show ?thesis
+ by (meson path_connectedin_continuous_map_image path_connectedin_path_component_of quotient_imp_continuous_map)
+ qed
+ show "\<not> disjnt C (f ` ?T)"
+ by (metis (no_types, lifting) \<open>f x \<in> C\<close> x disjnt_iff image_eqI)
+ qed
+ then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}"
+ by (force simp: path_component_of_equiv topspace_subtopology)
+ qed
+ qed
+ then show "openin Y C"
+ using f sub by (simp add: quotient_map_def)
+qed
+
+lemma homeomorphic_locally_path_connected_space:
+ assumes "X homeomorphic_space Y"
+ shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y"
+proof -
+ obtain f g where "homeomorphic_maps X Y f g"
+ using assms homeomorphic_space_def by fastforce
+ then show ?thesis
+ by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image)
+qed
+
+lemma locally_path_connected_space_retraction_map_image:
+ "\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk>
+ \<Longrightarrow> locally_path_connected_space Y"
+ using Abstract_Topology.retraction_imp_quotient_map locally_path_connected_space_quotient_map_image by blast
+
+lemma locally_path_connected_space_euclideanreal: "locally_path_connected_space euclideanreal"
+ unfolding locally_path_connected_space_def neighbourhood_base_of
+ proof clarsimp
+ fix W and x :: "real"
+ assume "open W" "x \<in> W"
+ then obtain e where "e > 0" and e: "\<And>x'. \<bar>x' - x\<bar> < e \<longrightarrow> x' \<in> W"
+ by (auto simp: open_real)
+ then show "\<exists>U. open U \<and> (\<exists>V. path_connected V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
+ by (force intro!: convex_imp_path_connected exI [where x = "{x-e<..<x+e}"])
+qed
+
+lemma locally_path_connected_space_discrete_topology:
+ "locally_path_connected_space (discrete_topology U)"
+ using locally_path_connected_space_open_path_components by fastforce
+
+lemma path_component_eq_connected_component_of:
+ assumes "locally_path_connected_space X"
+ shows "(path_component_of_set X x = connected_component_of_set X x)"
+proof (cases "x \<in> topspace X")
+ case True
+ then show ?thesis
+ using connectedin_connected_component_of [of X x]
+ apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong)
+ apply (drule_tac x="path_component_of_set X x" in spec)
+ by (metis assms closedin_closed_subtopology closedin_connected_component_of closedin_path_component_of_locally_path_connected_space inf.absorb_iff2 inf.orderE openin_path_component_of_locally_path_connected_space openin_subtopology path_component_of_eq_empty path_component_subset_connected_component_of)
+next
+ case False
+ then show ?thesis
+ using connected_component_of_eq_empty path_component_of_eq_empty by fastforce
+qed
+
+lemma path_components_eq_connected_components_of:
+ "locally_path_connected_space X \<Longrightarrow> (path_components_of X = connected_components_of X)"
+ by (simp add: path_components_of_def connected_components_of_def image_def path_component_eq_connected_component_of)
+
+lemma path_connected_eq_connected_space:
+ "locally_path_connected_space X
+ \<Longrightarrow> path_connected_space X \<longleftrightarrow> connected_space X"
+ by (metis connected_components_of_subset_sing path_components_eq_connected_components_of path_components_of_subset_singleton)
+
+lemma locally_path_connected_space_product_topology:
+ "locally_path_connected_space(product_topology X I) \<longleftrightarrow>
+ topspace(product_topology X I) = {} \<or>
+ finite {i. i \<in> I \<and> ~path_connected_space(X i)} \<and>
+ (\<forall>i \<in> I. locally_path_connected_space(X i))"
+ (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
+proof (cases ?empty)
+ case True
+ then show ?thesis
+ by (simp add: locally_path_connected_space_def neighbourhood_base_of openin_closedin_eq)
+next
+ case False
+ then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ by auto
+ have ?rhs if L: ?lhs
+ proof -
+ obtain U C where U: "openin (product_topology X I) U"
+ and V: "path_connectedin (product_topology X I) C"
+ and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
+ by (metis openin_topspace topspace_product_topology z)
+ then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
+ and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U"
+ by (force simp: openin_product_topology_alt)
+ show ?thesis
+ proof (intro conjI ballI)
+ have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
+ proof -
+ have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)"
+ apply (rule path_connectedin_continuous_map_image [OF _ V])
+ by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+ moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
+ proof
+ show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
+ by (simp add: pc path_connectedin_subset_topspace)
+ have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)"
+ by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1))
+ also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U"
+ using subU by blast
+ finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C"
+ using \<open>U \<subseteq> C\<close> that by blast
+ qed
+ ultimately show ?thesis
+ by (simp add: path_connectedin_topspace)
+ qed
+ then have "{i \<in> I. \<not> path_connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
+ by blast
+ with finV show "finite {i \<in> I. \<not> path_connected_space (X i)}"
+ using finite_subset by blast
+ next
+ show "locally_path_connected_space (X i)" if "i \<in> I" for i
+ apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"])
+ by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that)
+ qed
+ qed
+ moreover have ?lhs if R: ?rhs
+ proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
+ fix F z
+ assume "openin (product_topology X I) F" and "z \<in> F"
+ then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}"
+ and opeW: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (W i)" and "z \<in> Pi\<^sub>E I W" "Pi\<^sub>E I W \<subseteq> F"
+ by (auto simp: openin_product_topology_alt)
+ have "\<forall>i \<in> I. \<exists>U C. openin (X i) U \<and> path_connectedin (X i) C \<and> z i \<in> U \<and> U \<subseteq> C \<and> C \<subseteq> W i \<and>
+ (W i = topspace (X i) \<and>
+ path_connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))"
+ (is "\<forall>i \<in> I. ?\<Phi> i")
+ proof
+ fix i assume "i \<in> I"
+ have "locally_path_connected_space (X i)"
+ by (simp add: R \<open>i \<in> I\<close>)
+ moreover have "openin (X i) (W i) " "z i \<in> W i"
+ using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
+ ultimately obtain U C where UC: "openin (X i) U" "path_connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
+ using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of)
+ show "?\<Phi> i"
+ proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)")
+ case True
+ then show ?thesis
+ using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast
+ next
+ case False
+ then show ?thesis
+ by (meson UC)
+ qed
+ qed
+ then obtain U C where
+ *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> path_connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
+ (W i = topspace (X i) \<and> path_connected_space (X i)
+ \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))"
+ by metis
+ let ?A = "{i \<in> I. \<not> path_connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}"
+ have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A"
+ by (clarsimp simp add: "*")
+ moreover have "finite ?A"
+ by (simp add: that finW)
+ ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+ using finite_subset by auto
+ then have "openin (product_topology X I) (Pi\<^sub>E I U)"
+ using * by (simp add: openin_PiE_gen)
+ then show "\<exists>U. openin (product_topology X I) U \<and>
+ (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
+ apply (rule_tac x="PiE I U" in exI, simp)
+ apply (rule_tac x="PiE I C" in exI)
+ using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
+ apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
+ done
+ qed
+ ultimately show ?thesis
+ using False by blast
+qed
+
+end
--- a/src/HOL/Analysis/Product_Topology.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy Fri Mar 22 22:37:30 2019 +0100
@@ -1,7 +1,7 @@
section\<open>The binary product topology\<close>
theory Product_Topology
-imports Function_Topology
+imports Function_Topology Abstract_Limits
begin
section \<open>Product Topology\<close>
@@ -519,5 +519,49 @@
then show ?thesis by metis
qed
+lemma limitin_pairwise:
+ "limitin (prod_topology X Y) f l F \<longleftrightarrow> limitin X (fst \<circ> f) (fst l) F \<and> limitin Y (snd \<circ> f) (snd l) F"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then obtain a b where ev: "\<And>U. \<lbrakk>(a,b) \<in> U; openin (prod_topology X Y) U\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in F. f x \<in> U"
+ and a: "a \<in> topspace X" and b: "b \<in> topspace Y" and l: "l = (a,b)"
+ by (auto simp: limitin_def)
+ moreover have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" if "openin X U" "a \<in> U" for U
+ proof -
+ have "\<forall>\<^sub>F c in F. f c \<in> U \<times> topspace Y"
+ using b that ev [of "U \<times> topspace Y"] by (auto simp: openin_prod_topology_alt)
+ then show ?thesis
+ by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
+ qed
+ moreover have "\<forall>\<^sub>F x in F. snd (f x) \<in> U" if "openin Y U" "b \<in> U" for U
+ proof -
+ have "\<forall>\<^sub>F c in F. f c \<in> topspace X \<times> U"
+ using a that ev [of "topspace X \<times> U"] by (auto simp: openin_prod_topology_alt)
+ then show ?thesis
+ by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
+ qed
+ ultimately show ?rhs
+ by (simp add: limitin_def)
+next
+ have "limitin (prod_topology X Y) f (a,b) F"
+ if "limitin X (fst \<circ> f) a F" "limitin Y (snd \<circ> f) b F" for a b
+ using that
+ proof (clarsimp simp: limitin_def)
+ fix Z :: "('a \<times> 'b) set"
+ assume a: "a \<in> topspace X" "\<forall>U. openin X U \<and> a \<in> U \<longrightarrow> (\<forall>\<^sub>F x in F. fst (f x) \<in> U)"
+ and b: "b \<in> topspace Y" "\<forall>U. openin Y U \<and> b \<in> U \<longrightarrow> (\<forall>\<^sub>F x in F. snd (f x) \<in> U)"
+ and Z: "openin (prod_topology X Y) Z" "(a, b) \<in> Z"
+ then obtain U V where "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> Z"
+ using Z by (force simp: openin_prod_topology_alt)
+ then have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" "\<forall>\<^sub>F x in F. snd (f x) \<in> V"
+ by (simp_all add: a b)
+ then show "\<forall>\<^sub>F x in F. f x \<in> Z"
+ by (rule eventually_elim2) (use \<open>U \<times> V \<subseteq> Z\<close> subsetD in auto)
+ qed
+ then show "?rhs \<Longrightarrow> ?lhs"
+ by (metis prod.collapse)
+qed
+
end
--- a/src/HOL/Code_Numeral.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Code_Numeral.thy Fri Mar 22 22:37:30 2019 +0100
@@ -190,11 +190,18 @@
is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
.
+lemma integer_less_eq_iff:
+ "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
+ by (fact less_eq_integer.rep_eq)
lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
is "less :: int \<Rightarrow> int \<Rightarrow> bool"
.
+lemma integer_less_iff:
+ "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
+ by (fact less_integer.rep_eq)
+
lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
.
@@ -320,7 +327,7 @@
end
declare divmod_algorithm_code [where ?'a = integer,
- folded integer_of_num_def, unfolded integer_of_num_triv,
+ folded integer_of_num_def, unfolded integer_of_num_triv,
code]
lemma integer_of_nat_0: "integer_of_nat 0 = 0"
@@ -492,7 +499,7 @@
"divmod_abs 0 j = (0, 0)"
by (simp_all add: prod_eq_iff)
-lemma divmod_integer_code [code]:
+lemma divmod_integer_eq_cases:
"divmod_integer k l =
(if k = 0 then (0, 0) else if l = 0 then (0, k) else
(apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
@@ -500,14 +507,30 @@
else (let (r, s) = divmod_abs k l in
if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
proof -
- have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
+ have *: "sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0" for k l :: int
by (auto simp add: sgn_if)
- have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto
+ have **: "- k = l * q \<longleftrightarrow> k = - (l * q)" for k l q :: int
+ by auto
show ?thesis
- by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
- (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
+ by (simp add: divmod_integer_def divmod_abs_def)
+ (transfer, auto simp add: * ** not_less zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right)
qed
+lemma divmod_integer_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
+ "divmod_integer k l =
+ (if k = 0 then (0, 0)
+ else if l > 0 then
+ (if k > 0 then Code_Numeral.divmod_abs k l
+ else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
+ if s = 0 then (- r, 0) else (- r - 1, l - s))
+ else if l = 0 then (0, k)
+ else apsnd uminus
+ (if k < 0 then Code_Numeral.divmod_abs k l
+ else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
+ if s = 0 then (- r, 0) else (- r - 1, - l - s)))"
+ by (cases l "0 :: integer" rule: linorder_cases)
+ (auto split: prod.splits simp add: divmod_integer_eq_cases)
+
lemma div_integer_code [code]:
"k div l = fst (divmod_integer k l)"
by simp
@@ -743,6 +766,8 @@
code_identifier
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+export_code divmod_integer in Haskell
+
subsection \<open>Type of target language naturals\<close>
--- a/src/HOL/Library/Code_Target_Nat.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Fri Mar 22 22:37:30 2019 +0100
@@ -93,14 +93,26 @@
"integer_of_nat (m mod n) = of_nat m mod of_nat n"
by transfer (simp add: zmod_int)
-lemma [code]:
- "Divides.divmod_nat m n = (m div n, m mod n)"
- by (fact divmod_nat_def)
+context
+ includes integer.lifting
+begin
+
+lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
+ "Divides.divmod_nat m n = (
+ let k = integer_of_nat m; l = integer_of_nat n
+ in map_prod nat_of_integer nat_of_integer
+ (if k = 0 then (0, 0)
+ else if l = 0 then (0, k) else
+ Code_Numeral.divmod_abs k l))"
+ by (simp add: prod_eq_iff Let_def; transfer)
+ (simp add: nat_div_distrib nat_mod_distrib)
+
+end
lemma [code]:
"divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
- by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
- (transfer, simp_all only: nat_div_distrib nat_mod_distrib
+ by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv; transfer)
+ (simp_all only: nat_div_distrib nat_mod_distrib
zero_le_numeral nat_numeral)
lemma [code]:
--- a/src/HOL/Library/Dual_Ordered_Lattice.thy Fri Mar 22 22:26:57 2019 +0100
+++ b/src/HOL/Library/Dual_Ordered_Lattice.thy Fri Mar 22 22:37:30 2019 +0100
@@ -24,6 +24,8 @@
setup_lifting type_definition_dual
+code_datatype dual
+
lemma dual_eqI:
"x = y" if "undual x = undual y"
using that by transfer assumption
@@ -36,7 +38,7 @@
"dual x = dual y \<longleftrightarrow> x = y"
by transfer simp
-lemma undual_dual [simp]:
+lemma undual_dual [simp, code]:
"undual (dual x) = x"
by transfer rule
@@ -84,6 +86,17 @@
by (simp add: surj_dual)
qed
+instantiation dual :: (equal) equal
+begin
+
+lift_definition equal_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
+ is HOL.equal .
+
+instance
+ by (standard; transfer) (simp add: equal)
+
+end
+
subsection \<open>Pointwise ordering\<close>