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