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