src/HOL/Algebra/Divisibility.thy
changeset 68470 7ddcce75c3ee
parent 68399 0b71d08528f0
child 68474 346bdafaf5fa
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Jun 19 12:14:31 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Jun 19 23:11:00 2018 +0100
     1.3 @@ -189,39 +189,31 @@
     1.4    by (intro dividesI[of "\<one>"]) (simp_all add: carr)
     1.5  
     1.6  lemma (in monoid) divides_trans [trans]:
     1.7 -  assumes dvds: "a divides b"  "b divides c"
     1.8 +  assumes dvds: "a divides b" "b divides c"
     1.9      and acarr: "a \<in> carrier G"
    1.10    shows "a divides c"
    1.11    using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr)
    1.12  
    1.13  lemma (in monoid) divides_mult_lI [intro]:
    1.14 -  assumes ab: "a divides b"
    1.15 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
    1.16 +  assumes  "a divides b" "a \<in> carrier G" "c \<in> carrier G"
    1.17    shows "(c \<otimes> a) divides (c \<otimes> b)"
    1.18 -  using ab
    1.19 -  apply (elim dividesE)
    1.20 -  apply (simp add: m_assoc[symmetric] carr)
    1.21 -  apply (fast intro: dividesI)
    1.22 -  done
    1.23 +  by (metis assms factor_def m_assoc)
    1.24  
    1.25  lemma (in monoid_cancel) divides_mult_l [simp]:
    1.26    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
    1.27    shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b"
    1.28 -  apply safe
    1.29 -   apply (elim dividesE, intro dividesI, assumption)
    1.30 -   apply (rule l_cancel[of c])
    1.31 -      apply (simp add: m_assoc carr)+
    1.32 -  apply (fast intro: carr)
    1.33 -  done
    1.34 +proof
    1.35 +  show "c \<otimes> a divides c \<otimes> b \<Longrightarrow> a divides b"
    1.36 +    using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce
    1.37 +  show "a divides b \<Longrightarrow> c \<otimes> a divides c \<otimes> b"
    1.38 +  using carr(1) carr(3) by blast
    1.39 +qed
    1.40  
    1.41  lemma (in comm_monoid) divides_mult_rI [intro]:
    1.42    assumes ab: "a divides b"
    1.43      and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
    1.44    shows "(a \<otimes> c) divides (b \<otimes> c)"
    1.45 -  using carr ab
    1.46 -  apply (simp add: m_comm[of a c] m_comm[of b c])
    1.47 -  apply (rule divides_mult_lI, assumption+)
    1.48 -  done
    1.49 +  using carr ab by (metis divides_mult_lI m_comm)
    1.50  
    1.51  lemma (in comm_monoid_cancel) divides_mult_r [simp]:
    1.52    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
    1.53 @@ -230,18 +222,14 @@
    1.54  
    1.55  lemma (in monoid) divides_prod_r:
    1.56    assumes ab: "a divides b"
    1.57 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
    1.58 +    and carr: "a \<in> carrier G" "c \<in> carrier G"
    1.59    shows "a divides (b \<otimes> c)"
    1.60    using ab carr by (fast intro: m_assoc)
    1.61  
    1.62  lemma (in comm_monoid) divides_prod_l:
    1.63 -  assumes carr[intro]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
    1.64 -    and ab: "a divides b"
    1.65 +  assumes "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" "a divides b"
    1.66    shows "a divides (c \<otimes> b)"
    1.67 -  using ab carr
    1.68 -  apply (simp add: m_comm[of c b])
    1.69 -  apply (fast intro: divides_prod_r)
    1.70 -  done
    1.71 +  using assms  by (simp add: divides_prod_r m_comm)
    1.72  
    1.73  lemma (in monoid) unit_divides:
    1.74    assumes uunit: "u \<in> Units G"
    1.75 @@ -272,22 +260,20 @@
    1.76  
    1.77  lemma associatedI:
    1.78    fixes G (structure)
    1.79 -  assumes "a divides b"  "b divides a"
    1.80 +  assumes "a divides b" "b divides a"
    1.81    shows "a \<sim> b"
    1.82    using assms by (simp add: associated_def)
    1.83  
    1.84  lemma (in monoid) associatedI2:
    1.85    assumes uunit[simp]: "u \<in> Units G"
    1.86      and a: "a = b \<otimes> u"
    1.87 -    and bcarr[simp]: "b \<in> carrier G"
    1.88 +    and bcarr: "b \<in> carrier G"
    1.89    shows "a \<sim> b"
    1.90    using uunit bcarr
    1.91    unfolding a
    1.92    apply (intro associatedI)
    1.93 -   apply (rule dividesI[of "inv u"], simp)
    1.94 -   apply (simp add: m_assoc Units_closed)
    1.95 -  apply fast
    1.96 -  done
    1.97 +  apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)
    1.98 +  by blast
    1.99  
   1.100  lemma (in monoid) associatedI2':
   1.101    assumes "a = b \<otimes> u"
   1.102 @@ -304,7 +290,7 @@
   1.103  
   1.104  lemma (in monoid_cancel) associatedD2:
   1.105    assumes assoc: "a \<sim> b"
   1.106 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"
   1.107 +    and carr: "a \<in> carrier G" "b \<in> carrier G"
   1.108    shows "\<exists>u\<in>Units G. a = b \<otimes> u"
   1.109    using assoc
   1.110    unfolding associated_def
   1.111 @@ -370,13 +356,12 @@
   1.112  
   1.113  lemma (in monoid) associated_sym [sym]:
   1.114    assumes "a \<sim> b"
   1.115 -    and "a \<in> carrier G"  "b \<in> carrier G"
   1.116    shows "b \<sim> a"
   1.117    using assms by (iprover intro: associatedI elim: associatedE)
   1.118  
   1.119  lemma (in monoid) associated_trans [trans]:
   1.120    assumes "a \<sim> b"  "b \<sim> c"
   1.121 -    and "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   1.122 +    and "a \<in> carrier G" "c \<in> carrier G"
   1.123    shows "a \<sim> c"
   1.124    using assms by (iprover intro: associatedI divides_trans elim: associatedE)
   1.125  
   1.126 @@ -390,93 +375,48 @@
   1.127  
   1.128  subsubsection \<open>Division and associativity\<close>
   1.129  
   1.130 -lemma divides_antisym:
   1.131 -  fixes G (structure)
   1.132 -  assumes "a divides b"  "b divides a"
   1.133 -    and "a \<in> carrier G"  "b \<in> carrier G"
   1.134 -  shows "a \<sim> b"
   1.135 -  using assms by (fast intro: associatedI)
   1.136 +lemmas divides_antisym = associatedI
   1.137  
   1.138  lemma (in monoid) divides_cong_l [trans]:
   1.139 -  assumes "x \<sim> x'"
   1.140 -    and "x' divides y"
   1.141 -    and [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   1.142 +  assumes "x \<sim> x'" "x' divides y" "x \<in> carrier G" 
   1.143    shows "x divides y"
   1.144 -proof -
   1.145 -  from assms(1) have "x divides x'" by (simp add: associatedD)
   1.146 -  also note assms(2)
   1.147 -  finally show "x divides y" by simp
   1.148 -qed
   1.149 +  by (meson assms associatedD divides_trans)
   1.150  
   1.151  lemma (in monoid) divides_cong_r [trans]:
   1.152 -  assumes "x divides y"
   1.153 -    and "y \<sim> y'"
   1.154 -    and [simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   1.155 +  assumes "x divides y" "y \<sim> y'" "x \<in> carrier G" 
   1.156    shows "x divides y'"
   1.157 -proof -
   1.158 -  note assms(1)
   1.159 -  also from assms(2) have "y divides y'" by (simp add: associatedD)
   1.160 -  finally show "x divides y'" by simp
   1.161 -qed
   1.162 +  by (meson assms associatedD divides_trans)
   1.163  
   1.164  lemma (in monoid) division_weak_partial_order [simp, intro!]:
   1.165    "weak_partial_order (division_rel G)"
   1.166    apply unfold_locales
   1.167 -        apply simp_all
   1.168 -      apply (simp add: associated_sym)
   1.169 -     apply (blast intro: associated_trans)
   1.170 -    apply (simp add: divides_antisym)
   1.171 -   apply (blast intro: divides_trans)
   1.172 -  apply (blast intro: divides_cong_l divides_cong_r associated_sym)
   1.173 -  done
   1.174 +      apply (simp_all add: associated_sym divides_antisym)
   1.175 +     apply (metis associated_trans)
   1.176 +   apply (metis divides_trans)
   1.177 +  by (meson associated_def divides_trans)
   1.178  
   1.179  
   1.180  subsubsection \<open>Multiplication and associativity\<close>
   1.181  
   1.182  lemma (in monoid_cancel) mult_cong_r:
   1.183 -  assumes "b \<sim> b'"
   1.184 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
   1.185 +  assumes "b \<sim> b'" "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
   1.186    shows "a \<otimes> b \<sim> a \<otimes> b'"
   1.187 -  using assms
   1.188 -  apply (elim associatedE2, intro associatedI2)
   1.189 -      apply (auto intro: m_assoc[symmetric])
   1.190 -  done
   1.191 +  by (meson assms associated_def divides_mult_lI)
   1.192  
   1.193  lemma (in comm_monoid_cancel) mult_cong_l:
   1.194 -  assumes "a \<sim> a'"
   1.195 -    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   1.196 +  assumes "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   1.197    shows "a \<otimes> b \<sim> a' \<otimes> b"
   1.198 -  using assms
   1.199 -  apply (elim associatedE2, intro associatedI2)
   1.200 -      apply assumption
   1.201 -     apply (simp add: m_assoc Units_closed)
   1.202 -     apply (simp add: m_comm Units_closed)
   1.203 -    apply simp_all
   1.204 -  done
   1.205 +  using assms m_comm mult_cong_r by auto
   1.206  
   1.207  lemma (in monoid_cancel) assoc_l_cancel:
   1.208 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
   1.209 -    and "a \<otimes> b \<sim> a \<otimes> b'"
   1.210 +  assumes "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G" "a \<otimes> b \<sim> a \<otimes> b'"
   1.211    shows "b \<sim> b'"
   1.212 -  using assms
   1.213 -  apply (elim associatedE2, intro associatedI2)
   1.214 -      apply assumption
   1.215 -     apply (rule l_cancel[of a])
   1.216 -        apply (simp add: m_assoc Units_closed)
   1.217 -       apply fast+
   1.218 -  done
   1.219 +  by (meson assms associated_def divides_mult_l)
   1.220  
   1.221  lemma (in comm_monoid_cancel) assoc_r_cancel:
   1.222 -  assumes "a \<otimes> b \<sim> a' \<otimes> b"
   1.223 -    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   1.224 +  assumes "a \<otimes> b \<sim> a' \<otimes> b" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   1.225    shows "a \<sim> a'"
   1.226 -  using assms
   1.227 -  apply (elim associatedE2, intro associatedI2)
   1.228 -      apply assumption
   1.229 -     apply (rule r_cancel[of a b])
   1.230 -        apply (metis Units_closed assms(3) assms(4) m_ac)
   1.231 -       apply fast+
   1.232 -  done
   1.233 +  using assms assoc_l_cancel m_comm by presburger
   1.234  
   1.235  
   1.236  subsubsection \<open>Units\<close>
   1.237 @@ -507,29 +447,23 @@
   1.238    using units by (fast intro: associatedI unit_divides)
   1.239  
   1.240  lemma (in monoid) Units_are_ones: "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"
   1.241 -  apply (simp add: set_eq_def elem_def, rule, simp_all)
   1.242 -proof clarsimp
   1.243 -  fix a
   1.244 -  assume aunit: "a \<in> Units G"
   1.245 -  show "a \<sim> \<one>"
   1.246 -    apply (rule associatedI)
   1.247 -     apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])
   1.248 -    apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])
   1.249 -    done
   1.250 -next
   1.251 -  have "\<one> \<in> Units G" by simp
   1.252 -  moreover have "\<one> \<sim> \<one>" by simp
   1.253 -  ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast
   1.254 +proof -
   1.255 +  have "a .\<in>\<^bsub>division_rel G\<^esub> {\<one>}" if "a \<in> Units G" for a
   1.256 +  proof -
   1.257 +    have "a \<sim> \<one>"
   1.258 +      by (rule associatedI) (simp_all add: Units_closed that unit_divides)
   1.259 +    then show ?thesis
   1.260 +      by (simp add: elem_def)
   1.261 +  qed
   1.262 +  moreover have "\<one> .\<in>\<^bsub>division_rel G\<^esub> Units G"
   1.263 +    by (simp add: equivalence.mem_imp_elem)
   1.264 +  ultimately show ?thesis
   1.265 +    by (auto simp: set_eq_def)
   1.266  qed
   1.267  
   1.268  lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
   1.269 -  apply (simp add: Units_def Lower_def)
   1.270 -  apply (rule, rule)
   1.271 -   apply clarsimp
   1.272 -   apply (rule unit_divides)
   1.273 -    apply (unfold Units_def, fast)
   1.274 -   apply assumption
   1.275 -  apply clarsimp
   1.276 +  apply (auto simp add: Units_def Lower_def)
   1.277 +   apply (metis Units_one_closed unit_divides unit_factor)
   1.278    apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
   1.279    done
   1.280  
   1.281 @@ -557,7 +491,7 @@
   1.282  lemma (in comm_monoid_cancel) properfactorI3:
   1.283    assumes p: "p = a \<otimes> b"
   1.284      and nunit: "b \<notin> Units G"
   1.285 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "p \<in> carrier G"
   1.286 +    and carr: "a \<in> carrier G"  "b \<in> carrier G" 
   1.287    shows "properfactor G a p"
   1.288    unfolding p
   1.289    using carr
   1.290 @@ -609,7 +543,7 @@
   1.291  
   1.292  lemma (in monoid) properfactor_trans1 [trans]:
   1.293    assumes dvds: "a divides b"  "properfactor G b c"
   1.294 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   1.295 +    and carr: "a \<in> carrier G"  "c \<in> carrier G"
   1.296    shows "properfactor G a c"
   1.297    using dvds carr
   1.298    apply (elim properfactorE, intro properfactorI)
   1.299 @@ -618,7 +552,7 @@
   1.300  
   1.301  lemma (in monoid) properfactor_trans2 [trans]:
   1.302    assumes dvds: "properfactor G a b"  "b divides c"
   1.303 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   1.304 +    and carr: "a \<in> carrier G"  "b \<in> carrier G"
   1.305    shows "properfactor G a c"
   1.306    using dvds carr
   1.307    apply (elim properfactorE, intro properfactorI)
   1.308 @@ -628,12 +562,7 @@
   1.309  lemma properfactor_lless:
   1.310    fixes G (structure)
   1.311    shows "properfactor G = lless (division_rel G)"
   1.312 -  apply (rule ext)
   1.313 -  apply (rule ext)
   1.314 -  apply rule
   1.315 -   apply (fastforce elim: properfactorE2 intro: weak_llessI)
   1.316 -  apply (fastforce elim: weak_llessE intro: properfactorI2)
   1.317 -  done
   1.318 +  by (force simp: lless_def properfactor_def associated_def)
   1.319  
   1.320  lemma (in monoid) properfactor_cong_l [trans]:
   1.321    assumes x'x: "x' \<sim> x"
   1.322 @@ -666,7 +595,7 @@
   1.323  
   1.324  lemma (in monoid_cancel) properfactor_mult_lI [intro]:
   1.325    assumes ab: "properfactor G a b"
   1.326 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   1.327 +    and carr: "a \<in> carrier G" "c \<in> carrier G"
   1.328    shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
   1.329    using ab carr by (fastforce elim: properfactorE intro: properfactorI)
   1.330  
   1.331 @@ -677,7 +606,7 @@
   1.332  
   1.333  lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
   1.334    assumes ab: "properfactor G a b"
   1.335 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   1.336 +    and carr: "a \<in> carrier G" "c \<in> carrier G"
   1.337    shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
   1.338    using ab carr by (fastforce elim: properfactorE intro: properfactorI)
   1.339  
   1.340 @@ -727,14 +656,13 @@
   1.341  
   1.342  lemma (in monoid_cancel) irreducible_cong [trans]:
   1.343    assumes irred: "irreducible G a"
   1.344 -    and aa': "a \<sim> a'"
   1.345 -    and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"
   1.346 +    and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
   1.347    shows "irreducible G a'"
   1.348    using assms
   1.349    apply (elim irreducibleE, intro irreducibleI)
   1.350     apply simp_all
   1.351     apply (metis assms(2) assms(3) assoc_unit_l)
   1.352 -  apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r)
   1.353 +  apply (metis aa' associated_sym properfactor_cong_r)
   1.354    done
   1.355  
   1.356  lemma (in monoid) irreducible_prod_rI:
   1.357 @@ -743,20 +671,16 @@
   1.358      and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   1.359    shows "irreducible G (a \<otimes> b)"
   1.360    using airr carr bunit
   1.361 -  apply (elim irreducibleE, intro irreducibleI, clarify)
   1.362 -   apply (subgoal_tac "a \<in> Units G", simp)
   1.363 -   apply (intro prod_unit_r[of a b] carr bunit, assumption)
   1.364 -  apply (metis assms(2,3) associatedI2 m_closed properfactor_cong_r)
   1.365 -  done
   1.366 +  apply (elim irreducibleE, intro irreducibleI)
   1.367 +  using prod_unit_r apply blast
   1.368 +  using associatedI2' properfactor_cong_r by auto
   1.369  
   1.370  lemma (in comm_monoid) irreducible_prod_lI:
   1.371    assumes birr: "irreducible G b"
   1.372      and aunit: "a \<in> Units G"
   1.373      and carr [simp]: "a \<in> carrier G"  "b \<in> carrier G"
   1.374    shows "irreducible G (a \<otimes> b)"
   1.375 -  apply (subst m_comm, simp+)
   1.376 -  apply (intro irreducible_prod_rI assms)
   1.377 -  done
   1.378 +  by (metis aunit birr carr irreducible_prod_rI m_comm)
   1.379  
   1.380  lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
   1.381    assumes irr: "irreducible G (a \<otimes> b)"
   1.382 @@ -834,13 +758,12 @@
   1.383  
   1.384  lemma (in monoid_cancel) prime_cong [trans]:
   1.385    assumes pprime: "prime G p"
   1.386 -    and pp': "p \<sim> p'"
   1.387 -    and carr[simp]: "p \<in> carrier G"  "p' \<in> carrier G"
   1.388 +    and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
   1.389    shows "prime G p'"
   1.390    using pprime
   1.391    apply (elim primeE, intro primeI)
   1.392     apply (metis assms(2) assms(3) assoc_unit_l)
   1.393 -  apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
   1.394 +  apply (metis pp' associated_sym divides_cong_l)
   1.395    done
   1.396  
   1.397  
   1.398 @@ -883,15 +806,11 @@
   1.399      and "set bs \<subseteq> carrier G"
   1.400    shows "bs [\<sim>] as"
   1.401    using assms
   1.402 -proof (induct as arbitrary: bs, simp)
   1.403 +proof (induction as arbitrary: bs)
   1.404    case Cons
   1.405    then show ?case
   1.406 -    apply (induct bs)
   1.407 -     apply simp
   1.408 -    apply clarsimp
   1.409 -    apply (iprover intro: associated_sym)
   1.410 -    done
   1.411 -qed
   1.412 +    by (induction bs) (use associated_sym in auto)
   1.413 +qed auto
   1.414  
   1.415  lemma (in monoid) listassoc_trans [trans]:
   1.416    assumes "as [\<sim>] bs" and "bs [\<sim>] cs"
   1.417 @@ -899,11 +818,7 @@
   1.418    shows "as [\<sim>] cs"
   1.419    using assms
   1.420    apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
   1.421 -  apply (rule associated_trans)
   1.422 -      apply (subgoal_tac "as ! i \<sim> bs ! i", assumption)
   1.423 -      apply (simp, simp)
   1.424 -    apply blast+
   1.425 -  done
   1.426 +  by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)
   1.427  
   1.428  lemma (in monoid_cancel) irrlist_listassoc_cong:
   1.429    assumes "\<forall>a\<in>set as. irreducible G a"
   1.430 @@ -932,23 +847,41 @@
   1.431    assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
   1.432    shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
   1.433    using p a
   1.434 -  apply (induct bs cs arbitrary: as, simp)
   1.435 -    apply (clarsimp simp add: list_all2_Cons2, blast)
   1.436 -   apply (clarsimp simp add: list_all2_Cons2)
   1.437 -   apply blast
   1.438 -  apply blast
   1.439 -  done
   1.440 +proof (induction bs cs arbitrary: as)
   1.441 +  case (swap y x l)
   1.442 +  then show ?case
   1.443 +    by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)
   1.444 +next
   1.445 +case (Cons xs ys z)
   1.446 +  then show ?case
   1.447 +    by (metis list_all2_Cons2 perm.Cons)
   1.448 +next
   1.449 +  case (trans xs ys zs)
   1.450 +  then show ?case
   1.451 +    by (meson perm.trans)
   1.452 +qed auto
   1.453  
   1.454  lemma (in monoid) perm_assoc_switch_r:
   1.455    assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
   1.456    shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
   1.457    using p a
   1.458 -  apply (induct as bs arbitrary: cs, simp)
   1.459 -    apply (clarsimp simp add: list_all2_Cons1, blast)
   1.460 -   apply (clarsimp simp add: list_all2_Cons1)
   1.461 -   apply blast
   1.462 -  apply blast
   1.463 -  done
   1.464 +proof (induction as bs arbitrary: cs)
   1.465 +  case Nil
   1.466 +  then show ?case
   1.467 +    by auto
   1.468 +next
   1.469 +  case (swap y x l)
   1.470 +  then show ?case
   1.471 +    by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)
   1.472 +next
   1.473 +  case (Cons xs ys z)
   1.474 +  then show ?case
   1.475 +    by (metis list_all2_Cons1 perm.Cons)
   1.476 +next
   1.477 +  case (trans xs ys zs)
   1.478 +  then show ?case
   1.479 +    by (blast intro:  elim: )
   1.480 +qed
   1.481  
   1.482  declare perm_sym [sym]
   1.483  
   1.484 @@ -1015,15 +948,13 @@
   1.485    assume "abs [\<sim>] bs" and pb: "bs <~~> bcs"
   1.486    from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
   1.487      by blast
   1.488 -
   1.489    assume "as <~~> abs"
   1.490    with p have pp: "as <~~> bs'" by fast
   1.491 -
   1.492    from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
   1.493    from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
   1.494 -  note a
   1.495 -  also assume "bcs [\<sim>] cs"
   1.496 -  finally (listassoc_trans) have "bs' [\<sim>] cs" by (simp add: c1 c2 cscarr)
   1.497 +  assume "bcs [\<sim>] cs"
   1.498 +  then have "bs' [\<sim>] cs"
   1.499 +    using a c1 c2 cscarr listassoc_trans by blast
   1.500    with pp show ?thesis
   1.501      by (rule essentially_equalI)
   1.502  qed
   1.503 @@ -1038,46 +969,46 @@
   1.504    shows "foldr (\<otimes>) fs \<one> \<in> carrier G"
   1.505    using ascarr by (induct fs) simp_all
   1.506  
   1.507 -lemma  (in comm_monoid) multlist_dividesI (*[intro]*):
   1.508 -  assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G"
   1.509 +lemma  (in comm_monoid) multlist_dividesI:
   1.510 +  assumes "f \<in> set fs" and "set fs \<subseteq> carrier G"
   1.511    shows "f divides (foldr (\<otimes>) fs \<one>)"
   1.512    using assms
   1.513 -  apply (induct fs)
   1.514 -   apply simp
   1.515 -  apply (case_tac "f = a")
   1.516 -   apply simp
   1.517 -   apply (fast intro: dividesI)
   1.518 -  apply clarsimp
   1.519 -  apply (metis assms(2) divides_prod_l multlist_closed)
   1.520 -  done
   1.521 +proof (induction fs)
   1.522 +  case (Cons a fs)
   1.523 +  then have f: "f \<in> carrier G"
   1.524 +    by blast
   1.525 +  show ?case
   1.526 +  proof (cases "f = a")
   1.527 +    case True
   1.528 +    then show ?thesis
   1.529 +      using Cons.prems by auto
   1.530 +  next
   1.531 +    case False
   1.532 +    with Cons show ?thesis
   1.533 +      by clarsimp (metis f divides_prod_l multlist_closed)
   1.534 +  qed
   1.535 +qed auto
   1.536  
   1.537  lemma (in comm_monoid_cancel) multlist_listassoc_cong:
   1.538    assumes "fs [\<sim>] fs'"
   1.539      and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
   1.540    shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
   1.541    using assms
   1.542 -proof (induct fs arbitrary: fs', simp)
   1.543 +proof (induct fs arbitrary: fs')
   1.544    case (Cons a as fs')
   1.545    then show ?case
   1.546 -    apply (induct fs', simp)
   1.547 -  proof clarsimp
   1.548 -    fix b bs
   1.549 -    assume "a \<sim> b"
   1.550 -      and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
   1.551 -      and ascarr: "set as \<subseteq> carrier G"
   1.552 +  proof (induction fs')
   1.553 +    case (Cons b bs)
   1.554      then have p: "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) as \<one>"
   1.555 -      by (fast intro: mult_cong_l)
   1.556 -    also
   1.557 -    assume "as [\<sim>] bs"
   1.558 -      and bscarr: "set bs \<subseteq> carrier G"
   1.559 -      and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) fs' \<one>"
   1.560 -    then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by simp
   1.561 -    with ascarr bscarr bcarr have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
   1.562 -      by (fast intro: mult_cong_r)
   1.563 -    finally show "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
   1.564 -      by (simp add: ascarr bscarr acarr bcarr)
   1.565 -  qed
   1.566 -qed
   1.567 +      by (simp add: mult_cong_l)
   1.568 +    then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>"
   1.569 +      using Cons by auto
   1.570 +    with Cons have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
   1.571 +      by (simp add: mult_cong_r)
   1.572 +    then show ?case
   1.573 +      using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force
   1.574 +  qed auto
   1.575 +qed auto
   1.576  
   1.577  lemma (in comm_monoid) multlist_perm_cong:
   1.578    assumes prm: "as <~~> bs"
   1.579 @@ -1197,14 +1128,14 @@
   1.580      and asc: "fs [\<sim>] fs'"
   1.581      and carr: "a \<in> carrier G"  "set fs \<subseteq> carrier G"  "set fs' \<subseteq> carrier G"
   1.582    shows "wfactors G fs' a"
   1.583 +proof -
   1.584 +  { from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"
   1.585 +      by (simp add: multlist_listassoc_cong carr)
   1.586 +    also assume "foldr (\<otimes>) fs \<one> \<sim> a"
   1.587 +    finally have "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr) }
   1.588 +  then show ?thesis
   1.589    using fact
   1.590 -  apply (elim wfactorsE, intro wfactorsI)
   1.591 -   apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
   1.592 -proof -
   1.593 -  from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"
   1.594 -    by (simp add: multlist_listassoc_cong carr)
   1.595 -  also assume "foldr (\<otimes>) fs \<one> \<sim> a"
   1.596 -  finally show "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr)
   1.597 +  by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)
   1.598  qed
   1.599  
   1.600  lemma (in comm_monoid) wfactors_perm_cong_l:
   1.601 @@ -1212,11 +1143,7 @@
   1.602      and "fs <~~> fs'"
   1.603      and "set fs \<subseteq> carrier G"
   1.604    shows "wfactors G fs' a"
   1.605 -  using assms
   1.606 -  apply (elim wfactorsE, intro wfactorsI)
   1.607 -   apply (rule irrlist_perm_cong, assumption+)
   1.608 -  apply (simp add: multlist_perm_cong[symmetric])
   1.609 -  done
   1.610 +  using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce
   1.611  
   1.612  lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
   1.613    assumes ee: "essentially_equal G as bs"
   1.614 @@ -1255,28 +1182,40 @@
   1.615      and carr: "set as \<subseteq> carrier G"
   1.616    shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as"
   1.617      (is "essentially_equal G ?as' as")
   1.618 -  using assms
   1.619 -  apply (intro essentially_equalI[of _ ?as'], simp)
   1.620 -  apply (cases as, simp)
   1.621 -  apply (clarsimp, fast intro: associatedI2[of u])
   1.622 -  done
   1.623 +proof -
   1.624 +  have "as[0 := as ! 0 \<otimes> u] [\<sim>] as"
   1.625 +  proof (cases as)
   1.626 +    case (Cons a as')
   1.627 +    then show ?thesis
   1.628 +      using associatedI2 carr uunit by auto
   1.629 +  qed auto
   1.630 +  then show ?thesis
   1.631 +    using essentially_equal_def by blast
   1.632 +qed
   1.633  
   1.634  lemma (in comm_monoid_cancel) factors_cong_unit:
   1.635 -  assumes uunit: "u \<in> Units G"
   1.636 -    and anunit: "a \<notin> Units G"
   1.637 +  assumes u: "u \<in> Units G"
   1.638 +    and a: "a \<notin> Units G"
   1.639      and afs: "factors G as a"
   1.640      and ascarr: "set as \<subseteq> carrier G"
   1.641    shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)"
   1.642      (is "factors G ?as' ?a'")
   1.643 -  using assms
   1.644 -  apply (elim factorsE, clarify)
   1.645 -  apply (cases as)
   1.646 -   apply (simp add: nunit_factors)
   1.647 -  apply clarsimp
   1.648 -  apply (elim factorsE, intro factorsI)
   1.649 -   apply (clarsimp, fast intro: irreducible_prod_rI)
   1.650 -  apply (simp add: m_ac Units_closed)
   1.651 -  done
   1.652 +proof (cases as)
   1.653 +  case Nil
   1.654 +  then show ?thesis
   1.655 +    using afs a nunit_factors by auto
   1.656 +next
   1.657 +  case (Cons b bs)
   1.658 +  have *: "\<forall>f\<in>set as. irreducible G f" "foldr (\<otimes>) as \<one> = a"
   1.659 +    using afs  by (auto simp: factors_def)
   1.660 +  show ?thesis
   1.661 +  proof (intro factorsI)
   1.662 +    show "foldr (\<otimes>) (as[0 := as ! 0 \<otimes> u]) \<one> = a \<otimes> u"
   1.663 +      using Cons u ascarr * by (auto simp add: m_ac Units_closed)
   1.664 +    show "\<forall>f\<in>set (as[0 := as ! 0 \<otimes> u]). irreducible G f"
   1.665 +      using Cons u ascarr * by (force intro: irreducible_prod_rI)
   1.666 +  qed 
   1.667 +qed
   1.668  
   1.669  lemma (in comm_monoid) perm_wfactorsD:
   1.670    assumes prm: "as <~~> bs"
   1.671 @@ -1289,7 +1228,8 @@
   1.672  proof (elim wfactorsE)
   1.673    from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)
   1.674    assume "foldr (\<otimes>) as \<one> \<sim> a"
   1.675 -  then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)
   1.676 +  then have "a \<sim> foldr (\<otimes>) as \<one>"
   1.677 +    by (simp add: associated_sym)
   1.678    also from prm
   1.679    have "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>" by (rule multlist_perm_cong, simp)
   1.680    also assume "foldr (\<otimes>) bs \<one> \<sim> b"
   1.681 @@ -1306,7 +1246,7 @@
   1.682    using afs bfs
   1.683  proof (elim wfactorsE)
   1.684    assume "foldr (\<otimes>) as \<one> \<sim> a"
   1.685 -  then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)
   1.686 +  then have "a \<sim> foldr (\<otimes>) as \<one>" by (simp add: associated_sym)
   1.687    also from assoc
   1.688    have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by (rule multlist_listassoc_cong, simp+)
   1.689    also assume "foldr (\<otimes>) bs \<one> \<sim> b"