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