# HG changeset patch
# User paulson
# Date 1536679324 -3600
# Node ID 105bbce656a50383776c4d46705e23817a215b2b
# Parent  7a9118e63cad2f5515d6478aa7da3c6c563150a0# Parent  5ce4d117cea730dfa852b232a95a80e5f5b8ab3b
merged

diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Algebra/AbelCoset.thy
--- 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])
 
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Algebra/Chinese_Remainder.thy
--- 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)]
     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>"
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Algebra/Coset.thy
--- 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)
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Algebra/Group_Action.thy
--- 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:
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Algebra/Sym_Groups.thy
--- 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
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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"
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Finite_Set.thy
--- 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 @@
   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> {}"
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Groups_Big.thy
--- 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
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/HOL.thy
--- 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
 
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Hilbert_Choice.thy
--- 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>
 
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Hoare_Parallel/RG_Hoare.thy
--- 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
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Library/Stirling.thy
--- 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
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/List.thy
--- 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
 
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- 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)
diff -r 7a9118e63cad -r 105bbce656a5 src/HOL/Zorn.thy
--- 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>