# Theory Ring

Up to index of Isabelle/HOL/HOL-Algebra

theory Ring
imports Main
uses (order.ML) [Ring.ML]
begin

    (*
      Title:     The algebraic hierarchy of rings as axiomatic classes
      Id:        $Id: Ring.thy,v 1.15 2005/09/06 14:59:48 wenzelm Exp $
      Author:    Clemens Ballarin, started 9 December 1996
      Copyright: Clemens Ballarin
    *)

    header {* The algebraic hierarchy of rings as axiomatic classes *}

    theory Ring imports Main
    uses ("order.ML") begin

    section {* Constants *}

    text {* Most constants are already declared by HOL. *}

    consts
      assoc         :: "['a::times, 'a] => bool"              (infixl 50)
      irred         :: "'a::{zero, one, times} => bool"
      prime         :: "'a::{zero, one, times} => bool"

    section {* Axioms *}

    subsection {* Ring axioms *}

    axclass ring < zero, one, plus, minus, times, inverse, power

      a_assoc:      "(a + b) + c = a + (b + c)"
      l_zero:       "0 + a = a"
      l_neg:        "(-a) + a = 0"
      a_comm:       "a + b = b + a"

      m_assoc:      "(a * b) * c = a * (b * c)"
      l_one:        "1 * a = a"

      l_distr:      "(a + b) * c = a * c + b * c"

      m_comm:       "a * b = b * a"

      -- {* Definition of derived operations *}

      minus_def:    "a - b = a + (-b)"
      inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
      divide_def:   "a / b = a * inverse b"
      power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"

    defs
      assoc_def:    "a assoc b == a dvd b & b dvd a"
      irred_def:    "irred a == a ~= 0 & ~ a dvd 1
                              & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
      prime_def:    "prime p == p ~= 0 & ~ p dvd 1
                              & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"

    subsection {* Integral domains *}

    axclass
      "domain" < ring

      one_not_zero: "1 ~= 0"
      integral:     "a * b = 0 ==> a = 0 | b = 0"

    subsection {* Factorial domains *}

    axclass
      factorial < "domain"

    (*
      Proper definition using divisor chain condition currently not supported.
      factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
    *)
      factorial_divisor:    "True"
      factorial_prime:      "irred a ==> prime a"

    subsection {* Euclidean domains *}

    (*
    axclass
      euclidean < "domain"

      euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
                       a = b * q + r & e_size r < e_size b)"

      Nothing has been proved about Euclidean domains, yet.
      Design question:
        Fix quo, rem and e_size as constants that are axiomatised with
        euclidean_ax?
        - advantage: more pragmatic and easier to use
        - disadvantage: for every type, one definition of quo and rem will
            be fixed, users may want to use differing ones;
            also, it seems not possible to prove that fields are euclidean
            domains, because that would require generic (type-independent)
            definitions of quo and rem.
    *)

    subsection {* Fields *}

    axclass
      field < ring

      field_one_not_zero:    "1 ~= 0"
                    (* Avoid a common superclass as the first thing we will
                       prove about fields is that they are domains. *)
      field_ax:        "a ~= 0 ==> a dvd 1"

    section {* Basic facts *}

    subsection {* Normaliser for rings *}

    use "order.ML"

    method_setup ring =
      {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
      {* computes distributive normal form in rings *}

    subsection {* Rings and the summation operator *}

    (* Basic facts --- move to HOL!!! *)

    (* needed because natsum_cong (below) disables atMost_0 *)
    lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
    by simp
    (*
    lemma natsum_Suc [simp]:
      "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
    by (simp add: atMost_Suc)
    *)
    lemma natsum_Suc2:
      "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
    proof (induct n)
      case 0 show ?case by simp
    next
      case Suc thus ?case by (simp add: semigroup_add_class.add_assoc)
    qed

    lemma natsum_cong [cong]:
      "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
            setsum f {..j} = setsum g {..k}"
    by (induct j) auto

    lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
    by (induct n) simp_all

    lemma natsum_add [simp]:
      "!!f::nat=>'a::comm_monoid_add.
       setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
    by (induct n) (simp_all add: add_ac)

    (* Facts specific to rings *)

    instance ring < comm_monoid_add
    proof
      fix x y z
      show "(x::'a::ring) + y = y + x" by (rule a_comm)
      show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
      show "0 + (x::'a::ring) = x" by (rule l_zero)
    qed

    ML {*
      local
        val lhss =
            ["t + u::'a::ring",
             "t - u::'a::ring",
             "t * u::'a::ring",
             "- t::'a::ring"];
        fun proc sg ss t =
          let val rew = Tactic.prove sg [] []
                (HOLogic.mk_Trueprop
                  (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
                    (fn _ => simp_tac (Simplifier.inherit_bounds ss ring_ss) 1)
                |> mk_meta_eq;
              val (t', u) = Logic.dest_equals (Thm.prop_of rew);
          in if t' aconv u
            then NONE
            else SOME rew
        end;
      in
        val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss proc;
      end;
    *}

    ML_setup {* Addsimprocs [ring_simproc] *}

    lemma natsum_ldistr:
      "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
    by (induct n) simp_all

    lemma natsum_rdistr:
      "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
    by (induct n) simp_all

    subsection {* Integral Domains *}

    declare one_not_zero [simp]

    lemma zero_not_one [simp]:
      "0 ~= (1::'a::domain)"
    by (rule not_sym) simp

    lemma integral_iff: (* not by default a simp rule! *)
      "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
    proof
      assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
    next
      assume "a = 0 | b = 0" then show "a * b = 0" by auto
    qed

    (*
    lemma "(a::'a::ring) - (a - b) = b" apply simp
     simproc seems to fail on this example (fixed with new term order)
    *)
    (*
    lemma bug: "(b::'a::ring) - (b - a) = a" by simp
       simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
    *)
    lemma m_lcancel:
      assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
    proof
      assume eq: "a * b = a * c"
      then have "a * (b - c) = 0" by simp
      then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
      with prem have "b - c = 0" by auto
      then have "b = b - (b - c)" by simp
      also have "b - (b - c) = c" by simp
      finally show "b = c" .
    next
      assume "b = c" then show "a * b = a * c" by simp
    qed

    lemma m_rcancel:
      "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
    by (simp add: m_lcancel)

    end

## Constants

## Axioms

### Ring axioms

### Integral domains

### Factorial domains

### Euclidean domains

### Fields

## Basic facts

### Normaliser for rings

theorems ring_simps:

      (0::'a) + a = a

      a + (0::'a) = a

      - a + a = (0::'a)

      a + - a = (0::'a)

      - (- a) = a

      - (0::'a) = (0::'a)

      (1::'a) * a = a

      a * (1::'a) = a

      (0::'a) * a = (0::'a)

      a * (0::'a) = (0::'a)

      - a * b = - (a * b)

      a * - b = - (a * b)

### Rings and the summation operator

lemma natsum_0:

      setsum f {..0} = f 0

lemma natsum_Suc2:

      setsum f {..Suc n} = f 0 + (∑i≤n. f (Suc i))

lemma natsum_cong:

      [| j = k; !!i. i ≤ k ==> f i = g i |] ==> setsum f {..j} = setsum g {..k}

lemma natsum_zero:

      (∑i≤n. (0::'a)) = (0::'a)

lemma natsum_add:

      (∑i≤n. f i + g i) = setsum f {..n} + setsum g {..n}

lemma natsum_ldistr:

      setsum f {..n} * a = (∑i≤n. f i * a)

lemma natsum_rdistr:

      a * setsum f {..n} = (∑i≤n. a * f i)

### Integral Domains

lemma zero_not_one:

      (0::'a) ≠ (1::'a)

lemma integral_iff:

      (a * b = (0::'a)) = (a = (0::'a) ∨ b = (0::'a))

lemma conc:

      a ≠ (0::'a) ==> (a * b = a * c) = (b = c)

lemma m_rcancel:

      a ≠ (0::'a) ==> (b * a = c * a) = (b = c)

theorem power_0:

      a ^ 0 = (1::'a)

theorem power_Suc:

      a ^ Suc n = a ^ n * a

theorem power_one:

      (1::'a) ^ n = (1::'a)

theorem power_zero:

      n ≠ 0 ==> (0::'a) ^ n = (0::'a)

theorem power_mult:

      a ^ m * a ^ n = a ^ (m + n)

## Divisibility

theorem dvd_zero_right:

      a dvd (0::'a)

theorem dvd_zero_left:

      (0::'a) dvd a ==> a = (0::'a)

theorem dvd_refl_ring:

      a dvd a

theorem dvd_trans_ring:

      [| a dvd b; b dvd c |] ==> a dvd c

theorem unit_mult:

      [| a dvd (1::'a); b dvd (1::'a) |] ==> a * b dvd (1::'a)

theorem unit_power:

      a dvd (1::'a) ==> a ^ n dvd (1::'a)

theorem dvd_add_right:

      [| a dvd b; a dvd c |] ==> a dvd b + c

theorem dvd_uminus_right:

      a dvd b ==> a dvd - b

theorem dvd_l_mult_right:

      a dvd b ==> a dvd c * b

theorem dvd_r_mult_right:

      a dvd b ==> a dvd b * c

## inverse

theorem inverse_unique:

      [| a * x = (1::'a); a * y = (1::'a) |] ==> x = y

theorem r_inverse_ring:

      a dvd (1::'a) ==> a * inverse a = (1::'a)

theorem l_inverse_ring:

      a dvd (1::'a) ==> inverse a * a = (1::'a)

## Fields

theorem field_unit:

      (a dvd (1::'a)) = (a ≠ (0::'a))

theorem r_inverse:

      a ≠ (0::'a) ==> a * inverse a = (1::'a)

theorem l_inverse:

      a ≠ (0::'a) ==> inverse a * a = (1::'a)

theorem field_integral:

      a * b = (0::'a) ==> a = (0::'a) ∨ b = (0::'a)

theorem field_fact_prime:

      irred a ==> prime a