--- a/src/HOL/Algebra/AbelCoset.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Wed Sep 12 12:51:52 2018 +0100
@@ -403,8 +403,7 @@
by (rule group.rcos_equation [OF a_group a_subgroup,
folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
-lemma (in abelian_subgroup) a_rcos_disjoint:
- shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
+lemma (in abelian_subgroup) a_rcos_disjoint: "pairwise disjnt (a_rcosets H)"
by (rule group.rcos_disjoint [OF a_group a_subgroup,
folded A_RCOSETS_def, simplified monoid_record_simps])
--- a/src/HOL/Algebra/Chinese_Remainder.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Algebra/Chinese_Remainder.thy Wed Sep 12 12:51:52 2018 +0100
@@ -389,15 +389,14 @@
moreover have "(r1 \<otimes>\<^bsub>(DirProd_list (R # Rs))\<^esub> r2) ! 0 = (r1 ! 0) \<otimes>\<^bsub>R\<^esub> (r2 ! 0)"
using "2.prems"(2) "2.prems"(3) by auto
ultimately show ?case
- by (metis "2.prems"(1) atLeastLessThan_iff le_0_eq lessThan_iff not_less_eq_eq nth_Cons')
+ by (metis "2.prems"(1) atLeastLessThan_iff le_0_eq not_less_eq_eq nth_Cons')
qed
lemma DirProd_list_m_comm:
assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)"
and "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)"
- shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2 = r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1"
- apply (rule nth_equalityI) apply auto
-proof -
+ shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2 = r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1"
+proof (rule nth_equalityI)
show "length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) = length (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1)"
by (metis DirProd_list_carrier_elts DirProd_list_m_closed Group.comm_monoid.axioms(1) assms)
@@ -407,7 +406,7 @@
have "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)"
using i DirProd_list_m_output[OF assms(1-2)] by simp
also have " ... = (r2 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r1 ! i)"
- by (metis DirProd_list_carrier_elts DirProd_list_in_carrierE assms comm_monoid.m_comm i lessThan_iff)
+ by (metis DirProd_list_carrier_elts DirProd_list_in_carrierE assms comm_monoid.m_comm i)
also have " ... = (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i"
using i DirProd_list_m_output[OF assms(2) assms(1)] by simp
finally show "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) ! i = (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i" .
@@ -420,8 +419,7 @@
and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
shows "(r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2) \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r3 =
r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> (r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r3)"
- apply (rule nth_equalityI) apply auto
-proof -
+proof (rule nth_equalityI)
show "length ((r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3) =
length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3))"
by (metis DirProd_list_carrier_elts DirProd_list_m_closed assms)
@@ -431,11 +429,11 @@
by (metis DirProd_list_carrier_elts DirProd_list_m_closed assms)
have "((r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3) ! i =
((r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r3 ! i)"
- by (metis DirProd_list_m_closed DirProd_list_m_output i assms lessThan_iff)
+ by (metis DirProd_list_m_closed DirProd_list_m_output i assms)
also have " ... = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> ((r2 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r3 ! i))"
- by (metis DirProd_list_carrier_elts DirProd_list_in_carrierE assms i lessThan_iff monoid.m_assoc)
+ by (metis DirProd_list_carrier_elts DirProd_list_in_carrierE assms i monoid.m_assoc)
also have " ... = (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3)) ! i"
- by (metis DirProd_list_m_closed DirProd_list_m_output i assms lessThan_iff)
+ by (metis DirProd_list_m_closed DirProd_list_m_output i assms)
finally show "((r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3) ! i =
(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3))! i" .
qed
@@ -458,12 +456,11 @@
assumes "r1 \<in> carrier (DirProd_list Rs)"
and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
shows "\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1 = r1"
- apply (rule nth_equalityI) apply auto
-proof -
+proof (rule nth_equalityI)
show eq_len: "length (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) = length r1"
using DirProd_list_carrier_elts[of "\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1" Rs]
- DirProd_list_carrier_elts[OF assms(1)]
- DirProd_list_m_closed[OF DirProd_list_one_closed[OF assms(2)] assms(1)]
+ DirProd_list_carrier_elts[OF assms(1)]
+ DirProd_list_m_closed[OF DirProd_list_one_closed[OF assms(2)] assms(1)]
by (simp add: assms)
fix i assume "i < length (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1)"
hence i: "i < length Rs" using DirProd_list_carrier_elts[OF assms(1)] eq_len by simp
@@ -484,8 +481,7 @@
proof -
have "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> \<one>\<^bsub>(DirProd_list Rs)\<^esub> =
\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1"
- apply (rule nth_equalityI) apply auto
- proof -
+ proof (rule nth_equalityI)
show " length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>) =
length (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1)"
by (metis DirProd_list_carrier_elts DirProd_list_m_closed DirProd_list_one_closed assms)
@@ -494,11 +490,11 @@
hence i: "i < length Rs"
by (metis DirProd_list_carrier_elts DirProd_list_m_closed DirProd_list_one_closed assms)
hence "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> \<one>\<^bsub>(Rs ! i)\<^esub>"
- by (metis DirProd_list_m_output DirProd_list_one DirProd_list_one_closed assms lessThan_iff)
+ by (metis DirProd_list_m_output DirProd_list_one DirProd_list_one_closed assms)
also have " ... = \<one>\<^bsub>(Rs ! i)\<^esub> \<otimes>\<^bsub>(Rs ! i)\<^esub> (r1 ! i)"
using DirProd_list_carrier_elts DirProd_list_in_carrierE assms i by fastforce
also have " ... = (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i"
- by (metis DirProd_list_m_output DirProd_list_one DirProd_list_one_closed assms i lessThan_iff)
+ by (metis DirProd_list_m_output DirProd_list_one DirProd_list_one_closed assms i)
finally show "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>) ! i =
(\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i" .
qed
@@ -508,8 +504,8 @@
lemma DirProd_list_monoid:
assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
shows "monoid (DirProd_list Rs)"
- unfolding monoid_def apply auto
-proof -
+ unfolding monoid_def
+proof (intro conjI allI impI)
show "\<one>\<^bsub>DirProd_list Rs\<^esub> \<in> carrier (DirProd_list Rs)"
using DirProd_list_one_closed[of Rs] assms by simp
@@ -1029,7 +1025,7 @@
((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y)) ! j" .
qed
ultimately show "?\<phi> (x \<oplus> y) = ?\<phi> x \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> ?\<phi> y"
- by (simp add: nth_equalityI)
+ by (simp add: list_eq_iff_nth_eq)
qed
next
show "(?\<phi> \<one>) = \<one>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub>"
@@ -1071,7 +1067,7 @@
by (subst length_RDirProd_list_0) (simp_all add: length_RDirProd_list_0 assms(1) ideal.quotient_is_cring is_cring)
moreover have "length (?\<phi> s) = Suc n" by simp
ultimately have "?\<phi> s = \<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>"
- by (simp add: nth_equalityI)
+ by (simp add: list_eq_iff_nth_eq)
moreover have "s \<in> carrier R"
using additive_subgroup.a_Hcarr assms(1) ideal.axioms(1) s by fastforce
ultimately show "s \<in> a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi>"
--- a/src/HOL/Algebra/Coset.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy Wed Sep 12 12:51:52 2018 +0100
@@ -652,12 +652,11 @@
lemma (in group) rcos_disjoint:
assumes "subgroup H G"
- assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
- shows "a \<inter> b = {}"
+ shows "pairwise disjnt (rcosets H)"
proof -
interpret subgroup H G by fact
- from p show ?thesis
- unfolding RCOSETS_def r_coset_def
+ show ?thesis
+ unfolding RCOSETS_def r_coset_def pairwise_def disjnt_def
by (blast intro: rcos_equation assms sym)
qed
@@ -823,7 +822,7 @@
have "card H * card (rcosets H) = card (\<Union>(rcosets H))"
proof (rule card_partition)
show "\<And>c1 c2. \<lbrakk>c1 \<in> rcosets H; c2 \<in> rcosets H; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}"
- using HG rcos_disjoint by auto
+ using HG rcos_disjoint by (auto simp: pairwise_def disjnt_def)
qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
then show ?thesis
by (simp add: HG mult.commute order_def rcosets_part_G)
--- a/src/HOL/Algebra/Group_Action.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Algebra/Group_Action.thy Wed Sep 12 12:51:52 2018 +0100
@@ -415,8 +415,9 @@
using g2 r2 by blast
have "R1 \<inter> R2 \<noteq> {}" using inR1 inR2 r1 r2 by blast
- thus ?thesis using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G \<phi> x" R1 R2]
- assms group_hom group_hom.axioms(1) by blast
+ thus ?thesis
+ using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G \<phi> x"] assms group_hom group_hom.axioms(1)
+ unfolding disjnt_def pairwise_def by blast
qed
lemma (in group_action) orbit_stab_fun_is_surj:
--- a/src/HOL/Algebra/Sym_Groups.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy Wed Sep 12 12:51:52 2018 +0100
@@ -339,7 +339,7 @@
proof (intro nth_equalityI)
show "length cs = length [(cs ! 0), (cs ! 1), (cs ! 2)]"
using assms by simp
- show "\<forall> ia < length cs. cs ! ia = [(cs ! 0), (cs ! 1), (cs ! 2)] ! ia"
+ show "\<And>i. i < length cs \<Longrightarrow> cs ! i = [(cs ! 0), (cs ! 1), (cs ! 2)] ! i"
by (metis Suc_1 Suc_eq_plus1 add.left_neutral assms less_antisym
less_one nth_Cons' nth_Cons_Suc numeral_3_eq_3)
qed
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Sep 12 12:51:52 2018 +0100
@@ -2259,15 +2259,20 @@
from i have i': "i < length (replicate (k+1) 0)" "i < k+1"
unfolding length_replicate by presburger+
have "xs = replicate (k+1) 0 [i := n]"
- apply (rule nth_equalityI)
- unfolding xsl length_list_update length_replicate
- apply simp
- apply clarify
- unfolding nth_list_update[OF i'(1)]
- using i zxs
- apply (case_tac "ia = i")
- apply (auto simp del: replicate.simps)
- done
+ proof (rule nth_equalityI)
+ show "length xs = length (replicate (k + 1) 0[i := n])"
+ by (metis length_list_update length_replicate xsl)
+ show "xs ! j = replicate (k + 1) 0[i := n] ! j" if "j < length xs" for j
+ proof (cases "j = i")
+ case True
+ then show ?thesis
+ by (metis i'(1) i(2) nth_list_update)
+ next
+ case False
+ with that show ?thesis
+ by (simp add: xsl zxs del: replicate.simps split: nat.split)
+ qed
+ qed
then show "xs \<in> ?B" using i by blast
qed
show "?B \<subseteq> ?A"
--- a/src/HOL/Finite_Set.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Finite_Set.thy Wed Sep 12 12:51:52 2018 +0100
@@ -162,7 +162,7 @@
by (simp add: le_eq_less_or_eq Collect_disj_eq)
-subsubsection \<open>Finiteness and common set operations\<close>
+subsection \<open>Finiteness and common set operations\<close>
lemma rev_finite_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A"
proof (induct arbitrary: A rule: finite_induct)
@@ -319,15 +319,36 @@
next
case insert
then show ?case
- by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast (* slow *)
+ by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
qed
+lemma all_subset_image: "(\<forall>B. B \<subseteq> f ` A \<longrightarrow> P B) \<longleftrightarrow> (\<forall>B. B \<subseteq> A \<longrightarrow> P(f ` B))"
+ by (safe elim!: subset_imageE) (use image_mono in \<open>blast+\<close>) (* slow *)
+
+lemma all_finite_subset_image:
+ "(\<forall>B. finite B \<and> B \<subseteq> f ` A \<longrightarrow> P B) \<longleftrightarrow> (\<forall>B. finite B \<and> B \<subseteq> A \<longrightarrow> P (f ` B))"
+proof safe
+ fix B :: "'a set"
+ assume B: "finite B" "B \<subseteq> f ` A" and P: "\<forall>B. finite B \<and> B \<subseteq> A \<longrightarrow> P (f ` B)"
+ show "P B"
+ using finite_subset_image [OF B] P by blast
+qed blast
+
+lemma exists_finite_subset_image:
+ "(\<exists>B. finite B \<and> B \<subseteq> f ` A \<and> P B) \<longleftrightarrow> (\<exists>B. finite B \<and> B \<subseteq> A \<and> P (f ` B))"
+proof safe
+ fix B :: "'a set"
+ assume B: "finite B" "B \<subseteq> f ` A" and "P B"
+ show "\<exists>B. finite B \<and> B \<subseteq> A \<and> P (f ` B)"
+ using finite_subset_image [OF B] \<open>P B\<close> by blast
+qed blast
+
lemma finite_vimage_IntI: "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
- apply (induct rule: finite_induct)
- apply simp_all
- apply (subst vimage_insert)
- apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
- done
+proof (induct rule: finite_induct)
+ case (insert x F)
+ then show ?case
+ by (simp add: vimage_insert [of h x F] finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
+qed simp
lemma finite_finite_vimage_IntI:
assumes "finite F"
@@ -518,7 +539,7 @@
qed
-subsubsection \<open>Further induction rules on finite sets\<close>
+subsection \<open>Further induction rules on finite sets\<close>
lemma finite_ne_induct [case_names singleton insert, consumes 2]:
assumes "finite F" and "F \<noteq> {}"
--- a/src/HOL/Groups_Big.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Groups_Big.thy Wed Sep 12 12:51:52 2018 +0100
@@ -1006,9 +1006,18 @@
qed
lemma card_Union_disjoint:
- "finite C \<Longrightarrow> \<forall>A\<in>C. finite A \<Longrightarrow> \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
- card (\<Union>C) = sum card C"
- by (frule card_UN_disjoint [of C id]) simp_all
+ assumes "pairwise disjnt C" and fin: "\<And>A. A \<in> C \<Longrightarrow> finite A"
+ shows "card (\<Union>C) = sum card C"
+proof (cases "finite C")
+ case True
+ then show ?thesis
+ using card_UN_disjoint [OF True, of "\<lambda>x. x"] assms
+ by (simp add: disjnt_def fin pairwise_def)
+next
+ case False
+ then show ?thesis
+ using assms card_eq_0_iff finite_UnionD by fastforce
+qed
lemma sum_multicount_gen:
assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
@@ -1035,42 +1044,42 @@
lemma sum_card_image:
assumes "finite A"
- assumes "\<forall>s\<in>A. \<forall>t\<in>A. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}"
+ assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) A"
shows "sum card (f ` A) = sum (\<lambda>a. card (f a)) A"
using assms
proof (induct A)
- case empty
- from this show ?case by simp
-next
case (insert a A)
show ?case
proof cases
assume "f a = {}"
- from this insert show ?case
- by (subst sum.mono_neutral_right[where S="f ` A"]) auto
+ with insert show ?case
+ by (subst sum.mono_neutral_right[where S="f ` A"]) (auto simp: pairwise_insert)
next
assume "f a \<noteq> {}"
- from this have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)"
- using insert by (subst sum.insert) auto
- from this insert show ?case by simp
+ then have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)"
+ using insert
+ by (subst sum.insert) (auto simp: pairwise_insert)
+ with insert show ?case by (simp add: pairwise_insert)
qed
-qed
+qed simp
lemma card_Union_image:
assumes "finite S"
- assumes "\<forall>s\<in>f ` S. finite s"
- assumes "\<forall>s\<in>S. \<forall>t\<in>S. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}"
+ assumes "\<And>s. s \<in> S \<Longrightarrow> finite (f s)"
+ assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) S"
shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S"
proof -
- have "\<forall>A\<in>f ` S. \<forall>B\<in>f ` S. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
- using assms(3) by (metis image_iff)
- from this have "card (\<Union>(f ` S)) = sum card (f ` S)"
- using assms(1, 2) by (subst card_Union_disjoint) auto
+ have "pairwise disjnt (f ` S)"
+ using assms(3)
+ by (metis pairwiseD pairwise_imageI)
+ then have "card (\<Union>(f ` S)) = sum card (f ` S)"
+ by (subst card_Union_disjoint) (use assms in auto)
also have "... = sum (\<lambda>x. card (f x)) S"
- using assms(1, 3) by (auto simp add: sum_card_image)
+ by (metis (mono_tags, lifting) assms(1) assms(3) sum_card_image)
finally show ?thesis .
qed
+
subsubsection \<open>Cardinality of products\<close>
lemma card_SigmaI [simp]:
@@ -1152,7 +1161,7 @@
context linordered_nonzero_semiring
begin
-
+
lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A"
proof (induct A rule: infinite_finite_induct)
case infinite
@@ -1434,5 +1443,5 @@
using insert by auto
finally show ?case .
qed
-
+
end
--- a/src/HOL/HOL.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/HOL.thy Wed Sep 12 12:51:52 2018 +0100
@@ -1638,6 +1638,12 @@
subsection \<open>Other simple lemmas and lemma duplicates\<close>
+lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)"
+ by auto
+
+lemma ex_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. P' x)"
+ by auto
+
lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<forall>x. Q x \<longrightarrow> P x) = (\<forall>x. Q x \<longrightarrow> P' x)"
by auto
--- a/src/HOL/Hilbert_Choice.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Hilbert_Choice.thy Wed Sep 12 12:51:52 2018 +0100
@@ -124,6 +124,21 @@
by (induct n) auto
qed
+lemma finite_subset_Union:
+ assumes "finite A" "A \<subseteq> \<Union>\<B>"
+ obtains \<F> where "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
+proof -
+ have "\<forall>x\<in>A. \<exists>B\<in>\<B>. x\<in>B"
+ using assms by blast
+ then obtain f where f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<B> \<and> x \<in> f x"
+ by (auto simp add: bchoice_iff Bex_def)
+ show thesis
+ proof
+ show "finite (f ` A)"
+ using assms by auto
+ qed (use f in auto)
+qed
+
subsection \<open>Function Inverse\<close>
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Sep 12 12:51:52 2018 +0100
@@ -1058,7 +1058,6 @@
apply(rule nth_equalityI)
apply simp_all
apply(case_tac x,simp+)
-apply clarify
apply(case_tac i,simp+)
apply(case_tac x,simp+)
done
--- a/src/HOL/Library/Omega_Words_Fun.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy Wed Sep 12 12:51:52 2018 +0100
@@ -219,7 +219,7 @@
lemma prefix_conc_snd[simp]:
assumes "n \<ge> length u"
shows "prefix n (u \<frown> v) = u @ prefix (n - length u) v"
-proof (intro nth_equalityI allI impI)
+proof (intro nth_equalityI)
show "length (prefix n (u \<frown> v)) = length (u @ prefix (n - length u) v)"
using assms by simp
fix i
@@ -258,7 +258,7 @@
assume ?lhs
then have 1: "(v\<^sub>1 \<frown> u\<^sub>1) i = (v\<^sub>2 \<frown> u\<^sub>2) i" for i by auto
show ?rhs
- proof (intro conjI ext nth_equalityI allI impI)
+ proof (intro conjI ext nth_equalityI)
show "length v\<^sub>1 = length v\<^sub>2" by (rule assms(1))
next
fix i
--- a/src/HOL/Library/Stirling.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Library/Stirling.thy Wed Sep 12 12:51:52 2018 +0100
@@ -214,24 +214,6 @@
lemma stirling_row_nonempty [simp]: "stirling_row n \<noteq> []"
using length_stirling_row[of n] by (auto simp del: length_stirling_row)
-(* TODO Move *)
-lemma list_ext:
- assumes "length xs = length ys"
- assumes "\<And>i. i < length xs \<Longrightarrow> xs ! i = ys ! i"
- shows "xs = ys"
- using assms
-proof (induction rule: list_induct2)
- case Nil
- then show ?case by simp
-next
- case (Cons x xs y ys)
- from Cons.prems[of 0] have "x = y"
- by simp
- moreover from Cons.prems[of "Suc i" for i] have "xs = ys"
- by (intro Cons.IH) simp
- ultimately show ?case by simp
-qed
-
subsubsection \<open>Efficient code\<close>
@@ -287,7 +269,7 @@
case 2
have "stirling_row (Suc n) =
0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \<leftarrow> [0..<n]] @ [1]"
- proof (rule list_ext, goal_cases length nth)
+ proof (rule nth_equalityI, goal_cases length nth)
case (nth i)
from nth have "i \<le> Suc n"
by simp
--- a/src/HOL/List.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/List.thy Wed Sep 12 12:51:52 2018 +0100
@@ -3139,7 +3139,7 @@
qed simp
lemma nth_equalityI:
- "[| length xs = length ys; \<forall>i < length xs. xs!i = ys!i |] ==> xs = ys"
+ "\<lbrakk>length xs = length ys; \<And>i. i < length xs \<Longrightarrow> xs!i = ys!i\<rbrakk> \<Longrightarrow> xs = ys"
by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
lemma map_nth:
@@ -4775,7 +4775,7 @@
lemma transpose_map_map:
"transpose (map (map f) xs) = map (map f) (transpose xs)"
-proof (rule nth_equalityI, safe)
+proof (rule nth_equalityI)
have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"
by (simp add: length_transpose foldr_map comp_def)
show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp
@@ -5487,7 +5487,7 @@
assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))
= xs ! i" (is "?R = _")
-proof (rule nth_equalityI, safe)
+proof (rule nth_equalityI)
show length: "length ?R = length (xs ! i)"
using transpose_column_length[OF assms] by simp
@@ -5544,7 +5544,7 @@
moreover
{ fix i assume "i < n" hence "filter (\<lambda>ys. i < length ys) xs = xs"
using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
- ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
+ ultimately show "\<And>i. i < length (transpose xs) \<Longrightarrow> ?trans ! i = ?map ! i"
by (auto simp: nth_transpose intro: nth_equalityI)
qed
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Sep 12 12:51:52 2018 +0100
@@ -138,7 +138,7 @@
using inv unfolding inversion_def map_eq_conv payer_def coin_def
by fastforce
show "x = y"
- proof (rule nth_equalityI, simp, rule allI, rule impI)
+ proof (rule nth_equalityI, simp)
fix j assume "j < length x" hence "j < n" using \<open>length xs = n\<close> by simp
thus "x ! j = y ! j"
proof (induct j)
--- a/src/HOL/Zorn.thy Tue Sep 11 22:25:00 2018 +0200
+++ b/src/HOL/Zorn.thy Wed Sep 12 12:51:52 2018 +0100
@@ -376,6 +376,12 @@
ultimately show False using * by blast
qed
+lemma subset_chain_def: "\<And>\<A>. subset.chain \<A> \<C> = (\<C> \<subseteq> \<A> \<and> (\<forall>X\<in>\<C>. \<forall>Y\<in>\<C>. X \<subseteq> Y \<or> Y \<subseteq> X))"
+ by (auto simp: subset.chain_def)
+
+lemma subset_chain_insert:
+ "subset.chain \<A> (insert B \<B>) \<longleftrightarrow> B \<in> \<A> \<and> (\<forall>X\<in>\<B>. X \<subseteq> B \<or> B \<subseteq> X) \<and> subset.chain \<A> \<B>"
+ by (fastforce simp add: subset_chain_def)
subsubsection \<open>Zorn's lemma\<close>