1(***************************************************************************
2 *
3 *  Theory of ring properties of rational numbers.
4 *
5 *  Jens Brandt, November 2005
6 *
7 ***************************************************************************)
8
9open HolKernel boolLib Parse bossLib;
10
11(* interactive mode
12app load [
13        "integerTheory", "ratTheory", "ringLib", "schneiderUtils";
14*)
15
16open
17        integerTheory ratTheory ringLib schneiderUtils;
18
19val _ = new_theory "ratRing";
20
21(*--------------------------------------------------------------------------
22 *  RAT_IS_RING: thm
23 *  |- is_ring (ring rat_0 rat_1 rat_add rat_mul rat_ainv)
24 *--------------------------------------------------------------------------*)
25
26val RAT_IS_RING = store_thm("RAT_IS_RING",``is_ring (ring 0q 1q rat_add rat_mul rat_ainv)``,
27        RW_TAC intLib.int_ss[ ringTheory.is_ring_def, ringTheory.ring_accessors,
28                RAT_ADD_ASSOC, RAT_MUL_ASSOC,
29                RAT_ADD_LID, RAT_MUL_LID,
30                RAT_ADD_RINV,
31                RAT_RDISTRIB] THEN
32        MAP_FIRST MATCH_ACCEPT_TAC [
33                RAT_ADD_COMM, RAT_MUL_COMM
34                ] );
35
36val rat_ring_thms = ringLib.store_ring { Name = "rat", Theory = RAT_IS_RING };
37
38(*==========================================================================
39 * end of theory
40 *==========================================================================*)
41
42val _ = export_theory();
43