EVAL_numRingScript.sml

1(*
2load "ringLib";
3load "numeralTheory";
4load "bossLib";
5*)
6Theory EVAL_numRing
7Ancestors
8  arithmetic EVAL_semiring
9
10(* num is a semi-ring: *)
11Theorem num_semi_ring:
12       is_semi_ring (semi_ring 0 1 $+ $* : num semi_ring)
13Proof
14RW_TAC arith_ss [ is_semi_ring_def, semi_ring_accessors,
15                  RIGHT_ADD_DISTRIB, MULT_ASSOC ] THEN
16MATCH_ACCEPT_TAC MULT_SYM
17QED
18
19
20val num_ring_thms =
21  EVAL_ringLib.store_ring { Name = "num", Theory = num_semi_ring };
22
23
24local open numeralTheory in
25val num_rewrites = save_thm("num_rewrites", LIST_CONJ
26  [ numeral_distrib, numeral_eq, numeral_suc, numeral_iisuc,
27    numeral_add, numeral_mult, iDUB_removal,
28    ISPEC ``arithmetic$ZERO`` REFL_CLAUSE, ISPEC ``num$0`` REFL_CLAUSE ]);
29end;
30
31