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