src/HOL/Algebra/abstract/Ring2.thy
author haftmann
Wed Jan 02 15:14:02 2008 +0100 (2008-01-02)
changeset 25762 c03e9d04b3e4
parent 24993 92dfacb32053
child 26342 0f65fa163304
permissions -rw-r--r--
splitted class uminus from class minus
     1 (*
     2   Title:     The algebraic hierarchy of rings as axiomatic classes
     3   Id:        $Id$
     4   Author:    Clemens Ballarin, started 9 December 1996
     5   Copyright: Clemens Ballarin
     6 *)
     7 
     8 header {* The algebraic hierarchy of rings as axiomatic classes *}
     9 
    10 theory Ring2 imports Main
    11 begin
    12 
    13 section {* Constants *}
    14 
    15 text {* Most constants are already declared by HOL. *}
    16 
    17 consts
    18   assoc         :: "['a::Divides.div, 'a] => bool"              (infixl "assoc" 50)
    19   irred         :: "'a::{zero, one, Divides.div} => bool"
    20   prime         :: "'a::{zero, one, Divides.div} => bool"
    21 
    22 section {* Axioms *}
    23 
    24 subsection {* Ring axioms *}
    25 
    26 axclass ring < zero, one, plus, minus, uminus, times, inverse, power, Divides.div
    27 
    28   a_assoc:      "(a + b) + c = a + (b + c)"
    29   l_zero:       "0 + a = a"
    30   l_neg:        "(-a) + a = 0"
    31   a_comm:       "a + b = b + a"
    32 
    33   m_assoc:      "(a * b) * c = a * (b * c)"
    34   l_one:        "1 * a = a"
    35 
    36   l_distr:      "(a + b) * c = a * c + b * c"
    37 
    38   m_comm:       "a * b = b * a"
    39 
    40   -- {* Definition of derived operations *}
    41 
    42   minus_def:    "a - b = a + (-b)"
    43   inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
    44   divide_def:   "a / b = a * inverse b"
    45   power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
    46 
    47 defs
    48   assoc_def:    "a assoc b == a dvd b & b dvd a"
    49   irred_def:    "irred a == a ~= 0 & ~ a dvd 1
    50                           & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
    51   prime_def:    "prime p == p ~= 0 & ~ p dvd 1
    52                           & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
    53 
    54 subsection {* Integral domains *}
    55 
    56 axclass
    57   "domain" < ring
    58 
    59   one_not_zero: "1 ~= 0"
    60   integral:     "a * b = 0 ==> a = 0 | b = 0"
    61 
    62 subsection {* Factorial domains *}
    63 
    64 axclass
    65   factorial < "domain"
    66 
    67 (*
    68   Proper definition using divisor chain condition currently not supported.
    69   factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
    70 *)
    71   factorial_divisor:	"True"
    72   factorial_prime:      "irred a ==> prime a"
    73 
    74 subsection {* Euclidean domains *}
    75 
    76 (*
    77 axclass
    78   euclidean < "domain"
    79 
    80   euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
    81                    a = b * q + r & e_size r < e_size b)"
    82 
    83   Nothing has been proved about Euclidean domains, yet.
    84   Design question:
    85     Fix quo, rem and e_size as constants that are axiomatised with
    86     euclidean_ax?
    87     - advantage: more pragmatic and easier to use
    88     - disadvantage: for every type, one definition of quo and rem will
    89         be fixed, users may want to use differing ones;
    90         also, it seems not possible to prove that fields are euclidean
    91         domains, because that would require generic (type-independent)
    92         definitions of quo and rem.
    93 *)
    94 
    95 subsection {* Fields *}
    96 
    97 axclass
    98   field < ring
    99 
   100   field_one_not_zero:    "1 ~= 0"
   101                 (* Avoid a common superclass as the first thing we will
   102                    prove about fields is that they are domains. *)
   103   field_ax:        "a ~= 0 ==> a dvd 1"
   104 
   105 
   106 section {* Basic facts *}
   107 
   108 subsection {* Normaliser for rings *}
   109 
   110 (* derived rewrite rules *)
   111 
   112 lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)"
   113   apply (rule a_comm [THEN trans])
   114   apply (rule a_assoc [THEN trans])
   115   apply (rule a_comm [THEN arg_cong])
   116   done
   117 
   118 lemma r_zero: "(a::'a::ring) + 0 = a"
   119   apply (rule a_comm [THEN trans])
   120   apply (rule l_zero)
   121   done
   122 
   123 lemma r_neg: "(a::'a::ring) + (-a) = 0"
   124   apply (rule a_comm [THEN trans])
   125   apply (rule l_neg)
   126   done
   127 
   128 lemma r_neg2: "(a::'a::ring) + (-a + b) = b"
   129   apply (rule a_assoc [symmetric, THEN trans])
   130   apply (simp add: r_neg l_zero)
   131   done
   132 
   133 lemma r_neg1: "-(a::'a::ring) + (a + b) = b"
   134   apply (rule a_assoc [symmetric, THEN trans])
   135   apply (simp add: l_neg l_zero)
   136   done
   137 
   138 
   139 (* auxiliary *)
   140 
   141 lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
   142   apply (rule box_equals)
   143   prefer 2
   144   apply (rule l_zero)
   145   prefer 2
   146   apply (rule l_zero)
   147   apply (rule_tac a1 = a in l_neg [THEN subst])
   148   apply (simp add: a_assoc)
   149   done
   150 
   151 lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)"
   152   apply (rule_tac a = "a + b" in a_lcancel)
   153   apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm)
   154   done
   155 
   156 lemma minus_minus: "-(-(a::'a::ring)) = a"
   157   apply (rule a_lcancel)
   158   apply (rule r_neg [THEN trans])
   159   apply (rule l_neg [symmetric])
   160   done
   161 
   162 lemma minus0: "- 0 = (0::'a::ring)"
   163   apply (rule a_lcancel)
   164   apply (rule r_neg [THEN trans])
   165   apply (rule l_zero [symmetric])
   166   done
   167 
   168 
   169 (* derived rules for multiplication *)
   170 
   171 lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)"
   172   apply (rule m_comm [THEN trans])
   173   apply (rule m_assoc [THEN trans])
   174   apply (rule m_comm [THEN arg_cong])
   175   done
   176 
   177 lemma r_one: "(a::'a::ring) * 1 = a"
   178   apply (rule m_comm [THEN trans])
   179   apply (rule l_one)
   180   done
   181 
   182 lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c"
   183   apply (rule m_comm [THEN trans])
   184   apply (rule l_distr [THEN trans])
   185   apply (simp add: m_comm)
   186   done
   187 
   188 
   189 (* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
   190 lemma l_null: "0 * (a::'a::ring) = 0"
   191   apply (rule a_lcancel)
   192   apply (rule l_distr [symmetric, THEN trans])
   193   apply (simp add: r_zero)
   194   done
   195 
   196 lemma r_null: "(a::'a::ring) * 0 = 0"
   197   apply (rule m_comm [THEN trans])
   198   apply (rule l_null)
   199   done
   200 
   201 lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)"
   202   apply (rule a_lcancel)
   203   apply (rule r_neg [symmetric, THEN [2] trans])
   204   apply (rule l_distr [symmetric, THEN trans])
   205   apply (simp add: l_null r_neg)
   206   done
   207 
   208 lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)"
   209   apply (rule a_lcancel)
   210   apply (rule r_neg [symmetric, THEN [2] trans])
   211   apply (rule r_distr [symmetric, THEN trans])
   212   apply (simp add: r_null r_neg)
   213   done
   214 
   215 (*** Term order for commutative rings ***)
   216 
   217 ML {*
   218 fun ring_ord (Const (a, _)) =
   219     find_index (fn a' => a = a')
   220       [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus},
   221         @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
   222   | ring_ord _ = ~1;
   223 
   224 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
   225 
   226 val ring_ss = HOL_basic_ss settermless termless_ring addsimps
   227   [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
   228    thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def",
   229    thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add",
   230    thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*)
   231    thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"];
   232 *}   (* Note: r_one is not necessary in ring_ss *)
   233 
   234 method_setup ring =
   235   {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
   236   {* computes distributive normal form in rings *}
   237 
   238 lemmas ring_simps =
   239   l_zero r_zero l_neg r_neg minus_minus minus0
   240   l_one r_one l_null r_null l_minus r_minus
   241 
   242 
   243 subsection {* Rings and the summation operator *}
   244 
   245 (* Basic facts --- move to HOL!!! *)
   246 
   247 (* needed because natsum_cong (below) disables atMost_0 *)
   248 lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
   249 by simp
   250 (*
   251 lemma natsum_Suc [simp]:
   252   "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
   253 by (simp add: atMost_Suc)
   254 *)
   255 lemma natsum_Suc2:
   256   "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
   257 proof (induct n)
   258   case 0 show ?case by simp
   259 next
   260   case Suc thus ?case by (simp add: add_assoc) 
   261 qed
   262 
   263 lemma natsum_cong [cong]:
   264   "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
   265         setsum f {..j} = setsum g {..k}"
   266 by (induct j) auto
   267 
   268 lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
   269 by (induct n) simp_all
   270 
   271 lemma natsum_add [simp]:
   272   "!!f::nat=>'a::comm_monoid_add.
   273    setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
   274 by (induct n) (simp_all add: add_ac)
   275 
   276 (* Facts specific to rings *)
   277 
   278 instance ring < comm_monoid_add
   279 proof
   280   fix x y z
   281   show "(x::'a::ring) + y = y + x" by (rule a_comm)
   282   show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
   283   show "0 + (x::'a::ring) = x" by (rule l_zero)
   284 qed
   285 
   286 ML {*
   287   local
   288     val lhss = 
   289         ["t + u::'a::ring",
   290 	 "t - u::'a::ring",
   291 	 "t * u::'a::ring",
   292 	 "- t::'a::ring"];
   293     fun proc ss t = 
   294       let val rew = Goal.prove (Simplifier.the_context ss) [] []
   295             (HOLogic.mk_Trueprop
   296               (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
   297                 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
   298             |> mk_meta_eq;
   299           val (t', u) = Logic.dest_equals (Thm.prop_of rew);
   300       in if t' aconv u 
   301         then NONE
   302         else SOME rew 
   303     end;
   304   in
   305     val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
   306   end;
   307 *}
   308 
   309 ML_setup {* Addsimprocs [ring_simproc] *}
   310 
   311 lemma natsum_ldistr:
   312   "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
   313 by (induct n) simp_all
   314 
   315 lemma natsum_rdistr:
   316   "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
   317 by (induct n) simp_all
   318 
   319 subsection {* Integral Domains *}
   320 
   321 declare one_not_zero [simp]
   322 
   323 lemma zero_not_one [simp]:
   324   "0 ~= (1::'a::domain)" 
   325 by (rule not_sym) simp
   326 
   327 lemma integral_iff: (* not by default a simp rule! *)
   328   "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
   329 proof
   330   assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
   331 next
   332   assume "a = 0 | b = 0" then show "a * b = 0" by auto
   333 qed
   334 
   335 (*
   336 lemma "(a::'a::ring) - (a - b) = b" apply simp
   337  simproc seems to fail on this example (fixed with new term order)
   338 *)
   339 (*
   340 lemma bug: "(b::'a::ring) - (b - a) = a" by simp
   341    simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
   342 *)
   343 lemma m_lcancel:
   344   assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
   345 proof
   346   assume eq: "a * b = a * c"
   347   then have "a * (b - c) = 0" by simp
   348   then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
   349   with prem have "b - c = 0" by auto 
   350   then have "b = b - (b - c)" by simp 
   351   also have "b - (b - c) = c" by simp
   352   finally show "b = c" .
   353 next
   354   assume "b = c" then show "a * b = a * c" by simp
   355 qed
   356 
   357 lemma m_rcancel:
   358   "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
   359 by (simp add: m_lcancel)
   360 
   361 lemma power_0 [simp]:
   362   "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp
   363 
   364 lemma power_Suc [simp]:
   365   "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp
   366 
   367 lemma power_one [simp]:
   368   "1 ^ n = (1::'a::ring)" by (induct n) simp_all
   369 
   370 lemma power_zero [simp]:
   371   "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
   372 
   373 lemma power_mult [simp]:
   374   "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
   375   by (induct m) simp_all
   376 
   377 
   378 section "Divisibility"
   379 
   380 lemma dvd_zero_right [simp]:
   381   "(a::'a::ring) dvd 0"
   382 proof
   383   show "0 = a * 0" by simp
   384 qed
   385 
   386 lemma dvd_zero_left:
   387   "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
   388 
   389 lemma dvd_refl_ring [simp]:
   390   "(a::'a::ring) dvd a"
   391 proof
   392   show "a = a * 1" by simp
   393 qed
   394 
   395 lemma dvd_trans_ring:
   396   fixes a b c :: "'a::ring"
   397   assumes a_dvd_b: "a dvd b"
   398   and b_dvd_c: "b dvd c"
   399   shows "a dvd c"
   400 proof -
   401   from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
   402   moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
   403   ultimately have "c = a * (l * j)" by simp
   404   then have "\<exists>k. c = a * k" ..
   405   then show ?thesis using dvd_def by blast
   406 qed
   407 
   408 
   409 lemma unit_mult: 
   410   "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
   411   apply (unfold dvd_def)
   412   apply clarify
   413   apply (rule_tac x = "k * ka" in exI)
   414   apply simp
   415   done
   416 
   417 lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
   418   apply (induct_tac n)
   419    apply simp
   420   apply (simp add: unit_mult)
   421   done
   422 
   423 lemma dvd_add_right [simp]:
   424   "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"
   425   apply (unfold dvd_def)
   426   apply clarify
   427   apply (rule_tac x = "k + ka" in exI)
   428   apply (simp add: r_distr)
   429   done
   430 
   431 lemma dvd_uminus_right [simp]:
   432   "!! a::'a::ring. a dvd b ==> a dvd -b"
   433   apply (unfold dvd_def)
   434   apply clarify
   435   apply (rule_tac x = "-k" in exI)
   436   apply (simp add: r_minus)
   437   done
   438 
   439 lemma dvd_l_mult_right [simp]:
   440   "!! a::'a::ring. a dvd b ==> a dvd c*b"
   441   apply (unfold dvd_def)
   442   apply clarify
   443   apply (rule_tac x = "c * k" in exI)
   444   apply simp
   445   done
   446 
   447 lemma dvd_r_mult_right [simp]:
   448   "!! a::'a::ring. a dvd b ==> a dvd b*c"
   449   apply (unfold dvd_def)
   450   apply clarify
   451   apply (rule_tac x = "k * c" in exI)
   452   apply simp
   453   done
   454 
   455 
   456 (* Inverse of multiplication *)
   457 
   458 section "inverse"
   459 
   460 lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"
   461   apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals)
   462     apply (simp (no_asm))
   463   apply auto
   464   done
   465 
   466 lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
   467   apply (unfold inverse_def dvd_def)
   468   apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
   469   apply clarify
   470   apply (rule theI)
   471    apply assumption
   472   apply (rule inverse_unique)
   473    apply assumption
   474   apply assumption
   475   done
   476 
   477 lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
   478   by (simp add: r_inverse_ring)
   479 
   480 
   481 (* Fields *)
   482 
   483 section "Fields"
   484 
   485 lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)"
   486   by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero)
   487 
   488 lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
   489   by (simp add: r_inverse_ring)
   490 
   491 lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
   492   by (simp add: l_inverse_ring)
   493 
   494 
   495 (* fields are integral domains *)
   496 
   497 lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
   498   apply (tactic "step_tac @{claset} 1")
   499   apply (rule_tac a = " (a*b) * inverse b" in box_equals)
   500     apply (rule_tac [3] refl)
   501    prefer 2
   502    apply (simp (no_asm))
   503    apply auto
   504   done
   505 
   506 
   507 (* fields are factorial domains *)
   508 
   509 lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
   510   unfolding prime_def irred_def by (blast intro: field_ax)
   511 
   512 end