src/HOL/NewNumberTheory/MiscAlgebra.thy
author nipkow
Fri Jun 19 18:33:10 2009 +0200 (2009-06-19)
changeset 31719 29f5b20e8ee8
child 31721 b03270a8c23f
permissions -rw-r--r--
Added NewNumberTheory by Jeremy Avigad
nipkow@31719
     1
(*  Title:      MiscAlgebra.thy
nipkow@31719
     2
    ID:         
nipkow@31719
     3
    Author:     Jeremy Avigad
nipkow@31719
     4
nipkow@31719
     5
    These are things that can be added to the Algebra library,
nipkow@31719
     6
    as well as a few things that could possibly go in Main. 
nipkow@31719
     7
*)
nipkow@31719
     8
nipkow@31719
     9
theory MiscAlgebra
nipkow@31719
    10
imports 
nipkow@31719
    11
  "~~/src/HOL/Algebra/Ring"
nipkow@31719
    12
  "~~/src/HOL/Algebra/FiniteProduct"
nipkow@31719
    13
begin;
nipkow@31719
    14
nipkow@31719
    15
declare One_nat_def [simp del] 
nipkow@31719
    16
nipkow@31719
    17
nipkow@31719
    18
(* Some things for Main? *)
nipkow@31719
    19
nipkow@31719
    20
(* finiteness stuff *)
nipkow@31719
    21
nipkow@31719
    22
lemma int_bounded_set1 [intro]: "finite {(x::int). a < x & x < b & P x}" 
nipkow@31719
    23
  apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
nipkow@31719
    24
  apply (erule finite_subset)
nipkow@31719
    25
  apply auto
nipkow@31719
    26
done
nipkow@31719
    27
nipkow@31719
    28
lemma image_set_eq_image: "{ f x | x. P x} = f ` { x. P x}"
nipkow@31719
    29
  unfolding image_def apply auto
nipkow@31719
    30
done
nipkow@31719
    31
nipkow@31719
    32
lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow> 
nipkow@31719
    33
    finite { f x | x. P x}"
nipkow@31719
    34
  apply (subst image_set_eq_image)
nipkow@31719
    35
  apply auto
nipkow@31719
    36
done
nipkow@31719
    37
nipkow@31719
    38
(* Examples:
nipkow@31719
    39
nipkow@31719
    40
lemma "finite {x. 0 < x & x < 100 & prime (x::int)}"
nipkow@31719
    41
  by auto
nipkow@31719
    42
nipkow@31719
    43
lemma "finite { 3 * x | x. 0 < x & x < 100 & prime (x::int) }"
nipkow@31719
    44
  by auto
nipkow@31719
    45
nipkow@31719
    46
*)
nipkow@31719
    47
nipkow@31719
    48
(* This could go in Set.thy *)
nipkow@31719
    49
nipkow@31719
    50
lemma UNION_empty: "(UNION F A = {}) = (ALL x: F. (A x) = {})"
nipkow@31719
    51
  by auto
nipkow@31719
    52
nipkow@31719
    53
nipkow@31719
    54
(* The rest is for the algebra libraries *)
nipkow@31719
    55
nipkow@31719
    56
(* This goes in FuncSet.thy. Any reason not to make it a simp rule? *)
nipkow@31719
    57
nipkow@31719
    58
lemma funcset_id [simp]: "(%x. x): A \<rightarrow> A"
nipkow@31719
    59
  by (auto simp add: Pi_def);
nipkow@31719
    60
nipkow@31719
    61
(* These go in Group.thy. *)
nipkow@31719
    62
nipkow@31719
    63
(*
nipkow@31719
    64
  Show that the units in any monoid give rise to a group.
nipkow@31719
    65
nipkow@31719
    66
  The file Residues.thy provides some infrastructure to use
nipkow@31719
    67
  facts about the unit group within the ring locale.
nipkow@31719
    68
*)
nipkow@31719
    69
nipkow@31719
    70
nipkow@31719
    71
constdefs 
nipkow@31719
    72
  units_of :: "('a, 'b) monoid_scheme => 'a monoid"
nipkow@31719
    73
  "units_of G == (| carrier = Units G,
nipkow@31719
    74
     Group.monoid.mult = Group.monoid.mult G,
nipkow@31719
    75
     one  = one G |)";
nipkow@31719
    76
nipkow@31719
    77
