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