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