(*
nipkow@31719
    78
nipkow@31719
    79
lemma (in monoid) Units_mult_closed [intro]:
nipkow@31719
    80
  "x : Units G ==> y : Units G ==> x \<otimes> y : Units G"
nipkow@31719
    81
  apply (unfold Units_def)
nipkow@31719
    82
  apply (clarsimp)
nipkow@31719
    83
  apply (rule_tac x = "xaa \<otimes> xa" in bexI)
nipkow@31719
    84
  apply auto
nipkow@31719
    85
  apply (subst m_assoc)
nipkow@31719
    86
  apply auto
nipkow@31719
    87
  apply (subst (2) m_assoc [symmetric])
nipkow@31719
    88
  apply auto
nipkow@31719
    89
  apply (subst m_assoc)
nipkow@31719
    90
  apply auto
nipkow@31719
    91
  apply (subst (2) m_assoc [symmetric])
nipkow@31719
    92
  apply auto
nipkow@31719
    93
done
nipkow@31719
    94
nipkow@31719
    95
*)
nipkow@31719
    96
nipkow@31719
    97
lemma (in monoid) units_group: "group(units_of G)"
nipkow@31719
    98
  apply (unfold units_of_def)
nipkow@31719
    99
  apply (rule groupI)
nipkow@31719
   100
  apply auto
nipkow@31719
   101
  apply (subst m_assoc)
nipkow@31719
   102
  apply auto
nipkow@31719
   103
  apply (rule_tac x = "inv x" in bexI)
nipkow@31719
   104
  apply auto
nipkow@31719
   105
done
nipkow@31719
   106
nipkow@31719
   107
lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
nipkow@31719
   108
  apply (rule group.group_comm_groupI)
nipkow@31719
   109
  apply (rule units_group)
nipkow@31719
   110
  apply (insert prems)
nipkow@31719
   111
  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
nipkow@31719
   112
  apply auto;
nipkow@31719
   113
done;
nipkow@31719
   114
nipkow@31719
   115
lemma units_of_carrier: "carrier (units_of G) = Units G"
nipkow@31719
   116
  by (unfold units_of_def, auto)
nipkow@31719
   117
nipkow@31719
   118
lemma units_of_mult: "mult(units_of G) = mult G"
nipkow@31719
   119
  by (unfold units_of_def, auto)
nipkow@31719
   120
nipkow@31719
   121
lemma units_of_one: "one(units_of G) = one G"
nipkow@31719
   122
  by (unfold units_of_def, auto)
nipkow@31719
   123
nipkow@31719
   124
lemma (in monoid) units_of_inv: "x : Units G ==> 
nipkow@31719
   125
    m_inv (units_of G) x = m_inv G x"
nipkow@31719
   126
  apply (rule sym)
nipkow@31719
   127
  apply (subst m_inv_def)
nipkow@31719
   128
  apply (rule the1_equality)
nipkow@31719
   129
  apply (rule ex_ex1I)
nipkow@31719
   130
  apply (subst (asm) Units_def)
nipkow@31719
   131
  apply auto
nipkow@31719
   132
  apply (erule inv_unique)
nipkow@31719
   133
  apply auto
nipkow@31719
   134
  apply (rule Units_closed)
nipkow@31719
   135
  apply (simp_all only: units_of_carrier [symmetric])
nipkow@31719
   136
  apply (insert units_group)
nipkow@31719
   137
  apply auto
nipkow@31719
   138
  apply (subst units_of_mult [symmetric])
nipkow@31719
   139
  apply (subst units_of_one [symmetric])
nipkow@31719
   140
  apply (erule group.r_inv, assumption)
nipkow@31719
   141
  apply (subst units_of_mult [symmetric])
nipkow@31719
   142
  apply (subst units_of_one [symmetric])
nipkow@31719
   143
  apply (erule group.l_inv, assumption)
nipkow@31719
   144
done
nipkow@31719
   145
nipkow@31719
   146
lemma (in group) inj_on_const_mult: "a: (carrier G) ==> 
nipkow@31719
   147
    inj_on (%x. a \<otimes> x) (carrier G)"
nipkow@31719
   148
  by (unfold inj_on_def, auto)
nipkow@31719
   149
nipkow@31719
   150
