# HG changeset patch
# User paulson
# Date 1531212742 -3600
# Node ID 9963bb965a0ec0da9c8c47a25cfe66a16e04f627
# Parent  67bb59e49834ba962abf07a8d78420ff400a9a55# Parent  4a4c2bc4b869dfd820a54f5f3682a21120ddf11e
merged

diff -r 67bb59e49834 -r 9963bb965a0e src/HOL/Algebra/Chinese_Remainder.thy
--- a/src/HOL/Algebra/Chinese_Remainder.thy	Tue Jul 10 09:38:35 2018 +0200
+++ b/src/HOL/Algebra/Chinese_Remainder.thy	Tue Jul 10 09:52:22 2018 +0100
@@ -67,7 +67,7 @@
   using ring_iso_set_trans[OF ring_iso_set_trans[OF RDirProd_isomorphism1[of R S]
                                                     RDirProd_isomorphism4[OF assms, of R]]
                               RDirProd_isomorphism1[of T R]]
-  by (simp add: case_prod_unfold case_prod_unfold comp_def comp_def)
+  by (simp add: case_prod_unfold comp_def)
 
 lemma RDirProd_isomorphism6:
   assumes "f \<in> ring_iso R R'" and "g \<in> ring_iso S S'"
@@ -619,8 +619,7 @@
     using group_hom.hom_inv[of "R \<times>\<times> DirProd_list Rs" "DirProd_list (R # Rs)"
                                "\<lambda>(hd, tl). hd # tl" "(r', rs')"] r by simp
   thus ?case
-    by (smt "2.hyps"(1) "2.prems"(1) "2.prems"(3) One_nat_def Suc_less_eq Suc_pred length_Cons
-        lessThan_iff list.sel(3) not_gr0 nth_Cons' nth_tl r rs') 
+    using 2 by simp (metis (no_types, lifting) less_Suc_eq_0_disj list.sel(3) nth_Cons_0 nth_Cons_Suc r)
 qed
 
 
@@ -753,20 +752,19 @@
 lemma RDirProd_list_a_inv:
   fixes i
   assumes "r \<in> carrier (RDirProd_list Rs)"
-      and "\<And>i. i < length Rs \<Longrightarrow> abelian_group (Rs ! i)"
-      and "i < length Rs"
-    shows "(\<ominus>\<^bsub>(RDirProd_list Rs)\<^esub> r) ! i = \<ominus>\<^bsub>(Rs ! i)\<^esub> (r ! i)"
+    and "\<And>i. i < length Rs \<Longrightarrow> abelian_group (Rs ! i)"
+    and i: "i < length Rs"
+  shows "(\<ominus>\<^bsub>(RDirProd_list Rs)\<^esub> r) ! i = \<ominus>\<^bsub>(Rs ! i)\<^esub> (r ! i)"
 proof -
-  have f1: "m_inv (DirProd_list (map add_monoid Rs)) = a_inv (RDirProd_list Rs)"
+  have "m_inv (DirProd_list (map add_monoid Rs)) = a_inv (RDirProd_list Rs)"
     by (metis RDirProd_list_add_monoid a_inv_def)
-moreover
-  have f4: "r \<in> carrier (DirProd_list (map add_monoid Rs))"
+  moreover have "r \<in> carrier (DirProd_list (map add_monoid Rs))"
     by (metis RDirProd_list_add_monoid assms(1) partial_object.select_convs(1))
-moreover
-  have f3: "a_inv (Rs ! i) = m_inv (map add_monoid Rs ! i)"
-    by (simp add: a_inv_def assms(3))
-  ultimately show ?thesis  using RDirProd_list_add_monoid[of Rs] monoid.defs(3) DirProd_list_m_inv
-    by (smt abelian_group.a_group assms(2) assms(3) length_map nth_map)
+  moreover have "a_inv (Rs ! i) = m_inv (map add_monoid Rs ! i)"
+    by (simp add: a_inv_def i)
+  ultimately show ?thesis
+    by (metis (no_types, lifting) DirProd_list_carrier_elts DirProd_list_m_inv RDirProd_list_carrier_elts
+        abelian_group.a_group assms list_update_same_conv map_update)  
 qed
 
 lemma RDirProd_list_l_distr:
