1(*
2load "ringLib";
3load "numeralTheory";
4load "bossLib";
5*)
6open HolKernel Parse boolLib bossLib
7     arithmeticTheory semi_ringTheory;
8
9
10val _ = new_theory "numRing";
11
12(* num is a semi-ring: *)
13val num_semi_ring = store_thm
14    ("num_semi_ring",
15     ��� is_semi_ring (semi_ring 0 1 $+ $* : num semi_ring) ���,
16RW_TAC arith_ss [ is_semi_ring_def, semi_ring_accessors,
17                  RIGHT_ADD_DISTRIB, MULT_ASSOC ] THEN
18MATCH_ACCEPT_TAC MULT_SYM);
19
20
21val num_ring_thms =
22  ringLib.store_ring { Name = "num", Theory = num_semi_ring };
23
24
25local open numeralTheory in
26val num_rewrites = save_thm("num_rewrites", LIST_CONJ
27  [ numeral_distrib, numeral_eq, numeral_suc, numeral_iisuc,
28    numeral_add, numeral_mult, iDUB_removal,
29    ISPEC ``arithmetic$ZERO`` REFL_CLAUSE, ISPEC ``num$0`` REFL_CLAUSE ]);
30end;
31
32
33(* Hack to avoid (semi_ring 0 1 $+ $* ) to be confused with an end
34 * of comment.                      ^^^
35 *)
36val _ = temp_overload_on("mult",���$* : num->num->num���);
37
38val _ = export_theory();
39