lemma (in group) surj_const_mult: "a : (carrier G) ==>
nipkow@31719
   151
    (%x. a \<otimes> x) ` (carrier G) = (carrier G)" 
nipkow@31719
   152
  apply (auto simp add: image_def)
nipkow@31719
   153
  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
nipkow@31719
   154
  apply auto
nipkow@31719
   155
(* auto should get this. I suppose we need "comm_monoid_simprules"
nipkow@31719
   156
   for mult_ac rewriting. *)
nipkow@31719
   157
  apply (subst m_assoc [symmetric])
nipkow@31719
   158
  apply auto
nipkow@31719
   159
done
nipkow@31719
   160
nipkow@31719
   161
lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
nipkow@31719
   162
    (x \<otimes> a = x) = (a = one G)"
nipkow@31719
   163
  apply auto
nipkow@31719
   164
  apply (subst l_cancel [symmetric])
nipkow@31719
   165
  prefer 4
nipkow@31719
   166
  apply (erule ssubst)
nipkow@31719
   167
  apply auto
nipkow@31719
   168
done
nipkow@31719
   169
nipkow@31719
   170
lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
nipkow@31719
   171
    (a \<otimes> x = x) = (a = one G)"
nipkow@31719
   172
  apply auto
nipkow@31719
   173
  apply (subst r_cancel [symmetric])
nipkow@31719
   174
  prefer 4
nipkow@31719
   175
  apply (erule ssubst)
nipkow@31719
   176
  apply auto
nipkow@31719
   177
done
nipkow@31719
   178
nipkow@31719
   179
(* Is there a better way to do this? *)
nipkow@31719
   180
nipkow@31719
   181
lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
nipkow@31719
   182
    (x = x \<otimes> a) = (a = one G)"
nipkow@31719
   183
  by (subst eq_commute, simp)
nipkow@31719
   184
nipkow@31719
   185
lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
nipkow@31719
   186
    (x = a \<otimes> x) = (a = one G)"
nipkow@31719
   187
  by (subst eq_commute, simp)
nipkow@31719
   188
nipkow@31719
   189
(* This should be generalized to arbitrary groups, not just commutative
nipkow@31719
   190
   ones, using Lagrange's theorem. *)
nipkow@31719
   191
nipkow@31719
   192
lemma (in comm_group) power_order_eq_one:
nipkow@31719
   193
    assumes fin [simp]: "finite (carrier G)"
nipkow@31719
   194
        and a [simp]: "a : carrier G" 
nipkow@31719
   195
      shows "a (^) card(carrier G) = one G" 
nipkow@31719
   196
proof -
nipkow@31719
   197
  have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
nipkow@31719
   198
    by (subst (2) finprod_reindex [symmetric], 
nipkow@31719
   199
      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
nipkow@31719
   200
  also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
nipkow@31719
   201
    by (auto simp add: finprod_multf Pi_def)
nipkow@31719
   202
  also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
nipkow@31719
   203
    by (auto simp add: finprod_const)
nipkow@31719
   204
  finally show ?thesis
nipkow@31719
   205
(* uses the preceeding lemma *)
nipkow@31719
   206
    by auto
nipkow@31719
   207
qed
nipkow@31719
   208
nipkow@31719
   209
nipkow@31719
   210
(* Miscellaneous *)
nipkow@31719
   211
nipkow@31719
   212
lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
nipkow@31719
   213
    x : Units R \<Longrightarrow> field R"
nipkow@31719
   214
  apply (unfold_locales)
nipkow@31719
   215
  apply (insert prems, auto)
nipkow@31719
   216
  apply (rule trans)
nipkow@31719
   217
  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
nipkow@31719
   218
  apply assumption
nipkow@31719
   219
  apply (subst m_assoc) 
nipkow@31719
   220
  apply (auto simp add: Units_r_inv)
nipkow@31719
   221
  apply (unfold Units_def)
nipkow@31719
   222
  apply auto
nipkow@31719
   223
done
nipkow@31719
   224
nipkow@31719
   225
lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
nipkow@31719
   226
  x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
nipkow@31719
   227
  apply (subgoal_tac "x : Units G")
nipkow@31719
   228
  apply (subgoal_tac "y = inv x \<otimes> \<one>")
nipkow@31719
   229
  apply simp
nipkow@31719
   230
  apply (erule subst)
nipkow@31719
   231
  apply (subst m_assoc [symmetric])
nipkow@31719
   232
  apply auto
nipkow@31719
   233
  apply (unfold Units_def)
nipkow@31719
   234
  apply auto
nipkow@31719
   235
done
nipkow@31719
   236
nipkow@31719
   237
lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
nipkow@31719
   238
  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
nipkow@31719
   239
  apply (rule inv_char)
nipkow@31719
   240
  apply auto
nipkow@31719
   241
  apply (subst m_comm, auto) 
nipkow@31719
   242
done
nipkow@31719
   243
nipkow@31719
   244
lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"  
nipkow@31719
   245
  apply (rule inv_char)
nipkow@31719
   246
  apply (auto simp add: l_minus r_minus)
nipkow@31719
   247
done
nipkow@31719
   248
nipkow@31719
   249
lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow> 
nipkow@31719
   250
    inv x = inv y \<Longrightarrow> x = y"
nipkow@31719
   251
  apply (subgoal_tac "inv(inv x) = inv(inv y)")
nipkow@31719
   252
  apply (subst (asm) Units_inv_inv)+
nipkow@31719
   253
  apply auto
nipkow@31719
   254
done
nipkow@31719
   255
nipkow@31719
   256
lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
nipkow@31719
   257
  apply (unfold Units_def)
nipkow@31719
   258
  apply auto
nipkow@31719
   259
  apply (rule_tac x = "\<ominus> \<one>" in bexI)
nipkow@31719
   260
  apply auto
nipkow@31719
   261
  apply (simp add: l_minus r_minus)
nipkow@31719
   262
done
nipkow@31719
   263
nipkow@31719
   264
lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
nipkow@31719
   265
  apply (rule inv_char)
nipkow@31719
   266
  apply auto
nipkow@31719
   267
done
nipkow@31719
   268
nipkow@31719
   269
lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
nipkow@31719
   270
  apply auto
nipkow@31719
   271
  apply (subst Units_inv_inv [symmetric])
nipkow@31719
   272
  apply auto
nipkow@31719
   273
done
nipkow@31719
   274
nipkow@31719
   275
lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
nipkow@31719
   276
  apply auto
nipkow@31719
   277
  apply (subst Units_inv_inv [symmetric])
nipkow@31719
   278
  apply auto
nipkow@31719
   279
done
nipkow@31719
   280
nipkow@31719
   281
nipkow@31719
   282
(* This goes in FiniteProduct *)
nipkow@31719
   283
nipkow@31719
   284
lemma (in comm_monoid) finprod_UN_disjoint:
nipkow@31719
   285
  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
nipkow@31719
   286
     (A i) Int (A j) = {}) \<longrightarrow>
nipkow@31719
   287
      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
nipkow@31719
   288
        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
nipkow@31719
   289
  apply (induct set: finite)
nipkow@31719
   290
  apply force
nipkow@31719
   291
  apply clarsimp
nipkow@31719
   292
  apply (subst finprod_Un_disjoint)
nipkow@31719
   293
  apply blast
nipkow@31719
   294
  apply (erule finite_UN_I)
nipkow@31719
   295
  apply blast
nipkow@31719
   296
  apply (subst Int_UN_distrib)
nipkow@31719
   297
  apply (subst UNION_empty)
nipkow@31719
   298
  apply clarsimp
nipkow@31719
   299
  apply (drule_tac x = xa in bspec)back
nipkow@31719
   300
  apply (assumption, force)
nipkow@31719
   301
  apply (auto intro!: funcsetI finprod_closed) 
nipkow@31719
   302
  apply (subst finprod_insert)
nipkow@31719
   303
  apply (auto intro!: funcsetI finprod_closed)
nipkow@31719
   304
done
nipkow@31719
   305
nipkow@31719
   306
lemma (in comm_monoid) finprod_Union_disjoint:
nipkow@31719
   307
  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
nipkow@31719
   308
      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] 
nipkow@31719
   309
   ==> finprod G f (Union C) = finprod G (finprod G f) C" 
nipkow@31719
   310
  apply (frule finprod_UN_disjoint [of C id f])
nipkow@31719
   311
  apply (unfold Union_def id_def, auto)
nipkow@31719
   312
done
nipkow@31719
   313
nipkow@31719
   314
lemma (in comm_monoid) finprod_one [rule_format]: 
nipkow@31719
   315
  "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
nipkow@31719
   316
     finprod G f A = \<one>"
nipkow@31719
   317
  apply (induct set: finite)
nipkow@31719
   318
  apply auto
nipkow@31719
   319
  apply (subst finprod_insert)
nipkow@31719
   320
  apply (auto intro!: funcsetI)
nipkow@31719
   321
done
nipkow@31719
   322
nipkow@31719
   323
nipkow@31719
   324
(* need better simplification rules for rings *)
nipkow@31719
   325
(* the next one holds more generally for abelian groups *)
nipkow@31719
   326
nipkow@31719
   327
lemma (in cring) sum_zero_eq_neg:
nipkow@31719
   328
  "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
nipkow@31719
   329
  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y") 
nipkow@31719
   330
  apply (erule ssubst)back
nipkow@31719
   331
  apply (erule subst)
nipkow@31719
   332
  apply (simp add: ring_simprules)+
nipkow@31719
   333
done
nipkow@31719
   334
nipkow@31719
   335
(* there's a name conflict -- maybe "domain" should be
nipkow@31719
   336
   "integral_domain" *)
nipkow@31719
   337
nipkow@31719
   338
lemma (in Ring.domain) square_eq_one: 
nipkow@31719
   339
  fixes x
nipkow@31719
   340
  assumes [simp]: "x : carrier R" and
nipkow@31719
   341
    "x \<otimes> x = \<one>"
nipkow@31719
   342
  shows "x = \<one> | x = \<ominus>\<one>"
nipkow@31719
   343
proof -
nipkow@31719
   344
  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
nipkow@31719
   345
    by (simp add: ring_simprules)
nipkow@31719
   346
  also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
nipkow@31719
   347
    by (simp add: ring_simprules)
nipkow@31719
   348
  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
nipkow@31719
   349
  hence "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
nipkow@31719
   350
    by (intro integral, auto)
nipkow@31719
   351
  thus ?thesis
nipkow@31719
   352
    apply auto
nipkow@31719
   353
    apply (erule notE)
nipkow@31719
   354
    apply (rule sum_zero_eq_neg)
nipkow@31719
   355
    apply auto
nipkow@31719
   356
    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
nipkow@31719
   357
    apply (simp add: ring_simprules) 
nipkow@31719
   358
    apply (rule sum_zero_eq_neg)
nipkow@31719
   359
    apply auto
nipkow@31719
   360
    done
nipkow@31719
   361
qed
nipkow@31719
   362
nipkow@31719
   363
lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
nipkow@31719
   364
    x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
nipkow@31719
   365
  apply (rule square_eq_one)
nipkow@31719
   366
  apply auto
nipkow@31719
   367
  apply (erule ssubst)back
nipkow@31719
   368
  apply (erule Units_r_inv)
nipkow@31719
   369
done
nipkow@31719
   370
nipkow@31719
   371
nipkow@31719
   372
(*
nipkow@31719
   373
  The following translates theorems about groups to the facts about
nipkow@31719
   374
  the units of a ring. (The list should be expanded as more things are
nipkow@31719
   375
  needed.)
nipkow@31719
   376
*)
nipkow@31719
   377
nipkow@31719
   378
lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> 
nipkow@31719
   379
    finite (Units R)"
nipkow@31719
   380
  by (rule finite_subset, auto)
nipkow@31719
   381
nipkow@31719
   382
(* this belongs with MiscAlgebra.thy *)
nipkow@31719
   383
lemma (in monoid) units_of_pow: 
nipkow@31719
   384
    "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
nipkow@31719
   385
  apply (induct n)
nipkow@31719
   386
  apply (auto simp add: units_group group.is_monoid  
nipkow@31719
   387
    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
nipkow@31719
   388
    One_nat_def)
nipkow@31719
   389
done
nipkow@31719
   390
nipkow@31719
   391
lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
nipkow@31719
   392
    \<Longrightarrow> a (^) card(Units R) = \<one>"
nipkow@31719
   393
  apply (subst units_of_carrier [symmetric])
nipkow@31719
   394
  apply (subst units_of_one [symmetric])
nipkow@31719
   395
  apply (subst units_of_pow [symmetric])
nipkow@31719
   396
  apply assumption
nipkow@31719
   397
  apply (rule comm_group.power_order_eq_one)
nipkow@31719
   398
  apply (rule units_comm_group)
nipkow@31719
   399
  apply (unfold units_of_def, auto)
nipkow@31719
   400
done
nipkow@31719
   401
nipkow@31719
   402
end