removal of smt and certain refinements
authorpaulson <lp15@cam.ac.uk>
Mon Jul 09 21:55:40 2018 +0100 (11 months ago)
changeset 6860696a49db47c97
parent 68605 440aa6b7d99a
child 68607 67bb59e49834
child 68608 4a4c2bc4b869
removal of smt and certain refinements
src/HOL/Algebra/Chinese_Remainder.thy
src/HOL/Algebra/Group_Action.thy
src/HOL/Algebra/Ideal_Product.thy
src/HOL/Computational_Algebra/Factorial_Ring.thy
     1.1 --- a/src/HOL/Algebra/Chinese_Remainder.thy	Sun Jul 08 23:35:33 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Chinese_Remainder.thy	Mon Jul 09 21:55:40 2018 +0100
     1.3 @@ -133,9 +133,7 @@
     1.4      by (metis abelian_subgroup.a_rcos_sum abelian_subgroupI3 additive_subgroup.a_Hcarr assms(1-2)
     1.5          ideal.axioms(1) is_abelian_group j m_closed r_zero x zero_closed)
     1.6    finally have Ix: "I +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = I +> x" using mod_I
     1.7 -    by (smt additive_subgroup.a_Hcarr assms ideal.axioms(1) ideal.rcoset_mult_add j
     1.8 -        monoid.l_one monoid_axioms one_closed x)
     1.9 -
    1.10 +    by (metis (full_types) assms ideal.Icarr ideal.rcoset_mult_add is_monoid j monoid.l_one one_closed x)
    1.11    have "J +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = (J +> (j \<otimes> x)) <+> (J +> (i \<otimes> y))"
    1.12      by (metis abelian_subgroup.a_rcos_sum abelian_subgroupI3 assms i ideal.Icarr
    1.13          ideal.axioms(1) is_abelian_group j m_closed x y)
    1.14 @@ -147,9 +145,7 @@
    1.15          additive_subgroup.a_Hcarr additive_subgroup.a_subset assms i ideal.axioms(1)
    1.16          is_abelian_group m_closed y)
    1.17    finally have Jy: "J +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = J +> y" using mod_J
    1.18 -    by (smt additive_subgroup.a_Hcarr assms ideal.axioms(1) ideal.rcoset_mult_add i j
    1.19 -        monoid.l_one monoid_axioms one_closed y x)
    1.20 -  
    1.21 +    by (metis (full_types) assms i ideal.Icarr ideal.rcoset_mult_add local.semiring_axioms one_closed semiring.semiring_simprules(9) y)  
    1.22    have "(j \<otimes> x) \<oplus> (i \<otimes> y) \<in> carrier R"
    1.23      by (meson x y i j assms add.m_closed additive_subgroup.a_Hcarr ideal.axioms(1) m_closed)
    1.24    thus "\<exists>a \<in> carrier R. I +> a = I +> x \<and> J +> a = J +> y" using Ix Jy by blast
    1.25 @@ -231,21 +227,20 @@
    1.26  subsection \<open>First Generalization - The Extended Canonical Projection is Surjective\<close>
    1.27  
    1.28  lemma (in cring) canonical_proj_ext_is_surj:
    1.29 -  assumes "\<And>i. i \<in> {..n :: nat} \<Longrightarrow> x i \<in> carrier R"
    1.30 -      and "\<And>i. i \<in> {..n} \<Longrightarrow> ideal (I i) R"
    1.31 -      and "\<And>i j. \<lbrakk> i \<in> {..n}; j \<in> {..n}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
    1.32 -    shows "\<exists> a \<in> carrier R. \<forall> i \<in> {..n}. (I i) +> a = (I i) +> (x i)" using assms
    1.33 +  fixes n::nat
    1.34 +  assumes "\<And>i. i \<le> n \<Longrightarrow> x i \<in> carrier R"
    1.35 +      and "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R"
    1.36 +      and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
    1.37 +    shows "\<exists> a \<in> carrier R. \<forall> i \<le> n. (I i) +> a = (I i) +> (x i)" using assms
    1.38  proof (induct n)
    1.39    case 0 thus ?case by blast 
    1.40  next
    1.41    case (Suc n)
    1.42 -  then obtain a where a: "a \<in> carrier R" "\<And>i. i \<in> {..n :: nat} \<Longrightarrow> (I i) +> a = (I i) +> (x i)"
    1.43 +  then obtain a where a: "a \<in> carrier R" "\<And>i. i \<le> n \<Longrightarrow> (I i) +> a = (I i) +> (x i)"
    1.44      by force
    1.45    
    1.46    have inter_is_ideal: "ideal (\<Inter> i \<le> n. I i) R"
    1.47 -    by (metis (mono_tags, lifting) Suc.prems(2) atMost_Suc i_Intersect image_iff
    1.48 -        image_is_empty insert_iff not_empty_eq_Iic_eq_empty)
    1.49 -
    1.50 +    by (metis (mono_tags, lifting) Suc.prems(2) atMost_iff i_Intersect imageE image_is_empty le_SucI not_empty_eq_Iic_eq_empty)
    1.51    have "(\<Inter> i \<le> n. I i) <+> I (Suc n) = carrier R"
    1.52      using inter_plus_ideal_eq_carrier Suc by simp
    1.53    then obtain b where b: "b \<in> carrier R"
    1.54 @@ -255,36 +250,35 @@
    1.55    hence b_inter: "b \<in> (\<Inter> i \<le> n. I i)"
    1.56      using ideal.set_add_zero_imp_mem[OF inter_is_ideal b]
    1.57      by (metis additive_subgroup.zero_closed ideal.axioms(1) ideal.set_add_zero inter_is_ideal)
    1.58 -  hence eq_zero: "\<And>i. i \<in> {..n :: nat} \<Longrightarrow> (I i) +> b = (I i) +> \<zero>"
    1.59 +  hence eq_zero: "\<And>i. i \<le> n \<Longrightarrow> (I i) +> b = (I i) +> \<zero>"
    1.60    proof -
    1.61 -    fix i assume i: "i \<in> {..n :: nat}"
    1.62 +    fix i assume i: "i \<le> n"
    1.63      hence "b \<in> I i" using  b_inter by blast
    1.64      moreover have "ideal (I i) R" using Suc i by simp 
    1.65      ultimately show "(I i) +> b = (I i) +> \<zero>"
    1.66        by (metis b ideal.I_r_closed ideal.set_add_zero r_null zero_closed)
    1.67    qed
    1.68    
    1.69 -  have "\<And>i. i \<in> {..Suc n} \<Longrightarrow> (I i) +> (a \<oplus> b) = (I i) +> (x i)"
    1.70 +  have "(I i) +> (a \<oplus> b) = (I i) +> (x i)" if "i \<le> Suc n" for i
    1.71    proof -
    1.72 -    fix i assume i: "i \<in> {..Suc n}" thus "(I i) +> (a \<oplus> b) = (I i) +> (x i)"
    1.73 +    show "(I i) +> (a \<oplus> b) = (I i) +> (x i)"
    1.74 +      using that
    1.75      proof (cases)
    1.76 -      assume 1: "i \<in> {..n}"
    1.77 +      assume 1: "i \<le> n"
    1.78        hence "(I i) +> (a \<oplus> b) = ((I i) +> (x i)) <+> ((I i) +> b)"
    1.79 -        by (metis Suc.prems(2) a b i abelian_subgroup.a_rcos_sum
    1.80 -            abelian_subgroupI3 ideal.axioms(1) is_abelian_group)
    1.81 +        by (metis Suc.prems(2) a abelian_subgroup.a_rcos_sum abelian_subgroupI3 b ideal_def le_SucI ring_def)
    1.82        also have " ... = ((I i) +> (x i)) <+> ((I i) +> \<zero>)"
    1.83          using eq_zero[OF 1] by simp
    1.84        also have " ... = I i +> ((x i) \<oplus> \<zero>)"
    1.85 -        by (meson Suc abelian_subgroup.a_rcos_sum abelian_subgroupI3 i
    1.86 -                  ideal.axioms(1) is_abelian_group zero_closed)
    1.87 +        by (meson Suc.prems abelian_subgroup.a_rcos_sum abelian_subgroupI3 atMost_iff that ideal_def ring_def zero_closed)
    1.88        finally show "(I i) +> (a \<oplus> b) = (I i) +> (x i)"
    1.89 -        using Suc.prems(1) i by auto
    1.90 +        using Suc.prems(1) that by auto
    1.91      next
    1.92 -      assume "i \<notin> {..n}" hence 2: "i = Suc n" using i by simp
    1.93 +      assume "\<not> i \<le> n" hence 2: "i = Suc n" using that by simp
    1.94        hence "I i +> (a \<oplus> b) = I (Suc n) +> (a \<oplus> b)" by simp
    1.95        also have " ... = (I (Suc n) +> a) <+> (I (Suc n) +> (x (Suc n) \<ominus> a))"
    1.96 -        using S a b Suc.prems(2)[of "Suc n"] 2 abelian_subgroup.a_rcos_sum
    1.97 -              abelian_subgroupI3 i ideal.axioms(1) is_abelian_group by metis
    1.98 +        by (metis le_Suc_eq S a b Suc.prems(2)[of "Suc n"] 2 abelian_subgroup.a_rcos_sum
    1.99 +              abelian_subgroupI3 ideal.axioms(1) is_abelian_group)
   1.100        also have " ... = I (Suc n) +> (a \<oplus> (x (Suc n) \<ominus> a))"
   1.101          by (simp add: Suc.prems(1-2) a(1) abelian_subgroup.a_rcos_sum
   1.102                        abelian_subgroupI3 ideal.axioms(1) is_abelian_group)
   1.103 @@ -322,7 +316,7 @@
   1.104  qed
   1.105  
   1.106  lemma DirProd_list_in_carrierI:
   1.107 -  assumes "\<And>i. i \<in> {..<(length rs)} \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)"
   1.108 +  assumes "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)"
   1.109      and "length rs = length Rs"
   1.110    shows "rs \<in> carrier (DirProd_list Rs)" using assms
   1.111  proof (induct Rs arbitrary: rs rule: DirProd_list.induct)
   1.112 @@ -338,7 +332,7 @@
   1.113  
   1.114  lemma DirProd_list_in_carrierE:
   1.115    assumes "rs \<in> carrier (DirProd_list Rs)"
   1.116 -  shows "\<And>i. i \<in> {..<(length rs)} \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)" using assms
   1.117 +  shows "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)" using assms
   1.118  proof (induct Rs arbitrary: rs rule: DirProd_list.induct)
   1.119    case 1 thus ?case by simp 
   1.120  next
   1.121 @@ -358,7 +352,7 @@
   1.122  
   1.123  lemma DirProd_list_m_closed:
   1.124    assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)"
   1.125 -    and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.126 +    and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.127    shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2 \<in> carrier (DirProd_list Rs)" using assms
   1.128  proof (induct Rs arbitrary: r1 r2 rule: DirProd_list.induct)
   1.129    case 1 thus ?case by simp 
   1.130 @@ -370,7 +364,7 @@
   1.131        and "rs2' \<in> carrier (DirProd_list Rs)"
   1.132        and r1: "r1 = r1' # rs1'"
   1.133        and r2: "r2 = r2' # rs2'" by auto
   1.134 -  moreover have "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.135 +  moreover have "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.136      using "2.prems"(3) by force
   1.137    ultimately have "rs1' \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> rs2' \<in> carrier (DirProd_list Rs)"
   1.138      using "2.hyps"(1) by blast
   1.139 @@ -383,7 +377,7 @@
   1.140  
   1.141  lemma DirProd_list_m_output:
   1.142    assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)"
   1.143 -  shows "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow>
   1.144 +  shows "\<And>i. i < length Rs \<Longrightarrow>
   1.145               (r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)" using assms
   1.146  proof (induct Rs arbitrary: r1 r2 rule: DirProd_list.induct)
   1.147    case 1 thus ?case by simp 
   1.148 @@ -400,7 +394,7 @@
   1.149  
   1.150  lemma DirProd_list_m_comm:
   1.151    assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)"
   1.152 -    and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> comm_monoid (Rs ! i)"
   1.153 +    and "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)"
   1.154    shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2 = r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1"
   1.155    apply (rule nth_equalityI) apply auto
   1.156  proof -
   1.157 @@ -423,7 +417,7 @@
   1.158    assumes "r1 \<in> carrier (DirProd_list Rs)"
   1.159        and "r2 \<in> carrier (DirProd_list Rs)"
   1.160        and "r3 \<in> carrier (DirProd_list Rs)"
   1.161 -      and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.162 +      and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.163    shows "(r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2) \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r3 =
   1.164            r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> (r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r3)"
   1.165    apply (rule nth_equalityI) apply auto
   1.166 @@ -447,22 +441,22 @@
   1.167  qed
   1.168  
   1.169  lemma DirProd_list_one:
   1.170 -  "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> (\<one>\<^bsub>(DirProd_list Rs)\<^esub>) ! i =  \<one>\<^bsub>(Rs ! i)\<^esub>"
   1.171 +  "\<And>i. i < length Rs \<Longrightarrow> (\<one>\<^bsub>(DirProd_list Rs)\<^esub>) ! i =  \<one>\<^bsub>(Rs ! i)\<^esub>"
   1.172    by (induct Rs rule: DirProd_list.induct) (simp_all add: nth_Cons')
   1.173  
   1.174  lemma DirProd_list_one_closed:
   1.175 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.176 +  assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.177    shows "\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<in> carrier (DirProd_list Rs)"
   1.178  proof (rule DirProd_list_in_carrierI)
   1.179    show eq_len: "length \<one>\<^bsub>DirProd_list Rs\<^esub> = length Rs"
   1.180      by (induct Rs rule: DirProd_list.induct) (simp_all)
   1.181 -  show "\<And>i. i \<in> {..<length \<one>\<^bsub>DirProd_list Rs\<^esub>} \<Longrightarrow> \<one>\<^bsub>DirProd_list Rs\<^esub> ! i \<in> carrier (Rs ! i)"
   1.182 +  show "\<And>i. i < length \<one>\<^bsub>DirProd_list Rs\<^esub> \<Longrightarrow> \<one>\<^bsub>DirProd_list Rs\<^esub> ! i \<in> carrier (Rs ! i)"
   1.183      using eq_len DirProd_list_one[where ?Rs = Rs] monoid.one_closed by (simp add: assms)
   1.184  qed
   1.185  
   1.186  lemma DirProd_list_l_one:
   1.187    assumes "r1 \<in> carrier (DirProd_list Rs)"
   1.188 -    and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.189 +    and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.190    shows "\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1 = r1"
   1.191    apply (rule nth_equalityI) apply auto
   1.192  proof -
   1.193 @@ -485,7 +479,7 @@
   1.194  
   1.195  lemma DirProd_list_r_one:
   1.196    assumes "r1 \<in> carrier (DirProd_list Rs)"
   1.197 -    and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.198 +    and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.199    shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> \<one>\<^bsub>(DirProd_list Rs)\<^esub> = r1"
   1.200  proof -
   1.201    have "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> \<one>\<^bsub>(DirProd_list Rs)\<^esub> =
   1.202 @@ -512,7 +506,7 @@
   1.203  qed
   1.204  
   1.205  lemma DirProd_list_monoid:
   1.206 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.207 +  assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.208    shows "monoid (DirProd_list Rs)"
   1.209    unfolding monoid_def apply auto
   1.210  proof -
   1.211 @@ -535,7 +529,7 @@
   1.212  qed
   1.213  
   1.214  lemma DirProd_list_comm_monoid:
   1.215 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> comm_monoid (Rs ! i)"
   1.216 +  assumes "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)"
   1.217    shows "comm_monoid (DirProd_list Rs)"
   1.218    unfolding comm_monoid_def comm_monoid_axioms_def apply auto
   1.219    using DirProd_list_monoid Group.comm_monoid.axioms(1) assms apply blast
   1.220 @@ -557,7 +551,7 @@
   1.221  qed
   1.222  
   1.223  lemma DirProd_list_group:
   1.224 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> group (Rs ! i)"
   1.225 +  assumes "\<And>i. i < length Rs \<Longrightarrow> group (Rs ! i)"
   1.226    shows "group (DirProd_list Rs)" using assms
   1.227  proof (induction Rs rule: DirProd_list.induct)
   1.228    case 1 thus ?case
   1.229 @@ -577,7 +571,7 @@
   1.230  qed
   1.231  
   1.232  lemma DirProd_list_comm_group:
   1.233 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> comm_group (Rs ! i)"
   1.234 +  assumes "\<And>i. i < length Rs \<Longrightarrow> comm_group (Rs ! i)"
   1.235    shows "comm_group (DirProd_list Rs)"
   1.236    using assms unfolding comm_group_def
   1.237    using DirProd_list_group DirProd_list_comm_monoid by auto
   1.238 @@ -604,8 +598,8 @@
   1.239  
   1.240  lemma DirProd_list_m_inv:
   1.241    assumes "r \<in> carrier (DirProd_list Rs)"
   1.242 -      and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> group (Rs ! i)"
   1.243 -    shows "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> (inv\<^bsub>(DirProd_list Rs)\<^esub> r) ! i = inv\<^bsub>(Rs ! i)\<^esub> (r ! i)"
   1.244 +      and "\<And>i. i < length Rs \<Longrightarrow> group (Rs ! i)"
   1.245 +    shows "\<And>i. i < length Rs \<Longrightarrow> (inv\<^bsub>(DirProd_list Rs)\<^esub> r) ! i = inv\<^bsub>(Rs ! i)\<^esub> (r ! i)"
   1.246    using assms
   1.247  proof (induct Rs arbitrary: r rule: DirProd_list.induct)
   1.248    case 1
   1.249 @@ -656,7 +650,7 @@
   1.250    by (simp add: monoid.defs)
   1.251  
   1.252  lemma RDirProd_list_monoid:
   1.253 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> monoid (Rs ! i)"
   1.254 +  assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)"
   1.255    shows "monoid (RDirProd_list Rs)"
   1.256  proof -
   1.257    have "monoid (DirProd_list Rs)"
   1.258 @@ -670,7 +664,7 @@
   1.259  qed
   1.260  
   1.261  lemma RDirProd_list_comm_monoid:
   1.262 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> comm_monoid (Rs ! i)"
   1.263 +  assumes "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)"
   1.264    shows "comm_monoid (RDirProd_list Rs)"
   1.265  proof -
   1.266    have "comm_monoid (DirProd_list Rs)"
   1.267 @@ -686,10 +680,10 @@
   1.268  qed
   1.269  
   1.270  lemma RDirProd_list_abelian_monoid:
   1.271 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> abelian_monoid (Rs ! i)"
   1.272 +  assumes "\<And>i. i < length Rs \<Longrightarrow> abelian_monoid (Rs ! i)"
   1.273    shows "abelian_monoid (RDirProd_list Rs)"
   1.274  proof -
   1.275 -  have "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> comm_monoid ((map add_monoid Rs) ! i)"
   1.276 +  have "\<And>i. i < length Rs \<Longrightarrow> comm_monoid ((map add_monoid Rs) ! i)"
   1.277      using assms unfolding abelian_monoid_def by simp
   1.278    hence "comm_monoid (DirProd_list (map add_monoid Rs))"
   1.279      by (metis (no_types, lifting) DirProd_list_comm_monoid length_map)
   1.280 @@ -698,10 +692,10 @@
   1.281  qed
   1.282  
   1.283  lemma RDirProd_list_abelian_group:
   1.284 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> abelian_group (Rs ! i)"
   1.285 +  assumes "\<And>i. i < length Rs \<Longrightarrow> abelian_group (Rs ! i)"
   1.286    shows "abelian_group (RDirProd_list Rs)"
   1.287  proof -
   1.288 -  have "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> comm_group ((map add_monoid Rs) ! i)"
   1.289 +  have "\<And>i. i < length Rs \<Longrightarrow> comm_group ((map add_monoid Rs) ! i)"
   1.290      using assms unfolding abelian_group_def abelian_group_axioms_def by simp
   1.291    hence "comm_group (DirProd_list (map add_monoid Rs))"
   1.292      by (metis (no_types, lifting) DirProd_list_comm_group length_map)
   1.293 @@ -717,50 +711,69 @@
   1.294  
   1.295  lemma RDirProd_list_in_carrierE:
   1.296    assumes "rs \<in> carrier (RDirProd_list Rs)"
   1.297 -  shows "\<And>i. i \<in> {..<(length rs)} \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)"
   1.298 +  shows "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)"
   1.299    using assms by (simp add: DirProd_list_in_carrierE monoid.defs)
   1.300  
   1.301  lemma RDirProd_list_in_carrierI:
   1.302 -  assumes "\<And>i. i \<in> {..<(length rs)} \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)"
   1.303 +  assumes "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)"
   1.304        and "length rs = length Rs"
   1.305      shows "rs \<in> carrier (RDirProd_list Rs)"
   1.306    using DirProd_list_in_carrierI assms by (simp add: monoid.defs, blast)
   1.307  
   1.308  lemma RDirProd_list_one:
   1.309 -  "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> (\<one>\<^bsub>(RDirProd_list Rs)\<^esub>) ! i =  \<one>\<^bsub>(Rs ! i)\<^esub>"
   1.310 +  "\<And>i. i < length Rs \<Longrightarrow> (\<one>\<^bsub>(RDirProd_list Rs)\<^esub>) ! i =  \<one>\<^bsub>(Rs ! i)\<^esub>"
   1.311    by (simp add: DirProd_list_one monoid.defs)
   1.312  
   1.313  lemma RDirProd_list_zero:
   1.314 -  "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list Rs)\<^esub>) ! i =  \<zero>\<^bsub>(Rs ! i)\<^esub>"
   1.315 +  "\<And>i. i < length Rs \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list Rs)\<^esub>) ! i =  \<zero>\<^bsub>(Rs ! i)\<^esub>"
   1.316    by (induct Rs rule: DirProd_list.induct) (simp_all add: monoid.defs nth_Cons')
   1.317  
   1.318  lemma RDirProd_list_m_output:
   1.319    assumes "r1 \<in> carrier (RDirProd_list Rs)" "r2 \<in> carrier (RDirProd_list Rs)"
   1.320 -  shows "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow>
   1.321 +  shows "\<And>i. i < length Rs \<Longrightarrow>
   1.322               (r1 \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)"
   1.323    using assms by (simp add: DirProd_list_m_output monoid.defs)
   1.324  
   1.325  lemma RDirProd_list_a_output:
   1.326 -  assumes "r1 \<in> carrier (RDirProd_list Rs)" "r2 \<in> carrier (RDirProd_list Rs)"
   1.327 -  shows "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow>
   1.328 -             (r1 \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<oplus>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)"
   1.329 +  fixes i
   1.330 +  assumes "r1 \<in> carrier (RDirProd_list Rs)" "r2 \<in> carrier (RDirProd_list Rs)" "i < length Rs"
   1.331 +  shows "(r1 \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<oplus>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)"
   1.332    using RDirProd_list_add_monoid[of Rs] monoid.defs(3)
   1.333 -  by (smt DirProd_list_m_output assms length_map lessThan_iff
   1.334 -      monoid.select_convs(1) nth_map partial_object.select_convs(1))
   1.335 +proof -
   1.336 +  have "(\<otimes>\<^bsub>DirProd_list (map add_monoid Rs)\<^esub>) = (\<oplus>\<^bsub>RDirProd_list Rs\<^esub>)"
   1.337 +    by (metis \<open>add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)\<close> monoid.select_convs(1))
   1.338 +  moreover have "r1 \<in> carrier (DirProd_list (map add_monoid Rs))"
   1.339 +    by (metis \<open>add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)\<close> assms(1) partial_object.select_convs(1))
   1.340 +  moreover have "r2 \<in> carrier (DirProd_list (map add_monoid Rs))"
   1.341 +    by (metis \<open>add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)\<close> assms(2) partial_object.select_convs(1))
   1.342 +  ultimately show ?thesis
   1.343 +    by (simp add: DirProd_list_m_output assms(3))
   1.344 +qed
   1.345  
   1.346  lemma RDirProd_list_a_inv:
   1.347 +  fixes i
   1.348    assumes "r \<in> carrier (RDirProd_list Rs)"
   1.349 -      and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> abelian_group (Rs ! i)"
   1.350 -    shows "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> (\<ominus>\<^bsub>(RDirProd_list Rs)\<^esub> r) ! i = \<ominus>\<^bsub>(Rs ! i)\<^esub> (r ! i)"
   1.351 -  using RDirProd_list_add_monoid[of Rs] monoid.defs(3) DirProd_list_m_inv
   1.352 -  by (smt a_inv_def abelian_group.a_group assms length_map lessThan_iff
   1.353 -      monoid.surjective nth_map partial_object.ext_inject) 
   1.354 +      and "\<And>i. i < length Rs \<Longrightarrow> abelian_group (Rs ! i)"
   1.355 +      and "i < length Rs"
   1.356 +    shows "(\<ominus>\<^bsub>(RDirProd_list Rs)\<^esub> r) ! i = \<ominus>\<^bsub>(Rs ! i)\<^esub> (r ! i)"
   1.357 +proof -
   1.358 +  have f1: "m_inv (DirProd_list (map add_monoid Rs)) = a_inv (RDirProd_list Rs)"
   1.359 +    by (metis RDirProd_list_add_monoid a_inv_def)
   1.360 +moreover
   1.361 +  have f4: "r \<in> carrier (DirProd_list (map add_monoid Rs))"
   1.362 +    by (metis RDirProd_list_add_monoid assms(1) partial_object.select_convs(1))
   1.363 +moreover
   1.364 +  have f3: "a_inv (Rs ! i) = m_inv (map add_monoid Rs ! i)"
   1.365 +    by (simp add: a_inv_def assms(3))
   1.366 +  ultimately show ?thesis  using RDirProd_list_add_monoid[of Rs] monoid.defs(3) DirProd_list_m_inv
   1.367 +    by (smt abelian_group.a_group assms(2) assms(3) length_map nth_map)
   1.368 +qed
   1.369  
   1.370  lemma RDirProd_list_l_distr:
   1.371    assumes "x \<in> carrier (RDirProd_list Rs)"
   1.372        and "y \<in> carrier (RDirProd_list Rs)"
   1.373        and "z \<in> carrier (RDirProd_list Rs)"
   1.374 -      and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> ring (Rs ! i)"
   1.375 +      and "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)"
   1.376      shows "(x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z =
   1.377             (x \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (y \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z)"
   1.378  proof -
   1.379 @@ -802,7 +815,7 @@
   1.380    assumes "x \<in> carrier (RDirProd_list Rs)"
   1.381        and "y \<in> carrier (RDirProd_list Rs)"
   1.382        and "z \<in> carrier (RDirProd_list Rs)"
   1.383 -      and "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> ring (Rs ! i)"
   1.384 +      and "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)"
   1.385      shows "z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) =
   1.386            (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> x) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> y)"
   1.387  proof -
   1.388 @@ -841,19 +854,19 @@
   1.389  qed
   1.390  
   1.391  theorem RDirProd_list_ring:
   1.392 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> ring (Rs ! i)"
   1.393 +  assumes "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)"
   1.394    shows "ring (RDirProd_list Rs)"
   1.395    using assms unfolding ring_def ring_axioms_def using assms 
   1.396    by (meson RDirProd_list_abelian_group RDirProd_list_l_distr
   1.397              RDirProd_list_monoid RDirProd_list_r_distr)
   1.398  
   1.399  theorem RDirProd_list_cring:
   1.400 -  assumes "\<And>i. i \<in> {..<(length Rs)} \<Longrightarrow> cring (Rs ! i)"
   1.401 +  assumes "\<And>i. i < length Rs \<Longrightarrow> cring (Rs ! i)"
   1.402    shows "cring (RDirProd_list Rs)"
   1.403    by (meson RDirProd_list_comm_monoid RDirProd_list_ring assms cring_def)
   1.404  
   1.405  corollary (in cring) RDirProd_list_of_quot_is_cring:
   1.406 -  assumes "\<And>i. i \<in> {..< n} \<Longrightarrow> ideal (I i) R"
   1.407 +  assumes "\<And>i. i < n \<Longrightarrow> ideal (I i) R"
   1.408      shows "cring (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< n]))"
   1.409        (is "cring (RDirProd_list ?Rs)")
   1.410  proof -
   1.411 @@ -948,8 +961,9 @@
   1.412                                      Description of its Kernel\<close>
   1.413  
   1.414  theorem (in cring) canonical_proj_ext_is_hom:
   1.415 -  assumes "\<And>i. i \<in> {..< (n :: nat)} \<Longrightarrow> ideal (I i) R"
   1.416 -      and "\<And>i j. \<lbrakk> i \<in> {..< n}; j \<in> {..< n}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.417 +  fixes n::nat
   1.418 +  assumes "\<And>i. i < n \<Longrightarrow> ideal (I i) R"
   1.419 +      and "\<And>i j. \<lbrakk> i < n; j < n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.420      shows "(\<lambda>a. (map (\<lambda>i. (I i) +> a) [0..< n])) \<in>
   1.421              ring_hom R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< n]))" (is "?\<phi> \<in> ?ring_hom")
   1.422  proof (rule ring_hom_memI)
   1.423 @@ -960,7 +974,6 @@
   1.424    note aux_lemma = this
   1.425  
   1.426    fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R"
   1.427 -
   1.428    show x': "?\<phi> x \<in> carrier (RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))"
   1.429      using aux_lemma[OF x] .
   1.430    hence x'': "?\<phi> x \<in> carrier (DirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))"
   1.431 @@ -977,8 +990,7 @@
   1.432                   cring.cring_simprules(5) length_map x' y')
   1.433      apply (simp add: monoid.defs)
   1.434      using DirProd_list_m_output [of "?\<phi> x" "(map (\<lambda>i. R Quot I i) [0..<n])" "?\<phi> y"] x'' y''
   1.435 -    by (simp add: x'' y'' FactRing_def add.left_neutral assms(1) diff_zero ideal.rcoset_mult_add
   1.436 -                  length_map length_upt lessThan_iff monoid.simps(1) nth_map_upt x y)
   1.437 +    by (simp add: x'' y'' FactRing_def  assms(1) ideal.rcoset_mult_add x y)
   1.438  
   1.439    show "?\<phi> (x \<oplus> y) = ?\<phi> x \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> ?\<phi> y"
   1.440    proof -
   1.441 @@ -995,10 +1007,21 @@
   1.442        have "(?\<phi> (x \<oplus> y)) ! j = I j +> x \<oplus> y" using j by simp
   1.443        also have " ... = (I j +> x) \<oplus>\<^bsub>(R Quot I j)\<^esub> (I j +> y)"
   1.444          by (simp add: FactRing_def abelian_subgroup.a_rcos_sum abelian_subgroupI3
   1.445 -                      assms(1) ideal.axioms(1) is_abelian_group j x y)
   1.446 +            assms(1) ideal.axioms(1) is_abelian_group j x y)
   1.447        also have " ... = ((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y)) ! j"
   1.448 -        by (smt RDirProd_list_a_output add.left_neutral diff_zero j
   1.449 -            length_map length_upt lessThan_iff nth_map nth_upt x' y')
   1.450 +      proof -
   1.451 +        have "R Quot I j = map (\<lambda>n. R Quot I n) [0..<n] ! j"
   1.452 +             "I j +> x = I ([0..<n] ! j) +> x" 
   1.453 +             "I j +> y = I ([0..<n] ! j) +> y"
   1.454 +          by (simp_all add: j)
   1.455 +        moreover have "\<And>n ns f. n < length ns \<Longrightarrow> map f ns ! n = (f (ns ! n::nat)::'a set)"
   1.456 +          by simp
   1.457 +        moreover have "\<And>B ps C n. \<lbrakk>B \<in> carrier (RDirProd_list ps); C \<in> carrier (RDirProd_list ps); n < length ps\<rbrakk> 
   1.458 +                     \<Longrightarrow> (B \<oplus>\<^bsub>RDirProd_list ps\<^esub> C) ! n = (B ! n::'a set) \<oplus>\<^bsub>ps ! n\<^esub> C ! n"
   1.459 +          by (meson RDirProd_list_a_output)
   1.460 +        ultimately show ?thesis
   1.461 +          by (metis (mono_tags, lifting) diff_zero j length_map length_upt x' y') 
   1.462 +      qed
   1.463        finally show "(?\<phi> (x \<oplus> y)) ! j =
   1.464                      ((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y)) ! j" .
   1.465      qed
   1.466 @@ -1016,8 +1039,9 @@
   1.467  
   1.468  
   1.469  theorem (in cring) canonical_proj_ext_kernel:
   1.470 -  assumes "\<And>i. i \<in> {..(n :: nat)} \<Longrightarrow> ideal (I i) R"
   1.471 -      and "\<And>i j. \<lbrakk> i \<in> {..n}; j \<in> {..n}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.472 +  fixes n::nat
   1.473 +  assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R"
   1.474 +      and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.475      shows "(\<Inter>i \<le> n. I i) = a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))
   1.476                             (\<lambda>a. (map (\<lambda>i. (I i) +> a) [0..< Suc n]))"
   1.477  proof -
   1.478 @@ -1035,16 +1059,18 @@
   1.479          "\<And>i. i \<le> n \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) ! i =
   1.480                           \<zero>\<^bsub>(R Quot (I i))\<^esub>"
   1.481          using RDirProd_list_zero[where ?Rs = "map (\<lambda>i. R Quot I i) [0..<Suc n]"]
   1.482 -        by (metis (no_types, lifting) add.left_neutral atMost_iff le_imp_less_Suc
   1.483 -            length_map length_upt lessThan_Suc_atMost nth_map_upt diff_zero)
   1.484 +        by (metis (no_types, lifting) add.left_neutral le_imp_less_Suc
   1.485 +            length_map length_upt nth_map_upt diff_zero)
   1.486        hence 
   1.487          "\<And>i. i \<le> n \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) ! i = I i"
   1.488          unfolding FactRing_def by simp
   1.489        moreover
   1.490        have "length (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) = Suc n"
   1.491 +
   1.492          using RDirProd_list_carrier_elts RDirProd_list_cring
   1.493 -        by (smt add.left_neutral assms(1) cring.cring_simprules(2) diff_zero nth_map_upt
   1.494 -            ideal.quotient_is_cring is_cring length_map length_upt lessThan_Suc_atMost lessThan_iff)
   1.495 +         add.left_neutral assms(1) cring.cring_simprules(2) diff_zero nth_map_upt
   1.496 +            ideal.quotient_is_cring is_cring length_map length_upt lessThan_Suc_atMost lessThan_iff
   1.497 +        by (smt less_Suc_eq_le)
   1.498        moreover have "length (?\<phi> s) = Suc n" by simp
   1.499        ultimately have "?\<phi> s = \<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>"
   1.500          by (simp add: nth_equalityI)
   1.501 @@ -1060,10 +1086,9 @@
   1.502        fix s assume s: "s \<in> a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi>"
   1.503        hence "?\<phi> s = \<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>"
   1.504          unfolding a_kernel_def kernel_def by (simp add: monoid.defs)
   1.505 -      hence "\<And>i. i \<le> n \<Longrightarrow> (I i) +> s = \<zero>\<^bsub>(R Quot (I i))\<^esub>"
   1.506 +      hence "(I i) +> s = \<zero>\<^bsub>(R Quot (I i))\<^esub>" if "i \<le> n" for i
   1.507          using RDirProd_list_zero[where ?Rs = "map (\<lambda>i. R Quot I i) [0..<Suc n]"]
   1.508 -        by (smt add.left_neutral atMost_iff diff_zero le_imp_less_Suc
   1.509 -            length_map length_upt lessThan_Suc_atMost nth_map_upt)
   1.510 +          by (metis (no_types) that add.left_neutral diff_zero le_imp_less_Suc length_map length_upt nth_map_upt)
   1.511        hence "\<And>i. i \<le> n \<Longrightarrow> (I i) +> s = I i"
   1.512          unfolding FactRing_def by simp
   1.513        moreover have "s \<in> carrier R"
   1.514 @@ -1078,8 +1103,9 @@
   1.515  subsection \<open>Final Generalization\<close>
   1.516  
   1.517  theorem (in cring) chinese_remainder:
   1.518 -  assumes "\<And>i. i \<in> {..(n :: nat)} \<Longrightarrow> ideal (I i) R"
   1.519 -      and "\<And>i j. \<lbrakk> i \<in> {..n}; j \<in> {..n}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.520 +  fixes n::nat
   1.521 +  assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R"
   1.522 +      and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.523      shows "R Quot (\<Inter>i \<le> n. I i) \<simeq>  RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])"
   1.524    using assms
   1.525  proof (induct n)
   1.526 @@ -1100,9 +1126,8 @@
   1.527    have inter_ideal: "ideal (\<Inter> i \<le> n. I i) R"
   1.528      using Suc.prems(1) i_Intersect[of "I ` {..n}"] atMost_Suc atLeast1_atMost_eq_remove0 by auto
   1.529    hence "R Quot (\<Inter> i \<le> Suc n. I i) \<simeq> RDirProd (R Quot (\<Inter> i \<le> n. I i)) (R Quot (I (Suc n)))"
   1.530 -    using chinese_remainder_simple[of "\<Inter> i \<le> n. I i" "I (Suc n)"]
   1.531 -          inter_plus_ideal_eq_carrier[of n I] by (simp add: Int_commute Suc.prems(1-2) atMost_Suc)
   1.532 -
   1.533 +    using chinese_remainder_simple[of "\<Inter> i \<le> n. I i" "I (Suc n)"] inter_plus_ideal_eq_carrier[of n I]
   1.534 +    by (simp add: Int_commute Suc.prems(1-2) atMost_Suc)
   1.535    moreover have "R Quot (\<Inter> i \<le> n. I i) \<simeq> RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])"
   1.536      using Suc.hyps Suc.prems(1-2) by auto
   1.537    hence "RDirProd (R Quot (\<Inter> i \<le> n. I i)) (R Quot (I (Suc n))) \<simeq>
   1.538 @@ -1124,82 +1149,4 @@
   1.539    ultimately show ?case using ring_iso_trans by simp
   1.540  qed
   1.541  
   1.542 -theorem (in cring) (* chinese_remainder: another proof *)
   1.543 -  assumes "\<And>i. i \<in> {..(n :: nat)} \<Longrightarrow> ideal (I i) R"
   1.544 -      and "\<And>i j. \<lbrakk> i \<in> {..n}; j \<in> {..n}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
   1.545 -    shows "R Quot (\<Inter>i \<le> n. I i) \<simeq>  RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])"
   1.546 -proof -
   1.547 -  let ?\<phi> = "\<lambda>a. (map (\<lambda>i. (I i) +> a) [0..< Suc n])"
   1.548 -
   1.549 -  have phi_hom: "?\<phi> \<in> ring_hom R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
   1.550 -    using canonical_proj_ext_is_hom[of "Suc n"] assms by simp 
   1.551 -
   1.552 -  moreover have "?\<phi> ` (carrier R) = carrier (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
   1.553 -  proof
   1.554 -    show "carrier (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) \<subseteq> ?\<phi> ` (carrier R)"
   1.555 -    proof
   1.556 -      fix x assume x: "x \<in> carrier (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
   1.557 -      hence x_nth_eq: "\<And>i. i \<in> {..< Suc n} \<Longrightarrow> x ! i \<in> carrier (R Quot (I i))"
   1.558 -        using RDirProd_list_in_carrierE
   1.559 -        by (smt RDirProd_list_carrier_elts add.left_neutral diff_zero length_map
   1.560 -            length_upt lessThan_iff nth_map nth_upt)
   1.561 -      then obtain y where y: "\<And>i. i \<in> {..< Suc n} \<Longrightarrow> x ! i = (I i) +> (y i)"
   1.562 -                             "\<And>i. i \<in> {..< Suc n} \<Longrightarrow> y i \<in> carrier R"
   1.563 -      proof -
   1.564 -        from x_nth_eq have "\<exists>y. (\<forall>i \<in> {..< Suc n}. x ! i = (I i) +> (y i)) \<and>
   1.565 -                                (\<forall>i \<in> {..< Suc n}. y i \<in> carrier R)"
   1.566 -        proof (induct n)
   1.567 -          case 0
   1.568 -          have "x ! 0 \<in> carrier (R Quot (I 0))" using x_nth_eq by simp
   1.569 -          then obtain x_0 where x_0: "x ! 0 = (I 0) +> x_0" "x_0 \<in> carrier R"
   1.570 -            unfolding FactRing_def using A_RCOSETS_def'[of R "I 0"] by auto
   1.571 -          define y :: "nat \<Rightarrow> 'a"  where "y = (\<lambda>i. x_0)"
   1.572 -          hence "x ! 0 = (I 0) +> (y 0) \<and> (y 0) \<in> carrier R"
   1.573 -            using x_0 by simp
   1.574 -          thus ?case using x_0 by blast
   1.575 -        next
   1.576 -          case (Suc n)
   1.577 -          then obtain y' where y': "\<And>i. i \<in> {..<Suc n} \<Longrightarrow> x ! i = I i +> y' i"
   1.578 -                                   "\<And>i. i \<in> {..<Suc n} \<Longrightarrow> y' i \<in> carrier R" by auto
   1.579 -
   1.580 -          have "x ! (Suc n) \<in> carrier (R Quot (I (Suc n)))" using Suc by simp
   1.581 -          then obtain x_Sn where x_Sn: "x ! (Suc n) = (I (Suc n)) +> x_Sn"
   1.582 -                                       "x_Sn \<in> carrier R"
   1.583 -            unfolding FactRing_def using A_RCOSETS_def'[of R "I (Suc n)"] by auto
   1.584 -
   1.585 -          define y where "y = (\<lambda>i. if i = (Suc n) then x_Sn else (y' i))"
   1.586 -          thus ?case using y' x_Sn
   1.587 -            by (metis (full_types) insert_iff lessThan_Suc) 
   1.588 -        qed
   1.589 -        thus ?thesis using that by blast
   1.590 -      qed
   1.591 -
   1.592 -      then obtain a where a: "a \<in> carrier R"
   1.593 -                      and "\<And>i. i \<in> {..< Suc n} \<Longrightarrow> (I i) +> a = (I i) +> (y i)"
   1.594 -        using canonical_proj_ext_is_surj[of n y I] assms(1-2) by auto
   1.595 -      hence a_x: "\<And>i. i \<in> {..< Suc n} \<Longrightarrow> (I i) +> a = x ! i"
   1.596 -        using y by simp
   1.597 -      have "?\<phi> a = x"
   1.598 -        apply (rule nth_equalityI)
   1.599 -        using RDirProd_list_carrier_elts x apply fastforce
   1.600 -        by (metis a_x add.left_neutral diff_zero length_map length_upt lessThan_iff nth_map_upt)
   1.601 -      thus "x \<in> ?\<phi> ` (carrier R)"
   1.602 -        using a by blast
   1.603 -    qed
   1.604 -  next
   1.605 -    show "?\<phi> ` carrier R \<subseteq> carrier (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
   1.606 -      using phi_hom unfolding ring_hom_def by blast
   1.607 -  qed
   1.608 -
   1.609 -  moreover have "a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi> = (\<Inter>i \<le> n. I i)"
   1.610 -    using canonical_proj_ext_kernel assms by blast
   1.611 -
   1.612 -  moreover have "ring (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))"
   1.613 -    using RDirProd_list_of_quot_is_cring assms(1) cring_def lessThan_Suc_atMost by blast
   1.614 -
   1.615 -  ultimately show ?thesis
   1.616 -    using ring_hom_ring.FactRing_iso[of R "RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])" ?\<phi>]
   1.617 -          is_ring by (simp add: ring_hom_ringI2) 
   1.618 -qed
   1.619 -
   1.620  end
     2.1 --- a/src/HOL/Algebra/Group_Action.thy	Sun Jul 08 23:35:33 2018 +0100
     2.2 +++ b/src/HOL/Algebra/Group_Action.thy	Mon Jul 09 21:55:40 2018 +0100
     2.3 @@ -134,7 +134,7 @@
     2.4    shows "x \<in> orbit G \<phi> y"
     2.5  proof -
     2.6    have "\<exists> g \<in> carrier G. (\<phi> g) x = y"
     2.7 -    by (smt assms(3) mem_Collect_eq orbit_def)
     2.8 +    using assms by (auto simp: orbit_def)
     2.9    then obtain g where g: "g \<in> carrier G \<and> (\<phi> g) x = y" by blast
    2.10    hence "(\<phi> (inv g)) y = x"
    2.11      using orbit_sym_aux by (simp add: assms(1))
    2.12 @@ -149,15 +149,10 @@
    2.13  proof -
    2.14    interpret group G
    2.15      using group_hom group_hom.axioms(1) by auto
    2.16 -
    2.17 -  have "\<exists> g1 \<in> carrier G. (\<phi> g1) x = y"
    2.18 -    by (smt assms mem_Collect_eq orbit_def)
    2.19 -  then obtain g1 where g1: "g1 \<in> carrier G \<and> (\<phi> g1) x = y" by blast
    2.20 -
    2.21 -  have "\<exists> g2 \<in> carrier G. (\<phi> g2) y = z"
    2.22 -    by (smt assms mem_Collect_eq orbit_def)
    2.23 -  then obtain g2 where g2: "g2 \<in> carrier G \<and> (\<phi> g2) y = z" by blast
    2.24 -  
    2.25 +  obtain g1 where g1: "g1 \<in> carrier G \<and> (\<phi> g1) x = y" 
    2.26 +    using assms by (auto simp: orbit_def)
    2.27 +  obtain g2 where g2: "g2 \<in> carrier G \<and> (\<phi> g2) y = z" 
    2.28 +    using assms by (auto simp: orbit_def)  
    2.29    have "(\<phi> (g2 \<otimes> g1)) x = ((\<phi> g2) \<otimes>\<^bsub>BijGroup E\<^esub> (\<phi> g1)) x"
    2.30      using g1 g2 group_hom group_hom.hom_mult by fastforce
    2.31    also have " ... = (\<phi> g2) ((\<phi> g1) x)"
    2.32 @@ -170,12 +165,8 @@
    2.33  
    2.34  lemma (in group_action) orbits_as_classes:
    2.35    "classes\<^bsub>\<lparr> carrier = E, eq = \<lambda>x. \<lambda>y. y \<in> orbit G \<phi> x \<rparr>\<^esub> = orbits G E \<phi>"
    2.36 -  unfolding eq_classes_def eq_class_of_def orbits_def apply simp
    2.37 -proof -
    2.38 -  have "\<And>x. x \<in> E \<Longrightarrow> {y \<in> E. y \<in> orbit G \<phi> x} = orbit G \<phi> x"
    2.39 -    by (smt Collect_cong element_image mem_Collect_eq orbit_def)
    2.40 -  thus "{{y \<in> E. y \<in> orbit G \<phi> x} |x. x \<in> E} = {orbit G \<phi> x |x. x \<in> E}" by blast
    2.41 -qed
    2.42 +  unfolding eq_classes_def eq_class_of_def orbits_def orbit_def 
    2.43 +  using element_image by auto
    2.44  
    2.45  theorem (in group_action) orbit_partition:
    2.46    "partition E (orbits G E \<phi>)"
    2.47 @@ -722,14 +713,15 @@
    2.48    show " \<And> x y. \<lbrakk> x \<in> inv g <# H #> g; y \<in> inv g <# H #> g \<rbrakk> \<Longrightarrow> x \<otimes> y \<in> inv g <# H #> g"
    2.49    proof -
    2.50      fix x y assume "x \<in> inv g <# H #> g"  "y \<in> inv g <# H #> g"
    2.51 -    hence "\<exists> h1 \<in> H. \<exists> h2 \<in> H. x = (inv g) \<otimes> h1 \<otimes> g \<and> y = (inv g) \<otimes> h2 \<otimes> g"
    2.52 +    then obtain h1 h2 where h12: "h1 \<in> H" "h2 \<in> H" and "x = (inv g) \<otimes> h1 \<otimes> g \<and> y = (inv g) \<otimes> h2 \<otimes> g"
    2.53        unfolding l_coset_def r_coset_def by blast
    2.54 -    hence "\<exists> h1 \<in> H. \<exists> h2 \<in> H. x \<otimes> y = ((inv g) \<otimes> h1 \<otimes> g) \<otimes> ((inv g) \<otimes> h2 \<otimes> g)" by blast
    2.55 -    hence "\<exists> h1 \<in> H. \<exists> h2 \<in> H. x \<otimes> y = ((inv g) \<otimes> (h1 \<otimes> h2) \<otimes> g)"
    2.56 -      using assms is_group inv_closed l_one m_assoc m_closed
    2.57 -            monoid_axioms r_inv subgroup.mem_carrier by smt
    2.58 -    hence "\<exists> h \<in> H. x \<otimes> y = (inv g) \<otimes> h \<otimes> g"
    2.59 -      by (meson assms(2) subgroup_def)
    2.60 +    hence "x \<otimes> y = ((inv g) \<otimes> h1 \<otimes> g) \<otimes> ((inv g) \<otimes> h2 \<otimes> g)" by blast
    2.61 +    also have "\<dots> = ((inv g) \<otimes> h1 \<otimes> (g \<otimes> inv g) \<otimes> h2 \<otimes> g)"
    2.62 +      using h12 assms inv_closed  m_assoc m_closed subgroup.mem_carrier [OF \<open>subgroup H G\<close>] by presburger 
    2.63 +    also have "\<dots> = ((inv g) \<otimes> (h1 \<otimes> h2) \<otimes> g)"
    2.64 +      by (simp add: h12 assms m_assoc subgroup.mem_carrier [OF \<open>subgroup H G\<close>])
    2.65 +    finally have "\<exists> h \<in> H. x \<otimes> y = (inv g) \<otimes> h \<otimes> g"
    2.66 +      by (meson assms(2) h12 subgroup_def)
    2.67      thus "x \<otimes> y \<in> inv g <# H #> g"
    2.68        unfolding l_coset_def r_coset_def by blast
    2.69    qed
    2.70 @@ -741,11 +733,9 @@
    2.71        unfolding r_coset_def l_coset_def by blast
    2.72      then obtain h where h: "h \<in> H \<and> x = (inv g) \<otimes> h \<otimes> g" by blast
    2.73      hence "x \<otimes> (inv g) \<otimes> (inv h) \<otimes> g = \<one>"
    2.74 -      using assms inv_closed m_assoc m_closed monoid_axioms
    2.75 -            r_inv r_one subgroup.mem_carrier by smt
    2.76 +      using assms m_assoc monoid_axioms by (simp add: subgroup.mem_carrier)
    2.77      hence "inv x = (inv g) \<otimes> (inv h) \<otimes> g"
    2.78 -      using assms h inv_closed inv_inv inv_mult_group m_assoc
    2.79 -            m_closed monoid_axioms subgroup.mem_carrier by smt
    2.80 +      using assms h inv_mult_group m_assoc monoid_axioms by (simp add: subgroup.mem_carrier)
    2.81      moreover have "inv h \<in> H"
    2.82        by (simp add: assms h subgroup.m_inv_closed)
    2.83      ultimately show "inv x \<in> inv g <# H #> g" unfolding r_coset_def l_coset_def by blast
    2.84 @@ -843,8 +833,7 @@
    2.85      by (metis assms l_coset_subset_G mem_Collect_eq r_coset_subset_G subgroup_def subgroup_self)
    2.86    hence "{H. H \<subseteq> carrier G} \<subseteq> ?\<phi> ` {H. H \<subseteq> carrier G}" by blast
    2.87    moreover have "?\<phi> ` {H. H \<subseteq> carrier G} \<subseteq> {H. H \<subseteq> carrier G}"
    2.88 -    by (smt assms image_subsetI inv_closed l_coset_subset_G
    2.89 -            mem_Collect_eq r_coset_subset_G restrict_apply')
    2.90 +    by clarsimp (meson assms contra_subsetD inv_closed l_coset_subset_G r_coset_subset_G)
    2.91    ultimately show "?\<phi> ` {H. H \<subseteq> carrier G} = {H. H \<subseteq> carrier G}" by simp
    2.92  qed
    2.93  
     3.1 --- a/src/HOL/Algebra/Ideal_Product.thy	Sun Jul 08 23:35:33 2018 +0100
     3.2 +++ b/src/HOL/Algebra/Ideal_Product.thy	Mon Jul 09 21:55:40 2018 +0100
     3.3 @@ -400,7 +400,7 @@
     3.4  
     3.5  lemma (in cring) ideal_prod_eq_Inter_aux:
     3.6    assumes "I: {..(Suc n)} \<rightarrow> { J. ideal J R }" 
     3.7 -    and "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)} \<rbrakk> \<Longrightarrow>
     3.8 +    and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n \<rbrakk> \<Longrightarrow>
     3.9                   i \<noteq> j \<Longrightarrow> (I i) <+> (I j) = carrier R"
    3.10    shows "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. I k) <+> (I (Suc n)) = carrier R" using assms
    3.11  proof (induct n arbitrary: I)
    3.12 @@ -419,7 +419,7 @@
    3.13    let ?I' = "\<lambda>i. I (Suc i)"
    3.14    have "?I': {..(Suc n)} \<rightarrow> { J. ideal J R }"
    3.15      using Suc.prems(1) by auto
    3.16 -  moreover have "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)} \<rbrakk> \<Longrightarrow>
    3.17 +  moreover have "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n \<rbrakk> \<Longrightarrow>
    3.18                           i \<noteq> j \<Longrightarrow> (?I' i) <+> (?I' j) = carrier R"
    3.19      by (simp add: Suc.prems(2))
    3.20    ultimately have "(\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..n}. ?I' k) <+> (?I' (Suc n)) = carrier R"
    3.21 @@ -508,23 +508,23 @@
    3.22  qed
    3.23  
    3.24  corollary (in cring) inter_plus_ideal_eq_carrier:
    3.25 -  assumes "\<And>i. i \<in> {..(Suc n)} \<Longrightarrow> ideal (I i) R" 
    3.26 -      and "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
    3.27 +  assumes "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I i) R" 
    3.28 +      and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
    3.29    shows "(\<Inter> i \<le> n. I i) <+> (I (Suc n)) = carrier R"
    3.30    using ideal_prod_eq_Inter[of I n] ideal_prod_eq_Inter_aux[of I n] by (auto simp add: assms)
    3.31  
    3.32  corollary (in cring) inter_plus_ideal_eq_carrier_arbitrary:
    3.33 -  assumes "\<And>i. i \<in> {..(Suc n)} \<Longrightarrow> ideal (I i) R" 
    3.34 -      and "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)}; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
    3.35 -      and "j \<in> {..(Suc n)}"
    3.36 +  assumes "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I i) R" 
    3.37 +      and "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R"
    3.38 +      and "j \<le> Suc n"
    3.39    shows "(\<Inter> i \<in> ({..(Suc n)} - { j }). I i) <+> (I j) = carrier R"
    3.40  proof -
    3.41    define I' where "I' = (\<lambda>i. if i = Suc n then (I j) else
    3.42                               if i = j     then (I (Suc n))
    3.43                                            else (I i))"
    3.44 -  have "\<And>i. i \<in> {..(Suc n)} \<Longrightarrow> ideal (I' i) R"
    3.45 +  have "\<And>i. i \<le> Suc n \<Longrightarrow> ideal (I' i) R"
    3.46      using I'_def assms(1) assms(3) by auto
    3.47 -  moreover have "\<And>i j. \<lbrakk> i \<in> {..(Suc n)}; j \<in> {..(Suc n)}; i \<noteq> j \<rbrakk> \<Longrightarrow> I' i <+> I' j = carrier R"
    3.48 +  moreover have "\<And>i j. \<lbrakk> i \<le> Suc n; j \<le> Suc n; i \<noteq> j \<rbrakk> \<Longrightarrow> I' i <+> I' j = carrier R"
    3.49      using I'_def assms(2-3) by force
    3.50    ultimately have "(\<Inter> i \<le> n. I' i) <+> (I' (Suc n)) = carrier R"
    3.51      using inter_plus_ideal_eq_carrier by simp
     4.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sun Jul 08 23:35:33 2018 +0100
     4.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Jul 09 21:55:40 2018 +0100
     4.3 @@ -296,7 +296,7 @@
     4.4      with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
     4.5        by (auto intro: mult_dvd_mono)
     4.6      with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
     4.7 -      by force
     4.8 +      by blast
     4.9    qed
    4.10  qed
    4.11