src/HOL/Number_Theory/MiscAlgebra.thy
author wenzelm
Thu Jan 13 23:50:16 2011 +0100 (2011-01-13)
changeset 41541 1fa4725c4656
parent 35416 d8d7d1b785af
child 41959 b460124855b8
permissions -rw-r--r--
eliminated global prems;
tuned proofs;
     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 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 (unfold Union_def id_def, auto)
   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