src/HOL/Number_Theory/MiscAlgebra.thy
 author wenzelm Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) changeset 53374 a14d2a854c02 parent 44890 22f665a2e91c child 55322 3bf50e3cd727 permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
 wenzelm@41959 ` 1` ```(* Title: HOL/Number_Theory/MiscAlgebra.thy ``` nipkow@31719 ` 2` ``` Author: Jeremy Avigad ``` nipkow@31719 ` 3` haftmann@31772 ` 4` ```These are things that can be added to the Algebra library. ``` nipkow@31719 ` 5` ```*) ``` nipkow@31719 ` 6` nipkow@31719 ` 7` ```theory MiscAlgebra ``` haftmann@31772 ` 8` ```imports ``` nipkow@31719 ` 9` ``` "~~/src/HOL/Algebra/Ring" ``` nipkow@31719 ` 10` ``` "~~/src/HOL/Algebra/FiniteProduct" ``` haftmann@44106 ` 11` ```begin ``` nipkow@31719 ` 12` nipkow@31719 ` 13` ```(* finiteness stuff *) ``` nipkow@31719 ` 14` wenzelm@44872 ` 15` ```lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}" ``` nipkow@31719 ` 16` ``` apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<.. 'a monoid" where ``` nipkow@31719 ` 35` ``` "units_of G == (| carrier = Units G, ``` nipkow@31719 ` 36` ``` Group.monoid.mult = Group.monoid.mult G, ``` haftmann@44106 ` 37` ``` one = one G |)" ``` nipkow@31719 ` 38` nipkow@31719 ` 39` ```(* ``` nipkow@31719 ` 40` nipkow@31719 ` 41` ```lemma (in monoid) Units_mult_closed [intro]: ``` nipkow@31719 ` 42` ``` "x : Units G ==> y : Units G ==> x \ y : Units G" ``` nipkow@31719 ` 43` ``` apply (unfold Units_def) ``` nipkow@31719 ` 44` ``` apply (clarsimp) ``` nipkow@31719 ` 45` ``` apply (rule_tac x = "xaa \ xa" in bexI) ``` nipkow@31719 ` 46` ``` apply auto ``` nipkow@31719 ` 47` ``` apply (subst m_assoc) ``` nipkow@31719 ` 48` ``` apply auto ``` nipkow@31719 ` 49` ``` apply (subst (2) m_assoc [symmetric]) ``` nipkow@31719 ` 50` ``` apply auto ``` nipkow@31719 ` 51` ``` apply (subst m_assoc) ``` nipkow@31719 ` 52` ``` apply auto ``` nipkow@31719 ` 53` ``` apply (subst (2) m_assoc [symmetric]) ``` nipkow@31719 ` 54` ``` apply auto ``` nipkow@31719 ` 55` ```done ``` nipkow@31719 ` 56` nipkow@31719 ` 57` ```*) ``` nipkow@31719 ` 58` nipkow@31719 ` 59` ```lemma (in monoid) units_group: "group(units_of G)" ``` nipkow@31719 ` 60` ``` apply (unfold units_of_def) ``` nipkow@31719 ` 61` ``` apply (rule groupI) ``` nipkow@31719 ` 62` ``` apply auto ``` nipkow@31719 ` 63` ``` apply (subst m_assoc) ``` nipkow@31719 ` 64` ``` apply auto ``` nipkow@31719 ` 65` ``` apply (rule_tac x = "inv x" in bexI) ``` nipkow@31719 ` 66` ``` apply auto ``` wenzelm@44872 ` 67` ``` done ``` nipkow@31719 ` 68` nipkow@31719 ` 69` ```lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)" ``` nipkow@31719 ` 70` ``` apply (rule group.group_comm_groupI) ``` nipkow@31719 ` 71` ``` apply (rule units_group) ``` wenzelm@41541 ` 72` ``` apply (insert comm_monoid_axioms) ``` nipkow@31719 ` 73` ``` apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) ``` wenzelm@41541 ` 74` ``` apply auto ``` wenzelm@41541 ` 75` ``` done ``` nipkow@31719 ` 76` nipkow@31719 ` 77` ```lemma units_of_carrier: "carrier (units_of G) = Units G" ``` wenzelm@44872 ` 78` ``` unfolding units_of_def by auto ``` nipkow@31719 ` 79` nipkow@31719 ` 80` ```lemma units_of_mult: "mult(units_of G) = mult G" ``` wenzelm@44872 ` 81` ``` unfolding units_of_def by auto ``` nipkow@31719 ` 82` nipkow@31719 ` 83` ```lemma units_of_one: "one(units_of G) = one G" ``` wenzelm@44872 ` 84` ``` unfolding units_of_def by auto ``` nipkow@31719 ` 85` wenzelm@44872 ` 86` ```lemma (in monoid) units_of_inv: "x : Units G ==> ``` nipkow@31719 ` 87` ``` m_inv (units_of G) x = m_inv G x" ``` nipkow@31719 ` 88` ``` apply (rule sym) ``` nipkow@31719 ` 89` ``` apply (subst m_inv_def) ``` nipkow@31719 ` 90` ``` apply (rule the1_equality) ``` nipkow@31719 ` 91` ``` apply (rule ex_ex1I) ``` nipkow@31719 ` 92` ``` apply (subst (asm) Units_def) ``` nipkow@31719 ` 93` ``` apply auto ``` nipkow@31719 ` 94` ``` apply (erule inv_unique) ``` nipkow@31719 ` 95` ``` apply auto ``` nipkow@31719 ` 96` ``` apply (rule Units_closed) ``` nipkow@31719 ` 97` ``` apply (simp_all only: units_of_carrier [symmetric]) ``` nipkow@31719 ` 98` ``` apply (insert units_group) ``` nipkow@31719 ` 99` ``` apply auto ``` nipkow@31719 ` 100` ``` apply (subst units_of_mult [symmetric]) ``` nipkow@31719 ` 101` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 102` ``` apply (erule group.r_inv, assumption) ``` nipkow@31719 ` 103` ``` apply (subst units_of_mult [symmetric]) ``` nipkow@31719 ` 104` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 105` ``` apply (erule group.l_inv, assumption) ``` nipkow@31719 ` 106` ```done ``` nipkow@31719 ` 107` wenzelm@44872 ` 108` ```lemma (in group) inj_on_const_mult: "a: (carrier G) ==> ``` nipkow@31719 ` 109` ``` inj_on (%x. a \ x) (carrier G)" ``` wenzelm@44872 ` 110` ``` unfolding inj_on_def by auto ``` nipkow@31719 ` 111` nipkow@31719 ` 112` ```lemma (in group) surj_const_mult: "a : (carrier G) ==> ``` wenzelm@44872 ` 113` ``` (%x. a \ x) ` (carrier G) = (carrier G)" ``` nipkow@31719 ` 114` ``` apply (auto simp add: image_def) ``` nipkow@31719 ` 115` ``` apply (rule_tac x = "(m_inv G a) \ x" in bexI) ``` nipkow@31719 ` 116` ``` apply auto ``` nipkow@31719 ` 117` ```(* auto should get this. I suppose we need "comm_monoid_simprules" ``` nipkow@31719 ` 118` ``` for mult_ac rewriting. *) ``` nipkow@31719 ` 119` ``` apply (subst m_assoc [symmetric]) ``` nipkow@31719 ` 120` ``` apply auto ``` wenzelm@44872 ` 121` ``` done ``` nipkow@31719 ` 122` nipkow@31719 ` 123` ```lemma (in group) l_cancel_one [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 124` ``` (x \ a = x) = (a = one G)" ``` nipkow@31719 ` 125` ``` apply auto ``` nipkow@31719 ` 126` ``` apply (subst l_cancel [symmetric]) ``` nipkow@31719 ` 127` ``` prefer 4 ``` nipkow@31719 ` 128` ``` apply (erule ssubst) ``` nipkow@31719 ` 129` ``` apply auto ``` wenzelm@44872 ` 130` ``` done ``` nipkow@31719 ` 131` nipkow@31719 ` 132` ```lemma (in group) r_cancel_one [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 133` ``` (a \ x = x) = (a = one G)" ``` nipkow@31719 ` 134` ``` apply auto ``` nipkow@31719 ` 135` ``` apply (subst r_cancel [symmetric]) ``` nipkow@31719 ` 136` ``` prefer 4 ``` nipkow@31719 ` 137` ``` apply (erule ssubst) ``` nipkow@31719 ` 138` ``` apply auto ``` wenzelm@44872 ` 139` ``` done ``` nipkow@31719 ` 140` nipkow@31719 ` 141` ```(* Is there a better way to do this? *) ``` nipkow@31719 ` 142` nipkow@31719 ` 143` ```lemma (in group) l_cancel_one' [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 144` ``` (x = x \ a) = (a = one G)" ``` wenzelm@44872 ` 145` ``` apply (subst eq_commute) ``` wenzelm@44872 ` 146` ``` apply simp ``` wenzelm@44872 ` 147` ``` done ``` nipkow@31719 ` 148` nipkow@31719 ` 149` ```lemma (in group) r_cancel_one' [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 150` ``` (x = a \ x) = (a = one G)" ``` wenzelm@44872 ` 151` ``` apply (subst eq_commute) ``` wenzelm@44872 ` 152` ``` apply simp ``` wenzelm@44872 ` 153` ``` done ``` nipkow@31719 ` 154` nipkow@31719 ` 155` ```(* This should be generalized to arbitrary groups, not just commutative ``` nipkow@31719 ` 156` ``` ones, using Lagrange's theorem. *) ``` nipkow@31719 ` 157` nipkow@31719 ` 158` ```lemma (in comm_group) power_order_eq_one: ``` wenzelm@44872 ` 159` ``` assumes fin [simp]: "finite (carrier G)" ``` wenzelm@44872 ` 160` ``` and a [simp]: "a : carrier G" ``` wenzelm@44872 ` 161` ``` shows "a (^) card(carrier G) = one G" ``` nipkow@31719 ` 162` ```proof - ``` nipkow@31719 ` 163` ``` have "(\x:carrier G. x) = (\x:carrier G. a \ x)" ``` wenzelm@44872 ` 164` ``` by (subst (2) finprod_reindex [symmetric], ``` nipkow@31719 ` 165` ``` auto simp add: Pi_def inj_on_const_mult surj_const_mult) ``` nipkow@31719 ` 166` ``` also have "\ = (\x:carrier G. a) \ (\x:carrier G. x)" ``` nipkow@31719 ` 167` ``` by (auto simp add: finprod_multf Pi_def) ``` nipkow@31719 ` 168` ``` also have "(\x:carrier G. a) = a (^) card(carrier G)" ``` nipkow@31719 ` 169` ``` by (auto simp add: finprod_const) ``` nipkow@31719 ` 170` ``` finally show ?thesis ``` nipkow@31719 ` 171` ```(* uses the preceeding lemma *) ``` nipkow@31719 ` 172` ``` by auto ``` nipkow@31719 ` 173` ```qed ``` nipkow@31719 ` 174` nipkow@31719 ` 175` nipkow@31719 ` 176` ```(* Miscellaneous *) ``` nipkow@31719 ` 177` nipkow@31719 ` 178` ```lemma (in cring) field_intro2: "\\<^bsub>R\<^esub> ~= \\<^bsub>R\<^esub> \ ALL x : carrier R - {\\<^bsub>R\<^esub>}. ``` nipkow@31719 ` 179` ``` x : Units R \ field R" ``` nipkow@31719 ` 180` ``` apply (unfold_locales) ``` wenzelm@41541 ` 181` ``` apply (insert cring_axioms, auto) ``` nipkow@31719 ` 182` ``` apply (rule trans) ``` nipkow@31719 ` 183` ``` apply (subgoal_tac "a = (a \ b) \ inv b") ``` nipkow@31719 ` 184` ``` apply assumption ``` wenzelm@44872 ` 185` ``` apply (subst m_assoc) ``` wenzelm@41541 ` 186` ``` apply auto ``` nipkow@31719 ` 187` ``` apply (unfold Units_def) ``` nipkow@31719 ` 188` ``` apply auto ``` wenzelm@41541 ` 189` ``` done ``` nipkow@31719 ` 190` nipkow@31719 ` 191` ```lemma (in monoid) inv_char: "x : carrier G \ y : carrier G \ ``` wenzelm@41541 ` 192` ``` x \ y = \ \ y \ x = \ \ inv x = y" ``` nipkow@31719 ` 193` ``` apply (subgoal_tac "x : Units G") ``` nipkow@31719 ` 194` ``` apply (subgoal_tac "y = inv x \ \") ``` nipkow@31719 ` 195` ``` apply simp ``` nipkow@31719 ` 196` ``` apply (erule subst) ``` nipkow@31719 ` 197` ``` apply (subst m_assoc [symmetric]) ``` nipkow@31719 ` 198` ``` apply auto ``` nipkow@31719 ` 199` ``` apply (unfold Units_def) ``` nipkow@31719 ` 200` ``` apply auto ``` wenzelm@41541 ` 201` ``` done ``` nipkow@31719 ` 202` nipkow@31719 ` 203` ```lemma (in comm_monoid) comm_inv_char: "x : carrier G \ y : carrier G \ ``` nipkow@31719 ` 204` ``` x \ y = \ \ inv x = y" ``` nipkow@31719 ` 205` ``` apply (rule inv_char) ``` nipkow@31719 ` 206` ``` apply auto ``` wenzelm@44872 ` 207` ``` apply (subst m_comm, auto) ``` wenzelm@41541 ` 208` ``` done ``` nipkow@31719 ` 209` wenzelm@44872 ` 210` ```lemma (in ring) inv_neg_one [simp]: "inv (\ \) = \ \" ``` nipkow@31719 ` 211` ``` apply (rule inv_char) ``` nipkow@31719 ` 212` ``` apply (auto simp add: l_minus r_minus) ``` wenzelm@41541 ` 213` ``` done ``` nipkow@31719 ` 214` wenzelm@44872 ` 215` ```lemma (in monoid) inv_eq_imp_eq: "x : Units G \ y : Units G \ ``` nipkow@31719 ` 216` ``` inv x = inv y \ x = y" ``` nipkow@31719 ` 217` ``` apply (subgoal_tac "inv(inv x) = inv(inv y)") ``` nipkow@31719 ` 218` ``` apply (subst (asm) Units_inv_inv)+ ``` nipkow@31719 ` 219` ``` apply auto ``` wenzelm@44872 ` 220` ``` done ``` nipkow@31719 ` 221` nipkow@31719 ` 222` ```lemma (in ring) Units_minus_one_closed [intro]: "\ \ : Units R" ``` nipkow@31719 ` 223` ``` apply (unfold Units_def) ``` nipkow@31719 ` 224` ``` apply auto ``` nipkow@31719 ` 225` ``` apply (rule_tac x = "\ \" in bexI) ``` nipkow@31719 ` 226` ``` apply auto ``` nipkow@31719 ` 227` ``` apply (simp add: l_minus r_minus) ``` wenzelm@44872 ` 228` ``` done ``` nipkow@31719 ` 229` nipkow@31719 ` 230` ```lemma (in monoid) inv_one [simp]: "inv \ = \" ``` nipkow@31719 ` 231` ``` apply (rule inv_char) ``` nipkow@31719 ` 232` ``` apply auto ``` wenzelm@44872 ` 233` ``` done ``` nipkow@31719 ` 234` nipkow@31719 ` 235` ```lemma (in ring) inv_eq_neg_one_eq: "x : Units R \ (inv x = \ \) = (x = \ \)" ``` nipkow@31719 ` 236` ``` apply auto ``` nipkow@31719 ` 237` ``` apply (subst Units_inv_inv [symmetric]) ``` nipkow@31719 ` 238` ``` apply auto ``` wenzelm@44872 ` 239` ``` done ``` nipkow@31719 ` 240` nipkow@31719 ` 241` ```lemma (in monoid) inv_eq_one_eq: "x : Units G \ (inv x = \) = (x = \)" ``` nipkow@31719 ` 242` ``` apply auto ``` nipkow@31719 ` 243` ``` apply (subst Units_inv_inv [symmetric]) ``` nipkow@31719 ` 244` ``` apply auto ``` wenzelm@44872 ` 245` ``` done ``` nipkow@31719 ` 246` nipkow@31719 ` 247` nipkow@31719 ` 248` ```(* This goes in FiniteProduct *) ``` nipkow@31719 ` 249` nipkow@31719 ` 250` ```lemma (in comm_monoid) finprod_UN_disjoint: ``` nipkow@31719 ` 251` ``` "finite I \ (ALL i:I. finite (A i)) \ (ALL i:I. ALL j:I. i ~= j \ ``` nipkow@31719 ` 252` ``` (A i) Int (A j) = {}) \ ``` nipkow@31719 ` 253` ``` (ALL i:I. ALL x: (A i). g x : carrier G) \ ``` nipkow@31719 ` 254` ``` finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I" ``` nipkow@31719 ` 255` ``` apply (induct set: finite) ``` nipkow@31719 ` 256` ``` apply force ``` nipkow@31719 ` 257` ``` apply clarsimp ``` nipkow@31719 ` 258` ``` apply (subst finprod_Un_disjoint) ``` nipkow@31719 ` 259` ``` apply blast ``` nipkow@31719 ` 260` ``` apply (erule finite_UN_I) ``` nipkow@31719 ` 261` ``` apply blast ``` nipkow@44890 ` 262` ``` apply (fastforce) ``` wenzelm@44872 ` 263` ``` apply (auto intro!: funcsetI finprod_closed) ``` wenzelm@44872 ` 264` ``` done ``` nipkow@31719 ` 265` nipkow@31719 ` 266` ```lemma (in comm_monoid) finprod_Union_disjoint: ``` nipkow@31719 ` 267` ``` "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G)); ``` wenzelm@44872 ` 268` ``` (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] ``` wenzelm@44872 ` 269` ``` ==> finprod G f (Union C) = finprod G (finprod G f) C" ``` nipkow@31719 ` 270` ``` apply (frule finprod_UN_disjoint [of C id f]) ``` haftmann@44106 ` 271` ``` apply (auto simp add: SUP_def) ``` wenzelm@44872 ` 272` ``` done ``` nipkow@31719 ` 273` wenzelm@44872 ` 274` ```lemma (in comm_monoid) finprod_one: ``` wenzelm@44872 ` 275` ``` "finite A \ (\x. x:A \ f x = \) \ finprod G f A = \" ``` wenzelm@44872 ` 276` ``` by (induct set: finite) auto ``` nipkow@31719 ` 277` nipkow@31719 ` 278` nipkow@31719 ` 279` ```(* need better simplification rules for rings *) ``` nipkow@31719 ` 280` ```(* the next one holds more generally for abelian groups *) ``` nipkow@31719 ` 281` nipkow@31719 ` 282` ```lemma (in cring) sum_zero_eq_neg: ``` wenzelm@44872 ` 283` ``` "x : carrier R \ y : carrier R \ x \ y = \ \ x = \ y" ``` wenzelm@44872 ` 284` ``` apply (subgoal_tac "\ y = \ \ \ y") ``` nipkow@31719 ` 285` ``` apply (erule ssubst)back ``` nipkow@31719 ` 286` ``` apply (erule subst) ``` wenzelm@41541 ` 287` ``` apply (simp_all add: ring_simprules) ``` wenzelm@41541 ` 288` ``` done ``` nipkow@31719 ` 289` nipkow@31719 ` 290` ```(* there's a name conflict -- maybe "domain" should be ``` nipkow@31719 ` 291` ``` "integral_domain" *) ``` nipkow@31719 ` 292` wenzelm@44872 ` 293` ```lemma (in Ring.domain) square_eq_one: ``` nipkow@31719 ` 294` ``` fixes x ``` nipkow@31719 ` 295` ``` assumes [simp]: "x : carrier R" and ``` nipkow@31719 ` 296` ``` "x \ x = \" ``` nipkow@31719 ` 297` ``` shows "x = \ | x = \\" ``` nipkow@31719 ` 298` ```proof - ``` nipkow@31719 ` 299` ``` have "(x \ \) \ (x \ \ \) = x \ x \ \ \" ``` nipkow@31719 ` 300` ``` by (simp add: ring_simprules) ``` wenzelm@53374 ` 301` ``` also from `x \ x = \` have "\ = \" ``` nipkow@31719 ` 302` ``` by (simp add: ring_simprules) ``` nipkow@31719 ` 303` ``` finally have "(x \ \) \ (x \ \ \) = \" . ``` wenzelm@44872 ` 304` ``` then have "(x \ \) = \ | (x \ \ \) = \" ``` nipkow@31719 ` 305` ``` by (intro integral, auto) ``` wenzelm@44872 ` 306` ``` then show ?thesis ``` nipkow@31719 ` 307` ``` apply auto ``` nipkow@31719 ` 308` ``` apply (erule notE) ``` nipkow@31719 ` 309` ``` apply (rule sum_zero_eq_neg) ``` nipkow@31719 ` 310` ``` apply auto ``` nipkow@31719 ` 311` ``` apply (subgoal_tac "x = \ (\ \)") ``` wenzelm@44872 ` 312` ``` apply (simp add: ring_simprules) ``` nipkow@31719 ` 313` ``` apply (rule sum_zero_eq_neg) ``` nipkow@31719 ` 314` ``` apply auto ``` nipkow@31719 ` 315` ``` done ``` nipkow@31719 ` 316` ```qed ``` nipkow@31719 ` 317` nipkow@31719 ` 318` ```lemma (in Ring.domain) inv_eq_self: "x : Units R \ ``` nipkow@31719 ` 319` ``` x = inv x \ x = \ | x = \ \" ``` nipkow@31719 ` 320` ``` apply (rule square_eq_one) ``` nipkow@31719 ` 321` ``` apply auto ``` nipkow@31719 ` 322` ``` apply (erule ssubst)back ``` nipkow@31719 ` 323` ``` apply (erule Units_r_inv) ``` wenzelm@44872 ` 324` ``` done ``` nipkow@31719 ` 325` nipkow@31719 ` 326` nipkow@31719 ` 327` ```(* ``` nipkow@31719 ` 328` ``` The following translates theorems about groups to the facts about ``` nipkow@31719 ` 329` ``` the units of a ring. (The list should be expanded as more things are ``` nipkow@31719 ` 330` ``` needed.) ``` nipkow@31719 ` 331` ```*) ``` nipkow@31719 ` 332` wenzelm@44872 ` 333` ```lemma (in ring) finite_ring_finite_units [intro]: ``` wenzelm@44872 ` 334` ``` "finite (carrier R) \ finite (Units R)" ``` wenzelm@44872 ` 335` ``` by (rule finite_subset) auto ``` nipkow@31719 ` 336` nipkow@31719 ` 337` ```(* this belongs with MiscAlgebra.thy *) ``` wenzelm@44872 ` 338` ```lemma (in monoid) units_of_pow: ``` nipkow@31719 ` 339` ``` "x : Units G \ x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n" ``` nipkow@31719 ` 340` ``` apply (induct n) ``` wenzelm@44872 ` 341` ``` apply (auto simp add: units_group group.is_monoid ``` wenzelm@41541 ` 342` ``` monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult) ``` wenzelm@41541 ` 343` ``` done ``` nipkow@31719 ` 344` nipkow@31719 ` 345` ```lemma (in cring) units_power_order_eq_one: "finite (Units R) \ a : Units R ``` nipkow@31719 ` 346` ``` \ a (^) card(Units R) = \" ``` nipkow@31719 ` 347` ``` apply (subst units_of_carrier [symmetric]) ``` nipkow@31719 ` 348` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 349` ``` apply (subst units_of_pow [symmetric]) ``` nipkow@31719 ` 350` ``` apply assumption ``` nipkow@31719 ` 351` ``` apply (rule comm_group.power_order_eq_one) ``` nipkow@31719 ` 352` ``` apply (rule units_comm_group) ``` nipkow@31719 ` 353` ``` apply (unfold units_of_def, auto) ``` wenzelm@41541 ` 354` ``` done ``` nipkow@31719 ` 355` nipkow@31719 ` 356` ```end ```