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