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