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