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"
```