1structure ratRingLib :> ratRingLib = 2struct 3 4open HolKernel Parse boolLib; 5 6(* interactive mode 7app load ["ringLib","ratTheory","ratRingTheory","ratLib"] 8*) 9 10open ringLib ratTheory ratRingTheory ratSyntax ratLib; 11 12(*-------------------------------------------------------------------------- 13 * is_computable_frac, is_computable_rat 14 *--------------------------------------------------------------------------*) 15 16fun is_computable_frac t = 17 memt [``frac_0``,``frac_1``] t orelse 18 ((is_comb t) andalso (is_comb (rator t))) andalso 19 let 20 val rator_tm = rator (rator t); 21 val nmr_tm = rand (rator t); 22 val dnm_tm = rand t; 23 in 24 (rator_tm~~``frac_save``) andalso (intSyntax.is_int_literal nmr_tm) andalso (numSyntax.is_numeral dnm_tm) 25 end; 26 27fun is_computable_rat t = 28 memt [``rat_0``,``rat_1``] t orelse 29 (* ((is_comb t) andalso (rator t)=``rat_of_num``) andalso (numSyntax.is_numeral (rand t)) orelse *) 30 ((is_comb t) andalso (rator t)~~``abs_rat``) andalso (is_computable_frac (rand t)); 31 32(* test cases: 33is_computable_rat ``abs_rat f1`` 34is_computable_rat ``abs_rat frac_1`` 35is_computable_rat ``abs_rat (abs_frac(3,4))`` 36is_computable_rat ``abs_rat (frac_save 3 3)``*) 37 38(*-------------------------------------------------------------------------- 39 * ring declaration 40 *--------------------------------------------------------------------------*) 41 42val _ = ringLib.declare_ring 43 { RingThm = rat_ring_thms, 44 IsConst = is_computable_rat, 45 Rewrites = (ratLib.int_rewrites @ ratLib.rat_rewrites) }; 46 47(*-------------------------------------------------------------------------- 48 * define ring conversions, tactics and rules 49 *--------------------------------------------------------------------------*) 50 51val PRE_CONV = RAT_PRECALC_CONV; 52val POST_CONV = RAT_POSTCALC_CONV; 53 54val RAT_RING_NORM_CONV = PRE_CONV THENC ringLib.RING_NORM_CONV THENC POST_CONV; 55val RAT_RING_CONV = PRE_CONV THENC ringLib.RING_CONV THENC POST_CONV; 56 57val RAT_RING_NORM_TAC = CONV_TAC RAT_RING_NORM_CONV; 58val RAT_RING_TAC = CONV_TAC RAT_RING_CONV; 59 60val RAT_RING_NORM_RULE = CONV_RULE RAT_RING_NORM_CONV; 61val RAT_RING_RULE = CONV_RULE RAT_RING_CONV; 62 63(*========================================================================== 64 * end of structure 65 *==========================================================================*) 66end; 67