src/HOL/ex/Ring.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5078 7b5ea59c0275
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Integ/Ring.thy
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     2
    ID:         $Id$
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   1996 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     5
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
Bits of rings.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
Main output: a simplification tactic for commutative rings.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     9
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
Ring = Group +
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
(* Ring *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    13
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
axclass  ring < add_agroup, times
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
  times_assoc "(x*y)*z = x*(y*z)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
  distribL    "x*(y+z) = x*y + x*z"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
  distribR    "(x+y)*z = x*z + y*z"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
(* Commutative ring *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    20
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    21
axclass cring < ring
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    22
  times_commute "x*y = y*x"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    23
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
end