src/HOL/Number_Theory/MiscAlgebra.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44890 22f665a2e91c
child 53374 a14d2a854c02
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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   unfolding units_of_def by auto
    79 
    80 lemma units_of_mult: "mult(units_of G) = mult G"
    81   unfolding units_of_def by auto
    82 
    83 lemma units_of_one: "one(units_of G) = one G"
    84   unfolding units_of_def by 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   unfolding inj_on_def by 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   apply (subst eq_commute)
   146   apply simp
   147   done
   148 
   149 lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   150     (x = a \<otimes> x) = (a = one G)"
   151   apply (subst eq_commute)
   152   apply simp
   153   done
   154 
   155 (* This should be generalized to arbitrary groups, not just commutative
   156    ones, using Lagrange's theorem. *)
   157 
   158 lemma (in comm_group) power_order_eq_one:
   159   assumes fin [simp]: "finite (carrier G)"
   160     and a [simp]: "a : carrier G"
   161   shows "a (^) card(carrier G) = one G"
   162 proof -
   163   have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
   164     by (subst (2) finprod_reindex [symmetric],
   165       auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   166   also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
   167     by (auto simp add: finprod_multf Pi_def)
   168   also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
   169     by (auto simp add: finprod_const)
   170   finally show ?thesis
   171 (* uses the preceeding lemma *)
   172     by auto
   173 qed
   174 
   175 
   176 (* Miscellaneous *)
   177 
   178 lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
   179     x : Units R \<Longrightarrow> field R"
   180   apply (unfold_locales)
   181   apply (insert cring_axioms, auto)
   182   apply (rule trans)
   183   apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
   184   apply assumption
   185   apply (subst m_assoc)
   186   apply auto
   187   apply (unfold Units_def)
   188   apply auto
   189   done
   190 
   191 lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   192     x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
   193   apply (subgoal_tac "x : Units G")
   194   apply (subgoal_tac "y = inv x \<otimes> \<one>")
   195   apply simp
   196   apply (erule subst)
   197   apply (subst m_assoc [symmetric])
   198   apply auto
   199   apply (unfold Units_def)
   200   apply auto
   201   done
   202 
   203 lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   204   x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
   205   apply (rule inv_char)
   206   apply auto
   207   apply (subst m_comm, auto)
   208   done
   209 
   210 lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
   211   apply (rule inv_char)
   212   apply (auto simp add: l_minus r_minus)
   213   done
   214 
   215 lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
   216     inv x = inv y \<Longrightarrow> x = y"
   217   apply (subgoal_tac "inv(inv x) = inv(inv y)")
   218   apply (subst (asm) Units_inv_inv)+
   219   apply auto
   220   done
   221 
   222 lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
   223   apply (unfold Units_def)
   224   apply auto
   225   apply (rule_tac x = "\<ominus> \<one>" in bexI)
   226   apply auto
   227   apply (simp add: l_minus r_minus)
   228   done
   229 
   230 lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
   231   apply (rule inv_char)
   232   apply auto
   233   done
   234 
   235 lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
   236   apply auto
   237   apply (subst Units_inv_inv [symmetric])
   238   apply auto
   239   done
   240 
   241 lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   242   apply auto
   243   apply (subst Units_inv_inv [symmetric])
   244   apply auto
   245   done
   246 
   247 
   248 (* This goes in FiniteProduct *)
   249 
   250 lemma (in comm_monoid) finprod_UN_disjoint:
   251   "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
   252      (A i) Int (A j) = {}) \<longrightarrow>
   253       (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
   254         finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
   255   apply (induct set: finite)
   256   apply force
   257   apply clarsimp
   258   apply (subst finprod_Un_disjoint)
   259   apply blast
   260   apply (erule finite_UN_I)
   261   apply blast
   262   apply (fastforce)
   263   apply (auto intro!: funcsetI finprod_closed)
   264   done
   265 
   266 lemma (in comm_monoid) finprod_Union_disjoint:
   267   "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
   268       (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
   269    ==> finprod G f (Union C) = finprod G (finprod G f) C"
   270   apply (frule finprod_UN_disjoint [of C id f])
   271   apply (auto simp add: SUP_def)
   272   done
   273 
   274 lemma (in comm_monoid) finprod_one:
   275     "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
   276   by (induct set: finite) auto
   277 
   278 
   279 (* need better simplification rules for rings *)
   280 (* the next one holds more generally for abelian groups *)
   281 
   282 lemma (in cring) sum_zero_eq_neg:
   283     "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   284   apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
   285   apply (erule ssubst)back
   286   apply (erule subst)
   287   apply (simp_all add: ring_simprules)
   288   done
   289 
   290 (* there's a name conflict -- maybe "domain" should be
   291    "integral_domain" *)
   292 
   293 lemma (in Ring.domain) square_eq_one:
   294   fixes x
   295   assumes [simp]: "x : carrier R" and
   296     "x \<otimes> x = \<one>"
   297   shows "x = \<one> | x = \<ominus>\<one>"
   298 proof -
   299   have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
   300     by (simp add: ring_simprules)
   301   also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
   302     by (simp add: ring_simprules)
   303   finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   304   then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
   305     by (intro integral, auto)
   306   then show ?thesis
   307     apply auto
   308     apply (erule notE)
   309     apply (rule sum_zero_eq_neg)
   310     apply auto
   311     apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
   312     apply (simp add: ring_simprules)
   313     apply (rule sum_zero_eq_neg)
   314     apply auto
   315     done
   316 qed
   317 
   318 lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
   319     x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
   320   apply (rule square_eq_one)
   321   apply auto
   322   apply (erule ssubst)back
   323   apply (erule Units_r_inv)
   324   done
   325 
   326 
   327 (*
   328   The following translates theorems about groups to the facts about
   329   the units of a ring. (The list should be expanded as more things are
   330   needed.)
   331 *)
   332 
   333 lemma (in ring) finite_ring_finite_units [intro]:
   334     "finite (carrier R) \<Longrightarrow> finite (Units R)"
   335   by (rule finite_subset) auto
   336 
   337 (* this belongs with MiscAlgebra.thy *)
   338 lemma (in monoid) units_of_pow:
   339     "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
   340   apply (induct n)
   341   apply (auto simp add: units_group group.is_monoid
   342     monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
   343   done
   344 
   345 lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
   346     \<Longrightarrow> a (^) card(Units R) = \<one>"
   347   apply (subst units_of_carrier [symmetric])
   348   apply (subst units_of_one [symmetric])
   349   apply (subst units_of_pow [symmetric])
   350   apply assumption
   351   apply (rule comm_group.power_order_eq_one)
   352   apply (rule units_comm_group)
   353   apply (unfold units_of_def, auto)
   354   done
   355 
   356 end