@@ -876,6 +874,11 @@
     using RDirProd_list_cring by blast
 qed
 
+lemma length_RDirProd_list_0: 
+  assumes "\<And>i. i < n \<Longrightarrow> cring (F i)" 
+  shows "length (\<zero>\<^bsub>(RDirProd_list (map F [0..< n]))\<^esub>) = n"
+  by (metis (no_types, lifting) add_cancel_right_left RDirProd_list_carrier_elts RDirProd_list_cring cring.cring_simprules(2) diff_zero length_map length_upt nth_map_upt assms)
+
 lemma RDirProd_list_isomorphism1:
   "(\<lambda>(hd, tl). hd # tl) \<in> ring_iso (RDirProd R (RDirProd_list Rs)) (RDirProd_list (R # Rs))"
   unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def
@@ -1037,7 +1040,6 @@
     by (simp add: FactRing_def monoid.defs)
 qed
 
-
 theorem (in cring) canonical_proj_ext_kernel:
   fixes n::nat
   assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R"
@@ -1066,15 +1068,10 @@
         unfolding FactRing_def by simp
       moreover
       have "length (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) = Suc n"
-
-        using RDirProd_list_carrier_elts RDirProd_list_cring
-         add.left_neutral assms(1) cring.cring_simprules(2) diff_zero nth_map_upt
-            ideal.quotient_is_cring is_cring length_map length_upt lessThan_Suc_atMost lessThan_iff
-        by (smt less_Suc_eq_le)
+        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)
-
       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>"
@@ -1133,19 +1130,16 @@
   hence "RDirProd (R Quot (\<Inter> i \<le> n. I i)) (R Quot (I (Suc n))) \<simeq>
          RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n)))"
     unfolding is_ring_iso_def using RDirProd_isomorphism4 by blast
-
   ultimately
   have "R Quot (\<Inter> i \<le> Suc n. I i) \<simeq>
         RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n)))"
     using ring_iso_trans by simp
-
   moreover
   have "RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n))) \<simeq>
         RDirProd_list ((map (\<lambda>i. R Quot (I i)) [0..< Suc n]) @ [ R Quot (I (Suc n)) ])"
     using RDirProd_list_isomorphism3 unfolding is_ring_iso_def by blast
   hence "RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n))) \<simeq>
          RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc (Suc n)])" by simp
-
   ultimately show ?case using ring_iso_trans by simp
 qed
 
diff -r 67bb59e49834 -r 9963bb965a0e src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Tue Jul 10 09:38:35 2018 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Tue Jul 10 09:52:22 2018 +0100
@@ -590,16 +590,12 @@
     proof (induction n)
       case 0 thus ?case using A by simp
     next
-      case (Suc n) thus ?case
-        using aux_lemma1 derived_self_is_normal  normal_def o_apply  
-      proof auto  (*FIXME a mess*)
-        fix x :: 'a
-        assume a1: "derived G (carrier G) \<lhd> G"
-        assume a2: "x \<in> derived G ((derived G ^^ n) I)"
-        assume "\<And>Ja Ia. \<lbrakk>Ja \<subseteq> carrier G; Ia \<subseteq> Ja\<rbrakk> \<Longrightarrow> derived G Ia \<subseteq> derived G Ja"
-        then show "x \<in> carrier G"
-          using a2 a1 by (meson Suc.IH normal_def order_refl subgroup.subset subsetCE)
-      qed
+      case (Suc n)
+      with aux_lemma1 have "(derived G ^^ Suc n) I \<subseteq> derived G (carrier G)"
+        by auto
+      also have "... \<subseteq> carrier G"
+        by (simp add: derived_incl subgroup_self)
+      finally show ?case .
     qed } note aux_lemma2 = this
 
   show ?thesis