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