ratRingScript.sml

1(***************************************************************************
2 *
3 *  Theory of ring properties of rational numbers.
4 *
5 *  Jens Brandt, November 2005
6 *
7 ***************************************************************************)
8Theory ratRing
9Ancestors
10  integer rat EVAL_ring
11Libs
12  EVAL_ringLib schneiderUtils
13
14
15(*--------------------------------------------------------------------------
16 *  RAT_IS_RING: thm
17 *  |- is_ring (ring rat_0 rat_1 rat_add rat_mul rat_ainv)
18 *--------------------------------------------------------------------------*)
19
20Theorem RAT_IS_RING: is_ring (ring 0q 1q rat_add rat_mul rat_ainv)
21Proof
22  RW_TAC intLib.int_ss[
23      EVAL_ringTheory.is_ring_def, EVAL_ringTheory.ring_accessors,
24      RAT_ADD_ASSOC, RAT_MUL_ASSOC,
25      RAT_ADD_LID, RAT_MUL_LID,
26      RAT_ADD_RINV,
27      RAT_RDISTRIB] THEN
28  MAP_FIRST MATCH_ACCEPT_TAC [
29      RAT_ADD_COMM, RAT_MUL_COMM
30    ]
31QED
32
33val rat_ring_thms =
34  EVAL_ringLib.store_ring { Name = "rat", Theory = RAT_IS_RING };
35
36(*==========================================================================
37 * end of theory
38 *==========================================================================*)