author paulson Tue, 11 Sep 2018 16:22:04 +0100 changeset 68976 105bbce656a5 parent 68969 7a9118e63cad (current diff) parent 68975 5ce4d117cea7 (diff) child 68977 c73ca43087c0
merged
```--- a/src/HOL/Algebra/AbelCoset.thy	Tue Sep 11 14:56:45 2018 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Algebra/Chinese_Remainder.thy	Tue Sep 11 16:22:04 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)]
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"
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>"
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 14:56:45 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Algebra/Group_Action.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Sep 11 16:22:04 2018 +0100
@@ -162,7 +162,7 @@

-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 14:56:45 2018 +0200
+++ b/src/HOL/Groups_Big.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Tue Sep 11 16:22:04 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/Stirling.thy	Tue Sep 11 14:56:45 2018 +0200
+++ b/src/HOL/Library/Stirling.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/List.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Sep 11 16:22:04 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 14:56:45 2018 +0200
+++ b/src/HOL/Zorn.thy	Tue Sep 11 16:22:04 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>
```