integerRingScript.sml

1Theory integerRing
2Ancestors
3  integer EVAL_ring
4
5val _ = ParseExtras.temp_loose_equality()
6
7val ARW_TAC = RW_TAC arith_ss;
8
9Theorem int_is_ring:
10      is_ring (ring int_0 int_1 $+ $* $~)
11Proof
12ARW_TAC [ is_ring_def, ring_accessors, INT_0, INT_1,
13          INT_ADD_RINV, INT_RDISTRIB,
14          INT_ADD_ASSOC, INT_MUL_ASSOC, INT_ADD_LID, INT_MUL_LID] THEN
15MAP_FIRST MATCH_ACCEPT_TAC [ INT_ADD_SYM, INT_MUL_SYM ]
16QED
17
18val int_ring_thms =
19  EVAL_ringLib.store_ring { Name = "int", Theory = int_is_ring };
20
21(* Note: AND_CLAUSES is not lazy *)
22local open numeralTheory
23in
24val int_rewrites = save_thm("int_rewrites", LIST_CONJ
25  [ int_calculate, INT_0, INT_1,
26    numeral_lt, numeral_lte, numeral_sub, iSUB_THM, AND_CLAUSES ]);
27end;
28