1(*===========================================================================*)
2(* Construct positive (nonzero) rationals from natural numbers               *)
3(*===========================================================================*)
4
5open HolKernel boolLib;
6infix THEN THENL ORELSE;
7
8(*
9app load ["hol88Lib",
10          "numLib",
11          "reduceLib",
12          "pairLib",
13          "arithmeticTheory",
14          "quotient",
15          "jrhUtils"];
16*)
17
18open Parse boolLib hol88Lib numLib reduceLib
19     pairLib PairedLambda pairTheory
20     arithmeticTheory numTheory prim_recTheory jrhUtils;
21
22val _ = new_theory "hrat";
23
24(*---------------------------------------------------------------------------*)
25(* The following tactic gets rid of "PRE"s by implicitly bubbling out "SUC"s *)
26(* from sums and products - more complex terms may leave extra subgoals.     *)
27(*---------------------------------------------------------------------------*)
28
29val UNSUCK_TAC =
30 let val tac = W(MAP_EVERY (STRUCT_CASES_TAC o C SPEC num_CASES) o frees o snd)
31               THEN REWRITE_TAC[NOT_SUC, PRE, MULT_CLAUSES, ADD_CLAUSES]
32     val [sps, azero, mzero] = map (C (curry prove) tac)
33       [���~(x = 0) ==> (SUC(PRE x) = x)���,
34        ���(x + y = 0) = (x = 0) /\ (y = 0)���,
35        ���(x * y = 0) = (x = 0) \/ (y = 0)���] in
36 REPEAT (IMP_SUBST_TAC sps THENL
37         [REWRITE_TAC[azero, mzero, NOT_SUC], ALL_TAC]) end;
38
39(*---------------------------------------------------------------------------*)
40(* Definitions of operations on representatives                              *)
41(*---------------------------------------------------------------------------*)
42
43val trat_1 = new_definition("trat_1",
44  ���trat_1 = (0,0)���);
45
46val trat_inv = new_definition("trat_inv",
47  ���trat_inv (x:num,(y:num)) = (y,x)���);
48
49val trat_add = new_infixl_definition("trat_add",
50  ���trat_add (x,y) (x',y') =
51    (PRE(((SUC x)*(SUC y')) + ((SUC x')*(SUC y))),
52     PRE((SUC y)*(SUC y')))���,
53    500);
54
55val trat_mul = new_infixl_definition("trat_mul",
56  ���trat_mul (x,y) (x',y') =
57    (PRE((SUC x)*(SUC x')),
58     PRE((SUC y)*(SUC y')))���, 600);
59
60val trat_sucint = new_recursive_definition
61  {name = "trat_sucint",
62   def = ���(trat_sucint 0 = trat_1) /\
63              (trat_sucint (SUC n) = (trat_sucint n) trat_add trat_1)���,
64   rec_axiom = num_Axiom}
65
66(*---------------------------------------------------------------------------*)
67(* Definition of the equivalence relation, and proof that it *is* one        *)
68(*---------------------------------------------------------------------------*)
69
70val trat_eq = new_definition("trat_eq",
71  ���trat_eq (x,y) (x',y') =
72    (SUC x * SUC y' = SUC x' * SUC y)���);
73val _ = temp_set_fixity "trat_eq" (Infix(NONASSOC, 450))
74
75val TRAT_EQ_REFL = store_thm("TRAT_EQ_REFL",
76  ���!p. p trat_eq p���,
77  GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_eq]
78  THEN REFL_TAC);
79
80val TRAT_EQ_SYM = store_thm("TRAT_EQ_SYM",
81  ���!p q. (p trat_eq q) = (q trat_eq p)���,
82  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_eq]
83  THEN CONV_TAC(RAND_CONV SYM_CONV) THEN REFL_TAC);
84
85val TRAT_EQ_TRANS = store_thm("TRAT_EQ_TRANS",
86  ���!p q r. p trat_eq q /\ q trat_eq r ==> p trat_eq r���,
87  let val th = (GEN_ALL o fst o EQ_IMP_RULE o SPEC_ALL) MULT_SUC_EQ in
88  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_eq] THEN
89  DISCH_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
90  MATCH_MP_TAC th THEN EXISTS_TAC ���SND(q:num#num)��� THEN
91  REWRITE_TAC[GSYM MULT_ASSOC] THEN
92  POP_ASSUM(CONJUNCTS_THEN2 SUBST1_TAC (SUBST1_TAC o SYM)) THEN
93  CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)) end);
94
95val TRAT_EQ_AP = store_thm("TRAT_EQ_AP",
96  ���!p q. (p = q) ==> (p trat_eq q)���,
97  REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
98  MATCH_ACCEPT_TAC TRAT_EQ_REFL);
99
100(*---------------------------------------------------------------------------*)
101(* Prove that the operations are all well-defined                            *)
102(*---------------------------------------------------------------------------*)
103
104val TRAT_ADD_SYM_EQ = store_thm("TRAT_ADD_SYM_EQ",
105  ���!h i. (h trat_add i) =(i trat_add h)���,
106  REPEAT GEN_PAIR_TAC THEN
107  PURE_REWRITE_TAC[trat_add, PAIR_EQ] THEN CONJ_TAC THEN
108  AP_TERM_TAC THEN TRY (MATCH_ACCEPT_TAC MULT_SYM) THEN
109  GEN_REWR_TAC RAND_CONV [ADD_SYM]
110  THEN REFL_TAC);
111
112val TRAT_MUL_SYM_EQ = store_thm("TRAT_MUL_SYM_EQ",
113  ���!h i. h trat_mul i = i trat_mul h���,
114  REPEAT GEN_PAIR_TAC THEN
115  PURE_REWRITE_TAC[trat_mul, PAIR_EQ] THEN CONJ_TAC THEN
116  AP_TERM_TAC THEN TRY (MATCH_ACCEPT_TAC MULT_SYM) THEN
117  GEN_REWR_TAC RAND_CONV [MULT_SYM] THEN REFL_TAC);
118
119val TRAT_INV_WELLDEFINED = store_thm("TRAT_INV_WELLDEFINED",
120  ���!p q. p trat_eq q ==> (trat_inv p) trat_eq (trat_inv q)���,
121  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_inv, trat_eq] THEN
122  DISCH_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
123  POP_ASSUM(ACCEPT_TAC o SYM));
124
125val TRAT_ADD_WELLDEFINED = store_thm("TRAT_ADD_WELLDEFINED",
126  ���!p q r. p trat_eq q ==> (p trat_add r) trat_eq (q trat_add r)���,
127  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_add, trat_eq] THEN DISCH_TAC
128  THEN UNSUCK_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN BINOP_TAC THENL
129   [REWRITE_TAC[MULT_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
130    POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
131    REWRITE_TAC[MULT_ASSOC] THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC,
132    CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM))]);
133
134val TRAT_ADD_WELLDEFINED2 = store_thm("TRAT_ADD_WELLDEFINED2",
135  ���!p1 p2 q1 q2. (p1 trat_eq p2) /\ (q1 trat_eq q2)
136        ==> (p1 trat_add q1) trat_eq (p2 trat_add q2)���,
137  REPEAT GEN_TAC THEN DISCH_TAC THEN
138  MATCH_MP_TAC TRAT_EQ_TRANS THEN
139  EXISTS_TAC ���p1 trat_add q2��� THEN
140  CONJ_TAC THENL [ONCE_REWRITE_TAC[TRAT_ADD_SYM_EQ], ALL_TAC] THEN
141  MATCH_MP_TAC TRAT_ADD_WELLDEFINED THEN ASM_REWRITE_TAC[]);
142
143val TRAT_MUL_WELLDEFINED = store_thm("TRAT_MUL_WELLDEFINED",
144  ���!p q r. p trat_eq q ==> (p trat_mul r) trat_eq (q trat_mul r)���,
145  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_eq, trat_mul] THEN DISCH_TAC
146  THEN UNSUCK_TAC THEN REWRITE_TAC[MULT_ASSOC] THEN AP_THM_TAC THEN
147  AP_TERM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
148  REWRITE_TAC[MULT_ASSOC] THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC);
149
150val TRAT_MUL_WELLDEFINED2 = store_thm("TRAT_MUL_WELLDEFINED2",
151  ���!p1 p2 q1 q2. (p1 trat_eq p2) /\ (q1 trat_eq q2)
152        ==> (p1 trat_mul q1) trat_eq (p2 trat_mul q2)���,
153  REPEAT GEN_TAC THEN DISCH_TAC THEN
154  MATCH_MP_TAC TRAT_EQ_TRANS THEN
155  EXISTS_TAC ���p1 trat_mul q2��� THEN
156  CONJ_TAC THENL [ONCE_REWRITE_TAC[TRAT_MUL_SYM_EQ], ALL_TAC] THEN
157  MATCH_MP_TAC TRAT_MUL_WELLDEFINED THEN ASM_REWRITE_TAC[]);
158
159(*---------------------------------------------------------------------------*)
160(* Now theorems for the representatives.                                     *)
161(*---------------------------------------------------------------------------*)
162
163val TRAT_ADD_SYM = store_thm("TRAT_ADD_SYM",
164  ���!h i. (h trat_add i) trat_eq (i trat_add h)���,
165  REPEAT GEN_TAC THEN MATCH_MP_TAC TRAT_EQ_AP THEN
166  MATCH_ACCEPT_TAC TRAT_ADD_SYM_EQ);
167
168val TRAT_ADD_ASSOC = store_thm("TRAT_ADD_ASSOC",
169  ���!h i j. (h trat_add (i trat_add j)) trat_eq ((h trat_add i) trat_add j)���,
170  REPEAT GEN_PAIR_TAC THEN  MATCH_MP_TAC TRAT_EQ_AP THEN
171  PURE_REWRITE_TAC[trat_add]
172  THEN UNSUCK_TAC THEN REWRITE_TAC[PAIR_EQ, GSYM MULT_ASSOC,
173    GSYM ADD_ASSOC, RIGHT_ADD_DISTRIB] THEN REPEAT AP_TERM_TAC THEN
174  CONV_TAC(DEPTH_CONV(SYM_CANON_CONV MULT_SYM
175   (fn (a,b) => fst(dest_var(rand(rand a))) < fst(dest_var(rand(rand b))))
176  )) THEN REFL_TAC);
177
178val TRAT_MUL_SYM = store_thm("TRAT_MUL_SYM",
179  ���!h i. ($trat_mul h i) trat_eq ($trat_mul i h)���,
180  REPEAT GEN_TAC THEN MATCH_MP_TAC TRAT_EQ_AP THEN
181  MATCH_ACCEPT_TAC TRAT_MUL_SYM_EQ);
182
183val TRAT_MUL_ASSOC = store_thm("TRAT_MUL_ASSOC",
184  ���!h i j. ($trat_mul h ($trat_mul i j)) trat_eq ($trat_mul ($trat_mul h i) j)���,
185  REPEAT GEN_PAIR_TAC THEN MATCH_MP_TAC TRAT_EQ_AP THEN
186  PURE_REWRITE_TAC[trat_mul] THEN
187  UNSUCK_TAC THEN REWRITE_TAC[PAIR_EQ, MULT_ASSOC]);
188
189val TRAT_LDISTRIB = store_thm("TRAT_LDISTRIB",
190  ���!h i j. ($trat_mul h ($trat_add i j)) trat_eq
191              ($trat_add ($trat_mul h i) ($trat_mul h j))���,
192  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_mul, trat_add, trat_eq] THEN
193  UNSUCK_TAC THEN REWRITE_TAC[LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB]
194  THEN BINOP_TAC THEN CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));
195
196val TRAT_MUL_LID = store_thm("TRAT_MUL_LID",
197  ���!h. ($trat_mul trat_1 h) trat_eq h���,
198  GEN_PAIR_TAC THEN MATCH_MP_TAC TRAT_EQ_AP THEN
199  PURE_REWRITE_TAC[trat_1, trat_mul] THEN
200  REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES, PRE]);
201
202val TRAT_MUL_LINV = store_thm("TRAT_MUL_LINV",
203  ���!h. ($trat_mul (trat_inv h) h) trat_eq trat_1���,
204  GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_1, trat_inv, trat_mul, trat_eq]
205  THEN UNSUCK_TAC THEN CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));
206
207val TRAT_NOZERO = store_thm("TRAT_NOZERO",
208  ���!h i. ~(($trat_add h i) trat_eq h)���,
209  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_add, trat_eq] THEN
210  UNSUCK_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB, GSYM MULT_ASSOC] THEN
211  GEN_REWR_TAC (funpow 3 RAND_CONV) [MULT_SYM] THEN
212  REWRITE_TAC[ADD_INV_0_EQ] THEN
213  REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES, NOT_SUC]);
214
215val TRAT_ADD_TOTAL = store_thm("TRAT_ADD_TOTAL",
216  ���!h i. (h trat_eq i) \/
217         (?d. h trat_eq (i trat_add d)) \/
218         (?d. i trat_eq (h trat_add d))���,
219  REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[trat_eq, trat_add] THEN
220  W(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC o C SPECL LESS_LESS_CASES o
221    snd o strip_comb o find_term is_eq o snd) THEN
222  PURE_ASM_REWRITE_TAC[] THEN TRY(DISJ1_TAC THEN REFL_TAC) THEN DISJ2_TAC
223  THENL [DISJ2_TAC, DISJ1_TAC] THEN POP_ASSUM(X_CHOOSE_TAC ���p:num��� o
224  REWRITE_RULE[GSYM ADD1] o MATCH_MP LESS_ADD_1) THEN
225  EXISTS_TAC ���(p:num,PRE(SUC(SND(h:num#num)) * SUC(SND(i:num#num))))��� THEN
226  PURE_REWRITE_TAC[trat_add, trat_eq] THEN UNSUCK_TAC THEN
227  REWRITE_TAC[MULT_ASSOC] THEN POP_ASSUM SUBST1_TAC THEN
228  REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN BINOP_TAC THEN
229  CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));
230
231val TRAT_SUCINT_0 = store_thm("TRAT_SUCINT_0",
232���!n. (trat_sucint n) trat_eq (n,0)���,
233INDUCT_TAC THEN REWRITE_TAC[trat_sucint, trat_1, TRAT_EQ_REFL] THEN
234  MATCH_MP_TAC TRAT_EQ_TRANS THEN EXISTS_TAC ���(n,0) trat_add (0,0)��� THEN
235  CONJ_TAC THENL
236   [MATCH_MP_TAC TRAT_ADD_WELLDEFINED THEN POP_ASSUM ACCEPT_TAC,
237    REWRITE_TAC[trat_add, trat_eq] THEN UNSUCK_TAC THEN
238    (* for new term nets  REWRITE_TAC[SYM(num_CONV ���1���)] *)
239    REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES]]);
240
241(* Proof changed for new term nets *)
242val TRAT_ARCH = store_thm("TRAT_ARCH",
243���!h. ?n. ?d. (trat_sucint n) trat_eq (h trat_add d)���,
244 GEN_PAIR_TAC THEN EXISTS_TAC ���SUC(FST(h:num#num))��� THEN
245  EXISTS_TAC���(PRE((SUC(SUC(FST h))*(SUC(SND h))) - (SUC(FST h))),SND h)���
246  THEN MATCH_MP_TAC TRAT_EQ_TRANS THEN
247  EXISTS_TAC ���(SUC(FST(h:num#num)),0)���
248  THEN PURE_REWRITE_TAC[TRAT_SUCINT_0] THEN PURE_REWRITE_TAC[trat_add, trat_eq]
249  THEN REWRITE_TAC[] THEN UNSUCK_TAC THENL
250   [REWRITE_TAC[SUB_EQ_0, GSYM NOT_LESS],
251    REWRITE_TAC [RIGHT_SUB_DISTRIB,
252        RIGHT_ADD_DISTRIB,SYM(num_CONV ���1���), MULT_RIGHT_1] THEN
253    ONCE_REWRITE_TAC[ADD_SYM] THEN IMP_SUBST_TAC SUB_ADD THEN
254    REWRITE_TAC[MULT_ASSOC] THEN MATCH_MP_TAC LESS_MONO_MULT THEN
255   MATCH_MP_TAC LESS_IMP_LESS_OR_EQ] THEN
256  W(C (curry SPEC_TAC) ���x:num��� o rand o rator o snd) THEN GEN_TAC THEN
257  REWRITE_TAC [MULT_SUC,GSYM ADD_ASSOC,ADD1] THEN
258  MATCH_MP_TAC LESS_ADD_NONZERO THEN
259  REWRITE_TAC[ADD_CLAUSES, NOT_SUC, ONCE_REWRITE_RULE[ADD_SYM] (GSYM ADD1)]);
260
261(* original
262  REWRITE_TAC[MULT_CLAUSES, GSYM ADD_ASSOC] THEN MATCH_MP_TAC LESS_ADD_NONZERO
263  THEN REWRITE_TAC[ADD_CLAUSES, NOT_SUC]
264*)
265val TRAT_SUCINT = store_thm("TRAT_SUCINT",
266  ���((trat_sucint 0) trat_eq trat_1) /\
267   (!n. (trat_sucint(SUC n)) trat_eq ((trat_sucint n) trat_add trat_1))���,
268  CONJ_TAC THEN TRY GEN_TAC THEN MATCH_MP_TAC TRAT_EQ_AP THEN
269  REWRITE_TAC[trat_sucint]);
270
271(*---------------------------------------------------------------------------*)
272(* Define type of and functions over the equivalence classes                 *)
273(*---------------------------------------------------------------------------*)
274
275val TRAT_EQ_EQUIV = store_thm("TRAT_EQ_EQUIV",
276  ���!p q. p trat_eq q = ($trat_eq p = $trat_eq q)���,
277  REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
278  CONV_TAC (ONCE_DEPTH_CONV (X_FUN_EQ_CONV ���r:num#num���)) THEN
279  EQ_TAC THENL
280     [DISCH_THEN(MP_TAC o SPEC ���q:num#num���) THEN
281      REWRITE_TAC[TRAT_EQ_REFL],
282      DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL
283       [RULE_ASSUM_TAC(ONCE_REWRITE_RULE[TRAT_EQ_SYM]), ALL_TAC] THEN
284      POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
285      MATCH_ACCEPT_TAC TRAT_EQ_TRANS]);
286
287val [HRAT_ADD_SYM, HRAT_ADD_ASSOC, HRAT_MUL_SYM, HRAT_MUL_ASSOC,
288     HRAT_LDISTRIB, HRAT_MUL_LID, HRAT_MUL_LINV, HRAT_NOZERO,
289     HRAT_ADD_TOTAL, HRAT_ARCH, HRAT_SUCINT] =
290  quotient.define_equivalence_type
291    {name = "hrat",
292     equiv = TRAT_EQ_EQUIV, defs =
293     [{def_name="hrat_1",   fname="hrat_1",
294       func=Term`trat_1`, fixity=NONE},
295      {def_name="hrat_inv", fname="hrat_inv",
296       func=Term`trat_inv`, fixity=NONE},
297      {def_name="hrat_add", fname="hrat_add",
298       func=Term`$trat_add`, fixity=SOME(Infixl 500)},
299      {def_name="hrat_mul", fname="hrat_mul",
300       func=Term`$trat_mul`, fixity=SOME(Infixl 600)},
301      {def_name="hrat_sucint", fname="hrat_sucint",
302       func=Term`trat_sucint`, fixity=NONE}],
303     welldefs = [TRAT_INV_WELLDEFINED, TRAT_ADD_WELLDEFINED2,
304                 TRAT_MUL_WELLDEFINED2],
305     old_thms = [TRAT_ADD_SYM, TRAT_ADD_ASSOC, TRAT_MUL_SYM, TRAT_MUL_ASSOC,
306                 TRAT_LDISTRIB, TRAT_MUL_LID, TRAT_MUL_LINV, TRAT_NOZERO,
307                 TRAT_ADD_TOTAL, TRAT_ARCH, TRAT_SUCINT]};
308
309(*---------------------------------------------------------------------------*)
310(* Save theorems and make sure they are all of the right form                *)
311(*---------------------------------------------------------------------------*)
312
313val HRAT_ADD_SYM = store_thm("HRAT_ADD_SYM",
314  ���!h i. h hrat_add i = i hrat_add h���,
315  MATCH_ACCEPT_TAC HRAT_ADD_SYM);
316
317val HRAT_ADD_ASSOC = store_thm("HRAT_ADD_ASSOC",
318  ���!h i j. h hrat_add (i hrat_add j) = (h hrat_add i) hrat_add j���,
319  MATCH_ACCEPT_TAC HRAT_ADD_ASSOC);
320
321val HRAT_MUL_SYM = store_thm("HRAT_MUL_SYM",
322  ���!h i. h hrat_mul i = i hrat_mul h���,
323  MATCH_ACCEPT_TAC HRAT_MUL_SYM);
324
325val HRAT_MUL_ASSOC = store_thm("HRAT_MUL_ASSOC",
326  ���!h i j. h hrat_mul (i hrat_mul j) = (h hrat_mul i) hrat_mul j���,
327  MATCH_ACCEPT_TAC HRAT_MUL_ASSOC);
328
329val HRAT_LDISTRIB = store_thm("HRAT_LDISTRIB",
330  ���!h i j. h hrat_mul (i hrat_add j) = (h hrat_mul i) hrat_add (h hrat_mul j)���,
331  MATCH_ACCEPT_TAC HRAT_LDISTRIB);
332
333val HRAT_MUL_LID = store_thm("HRAT_MUL_LID",
334  ���!h. hrat_1 hrat_mul h = h���,
335  MATCH_ACCEPT_TAC HRAT_MUL_LID);
336
337val HRAT_MUL_LINV = store_thm("HRAT_MUL_LINV",
338  ���!h. (hrat_inv h) hrat_mul h = hrat_1���,
339  MATCH_ACCEPT_TAC HRAT_MUL_LINV);
340
341val HRAT_NOZERO = store_thm("HRAT_NOZERO",
342  ���!h i. ~(h hrat_add i = h)���,
343  MATCH_ACCEPT_TAC HRAT_NOZERO);
344
345val HRAT_ADD_TOTAL = store_thm("HRAT_ADD_TOTAL",
346  ���!h i. (h = i) \/ (?d. h = i hrat_add d) \/ (?d. i = h hrat_add d)���,
347  MATCH_ACCEPT_TAC HRAT_ADD_TOTAL);
348
349val HRAT_ARCH = store_thm("HRAT_ARCH",
350  ���!h. ?n d. hrat_sucint n = h hrat_add d���,
351  MATCH_ACCEPT_TAC HRAT_ARCH);
352
353val HRAT_SUCINT = store_thm("HRAT_SUCINT",
354  ���((hrat_sucint 0) = hrat_1) /\
355   (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1)���,
356  MATCH_ACCEPT_TAC HRAT_SUCINT);
357
358val _ = export_theory();
359