totoScript.sml
1(* file HS/FIN/totoScript.sml, created 12/21-30/09 as TotOrdScript, L. Morris *)
2(* Revised to make part of efficient-set-represetation project Feb.14 2012 *)
3(* Revised for PIN directory April 14 2013; revised for intto Sept 23 2013 *)
4(* Revised to narrow interface with wotTheory Sept 27 2013. *)
5
6(* ****************************************************************** *)
7(* Basic theory of total orders modeled not as in relation theory, but *)
8(* rather in imitation of ML's facilities stemming from the 3-element *)
9(* "order" type - here called "cpn" for "comparison". It is believed *)
10(* that total orders done this way will lead to more efficient *)
11(* conversions implementing the common algorithms and data structures *)
12(* based on a total order. *)
13(* ****************************************************************** *)
14
15Theory toto
16Ancestors
17 pred_set relation pair arithmetic numeral string list
18 ternaryComparisons[qualified] set_relation[qualified]
19Libs
20 pred_setLib PairRules Defn
21
22
23val _ = set_trace "Unicode" 0;
24val _ = ParseExtras.temp_loose_equality()
25(* My habitual abbreviations: *)
26
27Type reln = “:'a -> 'a -> bool”
28
29val AR = ASM_REWRITE_TAC [];
30fun ulist x = [x];
31
32Theorem StrongLinearOrderExists:
33 ?R:'a reln. StrongLinearOrder R
34Proof
35 ‘StrongOrder (REMPTY : 'a reln)’
36 by simp[StrongOrder, irreflexive_def, transitive_def] >>
37 drule set_relationTheory.StrongOrder_extends_to_StrongLinearOrder >>
38 simp[]
39QED
40
41(* Define cpn: *)
42
43val cpn_distinct = TypeBase.distinct_of ``:ordering``
44(* |- LESS <> EQUAL /\ LESS <> GREATER /\ EQUAL <> GREATER *)
45
46val cpn_case_def = TypeBase.case_def_of ``:ordering``
47
48(* cpn_case_def =
49|- (!v0 v1 v2. (case LESS of LESS => v0 | EQUAL => v1 | GREATER => v2) = v0) /\
50 (!v0 v1 v2. (case EQUAL of LESS => v0 | EQUAL => v1 | GREATER => v2) = v1) /\
51 !v0 v1 v2. (case GREATER of LESS => v0 | EQUAL => v1 | GREATER => v2) = v2 *)
52
53val cpn_nchotomy = TypeBase.nchotomy_of ``:ordering``
54
55(* Define being a (cpn-valued) total order: *)
56
57Type cpn = ``:ordering``
58Type comp = “:'a->'a->cpn”
59
60Definition TotOrd: TotOrd (c: 'a comp) =
61 (!x y. (c x y = EQUAL) <=> (x = y)) /\
62 (!x y. (c x y = GREATER) <=> (c y x = LESS)) /\
63 (!x y z. (c x y = LESS) /\ (c y z = LESS) ==> (c x z = LESS))
64End
65
66Definition TO_of_LinearOrder:
67 TO_of_LinearOrder (r:'a->'a->bool) x y =
68 if x = y then EQUAL else if r x y then LESS
69 else GREATER
70End
71
72(* lemma to ease use of "trichotomous" and work with disjunctions *)
73
74Theorem trichotomous_ALT: !R:'a->'a->bool.
75 trichotomous R <=> !x y. ~R x y /\ ~R y x ==> (x = y)
76Proof
77REWRITE_TAC [trichotomous, IMP_DISJ_THM, DE_MORGAN_THM, GSYM DISJ_ASSOC]
78QED
79
80Theorem TotOrd_TO_of_LO: !r:'a->'a->bool.
81 LinearOrder r ==> TotOrd (TO_of_LinearOrder r)
82Proof
83SRW_TAC [] [LinearOrder, Order, antisymmetric_def,
84 transitive_def, TO_of_LinearOrder, TotOrd, trichotomous_ALT] THEN
85METIS_TAC [cpn_distinct]
86QED
87
88(* Utility theorem for equality of pairs: *)
89
90Theorem SPLIT_PAIRS:
91 !x y:'a#'b. (x = y) <=> (FST x = FST y) /\ (SND x = SND y)
92Proof
93REPEAT GEN_TAC THEN
94CONV_TAC (LAND_CONV (BINOP_CONV (REWR_CONV (GSYM PAIR)))) THEN
95REWRITE_TAC [PAIR_EQ]
96QED
97
98(* cpn_nchotomy = |- !a. (a = LESS) \/ (a = EQUAL) \/ (a = GREATER) *)
99
100(* cpn_distinct |- LESS <> EQUAL /\ LESS <> GREATER /\ EQUAL <> GREATER *)
101
102Theorem all_cpn_distinct =
103CONJ cpn_distinct (GSYM cpn_distinct);
104
105(* We now follow boilerplate from S-K Chin, aclFoundationScript *)
106
107Theorem TO_exists: ?x:'a comp. TotOrd x
108Proof
109STRIP_ASSUME_TAC StrongLinearOrderExists THEN
110Q.EXISTS_TAC `TO_of_LinearOrder R` THEN
111MATCH_MP_TAC TotOrd_TO_of_LO THEN
112METIS_TAC [StrongLinearOrder, LinearOrder, StrongOrd_Ord]
113QED
114
115val toto_type_definition = new_type_definition ("toto", TO_exists);
116(* toto_type_definition =
117|- ?(rep :'x toto -> 'x comp). TYPE_DEFINITION (TotOrd :'x comp -> bool) rep*)
118
119(* but we call the representation function "apto", rather than rep_anything,
120 because we always need it when applying an a' toto to arguments. *)
121
122val to_bij = define_new_type_bijections
123 {name="to_bij", ABS="TO", REP="apto", tyax=toto_type_definition};
124
125local val [TO_apto_ID, TO_apto_TO_ID] = CONJUNCTS to_bij in
126Theorem TO_apto_ID = TO_apto_ID
127Theorem TO_apto_TO_ID = TO_apto_TO_ID;
128end
129
130(* TO_apto_ID = |- !(a :'x toto). TO (apto a) = a : thm
131 TO_apto_TO_ID = |- !(r :'x comp). TotOrd r <=> (apto (TO r) = r) *)
132
133Theorem TO_11 = prove_abs_fn_one_one to_bij;
134
135(* TO_11 = |- !(r :'x comp) (r' :'x comp).
136 TotOrd r ==> TotOrd r' ==> ((TO r = TO r') <=> (r = r')) *)
137
138Theorem onto_apto = prove_rep_fn_onto to_bij;
139
140(* onto_apto = |- !(r :'x comp). TotOrd r <=> ?(a :'x toto). r = apto a *)
141
142Theorem TO_onto = prove_abs_fn_onto to_bij;
143
144(* TO_onto = |- !(a :'x toto). ?(r :'x comp). (a = TO r) /\ TotOrd r *)
145
146(* With introduction of 'a toto, we should now have "... c:'a toto ..."
147 wherever was previously "TotOrd (c:'a comp) ==> ... c ... . *)
148
149Theorem TotOrd_apto: !c:'a toto. TotOrd (apto c)
150Proof
151GEN_TAC THEN MATCH_MP_TAC (CONJUNCT2 (ISPEC (Term`apto (c:'a toto)`)
152 (REWRITE_RULE [EQ_IMP_THM] onto_apto))) THEN
153EXISTS_TAC (Term`c:'a toto`) THEN REFL_TAC
154QED
155
156Theorem TO_apto_TO_IMP =
157GEN_ALL (fst (EQ_IMP_RULE (SPEC_ALL TO_apto_TO_ID)));
158
159(* TO_apto_TO_IMP = |- !r. TotOrd r ==> (apto (TO r) = r) *)
160
161Theorem toto_thm: !c:'a toto. (!x y. (apto c x y = EQUAL) <=> (x = y)) /\
162 (!x y. (apto c x y = GREATER) <=> (apto c y x = LESS)) /\
163(!x y z. (apto c x y = LESS) /\ (apto c y z = LESS) ==> (apto c x z = LESS))
164Proof
165MATCH_ACCEPT_TAC (REWRITE_RULE [TotOrd] TotOrd_apto)
166QED
167
168Theorem TO_equal_eq:
169!c:'a comp. TotOrd c ==> (!x y. (c x y = EQUAL) <=> (x = y))
170Proof
171REWRITE_TAC [TotOrd] THEN REPEAT STRIP_TAC THEN AR
172QED
173
174Theorem toto_equal_eq:
175!c:'a toto x y. (apto c x y = EQUAL) <=> (x = y)
176Proof
177REWRITE_TAC [toto_thm]
178QED
179
180Theorem toto_equal_imp_eq:
181!c:'a toto x y. (apto c x y = EQUAL) ==> (x = y)
182Proof
183REWRITE_TAC [toto_equal_eq]
184QED
185
186Theorem TO_refl:
187!c:'a comp. TotOrd c ==> (!x. c x x = EQUAL)
188Proof
189REPEAT STRIP_TAC THEN
190IMP_RES_THEN (MATCH_MP_TAC o snd o EQ_IMP_RULE o SPEC_ALL) TO_equal_eq THEN
191REFL_TAC
192QED
193
194Theorem toto_refl:
195!c:'a toto x. apto c x x = EQUAL
196Proof
197REWRITE_TAC [toto_thm]
198QED
199
200Theorem toto_equal_sym:
201!c:'a toto x y. (apto c x y = EQUAL) <=> (apto c y x = EQUAL)
202Proof
203REWRITE_TAC [toto_equal_eq] THEN MATCH_ACCEPT_TAC EQ_SYM_EQ
204QED
205
206Theorem TO_antisym:
207!c:'a comp. TotOrd c ==> (!x y. (c x y = GREATER) <=> (c y x = LESS))
208Proof
209REWRITE_TAC [TotOrd] THEN REPEAT STRIP_TAC THEN AR
210QED
211
212Theorem toto_antisym:
213!c:'a toto x y. (apto c x y = GREATER) <=> (apto c y x = LESS)
214Proof
215REWRITE_TAC [toto_thm]
216QED
217
218Theorem toto_not_less_refl:
219 !cmp:'a toto h. (apto cmp h h = LESS) <=> F
220Proof
221SRW_TAC [] [toto_antisym, toto_refl]
222QED
223
224Theorem toto_swap_cases:
225!c:'a toto x y. apto c y x =
226 case apto c x y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS
227Proof
228REPEAT GEN_TAC THEN Cases_on `apto c x y` THEN
229REWRITE_TAC [cpn_case_def] THENL
230[IMP_RES_TAC toto_antisym
231,IMP_RES_TAC toto_equal_sym
232,IMP_RES_TAC toto_antisym]
233QED
234
235Theorem toto_glneq: (!c x y:'a. (apto c x y = LESS) ==> x <> y) /\
236 (!c x y:'a. (apto c x y = GREATER) ==> x <> y)
237Proof
238CONJ_TAC THEN REPEAT GEN_TAC THEN
239SUBST1_TAC (SYM (SPEC_ALL toto_equal_eq)) THEN
240DISCH_TAC THEN ASM_REWRITE_TAC [all_cpn_distinct]
241QED
242
243Theorem toto_cpn_eqn = CONJ toto_equal_imp_eq toto_glneq;
244
245(* toto_cpn_eqn = |- (!c x y. (apto c x y = EQUAL) ==> (x = y)) /\
246 (!c x y. (apto c x y = LESS) ==> x <> y) /\
247 !c x y. (apto c x y = GREATER) ==> x <> y *)
248
249Theorem TO_cpn_eqn: !c. TotOrd c ==> (!x y:'a. (c x y = LESS) ==> x <> y) /\
250 (!x y:'a. (c x y = GREATER) ==> x <> y) /\
251 (!x y:'a. (c x y = EQUAL) ==> (x = y))
252Proof
253GEN_TAC THEN DISCH_TAC THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
254IMP_RES_THEN (SUBST1_TAC o SYM o SPEC_ALL) TO_equal_eq THEN
255DISCH_TAC THEN ASM_REWRITE_TAC [all_cpn_distinct]
256QED
257
258Theorem NOT_EQ_LESS_IMP:
259 !cmp:'a toto x y. apto cmp x y <> LESS ==> (x = y) \/ (apto cmp y x = LESS)
260Proof
261METIS_TAC [cpn_nchotomy, toto_equal_eq, toto_antisym]
262QED
263
264(* Seven forms of transitivity: *)
265
266Theorem totoEEtrans: !c:'a toto x y z.
267 ((apto c x y = EQUAL) /\ (apto c y z = EQUAL) ==> (apto c x z = EQUAL)) /\
268 ((apto c x y = EQUAL) /\ (apto c z y = EQUAL) ==> (apto c x z = EQUAL))
269Proof
270REPEAT GEN_TAC THEN REWRITE_TAC [toto_equal_eq] THEN REPEAT STRIP_TAC THEN AR
271QED
272
273Theorem totoLLtrans: !c:'a toto x y z.
274 (apto c x y = LESS) /\ (apto c y z = LESS) ==> (apto c x z = LESS)
275Proof
276REWRITE_TAC [toto_thm]
277QED
278
279Theorem totoLGtrans: !c:'a toto x y z.
280 (apto c x y = LESS) /\ (apto c z y = GREATER) ==> (apto c x z = LESS)
281Proof
282REPEAT STRIP_TAC THEN IMP_RES_TAC toto_antisym THEN IMP_RES_TAC totoLLtrans
283QED
284
285Theorem totoGGtrans: !c:'a toto x y z.
286 (apto c y x = GREATER) /\ (apto c z y = GREATER) ==> (apto c x z = LESS)
287Proof
288REPEAT STRIP_TAC THEN IMP_RES_TAC toto_antisym THEN IMP_RES_TAC totoLLtrans
289QED
290
291Theorem totoGLtrans: !c:'a toto x y z.
292 (apto c y x = GREATER) /\ (apto c y z = LESS) ==> (apto c x z = LESS)
293Proof
294REPEAT STRIP_TAC THEN IMP_RES_TAC toto_antisym THEN IMP_RES_TAC totoLLtrans
295QED
296
297Theorem totoLEtrans: !c:'a toto x y z.
298 (apto c x y = LESS) /\ (apto c y z = EQUAL) ==> (apto c x z = LESS)
299Proof
300REWRITE_TAC [toto_equal_eq] THEN
301PURE_ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN AR
302QED
303
304Theorem totoELtrans: !c:'a toto x y z.
305 (apto c x y = EQUAL) /\ (apto c y z = LESS) ==> (apto c x z = LESS)
306Proof
307REWRITE_TAC [toto_equal_eq] THEN REPEAT STRIP_TAC THEN AR
308QED
309
310Theorem toto_trans_less =
311 CONJ totoLLtrans (CONJ totoLGtrans (CONJ totoGGtrans
312 (CONJ totoGLtrans (CONJ totoLEtrans totoELtrans))));
313
314Definition WeakLinearOrder_of_TO:
315 WeakLinearOrder_of_TO (c:'a comp) x y =
316 case c x y of LESS => T | EQUAL => T | GREATER => F
317End
318
319Definition StrongLinearOrder_of_TO:
320 StrongLinearOrder_of_TO (c:'a comp) x y =
321 case c x y of LESS => T | EQUAL => F | GREATER => F
322End
323
324(* TO_of_LinearOrder is defined in totoTheory. *)
325
326Definition toto_of_LinearOrder:
327 toto_of_LinearOrder (r:'a reln) = TO (TO_of_LinearOrder r)
328End
329
330Theorem Weak_Weak_of:
331!c:'a toto. WeakLinearOrder (WeakLinearOrder_of_TO (apto c))
332Proof
333REPEAT STRIP_TAC THEN
334REWRITE_TAC [WeakLinearOrder, WeakOrder, reflexive_def, antisymmetric_def,
335 transitive_def, trichotomous, WeakLinearOrder_of_TO] THEN
336REPEAT CONJ_TAC THEN REPEAT GEN_TAC THENL
337[REWRITE_TAC [toto_refl, cpn_case_def]
338,Cases_on `apto c x y` THENL
339 [IMP_RES_TAC toto_antisym THEN ASM_REWRITE_TAC [cpn_case_def]
340 ,IMP_RES_TAC toto_equal_eq THEN AR
341 ,IMP_RES_TAC toto_antisym THEN ASM_REWRITE_TAC [cpn_case_def]
342 ]
343,Cases_on `apto c x y` THEN REWRITE_TAC [cpn_case_def] THENL
344 [Cases_on `apto c y z` THEN REWRITE_TAC [cpn_case_def] THENL
345 [IMP_RES_TAC totoLLtrans THEN ASM_REWRITE_TAC [cpn_case_def]
346 ,IMP_RES_TAC totoLEtrans THEN ASM_REWRITE_TAC [cpn_case_def]
347 ]
348 ,Cases_on `apto c y z` THEN REWRITE_TAC [cpn_case_def] THENL
349 [IMP_RES_TAC totoELtrans THEN ASM_REWRITE_TAC [cpn_case_def]
350 ,IMP_RES_TAC toto_equal_eq THEN ASM_REWRITE_TAC [toto_refl, cpn_case_def]
351 ]]
352,Cases_on `apto c a b` THEN IMP_RES_TAC toto_antisym THEN
353 IMP_RES_TAC toto_equal_sym THEN ASM_REWRITE_TAC [cpn_case_def]
354]
355QED
356
357Theorem STRORD_SLO: !R:'a reln.
358 WeakLinearOrder R ==> StrongLinearOrder (STRORD R)
359Proof
360RW_TAC bool_ss [WeakLinearOrder, StrongLinearOrder, trichotomous_STRORD] THEN
361METIS_TAC [WeakOrd_Ord, STRORD_Strong]
362QED
363
364Theorem Strongof_toto_STRORD: !c:'a toto.
365StrongLinearOrder_of_TO (apto c) = STRORD (WeakLinearOrder_of_TO (apto c))
366Proof
367REPEAT STRIP_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
368REWRITE_TAC [StrongLinearOrder_of_TO, STRORD, WeakLinearOrder_of_TO] THEN
369Cases_on `apto c x x'` THEN ASM_REWRITE_TAC [cpn_case_def] THEN
370ONCE_REWRITE_TAC [GSYM toto_equal_eq] THEN ASM_REWRITE_TAC [cpn_distinct]
371QED
372
373(* Previous three theorems all to avoid duplicating the Weak_Weak_of
374 proof for Strong_Strong_of *)
375
376Theorem Strong_Strong_of: !c:'a toto.
377 StrongLinearOrder (StrongLinearOrder_of_TO (apto c))
378Proof
379GEN_TAC THEN REWRITE_TAC [Strongof_toto_STRORD] THEN
380MATCH_MP_TAC STRORD_SLO THEN MATCH_ACCEPT_TAC Weak_Weak_of
381QED
382
383Theorem Strong_Strong_of_TO: !c:'a comp.
384 TotOrd c ==> StrongLinearOrder (StrongLinearOrder_of_TO c)
385Proof
386REPEAT STRIP_TAC THEN
387IMP_RES_THEN (CONV_TAC o RAND_CONV o RAND_CONV o REWR_CONV o GSYM)
388 TO_apto_TO_IMP THEN
389MATCH_ACCEPT_TAC Strong_Strong_of
390QED
391
392Theorem TotOrd_TO_of_Weak: !r:'a reln.
393 WeakLinearOrder r ==> TotOrd (TO_of_LinearOrder r)
394Proof
395REPEAT STRIP_TAC THEN MATCH_MP_TAC TotOrd_TO_of_LO THEN
396IMP_RES_TAC WeakLinearOrder THEN ASM_REWRITE_TAC [LinearOrder] THEN
397IMP_RES_TAC WeakOrd_Ord
398QED
399
400Theorem TotOrd_TO_of_Strong: !r:'a reln.
401 StrongLinearOrder r ==> TotOrd (TO_of_LinearOrder r)
402Proof
403REPEAT STRIP_TAC THEN MATCH_MP_TAC TotOrd_TO_of_LO THEN
404IMP_RES_TAC StrongLinearOrder THEN ASM_REWRITE_TAC [LinearOrder] THEN
405IMP_RES_TAC StrongOrd_Ord
406QED
407
408Theorem toto_Weak_thm: !c:'a toto. toto_of_LinearOrder (WeakLinearOrder_of_TO (apto c)) = c
409Proof
410GEN_TAC THEN REWRITE_TAC [toto_of_LinearOrder] THEN
411CONV_TAC (RAND_CONV (REWR_CONV (GSYM TO_apto_ID))) THEN AP_TERM_TAC THEN
412REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
413REWRITE_TAC [TO_of_LinearOrder, WeakLinearOrder_of_TO] THEN
414Cases_on `x:'a = x'` THEN AR THENL
415[ASM_REWRITE_TAC [toto_refl]
416,Cases_on `apto c x x'` THEN ASM_REWRITE_TAC [cpn_case_def] THEN
417 IMP_RES_TAC toto_equal_eq]
418QED
419
420Theorem toto_Strong_thm: !c:'a toto. toto_of_LinearOrder (StrongLinearOrder_of_TO (apto c)) = c
421Proof
422GEN_TAC THEN REWRITE_TAC [toto_of_LinearOrder] THEN
423CONV_TAC (RAND_CONV (REWR_CONV (GSYM TO_apto_ID))) THEN AP_TERM_TAC THEN
424REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
425REWRITE_TAC [TO_of_LinearOrder, StrongLinearOrder_of_TO] THEN
426Cases_on `x:'a = x'` THEN AR THENL
427[ASM_REWRITE_TAC [toto_refl]
428,Cases_on `apto c x x'` THEN ASM_REWRITE_TAC [cpn_case_def] THEN
429 IMP_RES_TAC toto_equal_eq]
430QED
431
432Theorem Weak_toto_thm:
433!r:'a reln. WeakLinearOrder r ==>
434 (WeakLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)
435Proof
436REPEAT STRIP_TAC THEN IMP_RES_TAC TotOrd_TO_of_Weak THEN
437IMP_RES_TAC WeakLinearOrder THEN IMP_RES_TAC WeakOrder THEN
438REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
439REWRITE_TAC [toto_of_LinearOrder, WeakLinearOrder_of_TO] THEN
440IMP_RES_THEN (REWRITE_TAC o ulist) TO_apto_TO_IMP THEN
441REWRITE_TAC [TO_of_LinearOrder] THEN
442Cases_on `x:'a = x'` THEN ASM_REWRITE_TAC [cpn_case_def] THENL
443[IMP_RES_TAC reflexive_def THEN AR
444,Cases_on `(r:'a reln) x x'` THEN AR THEN
445 REWRITE_TAC [cpn_case_def]]
446QED
447
448Theorem Strong_toto_thm:
449!r:'a reln. StrongLinearOrder r ==>
450 (StrongLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)
451Proof
452REPEAT STRIP_TAC THEN IMP_RES_TAC TotOrd_TO_of_Strong THEN
453IMP_RES_TAC StrongLinearOrder THEN IMP_RES_TAC StrongOrder THEN
454REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
455REWRITE_TAC [toto_of_LinearOrder, StrongLinearOrder_of_TO] THEN
456IMP_RES_THEN (REWRITE_TAC o ulist) TO_apto_TO_IMP THEN
457REWRITE_TAC [TO_of_LinearOrder] THEN
458Cases_on `x:'a = x'` THEN ASM_REWRITE_TAC [cpn_case_def] THENL
459[IMP_RES_TAC irreflexive_def THEN AR
460,Cases_on `(r:'a reln) x x'` THEN AR THEN
461 REWRITE_TAC [cpn_case_def]]
462QED
463
464(* Converse of a total order; its correspondence to inv for relations. *)
465
466Definition TO_inv: TO_inv (c:'a comp) x y = c y x
467End
468
469Theorem TotOrd_inv: !c:'a comp. TotOrd c ==> TotOrd (TO_inv c)
470Proof
471GEN_TAC THEN REWRITE_TAC [TotOrd, TO_inv] THEN
472REPEAT STRIP_TAC THEN AR THENL [MATCH_ACCEPT_TAC EQ_SYM_EQ, RES_TAC]
473QED
474
475Definition toto_inv: toto_inv (c:'a toto) = TO (TO_inv (apto c))
476End
477
478Theorem inv_TO: !r:'a comp. TotOrd r ==> (toto_inv (TO r) = TO (TO_inv r))
479Proof
480REPEAT STRIP_TAC THEN IMP_RES_TAC TO_apto_TO_IMP THEN
481ASM_REWRITE_TAC [toto_inv]
482QED
483
484Theorem apto_inv: !c:'a toto. apto (toto_inv c) = TO_inv (apto c)
485Proof
486METIS_TAC [TotOrd_apto, TO_apto_ID, TotOrd_inv, inv_TO, TO_apto_TO_IMP]
487QED
488
489Theorem Weak_toto_inv: !c:'a toto. WeakLinearOrder_of_TO (apto (toto_inv c)) =
490 inv (WeakLinearOrder_of_TO (apto c))
491Proof
492GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
493REWRITE_TAC [WeakLinearOrder_of_TO, toto_inv, inv_DEF] THEN
494ASSUME_TAC (SPEC_ALL TotOrd_apto) THEN IMP_RES_TAC TotOrd_inv THEN
495IMP_RES_TAC TO_apto_TO_IMP THEN ASM_REWRITE_TAC [TO_inv]
496QED
497
498Theorem Strong_toto_inv: !c:'a toto. StrongLinearOrder_of_TO (apto (toto_inv c)) =
499 inv (StrongLinearOrder_of_TO (apto c))
500Proof
501GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
502REWRITE_TAC [StrongLinearOrder_of_TO, toto_inv, inv_DEF] THEN
503ASSUME_TAC (SPEC_ALL TotOrd_apto) THEN IMP_RES_TAC TotOrd_inv THEN
504IMP_RES_TAC TO_apto_TO_IMP THEN ASM_REWRITE_TAC [TO_inv]
505QED
506
507Theorem TO_inv_TO_inv:
508!c:'a comp. TO_inv (TO_inv c) = c
509Proof
510GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
511REWRITE_TAC [TO_inv]
512QED
513
514Theorem toto_inv_toto_inv:
515!c:'a toto. toto_inv (toto_inv c) = c
516Proof
517REWRITE_TAC [toto_inv, apto_inv, TO_inv_TO_inv, TO_apto_ID]
518QED
519
520Theorem TO_inv_Ord: !r:'a reln.
521 (TO_of_LinearOrder (inv r) = TO_inv (TO_of_LinearOrder r))
522Proof
523GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
524REWRITE_TAC [TO_inv, inv_DEF, TO_of_LinearOrder] THEN
525CONV_TAC (RAND_CONV (ONCE_DEPTH_CONV (REWR_CONV EQ_SYM_EQ))) THEN REFL_TAC
526QED
527
528(* **** Translation of TotOrd cpn values back to relation truth values. **** *)
529
530Theorem TO_of_less_rel: !r:'a reln. StrongLinearOrder r ==>
531 !x y. ((TO_of_LinearOrder r x y = LESS) <=> r x y)
532Proof
533REWRITE_TAC
534 [StrongLinearOrder, StrongOrder, irreflexive_def, TO_of_LinearOrder] THEN
535REPEAT STRIP_TAC THEN
536Cases_on `x=y` THEN ASM_REWRITE_TAC [all_cpn_distinct] THEN
537Cases_on `r x y` THEN ASM_REWRITE_TAC [all_cpn_distinct]
538QED
539
540Theorem TO_of_greater_ler: !r:'a reln. StrongLinearOrder r ==>
541 !x y. ((TO_of_LinearOrder r x y = GREATER) <=> r y x)
542Proof
543REPEAT STRIP_TAC THEN IMP_RES_TAC TotOrd_TO_of_Strong THEN
544IMP_RES_THEN (REWRITE_TAC o ulist) TO_antisym THEN
545IMP_RES_THEN (REWRITE_TAC o ulist) TO_of_less_rel
546QED
547
548(* Consequences of TO_of_LenearOrder, toto_of_LinearOrder definitions,
549 tailor-made for use by toto_CONV. *)
550
551Theorem toto_equal_imp: !cmp:'a toto phi. LinearOrder phi /\ (cmp = toto_of_LinearOrder phi) ==>
552 !x y. ((x = y) = T) ==> (apto cmp x y = EQUAL)
553Proof
554REPEAT GEN_TAC THEN REWRITE_TAC [toto_of_LinearOrder] THEN
555STRIP_TAC THEN AR THEN
556IMP_RES_TAC TotOrd_TO_of_LO THEN
557IMP_RES_THEN SUBST1_TAC TO_apto_TO_ID THEN
558REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [TO_of_LinearOrder]
559QED
560
561Theorem toto_unequal_imp: !cmp:'a toto phi. LinearOrder phi /\ (cmp = toto_of_LinearOrder phi) ==>
562 !x y. ((x = y) = F) ==>
563 (if phi x y
564 then apto cmp x y = LESS
565 else apto cmp x y = GREATER)
566Proof
567REPEAT GEN_TAC THEN REWRITE_TAC [toto_of_LinearOrder] THEN
568STRIP_TAC THEN AR THEN
569IMP_RES_TAC TotOrd_TO_of_LO THEN
570IMP_RES_THEN SUBST1_TAC TO_apto_TO_ID THEN
571REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [TO_of_LinearOrder] THEN
572Cases_on `phi x y` THEN AR
573QED
574
575(* TO_inv_Ord did not require r to be a linear order; hence no toto analog.*)
576
577(* constructions of total orders to go with constructions on types;
578 "lexicographic order" is the idea throughout. Since, as hinted by
579 Exercise 3 after Sect. 6.6.3 in Gleason, Fundamentals of Abstract
580 Analysis, the domain ordering for functions must be a well-order, and
581 WF and LEX are both defined in relationTheory, it seems most natural
582 to work with StrongLinearOrder, and transfer the results to TotOrd. *)
583
584Theorem StrongOrder_ALT:
585 !Z:'a reln. StrongOrder Z <=> irreflexive Z /\ transitive Z
586Proof
587GEN_TAC THEN REWRITE_TAC [StrongOrder] THEN EQ_TAC THEN
588STRIP_TAC THEN AR THEN
589REWRITE_TAC [antisymmetric_def] THEN
590REPEAT STRIP_TAC THEN IMP_RES_TAC transitive_def THEN
591IMP_RES_TAC irreflexive_def
592QED
593
594val _ = set_fixity "lexTO" (Infixr 850);
595val _ = set_fixity "lextoto" (Infixr 850);
596
597Theorem LEX_ALT: !R:'a reln U:'b->'b->bool c d.
598(R LEX U) c d = R (FST c) (FST d) \/ (FST c = FST d) /\ U (SND c) (SND d)
599Proof
600REPEAT GEN_TAC THEN REWRITE_TAC [LEX_DEF] THEN
601CONV_TAC (ONCE_DEPTH_CONV (PALPHA_CONV (Term`x:'a#'b`)) THENC
602 LAND_CONV (RATOR_CONV BETA_CONV) THENC
603 ONCE_DEPTH_CONV (PALPHA_CONV (Term`y:'a#'b`)) THENC
604 LAND_CONV BETA_CONV)
605THEN REFL_TAC
606QED
607
608Theorem SLO_LEX: !R:'a reln V:'b->'b->bool.
609StrongLinearOrder R /\ StrongLinearOrder V ==> StrongLinearOrder (R LEX V)
610Proof
611REWRITE_TAC [StrongLinearOrder] THEN REPEAT STRIP_TAC THEN
612IMP_RES_TAC StrongOrder_ALT THENL
613[REWRITE_TAC [StrongOrder_ALT, irreflexive_def, transitive_def, LEX_ALT] THEN
614 REPEAT STRIP_TAC THEN IMP_RES_TAC irreflexive_def THENL
615 [IMP_RES_TAC transitive_def THEN AR
616 ,DISJ1_TAC THEN
617 UNDISCH_THEN (Term`FST (y:'a#'b) = FST (z:'a#'b)`)
618 (REWRITE_TAC o ulist o SYM) THEN AR
619 ,AR
620 ,IMP_RES_TAC transitive_def THEN AR
621 ]
622,IMP_RES_TAC trichotomous_ALT THEN
623 REWRITE_TAC [trichotomous, LEX_ALT] THEN REPEAT GEN_TAC THEN
624 Cases_on `R:'a reln (FST (a:'a#'b)) (FST (b:'a#'b))` THEN AR THEN
625 Cases_on `R:'a reln (FST (b:'a#'b)) (FST (a:'a#'b))` THEN AR THEN
626 RES_TAC THEN UNDISCH_TAC (Term`FST (b:'a#'b) = FST (a:'a#'b)`) THEN AR THEN
627 Cases_on `V:'b->'b->bool (SND (a:'a#'b)) (SND (b:'a#'b))` THEN AR THEN
628 Cases_on `V:'b->'b->bool (SND (b:'a#'b)) (SND (a:'a#'b))` THEN AR THEN
629 RES_TAC THEN UNDISCH_TAC (Term`SND (b:'a#'b) = SND (a:'a#'b)`) THEN
630 UNDISCH_TAC (Term`FST (b:'a#'b) = FST (a:'a#'b)`) THEN
631 ASM_REWRITE_TAC [SPLIT_PAIRS]
632]
633QED
634
635Definition lexTO: (R:'a comp) lexTO (V:'b comp) = TO_of_LinearOrder (
636 StrongLinearOrder_of_TO R LEX StrongLinearOrder_of_TO V)
637End
638
639Definition lextoto:
640 (c:'a toto) lextoto (v:'b toto) = TO (apto c lexTO apto v)
641End
642
643Theorem lexTO_thm:
644!R:'a comp V:'b comp. TotOrd R /\ TotOrd V ==> !x y.
645 ((R lexTO V) x y = case R (FST x) (FST y) of LESS => LESS |
646 EQUAL => V (SND x) (SND y) |
647 GREATER => GREATER)
648Proof
649REWRITE_TAC [TO_of_LinearOrder, lexTO, StrongLinearOrder_of_TO,
650 LEX_ALT] THEN REPEAT STRIP_TAC THEN
651REWRITE_TAC [SPLIT_PAIRS] THEN
652Cases_on `FST (x:'a#'b) = FST (y:'a#'b)` THEN AR THENL
653[IMP_RES_THEN (REWRITE_TAC o ulist) TO_refl THEN
654 REWRITE_TAC [cpn_case_def] THEN
655 Cases_on `SND (x:'a#'b) = SND (y:'a#'b)` THEN AR THENL
656 [IMP_RES_THEN (REWRITE_TAC o ulist) TO_refl
657 ,Cases_on `V:'b comp (SND (x:'a#'b)) (SND (y:'a#'b))` THEN
658 ASM_REWRITE_TAC [cpn_case_def] THEN IMP_RES_TAC TO_equal_eq
659 ]
660,Cases_on `R (FST (x:'a#'b)) (FST (y:'a#'b))` THEN
661 REWRITE_TAC [cpn_case_def] THEN IMP_RES_TAC TO_equal_eq
662]
663QED
664
665Theorem lexTO_ALT: !R:'a comp V:'b comp.
666TotOrd R /\ TotOrd V ==> (!(r,u) (r',u'). (R lexTO V) (r,u) (r',u') =
667 case R r r' of LESS => LESS | EQUAL => V u u'| GREATER => GREATER)
668Proof
669REPEAT GEN_TAC THEN STRIP_TAC THEN
670CONV_TAC (GEN_PALPHA_CONV (Term`x:'a#'b`)) THEN GEN_TAC THEN
671CONV_TAC (GEN_PALPHA_CONV (Term`y:'a#'b`)) THEN GEN_TAC THEN
672MATCH_MP_TAC lexTO_thm THEN AR
673QED
674
675Theorem TO_lexTO: !R:'a comp V:'b comp.
676 TotOrd R /\ TotOrd V ==> TotOrd (R lexTO V)
677Proof
678REPEAT STRIP_TAC THEN REWRITE_TAC [lexTO] THEN
679MATCH_MP_TAC TotOrd_TO_of_Strong THEN
680MATCH_MP_TAC SLO_LEX THEN CONJ_TAC THEN
681IMP_RES_TAC Strong_Strong_of_TO
682QED
683
684Theorem pre_aplextoto:
685!c:'a toto v:'b toto x y.
686 (apto (c lextoto v) x y = case apto c (FST x) (FST y) of LESS => LESS |
687 EQUAL => apto v (SND x) (SND y) |
688 GREATER => GREATER)
689Proof
690REPEAT GEN_TAC THEN REWRITE_TAC [lextoto] THEN
691ASSUME_TAC (ISPEC (Term`c:'a toto`) TotOrd_apto) THEN
692ASSUME_TAC (ISPEC (Term`v:'b toto`) TotOrd_apto) THEN
693IMP_RES_TAC (GSYM lexTO_thm) THEN AR THEN REPEAT AP_THM_TAC THEN
694MATCH_MP_TAC TO_apto_TO_IMP THEN
695IMP_RES_TAC TO_lexTO
696QED
697
698Theorem aplextoto: !c:'a toto v:'b toto x1 x2 y1 y2. (apto (c lextoto v) (x1,x2) (y1,y2) =
699 case apto c x1 y1 of LESS => LESS
700 | EQUAL => apto v x2 y2
701 | GREATER => GREATER)
702Proof
703REPEAT GEN_TAC THEN PURE_ONCE_REWRITE_TAC [GSYM PAIR] THEN
704REWRITE_TAC [pre_aplextoto]
705QED
706
707(* **** Some particular total order generators, additional to lextoto: **** *)
708
709(* *********** num -- redone with numerals Oct. 2012 ************ *)
710
711(* Theory: numto defined from numTheory.LESS *)
712
713Theorem StrongLinearOrder_LESS:
714 StrongLinearOrder ($< :num reln)
715Proof
716SRW_TAC [ARITH_ss] [StrongLinearOrder, StrongOrder_ALT,
717 trichotomous, Order, irreflexive_def]
718QED
719(* ******
720val StrongWellOrder_LESS = store_thm ("StrongWellOrder_LESS",
721 Term`StrongWellOrder ($< :num reln)`,
722REWRITE_TAC [StrongWellOrder, prim_recTheory.WF_LESS, StrongLinearOrder,
723 StrongOrder_ALT, trichotomous, Order, irreflexive_def, transitive_def]
724THEN REPEAT CONJ_TAC THENL
725[ACCEPT_TAC prim_recTheory.LESS_REFL
726,ACCEPT_TAC LESS_TRANS
727,REWRITE_TAC [DISJ_ASSOC] THEN ACCEPT_TAC (CONV_RULE (ONCE_DEPTH_CONV
728 (REWR_CONV DISJ_SYM)) LESS_LESS_CASES)]);
729**** *)
730Definition numOrd: numOrd = TO_of_LinearOrder ($< :num reln)
731End
732
733Theorem TO_numOrd: TotOrd numOrd
734Proof
735REWRITE_TAC [numOrd] THEN MATCH_MP_TAC TotOrd_TO_of_Strong THEN
736ACCEPT_TAC StrongLinearOrder_LESS
737QED
738
739Definition numto: numto = TO numOrd
740End
741
742Theorem apnumto_thm: apto numto = numOrd
743Proof
744REWRITE_TAC [numto, GSYM TO_apto_TO_ID, TO_numOrd]
745QED
746
747(* Practice: re_define numOrd, numto for computation on numerals. *)
748
749Theorem numeralOrd: !x y.
750 (numOrd ZERO ZERO = EQUAL) /\
751 (numOrd ZERO (BIT1 y) = LESS) /\
752 (numOrd ZERO (BIT2 y) = LESS) /\
753 (numOrd (BIT1 x) ZERO = GREATER) /\
754 (numOrd (BIT2 x) ZERO = GREATER) /\
755 (numOrd (BIT1 x) (BIT1 y) = numOrd x y) /\
756 (numOrd (BIT2 x) (BIT2 y) = numOrd x y) /\
757 (numOrd (BIT1 x) (BIT2 y) =
758 case numOrd x y of LESS => LESS | EQUAL => LESS | GREATER => GREATER) /\
759 (numOrd (BIT2 x) (BIT1 y) =
760 case numOrd x y of LESS => LESS | EQUAL => GREATER | GREATER => GREATER)
761Proof
762REPEAT GEN_TAC THEN
763ASSUME_TAC (REWRITE_RULE [numOrd] (MATCH_MP TO_equal_eq TO_numOrd)) THEN
764ASSUME_TAC (MATCH_MP TO_of_less_rel StrongLinearOrder_LESS) THEN
765ASSUME_TAC (MATCH_MP TO_of_greater_ler StrongLinearOrder_LESS) THEN
766REWRITE_TAC [numOrd] THEN Cases_on `TO_of_LinearOrder $< x y` THEN
767RES_TAC THEN ASM_REWRITE_TAC [numeral_lt, cpn_case_def] THENL
768[DISCH_TAC THEN IMP_RES_TAC LESS_ANTISYM
769,MATCH_ACCEPT_TAC prim_recTheory.LESS_REFL
770,DISCH_TAC THEN IMP_RES_TAC LESS_ANTISYM]
771QED
772
773(* ********************************************************************* *)
774(* qk_numto_CONV, a nonstandard ordering of num *)
775(* ********************************************************************* *)
776
777(* qk_numOrd is lexicographic ordering of numerals, regarded as binary
778v lists, least significant bit first. *)
779
780(* Doubtless there is a better way, but all I can see to do is define
781 a datatype like numerals as a crutch for getting qk_numOrd defined. *)
782
783Datatype: num_dt = zer | bit1 num_dt | bit2 num_dt
784End
785
786val num_to_dt_defn = Hol_defn "num_to_dt"
787`num_to_dt n = if n = 0 then zer
788 else if ODD n then bit1 (num_to_dt (DIV2 (n - 1)))
789 else bit2 (num_to_dt (DIV2 (n - 2)))`;
790
791Theorem half_lem[local]:
792 !m. m DIV 2 <= m
793Proof
794GEN_TAC THEN SIMP_TAC arith_ss [DIV_LESS_EQ]
795QED
796
797val (num_to_dt, num_to_dt_ind) = tprove (num_to_dt_defn,
798WF_REL_TAC `measure I` THEN
799CONJ_TAC THEN GEN_TAC THEN
800SIMP_TAC arith_ss [DIV2_def] THEN STRIP_TAC THEN
801MATCH_MP_TAC LESS_EQ_LESS_TRANS THENL
802[EXISTS_TAC (Term`n - 1`), EXISTS_TAC (Term`n - 2`)] THEN
803ASM_SIMP_TAC arith_ss [half_lem]);
804
805Definition num_dtOrd:
806 (num_dtOrd zer zer = EQUAL) /\
807 (num_dtOrd zer (bit1 x) = LESS) /\
808 (num_dtOrd zer (bit2 x) = LESS) /\
809 (num_dtOrd (bit1 x) zer = GREATER) /\
810 (num_dtOrd (bit2 x) zer = GREATER) /\
811 (num_dtOrd (bit1 x) (bit2 y) = LESS) /\
812 (num_dtOrd (bit2 x) (bit1 y) = GREATER) /\
813 (num_dtOrd (bit1 x) (bit1 y) = num_dtOrd x y) /\
814 (num_dtOrd (bit2 x) (bit2 y) = num_dtOrd x y)
815End
816
817val num_dt_distinct = theorem "num_dt_distinct";
818
819val all_dt_distinct = CONJ num_dt_distinct (GSYM num_dt_distinct);
820
821val num_dt_11 = theorem "num_dt_11";
822
823Theorem TO_num_dtOrd[local]:
824 TotOrd num_dtOrd
825Proof
826REWRITE_TAC [TotOrd] THEN REPEAT CONJ_TAC THEN
827Induct THEN GEN_TAC THEN Cases_on `y` THEN
828ASM_REWRITE_TAC [num_dtOrd, all_cpn_distinct, all_dt_distinct, num_dt_11] THEN
829GEN_TAC THEN Cases_on `z` THEN
830ASM_REWRITE_TAC [num_dtOrd, all_cpn_distinct, all_dt_distinct, num_dt_11]
831QED
832
833Definition qk_numOrd_def:
834 qk_numOrd m n = num_dtOrd (num_to_dt m) (num_to_dt n)
835End
836
837(* Most of the work to prove TO_qk_numOrd (below) comes in showing that
838 num_to_dt is a bijection, which we do first, with help of some lemmas. *)
839
840Theorem zer_bit_neq[local]:
841 !P a b. zer <> (if P then bit1 a else bit2 b) /\
842 (if P then bit1 a else bit2 b) <> zer
843Proof
844REPEAT GEN_TAC THEN CONJ_TAC THEN
845Cases_on `P` THEN ASM_REWRITE_TAC [all_dt_distinct]
846QED
847
848Theorem TWICE_DIV_2[local]:
849 !n. 2 * n DIV 2 = n
850Proof
851GEN_TAC THEN
852CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV MULT_COMM))) THEN
853SUBGOAL_THEN (Term`0 < 2`) (REWRITE_TAC o ulist o MATCH_MP MULT_DIV) THEN
854SIMP_TAC arith_ss []
855QED
856
857Theorem DIV2_ODD_EQ[local]:
858 !x y. x <> 0 /\ y <> 0 /\ ODD x /\ ODD y ==>
859 (DIV2 (x - 1) = DIV2 (y - 1)) ==> (x = y)
860Proof
861REPEAT GEN_TAC THEN REWRITE_TAC [ODD_EXISTS] THEN STRIP_TAC THEN AR THEN
862SIMP_TAC arith_ss [DIV2_def] THEN
863REWRITE_TAC [TWICE_DIV_2] THEN DISCH_TAC THEN AR
864QED
865
866Theorem EVEN_NZ[local]:
867 !z. z <> 0 /\ ~ODD z ==> z - 1 <> 0 /\ ODD (z - 1)
868Proof
869Cases THENL
870[REWRITE_TAC []
871,SIMP_TAC arith_ss [ODD] THEN Cases_on `n` THEN SIMP_TAC arith_ss [ODD]]
872QED
873
874Theorem DIV2_EVEN_EQ[local]:
875 x <> 0 /\ y <> 0 /\ ~ODD x /\ ~ODD y ==>
876 (DIV2 (x - 2) = DIV2 (y - 2)) ==> (x = y)
877Proof
878STRIP_TAC THEN
879SUBGOAL_THEN (Term`x - 1 <> 0 /\ y-1 <> 0 /\ ODD (x - 1) /\ ODD (y - 1)`)
880 MP_TAC THENL
881[IMP_RES_TAC EVEN_NZ THEN AR
882,DISCH_THEN (fn cj => MP_TAC (MATCH_MP DIV2_ODD_EQ cj)) THEN
883 SIMP_TAC arith_ss [] THEN
884 DISCH_THEN (fn imp => DISCH_THEN (fn eq => MP_TAC (MATCH_MP imp eq))) THEN
885 ASM_SIMP_TAC arith_ss []]
886QED
887
888Theorem num_to_dt_bij[local]:
889 !x y. (num_to_dt x = num_to_dt y) <=> (x = y)
890Proof
891INDUCT_THEN num_to_dt_ind ASSUME_TAC THEN
892INDUCT_THEN num_to_dt_ind ASSUME_TAC THEN
893ONCE_REWRITE_TAC [num_to_dt] THEN EQ_TAC THENL
894[Cases_on `x = 0` THEN Cases_on `y = 0` THEN
895 ASM_REWRITE_TAC [zer_bit_neq] THEN
896 Cases_on `ODD x` THEN Cases_on `ODD y` THEN RES_TAC THEN
897 ASM_REWRITE_TAC [all_dt_distinct, num_dt_11] THENL
898 [MATCH_MP_TAC DIV2_ODD_EQ THEN AR
899 ,MATCH_MP_TAC DIV2_EVEN_EQ THEN AR]
900,DISCH_TAC THEN AR]
901QED
902
903Theorem TO_qk_numOrd: TotOrd qk_numOrd
904Proof
905REWRITE_TAC
906 [TotOrd, qk_numOrd_def, REWRITE_RULE [TotOrd] TO_num_dtOrd] THEN
907MATCH_ACCEPT_TAC num_to_dt_bij
908QED
909
910(* ******* At last we can prove (given a few more lemmas) what would ****** *)
911(* ******* be a definition if only numeral were a datatype: ****** *)
912
913Theorem ZERO_to_dt[local]:
914 num_to_dt ZERO = zer
915Proof
916ONCE_REWRITE_TAC [num_to_dt] THEN REWRITE_TAC [ALT_ZERO]
917QED
918
919Theorem BIT_NZ[local]:
920 !n. BIT1 n <> 0 /\ BIT2 n <> 0
921Proof
922GEN_TAC THEN REWRITE_TAC [BIT1, BIT2] THEN
923Cases_on `n` THEN SIMP_TAC arith_ss []
924QED
925
926Theorem BIT1_to_dt[local]:
927 !n. num_to_dt (BIT1 n) = bit1 (num_to_dt n)
928Proof
929GEN_TAC THEN CONV_TAC (LAND_CONV (REWR_CONV num_to_dt)) THEN
930REWRITE_TAC [numeral_evenodd, BIT_NZ, DIV2_def] THEN
931REPEAT AP_TERM_TAC THEN
932CONV_TAC (LAND_CONV (LAND_CONV (LAND_CONV (REWR_CONV BIT1)))) THEN
933SIMP_TAC arith_ss [TWICE_DIV_2]
934QED
935
936Theorem BIT2_to_dt[local]:
937 !n. num_to_dt (BIT2 n) = bit2 (num_to_dt n)
938Proof
939GEN_TAC THEN CONV_TAC (LAND_CONV (REWR_CONV num_to_dt)) THEN
940REWRITE_TAC [numeral_evenodd, BIT_NZ, DIV2_def] THEN
941REPEAT AP_TERM_TAC THEN
942CONV_TAC (LAND_CONV (LAND_CONV (LAND_CONV (REWR_CONV BIT2)))) THEN
943SIMP_TAC arith_ss [TWICE_DIV_2]
944QED
945
946Theorem qk_numeralOrd: !x y.
947 (qk_numOrd ZERO ZERO = EQUAL) /\
948 (qk_numOrd ZERO (BIT1 y) = LESS) /\
949 (qk_numOrd ZERO (BIT2 y) = LESS) /\
950 (qk_numOrd (BIT1 x) ZERO = GREATER) /\
951 (qk_numOrd (BIT2 x) ZERO = GREATER) /\
952 (qk_numOrd (BIT1 x) (BIT1 y) = qk_numOrd x y) /\
953 (qk_numOrd (BIT2 x) (BIT2 y) = qk_numOrd x y) /\
954 (qk_numOrd (BIT1 x) (BIT2 y) = LESS) /\
955 (qk_numOrd (BIT2 x) (BIT1 y) = GREATER)
956Proof
957REWRITE_TAC [qk_numOrd_def, ZERO_to_dt, BIT1_to_dt, BIT2_to_dt, num_dtOrd]
958QED
959
960(* ******** From here on we can imitate the treatment of numOrd ********** *)
961
962Definition qk_numto: qk_numto = TO qk_numOrd
963End
964
965Theorem ap_qk_numto_thm: apto qk_numto = qk_numOrd
966Proof
967REWRITE_TAC [qk_numto, GSYM TO_apto_TO_ID, TO_qk_numOrd]
968QED
969
970(* ******************************************************************** *)
971(* charOrd seems to be a serious problem. It takes some ingenuity to *)
972(* make one character comparison with only two num comparisons, and I *)
973(* see no way to bring that down to one. *)
974(* ******************************************************************** *)
975
976Definition charOrd: charOrd (a:char) (b:char) = numOrd (ORD a) (ORD b)
977End
978
979Definition charto: charto = TO (charOrd)
980End
981
982Theorem TO_charOrd: TotOrd charOrd
983Proof
984REWRITE_TAC [TotOrd, charOrd] THEN
985STRIP_ASSUME_TAC (REWRITE_RULE [TotOrd] TO_numOrd) THEN
986REPEAT STRIP_TAC THEN AR THENL
987[MATCH_ACCEPT_TAC ORD_11, RES_TAC]
988QED
989
990Theorem apcharto_thm: apto charto = charOrd
991Proof
992REWRITE_TAC [charto, SYM (ISPEC (Term`charOrd`) TO_apto_TO_ID), TO_charOrd]
993QED
994
995Theorem charOrd_lt_lem: !a b.
996 (numOrd a b = LESS) ==> (b < 256 = T) ==> (charOrd (CHR a) (CHR b) = LESS)
997Proof
998REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
999SUBGOAL_THEN (Term`a:num < b`) ASSUME_TAC THENL
1000[SUBGOAL_THEN (Term`(numOrd a b = LESS) <=> a < b`)
1001 (ASM_REWRITE_TAC o ulist o SYM) THEN
1002 REWRITE_TAC [numOrd] THEN MATCH_MP_TAC TO_of_less_rel THEN
1003 ACCEPT_TAC StrongLinearOrder_LESS
1004,IMP_RES_TAC LESS_TRANS THEN REWRITE_TAC [charOrd] THEN
1005 IMP_RES_THEN SUBST1_TAC ORD_CHR_RWT THEN AR]
1006QED
1007
1008Theorem charOrd_gt_lem: !a b. (numOrd a b = GREATER) ==> (a < 256 = T) ==>
1009 (charOrd (CHR a) (CHR b) = GREATER)
1010Proof
1011REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1012SUBGOAL_THEN (Term`b:num < a`) ASSUME_TAC THENL
1013[SUBGOAL_THEN (Term`(numOrd a b = GREATER) <=> b < a`)
1014 (ASM_REWRITE_TAC o ulist o SYM) THEN
1015 REWRITE_TAC [numOrd] THEN MATCH_MP_TAC TO_of_greater_ler THEN
1016 ACCEPT_TAC StrongLinearOrder_LESS
1017,IMP_RES_TAC LESS_TRANS THEN REWRITE_TAC [charOrd] THEN
1018 IMP_RES_THEN SUBST1_TAC ORD_CHR_RWT THEN AR]
1019QED
1020
1021Theorem charOrd_eq_lem: !a b. (numOrd a b = EQUAL) ==> (charOrd (CHR a) (CHR b) = EQUAL)
1022Proof
1023REPEAT GEN_TAC THEN
1024REWRITE_TAC [charOrd, MATCH_MP TO_equal_eq TO_numOrd] THEN DISCH_TAC THEN AR
1025QED
1026
1027Theorem charOrd_thm: charOrd = TO_of_LinearOrder $<
1028Proof
1029REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
1030REWRITE_TAC [charOrd, numOrd, TO_of_LinearOrder] THEN
1031REWRITE_TAC [char_lt_def, ORD_11]
1032QED
1033
1034(* ********************************************************************** *)
1035(* A similar exercise to the above for lists should be useful itself, and *)
1036(* an exemplar of how any datatype can be ordered if its components are. *)
1037(* ********************************************************************** *)
1038
1039Definition listorder: (listorder (V:'a reln) l [] = F) /\
1040 (listorder V [] (s :: m) = T) /\
1041 (listorder V (r :: l) (s :: m) =
1042 V r s \/ (r = s) /\ listorder V l m)
1043End
1044
1045Theorem SLO_listorder: !V:'a reln.
1046 StrongLinearOrder V ==> StrongLinearOrder (listorder V)
1047Proof
1048GEN_TAC THEN
1049REWRITE_TAC [StrongLinearOrder, StrongOrder_ALT] THEN
1050STRIP_TAC THEN
1051REWRITE_TAC [irreflexive_def, transitive_def, trichotomous_ALT] THEN
1052REPEAT CONJ_TAC THENL
1053[Induct THEN ASM_REWRITE_TAC [listorder, DE_MORGAN_THM] THEN
1054 IMP_RES_TAC irreflexive_def
1055,Induct THENL
1056 [REPEAT (Cases THEN REWRITE_TAC [listorder])
1057 ,REPEAT (GEN_TAC THEN Induct THEN ASM_REWRITE_TAC [listorder]) THEN
1058 REPEAT STRIP_TAC THEN IMP_RES_TAC transitive_def THEN RES_TAC THEN AR THEN
1059 UNDISCH_THEN (Term`(h':'a) = h''`) (ASM_REWRITE_TAC o ulist o SYM)
1060 ]
1061,Induct THENL
1062 [Cases THEN REWRITE_TAC [listorder]
1063 ,GEN_TAC THEN Induct THEN ASM_REWRITE_TAC [listorder] THEN
1064 GEN_TAC THEN Cases_on `(V:'a reln) h h'` THEN AR THEN
1065 Cases_on `(V:'a reln) h' h` THEN AR THEN
1066 IMP_RES_TAC trichotomous_ALT THEN
1067 UNDISCH_TAC (Term`h:'a = h'`) THEN AR THEN
1068 STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC [CONS_11]
1069]]
1070QED
1071
1072Definition ListOrd: ListOrd (c:'a toto) =
1073 TO_of_LinearOrder (listorder (StrongLinearOrder_of_TO (apto c)))
1074End
1075
1076Theorem TO_ListOrd:
1077 !c:'a toto. TotOrd (ListOrd c)
1078Proof
1079GEN_TAC THEN REWRITE_TAC [ListOrd] THEN
1080ASSUME_TAC (ISPEC (Term`c:'a toto`) TotOrd_apto) THEN
1081IMP_RES_TAC Strong_Strong_of_TO THEN
1082IMP_RES_TAC SLO_listorder THEN
1083IMP_RES_TAC TotOrd_TO_of_Strong
1084QED
1085
1086Theorem ListOrd_THM:
1087(!c:'a toto. (ListOrd c ([]:'a list) [] = EQUAL) /\
1088 (!b:'a y. ListOrd c [] (b :: y) = LESS) /\
1089 (!a:'a x. ListOrd c (a :: x) [] = GREATER) /\
1090 (!a:'a x b y. ListOrd c (a :: x) (b :: y) =
1091 case apto c a b of LESS => LESS |
1092 EQUAL => ListOrd c x y |
1093 GREATER => GREATER))
1094Proof
1095GEN_TAC THEN ASSUME_TAC (SPEC_ALL TotOrd_apto) THEN
1096REWRITE_TAC [ListOrd, TO_of_LinearOrder, list_distinct,
1097 GSYM list_distinct, list_11] THEN
1098IMP_RES_TAC Strong_Strong_of_TO THEN
1099REWRITE_TAC [listorder, StrongLinearOrder_of_TO] THEN
1100REPEAT GEN_TAC THEN
1101Cases_on `apto c a b` THEN
1102ASM_REWRITE_TAC [cpn_case_def, all_cpn_distinct] THEN
1103IMP_RES_TAC toto_cpn_eqn THEN ASM_REWRITE_TAC [all_cpn_distinct]
1104QED
1105
1106Definition listoto: listoto (c:'a toto) = TO (ListOrd c)
1107End
1108
1109Theorem aplistoto: !c:'a toto.
1110(apto (listoto c) [] [] = EQUAL) /\
1111(!b y. apto (listoto c) [] (b :: y) = LESS) /\
1112(!a x. apto (listoto c) (a :: x) [] = GREATER) /\
1113(!a x b y. apto (listoto c) (a :: x) (b :: y) =
1114 case apto c a b of LESS => LESS |
1115 EQUAL => apto (listoto c) x y |
1116 GREATER => GREATER)
1117Proof
1118GEN_TAC THEN ASSUME_TAC (SPEC_ALL TO_ListOrd) THEN
1119REWRITE_TAC [listoto] THEN
1120IMP_RES_THEN (REWRITE_TAC o ulist) TO_apto_TO_IMP THEN
1121MATCH_ACCEPT_TAC ListOrd_THM
1122QED
1123
1124(* ***** string a synonym for char list -- makes stringto very easy. ***** *)
1125
1126Definition stringto: stringto = listoto charto
1127End
1128
1129(* *********************************************************************** *)
1130(* ********* what was btOrd, etc. to be rethought - April 2013 *********** *)
1131(* (consult this section of ORT/TotOrdScript.sml) *)
1132(* *********************************************************************** *)
1133
1134(* ********************************************************************** *)
1135(* Following may be useful for obtaining total orders on abstract types *)
1136(* from total orders on their representations. *)
1137(* ********************************************************************** *)
1138Definition imageOrd: imageOrd (f:'a->'c) (cp:'c comp) a b = cp (f a) (f b)
1139End
1140
1141Theorem TO_injection: !cp:'c comp. TotOrd cp ==> !f:'d->'c.
1142 ONE_ONE f ==> TotOrd (imageOrd f cp)
1143Proof
1144REWRITE_TAC [TotOrd, imageOrd, ONE_ONE_THM] THEN REPEAT STRIP_TAC THEN
1145AR THEN RES_TAC THEN EQ_TAC THEN DISCH_TAC THEN RES_TAC THEN AR
1146QED
1147
1148(* **************************************************************** *)
1149(* The following treatment of total order on type one is completely *)
1150(* silly, but might be prudent to have. SUPPRESSED FOR NOW. *)
1151(* **************************************************************** *)
1152(* ************************
1153val oneOrd = Define`oneOrd (x:one) (y:one) = EQUAL`;
1154
1155val TO_oneOrd = store_thm ("TO_oneOrd", Term`TotOrd oneOrd`,
1156REWRITE_TAC [TotOrd, oneOrd, all_cpn_distinct] THEN
1157ONCE_REWRITE_TAC [one] THEN REWRITE_TAC []);
1158
1159val oneto = Define`oneto = TO oneOrd`;
1160
1161val aponeto = store_thm ("aponeto", Term`!x y. apto oneto x y = EQUAL`,
1162ASSUME_TAC TO_oneOrd THEN REWRITE_TAC [oneto] THEN
1163IMP_RES_THEN SUBST1_TAC TO_apto_TO_IMP THEN REWRITE_TAC [oneOrd]);
1164************************** *)
1165
1166(* intto moved to inttoTheory, to avoid always loading intLib *)
1167
1168Theorem StrongLinearOrder_of_TO_TO_of_LinearOrder:
1169 !R. irreflexive R ==> (StrongLinearOrder_of_TO (TO_of_LinearOrder R) = R)
1170Proof
1171 srw_tac[][irreflexive_def] >>
1172 srw_tac[][FUN_EQ_THM,StrongLinearOrder_of_TO,TO_of_LinearOrder] >>
1173 srw_tac[][]
1174QED
1175
1176Theorem TO_of_LinearOrder_LEX:
1177 !R V. irreflexive R /\ irreflexive V
1178 ==> (TO_of_LinearOrder (R LEX V) = (TO_of_LinearOrder R) lexTO (TO_of_LinearOrder V))
1179Proof
1180 simp[lexTO,StrongLinearOrder_of_TO_TO_of_LinearOrder]
1181QED