--- a/src/HOL/Algebra/Coset.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Coset.thy Mon Apr 01 17:02:43 2019 +0100
@@ -1379,7 +1379,7 @@
qed
qed
-lemma (in group) normal_inter_subgroup:
+lemma (in group) normal_Int_subgroup:
assumes "subgroup H G"
and "N \<lhd> G"
shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
--- a/src/HOL/Algebra/Generated_Groups.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy Mon Apr 01 17:02:43 2019 +0100
@@ -563,4 +563,13 @@
by (simp add: int_pow_def2 pow_subgroup_generated)
qed
+lemma kernel_from_subgroup_generated [simp]:
+ "subgroup S G \<Longrightarrow> kernel (subgroup_generated G S) H f = kernel G H f \<inter> S"
+ using subgroup.carrier_subgroup_generated_subgroup subgroup.subset
+ by (fastforce simp add: kernel_def set_eq_iff)
+
+lemma kernel_to_subgroup_generated [simp]:
+ "kernel G (subgroup_generated H S) f = kernel G H f"
+ by (simp add: kernel_def)
+
end
\ No newline at end of file
--- a/src/HOL/Algebra/Group.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Group.thy Mon Apr 01 17:02:43 2019 +0100
@@ -425,7 +425,20 @@
end
lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
-by(simp add: int_pow_def nat_pow_def)
+ by(simp add: int_pow_def nat_pow_def)
+
+lemma pow_nat:
+ assumes "i\<ge>0"
+ shows "x [^]\<^bsub>G\<^esub> nat i = x [^]\<^bsub>G\<^esub> i"
+proof (cases i rule: int_cases)
+ case (nonneg n)
+ then show ?thesis
+ by (simp add: int_pow_int)
+next
+ case (neg n)
+ then show ?thesis
+ using assms by linarith
+qed
lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \<one>\<^bsub>G\<^esub>"
by (simp add: int_pow_def)
@@ -450,6 +463,9 @@
"x \<in> carrier G \<Longrightarrow> x [^] (-i::int) = inv (x [^] i)"
by (simp add: int_pow_def2)
+lemma (in group) int_pow_neg_int: "x \<in> carrier G \<Longrightarrow> x [^] -(int n) = inv (x [^] n)"
+ by (simp add: int_pow_neg int_pow_int)
+
lemma (in group) int_pow_mult:
assumes "x \<in> carrier G" shows "x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
proof -
@@ -502,6 +518,38 @@
by(simp add: inj_on_def)
+lemma (in monoid) group_commutes_pow:
+ fixes n::nat
+ shows "\<lbrakk>x \<otimes> y = y \<otimes> x; x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x [^] n \<otimes> y = y \<otimes> x [^] n"
+ apply (induction n, auto)
+ by (metis m_assoc nat_pow_closed)
+
+lemma (in monoid) pow_mult_distrib:
+ assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
+proof (induct n)
+ case (Suc n)
+ have "x \<otimes> (y [^] n \<otimes> y) = y [^] n \<otimes> x \<otimes> y"
+ by (simp add: eq group_commutes_pow m_assoc xy)
+ then show ?case
+ using assms Suc.hyps m_assoc by auto
+qed auto
+
+lemma (in group) int_pow_mult_distrib:
+ assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+proof (cases i rule: int_cases)
+ case (nonneg n)
+ then show ?thesis
+ by (metis eq int_pow_int pow_mult_distrib xy)
+next
+ case (neg n)
+ then show ?thesis
+ unfolding neg
+ apply (simp add: xy int_pow_neg_int del: of_nat_Suc)
+ by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
+qed
+
subsection \<open>Submonoids\<close>
locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
@@ -852,7 +900,7 @@
lemma id_iso: "id \<in> iso G G"
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
-corollary iso_refl : "G \<cong> G"
+corollary iso_refl [simp]: "G \<cong> G"
using iso_set_refl unfolding is_iso_def by auto
lemma trivial_hom:
@@ -901,11 +949,11 @@
corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
using iso_set_sym unfolding is_iso_def by auto
-lemma (in group) iso_set_trans:
- "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
- by (auto simp add: iso_def hom_compose bij_betw_compose)
+lemma iso_set_trans:
+ "\<lbrakk>h \<in> Group.iso G H; i \<in> Group.iso H I\<rbrakk> \<Longrightarrow> i \<circ> h \<in> Group.iso G I"
+ by (force simp: iso_def hom_compose intro: bij_betw_trans)
-corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
+corollary iso_trans [trans]: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
using iso_set_trans unfolding is_iso_def by blast
lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
@@ -1081,6 +1129,8 @@
fixes h
assumes homh [simp]: "h \<in> hom G H"
+declare group_hom.homh [simp]
+
lemma (in group_hom) hom_mult [simp]:
"[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
proof -
@@ -1170,14 +1220,21 @@
using subgroup.subgroup_is_group[OF assms is_group]
is_group subgroup.subset[OF assms] by auto
-lemma (in group_hom) nat_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_nat_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
"x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
by (induction n) auto
-lemma (in group_hom) int_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_int_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
"x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
- using nat_pow_hom by (simp add: int_pow_def2)
+ using hom_nat_pow by (simp add: int_pow_def2)
+lemma hom_nat_pow:
+ "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
+ by (simp add: group_hom.hom_nat_pow group_hom_axioms_def group_hom_def)
+
+lemma hom_int_pow:
+ "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
+ by (simp add: group_hom.hom_int_pow group_hom_axioms.intro group_hom_def)
subsection \<open>Commutative Structures\<close>
@@ -1225,11 +1282,6 @@
shows "comm_monoid G"
by (rule comm_monoidI) (auto intro: m_assoc m_comm)
-lemma (in comm_monoid) nat_pow_distr:
- "[| x \<in> carrier G; y \<in> carrier G |] ==>
- (x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
- by (induct n) (simp, simp add: m_ac)
-
lemma (in comm_monoid) submonoid_is_comm_monoid :
assumes "submonoid H G"
shows "comm_monoid (G\<lparr>carrier := H\<rparr>)"
@@ -1279,6 +1331,17 @@
"[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
by (simp add: m_ac inv_mult_group)
+lemma (in comm_monoid) nat_pow_distrib:
+ fixes n::nat
+ assumes "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] n = x [^] n \<otimes> y [^] n"
+ by (simp add: assms pow_mult_distrib m_comm)
+
+lemma (in comm_group) int_pow_distrib:
+ assumes "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+ by (simp add: assms int_pow_mult_distrib m_comm)
+
lemma (in comm_monoid) hom_imp_img_comm_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "h \<in> hom G H"
shows "comm_monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "comm_monoid ?h_img")
--- a/src/HOL/Algebra/Polynomials.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Polynomials.thy Mon Apr 01 17:02:43 2019 +0100
@@ -2190,7 +2190,7 @@
have eq: "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t)) = (h \<circ> ?f) t"
using ring_hom_memE(2)[OF ring_hom_ring.homh[OF assms(3)]
const_in_carrier var_pow_closed[OF assms(1)]]
- ring_hom_ring.nat_pow_hom[OF assms(3) var_closed(1)[OF assms(1)]] by auto
+ ring_hom_ring.hom_nat_pow[OF assms(3) var_closed(1)[OF assms(1)]] by auto
show ?thesis
using A.add.finprod_cong'[OF _ h eq] hp by simp
qed
--- a/src/HOL/Algebra/RingHom.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/RingHom.thy Mon Apr 01 17:02:43 2019 +0100
@@ -176,7 +176,7 @@
using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
qed
-lemma (in ring_hom_ring) nat_pow_hom:
+lemma (in ring_hom_ring) hom_nat_pow:
"x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n"
by (induct n) (auto)
--- a/src/HOL/Algebra/Zassenhaus.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Zassenhaus.thy Mon Apr 01 17:02:43 2019 +0100
@@ -203,7 +203,7 @@
hence N_incl : "N \<subseteq> N <#> H"
by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def)
thus "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
- using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
+ using normal_Int_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
by (simp add : inf_absorb1)
qed
@@ -308,7 +308,7 @@
ultimately have "(G\<lparr>carrier := H\<rparr> Mod N \<inter> H) \<cong> (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
using group_hom.FactGroup_iso[OF homomorphism im_f] by auto
hence "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H"
- by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup)
+ by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_Int_subgroup)
thus "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
qed
@@ -636,8 +636,7 @@
qed
hence "Gmod3 = Gmod4" using Hp Gmod4_def by simp
hence "Gmod1 \<cong> Gmod2"
- using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group
- by (metis assms Gmod1_def Gmod2_def preliminary2)
+ by (metis assms group.iso_sym iso_trans Hyp normal.factorgroup_is_group Gmod2_def preliminary2)
thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute)
qed
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Mon Apr 01 17:02:43 2019 +0100
@@ -81,13 +81,13 @@
"\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
\<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
unfolding Euclidean_space_def continuous_map_in_subtopology
- by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_add)
+ by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_add)
lemma continuous_map_Euclidean_space_diff [continuous_intros]:
"\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
\<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
unfolding Euclidean_space_def continuous_map_in_subtopology
- by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_diff)
+ by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)
lemma homeomorphic_Euclidean_space_product_topology:
"Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}"
@@ -158,12 +158,11 @@
lemma continuous_map_nsphere_reflection:
"continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)"
proof -
- have cm: "continuous_map (powertop_real UNIV)
- euclideanreal (\<lambda>x. if j = k then - x j else x j)" for j
+ have cm: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. if j = k then - x j else x j)" for j
proof (cases "j=k")
case True
then show ?thesis
- by simp (metis UNIV_I continuous_map_product_projection continuous_map_real_minus)
+ by simp (metis UNIV_I continuous_map_product_projection)
next
case False
then show ?thesis
@@ -173,7 +172,7 @@
by simp
show ?thesis
apply (simp add: nsphere continuous_map_in_subtopology continuous_map_componentwise_UNIV
- continuous_map_from_subtopology cm topspace_subtopology)
+ continuous_map_from_subtopology cm)
apply (intro conjI allI impI continuous_intros continuous_map_from_subtopology continuous_map_product_projection)
apply (auto simp: power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] eq cong: if_cong)
done
--- a/src/HOL/Analysis/Abstract_Limits.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy Mon Apr 01 17:02:43 2019 +0100
@@ -47,7 +47,7 @@
definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
"limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
-lemma limitin_euclideanreal_iff [simp]: "limitin euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
+lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
by (auto simp: limitin_def tendsto_def)
lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
@@ -203,8 +203,8 @@
subsection\<open>Combining theorems for continuous functions into the reals\<close>
-lemma continuous_map_real_const [simp,continuous_intros]:
- "continuous_map X euclideanreal (\<lambda>x. c)"
+lemma continuous_map_canonical_const [continuous_intros]:
+ "continuous_map X euclidean (\<lambda>x. c)"
by simp
lemma continuous_map_real_mult [continuous_intros]:
@@ -240,24 +240,31 @@
"continuous_map X euclideanreal (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)
-lemma continuous_map_real_minus [continuous_intros]:
- "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. - f x)"
+lemma continuous_map_minus [continuous_intros]:
+ fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+ shows "continuous_map X euclidean f \<Longrightarrow> continuous_map X euclidean (\<lambda>x. - f x)"
by (simp add: continuous_map_atin tendsto_minus)
-lemma continuous_map_real_minus_eq:
- "continuous_map X euclideanreal (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclideanreal f"
- using continuous_map_real_mult_left_eq [where c = "-1"] by auto
+lemma continuous_map_minus_eq [simp]:
+ fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+ shows "continuous_map X euclidean (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclidean f"
+ using continuous_map_minus add.inverse_inverse continuous_map_eq by fastforce
-lemma continuous_map_real_add [continuous_intros]:
- "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
- \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x + g x)"
+lemma continuous_map_add [continuous_intros]:
+ fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+ shows "\<lbrakk>continuous_map X euclidean f; continuous_map X euclidean g\<rbrakk> \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x + g x)"
by (simp add: continuous_map_atin tendsto_add)
-lemma continuous_map_real_diff [continuous_intros]:
- "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
- \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x - g x)"
+lemma continuous_map_diff [continuous_intros]:
+ fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+ shows "\<lbrakk>continuous_map X euclidean f; continuous_map X euclidean g\<rbrakk> \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x - g x)"
by (simp add: continuous_map_atin tendsto_diff)
+lemma continuous_map_norm [continuous_intros]:
+ fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+ shows "continuous_map X euclidean f \<Longrightarrow> continuous_map X euclidean (\<lambda>x. norm(f x))"
+ by (simp add: continuous_map_atin tendsto_norm)
+
lemma continuous_map_real_abs [continuous_intros]:
"continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. abs(f x))"
by (simp add: continuous_map_atin tendsto_rabs)
@@ -273,8 +280,9 @@
by (simp add: continuous_map_atin tendsto_min)
lemma continuous_map_sum [continuous_intros]:
- "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
- \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sum (f x) I)"
+ fixes f :: "'a\<Rightarrow>'b\<Rightarrow>'c::real_normed_vector"
+ shows "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)\<rbrakk>
+ \<Longrightarrow> continuous_map X euclidean (\<lambda>x. sum (f x) I)"
by (simp add: continuous_map_atin tendsto_sum)
lemma continuous_map_prod [continuous_intros]:
--- a/src/HOL/Analysis/Function_Topology.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Mon Apr 01 17:02:43 2019 +0100
@@ -608,7 +608,7 @@
using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
-lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+lemma continuous_on_coordinatewise_then_product [continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
shows "continuous_on S f"
@@ -635,7 +635,7 @@
lemma continuous_on_coordinatewise_iff:
fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
- by (auto simp: continuous_on_product_then_coordinatewise)
+ by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product)
subsubsection%important \<open>Topological countability for product spaces\<close>
--- a/src/HOL/Analysis/T1_Spaces.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy Mon Apr 01 17:02:43 2019 +0100
@@ -411,7 +411,7 @@
"\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> closedin X S \<longleftrightarrow> S \<subseteq> topspace X"
by (meson closedin_Hausdorff_finite closedin_def)
-lemma derived_set_of_infinite_open_in:
+lemma derived_set_of_infinite_openin:
"Hausdorff_space X
\<Longrightarrow> X derived_set_of S =
{x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)}"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Apr 01 17:02:43 2019 +0100
@@ -879,7 +879,7 @@
"is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
unfolding is_interval_def by auto
-lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+lemma is_interval_Int: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
unfolding is_interval_def
by blast
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Apr 01 17:02:43 2019 +0100
@@ -319,12 +319,12 @@
proof (cases "even k")
case True
with * \<open>in_carrier ls\<close> show ?thesis
- by (simp add: even_pow sqr_ci nat_pow_distr nat_pow_mult
+ by (simp add: even_pow sqr_ci nat_pow_distrib nat_pow_mult
mult_2 [symmetric] even_two_times_div_two)
next
case False
with * \<open>in_carrier ls\<close> show ?thesis
- by (simp add: odd_pow mul_ci sqr_ci nat_pow_distr nat_pow_mult
+ by (simp add: odd_pow mul_ci sqr_ci nat_pow_distrib nat_pow_mult
mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
qed
qed
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Mon Apr 01 17:02:43 2019 +0100
@@ -159,7 +159,7 @@
proof (cases x y rule: pexpr_cases2)
case (PPow_PPow e n e' m)
then show ?thesis
- by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distr
+ by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distrib
npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"])
qed simp_all
qed
@@ -258,7 +258,7 @@
by (induct e n e' m arbitrary: p e'' rule: isin.induct)
(force
simp add:
- nat_pow_distr nat_pow_pow nat_pow_mult m_ac
+ nat_pow_distrib nat_pow_pow nat_pow_mult m_ac
npemul_correct npepow_correct
split: option.split_asm prod.split_asm if_split_asm)+
@@ -323,7 +323,7 @@
peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct)
(auto simp add: split_beta
- nat_pow_distr nat_pow_pow nat_pow_mult m_ac
+ nat_pow_distrib nat_pow_pow nat_pow_mult m_ac
npemul_correct npepow_correct isin_correct'
split: option.split)
--- a/src/HOL/Finite_Set.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Finite_Set.thy Mon Apr 01 17:02:43 2019 +0100
@@ -2045,24 +2045,49 @@
for f :: "'a \<Rightarrow> 'a"
by (fastforce simp:surj_def dest!: endo_inj_surj)
-corollary infinite_UNIV_nat [iff]: "\<not> finite (UNIV :: nat set)"
-proof
- assume "finite (UNIV :: nat set)"
- with finite_UNIV_inj_surj [of Suc] show False
- by simp (blast dest: Suc_neq_Zero surjD)
-qed
-
-lemma infinite_UNIV_char_0: "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
+lemma surjective_iff_injective_gen:
+ assumes fS: "finite S"
+ and fT: "finite T"
+ and c: "card S = card T"
+ and ST: "f ` S \<subseteq> T"
+ shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
+ (is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume "finite (UNIV :: 'a set)"
- with subset_UNIV have "finite (range of_nat :: 'a set)"
- by (rule finite_subset)
- moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
- by (simp add: inj_on_def)
- ultimately have "finite (UNIV :: nat set)"
- by (rule finite_imageD)
- then show False
- by simp
+ assume h: "?lhs"
+ {
+ fix x y
+ assume x: "x \<in> S"
+ assume y: "y \<in> S"
+ assume f: "f x = f y"
+ from x fS have S0: "card S \<noteq> 0"
+ by auto
+ have "x = y"
+ proof (rule ccontr)
+ assume xy: "\<not> ?thesis"
+ have th: "card S \<le> card (f ` (S - {y}))"
+ unfolding c
+ proof (rule card_mono)
+ show "finite (f ` (S - {y}))"
+ by (simp add: fS)
+ have "\<lbrakk>x \<noteq> y; x \<in> S; z \<in> S; f x = f y\<rbrakk>
+ \<Longrightarrow> \<exists>x \<in> S. x \<noteq> y \<and> f z = f x" for z
+ by (case_tac "z = y \<longrightarrow> z = x") auto
+ then show "T \<subseteq> f ` (S - {y})"
+ using h xy x y f by fastforce
+ qed
+ also have " \<dots> \<le> card (S - {y})"
+ by (simp add: card_image_le fS)
+ also have "\<dots> \<le> card S - 1" using y fS by simp
+ finally show False using S0 by arith
+ qed
+ }
+ then show ?rhs
+ unfolding inj_on_def by blast
+next
+ assume h: ?rhs
+ have "f ` S = T"
+ by (simp add: ST c card_image card_subset_eq fT h)
+ then show ?lhs by blast
qed
hide_const (open) Finite_Set.fold
@@ -2084,6 +2109,26 @@
infinite set, the result is still infinite.
\<close>
+lemma infinite_UNIV_nat [iff]: "infinite (UNIV :: nat set)"
+proof
+ assume "finite (UNIV :: nat set)"
+ with finite_UNIV_inj_surj [of Suc] show False
+ by simp (blast dest: Suc_neq_Zero surjD)
+qed
+
+lemma infinite_UNIV_char_0: "infinite (UNIV :: 'a::semiring_char_0 set)"
+proof
+ assume "finite (UNIV :: 'a set)"
+ with subset_UNIV have "finite (range of_nat :: 'a set)"
+ by (rule finite_subset)
+ moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
+ by (simp add: inj_on_def)
+ ultimately have "finite (UNIV :: nat set)"
+ by (rule finite_imageD)
+ then show False
+ by simp
+qed
+
lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
by auto
--- a/src/HOL/Real_Vector_Spaces.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Apr 01 17:02:43 2019 +0100
@@ -148,6 +148,10 @@
by simp
qed
+lemma linear_scale_real:
+ fixes r::real shows "linear f \<Longrightarrow> f (r * b) = r * f b"
+ using linear_scale by fastforce
+
interpretation scaleR_left: additive "(\<lambda>a. scaleR a x :: 'a::real_vector)"
by standard (rule scaleR_left_distrib)
--- a/src/HOL/Vector_Spaces.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Vector_Spaces.thy Mon Apr 01 17:02:43 2019 +0100
@@ -993,48 +993,6 @@
end
-lemma surjective_iff_injective_gen:
- assumes fS: "finite S"
- and fT: "finite T"
- and c: "card S = card T"
- and ST: "f ` S \<subseteq> T"
- shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
- (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume h: "?lhs"
- {
- fix x y
- assume x: "x \<in> S"
- assume y: "y \<in> S"
- assume f: "f x = f y"
- from x fS have S0: "card S \<noteq> 0"
- by auto
- have "x = y"
- proof (rule ccontr)
- assume xy: "\<not> ?thesis"
- have th: "card S \<le> card (f ` (S - {y}))"
- unfolding c
- proof (rule card_mono)
- show "finite (f ` (S - {y}))"
- by (simp add: fS)
- show "T \<subseteq> f ` (S - {y})"
- using h xy x y f unfolding subset_eq image_iff
- by (metis member_remove remove_def)
- qed
- also have " \<dots> \<le> card (S - {y})"
- by (simp add: card_image_le fS)
- also have "\<dots> \<le> card S - 1" using y fS by simp
- finally show False using S0 by arith
- qed
- }
- then show ?rhs
- unfolding inj_on_def by blast
-next
- assume h: ?rhs
- have "f ` S = T"
- by (simp add: ST c card_image card_subset_eq fT h)
- then show ?lhs by blast
-qed
locale finite_dimensional_vector_space = vector_space +
fixes Basis :: "'b set"