1structure fracUtils :> fracUtils =
2struct
3
4open HolKernel boolLib Parse bossLib;
5
6(* interactive mode
7app load ["pairTheory", "pairLib",
8        "integerTheory", "intLib",
9        "jbUtils"];
10*)
11
12open
13        pairTheory pairLib
14        integerTheory intLib
15        jbUtils;
16
17(*--------------------------------------------------------------------------
18 *  dest_frac : term -> term * term list
19 *--------------------------------------------------------------------------*)
20
21fun dest_frac (t1:term) =
22  if is_comb t1 then
23    let
24      val (top_rator, top_rand) = dest_comb t1
25    in
26      if top_rator ~~ ``abs_frac`` then
27        let
28          val (this_nmr, this_dnm) = dest_pair (top_rand);
29        in
30          (``abs_frac``,[this_nmr,this_dnm])
31        end
32      else
33        if top_rator ~~ ``frac_ainv`` orelse top_rator ~~ ``frac_minv`` orelse
34           top_rator ~~ ``rep_rat``
35        then
36          (top_rator, [top_rand])
37        else
38          let
39            val (this_op, this_first, this_second) = dest_binop_triple t1
40          in
41            (this_op, [this_first, this_second])
42          end
43    end
44  else (* t1 must be a variable *)
45    (t1,[])
46
47(* ---------- test cases ---------- *
48        dest_frac ``f1:frac``;
49        dest_frac ``abs_frac(3i,4i)``;
50        dest_frac ``frac_add f1 f2``;
51        dest_frac ``frac_add (frac_sub f1 f2) f3``;
52        dest_frac ``frac_add (abs_frac(3i,4i)) (abs_frac(4i,5i))``;
53 * ---------- test cases ---------- *)
54
55(*--------------------------------------------------------------------------
56 *  extract_frac : term -> term list
57 *--------------------------------------------------------------------------*)
58
59fun extract_frac (t1:term) = extract_terms_of_type ``:frac`` t1;
60
61(* ---------- test cases ---------- *
62        extract_frac ``4i + (frac_nmr(abs_frac(3i,4i))) = 3``;
63        extract_frac ``frac_add f1 f2 = sub f1 f2``;
64        extract_frac ``!f1 f2. nmr (frac_add f1 f2) = frac_dnm (frac_sub f1 f2)``;
65        extract_frac ``frac_nmr (frac_add f1 f2) = frac_dnm (frac_sub f1 f2)``;
66 * ---------- test cases ---------- *)
67
68(*--------------------------------------------------------------------------
69 *  extract_abs_frac : term -> term list
70 *--------------------------------------------------------------------------*)
71
72fun extract_abs_frac (t1:term) =
73  if is_comb t1 then
74    let
75      val (top_rator, top_rand) = dest_comb t1
76    in
77      if top_rator ~~ ``abs_frac`` then [t1]
78      else
79        op_union aconv (extract_abs_frac top_rator) (extract_abs_frac top_rand)
80    end
81  else
82    [];
83
84(* ---------- test cases ---------- *
85        extract_abs_frac ``abs_rat( abs_frac(1,2) ) + abs_rat (abs_frac(1,3) ) = abs_rat(abs_frac (5,6))``;
86        extract_abs_frac ``4i + (frac_nmr(abs_frac(3i,4i))) = 3``;
87        extract_abs_frac ``frac_nmr (abs_frac(4,frac_nmr(abs_frac(3,4))))``;
88 * ---------- test cases ---------- *)
89
90(*--------------------------------------------------------------------------
91 *  extract_frac_fun : term list -> term -> (term * term * term) list
92 *--------------------------------------------------------------------------*)
93
94fun ttrip_eq (t1,t2,t3) (ta,tb,tc) =
95  pair_eq (pair_eq aconv aconv) aconv ((t1,t2),t3) ((ta,tb),tc)
96
97fun extract_frac_fun (l2:term list) (t1:term) =
98  if is_comb t1 then
99    let
100      val (top_rator, top_rand) = dest_comb t1;
101    in
102      if tmem top_rator l2 andalso is_comb top_rand then
103        let
104          val (second_rator, second_rand) = dest_comb top_rand;
105        in
106          if second_rator ~~ ``abs_frac`` then
107            let
108              val (this_nmr, this_dnm) = dest_pair (second_rand)
109              val sub_fracs =
110                  op_union ttrip_eq
111                           (extract_frac_fun l2 this_nmr)
112                           (extract_frac_fun l2 this_dnm)
113            in
114                [(top_rator,this_nmr,this_dnm)] @ sub_fracs
115            end
116          else (* not second_rator = ``abs_frac`` *)
117            extract_frac_fun l2 top_rand
118        end
119      else (* not (top_rator = l2 andalso is_comb top_rand) *)
120        op_union ttrip_eq (extract_frac_fun l2 top_rator)
121                 (extract_frac_fun l2 top_rand)
122    end
123  else (* not is_comb t1 *)
124    [];
125
126(* ---------- test cases ---------- *
127        extract_frac_fun [``frac_nmr``] ``4i + (nmr(abs_frac(3i,4i)))``;
128        extract_frac_fun [``frac_nmr``] ``frac_add (abs_frac(4,frac_nmr(abs_frac(3,4)))) (abs_frac(3,4))``;
129        extract_frac_fun [``frac_nmr``] ``frac_nmr(abs_frac(3,4)) + frac_dnm(abs_frac(4,5))``;
130        extract_frac_fun [``frac_nmr``] ``frac_nmr (abs_frac(4,frac_nmr(abs_frac(3,4))))``;
131        extract_frac_fun [``frac_nmr``] ``frac_nmr (abs_frac(4,frac_nmr(abs_frac(3,4))))``;
132        extract_frac_fun [``frac_nmr``,``frac_dnm``] ``nmr(abs_frac(3,4)) + dnm(abs_frac(4,5))``;
133 * ---------- test cases ---------- *)
134
135(*--------------------------------------------------------------------------
136 *  INT_GT0_CONV : conv
137 *
138 *    t1          (with t1 greater than zero)
139 *   -----------
140 *    |- 0 < t1
141 *--------------------------------------------------------------------------*)
142
143fun INT_GT0_CONV (t1:term) =
144        EQT_ELIM (intLib.ARITH_CONV ``0 < ^t1``);
145
146(*==========================================================================
147 * end of structure
148 *==========================================================================*)
149end;
150