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