1open HolKernel Parse boolLib bossLib BasicProvers; 2open optionTheory pairTheory stringTheory listTheory arithmeticTheory totoTheory; 3open lcsymtacs; 4 5val _ = new_theory "comparison"; 6 7val _ = temp_tight_equality (); 8val every_case_tac = BasicProvers.EVERY_CASE_TAC; 9 10val comparison_distinct = TypeBase.distinct_of ``:ordering`` 11val comparison_case_def = TypeBase.case_def_of ``:ordering`` 12val comparison_nchotomy = TypeBase.nchotomy_of ``:ordering`` 13val _ = Parse.overload_on("Less",``LESS``) 14val _ = Parse.overload_on("Equal",``EQUAL``) 15val _ = Parse.overload_on("Greater",``GREATER``) 16 17val good_cmp_def = Define ` 18good_cmp cmp <=> 19 (!x. cmp x x = Equal) /\ 20 (!x y. cmp x y = Equal ==> cmp y x = Equal) /\ 21 (!x y. cmp x y = Greater <=> cmp y x = Less) /\ 22 (!x y z. cmp x y = Equal /\ cmp y z = Less ==> cmp x z = Less) /\ 23 (!x y z. cmp x y = Less /\ cmp y z = Equal ==> cmp x z = Less) /\ 24 (!x y z. cmp x y = Equal /\ cmp y z = Equal ==> cmp x z = Equal) /\ 25 (!x y z. cmp x y = Less /\ cmp y z = Less ==> cmp x z = Less)`; 26 27val good_cmp_thm = Q.store_thm ("good_cmp_thm", 28`!cmp. 29 good_cmp cmp <=> 30 (!x. cmp x x = Equal) /\ 31 (!x y z. 32 (cmp x y = Greater <=> cmp y x = Less) /\ 33 (cmp x y = Less /\ cmp y z = Equal ==> cmp x z = Less) /\ 34 (cmp x y = Less /\ cmp y z = Less ==> cmp x z = Less))`, 35 rw [good_cmp_def] >> 36 metis_tac [comparison_distinct, comparison_nchotomy]); 37 38val cmp_thms = save_thm ("cmp_thms", LIST_CONJ [comparison_distinct, comparison_case_def, comparison_nchotomy, good_cmp_def]) 39 40val _ = overload_on ("option_cmp", ``option_compare``); 41val option_cmp_def = save_thm("option_cmp_def", 42 ternaryComparisonsTheory.option_compare_def) 43 44val option_cmp2_def = Define` 45 (option_cmp2 cmp NONE NONE = Equal) /\ 46 (option_cmp2 cmp NONE (SOME x) = Greater) /\ 47 (option_cmp2 cmp (SOME x) NONE = Less) /\ 48 (option_cmp2 cmp (SOME x) (SOME y) = cmp x y)` 49 50val _ = overload_on ("list_cmp", ``list_compare``) 51val list_cmp_def = ternaryComparisonsTheory.list_compare_def 52val list_cmp_ind = ternaryComparisonsTheory.list_compare_ind 53 54val _ = overload_on ("pair_cmp", ``pair_compare``) 55val pair_cmp_def = save_thm( 56 "pair_cmp_def", 57 PART_MATCH lhs ternaryComparisonsTheory.pair_compare_def 58 ``pair_cmp c1 c2 (FST x, SND x) (FST y, SND y)`` 59 |> REWRITE_RULE [pairTheory.PAIR]); 60 61val _ = overload_on ("bool_cmp", ``bool_compare``) 62val bool_cmp_def = save_thm( 63 "bool_cmp_def", 64 ternaryComparisonsTheory.bool_compare_def) 65 66val _ = overload_on ("num_cmp", ``num_compare``) 67val num_cmp_def = save_thm( 68 "num_cmp_def", 69 ternaryComparisonsTheory.num_compare_def) 70 71val _ = overload_on ("char_cmp", ``char_compare``); 72val char_cmp_def = save_thm( 73 "char_cmp_def", 74 ternaryComparisonsTheory.char_compare_def); 75 76val _ = overload_on ("string_cmp", ``string_compare``); 77val string_cmp_def = save_thm( 78 "string_cmp_def", 79 ternaryComparisonsTheory.string_compare_def) 80(* relationship to toto *) 81 82val TotOrd_imp_good_cmp = store_thm("TotOrder_imp_good_cmp", 83 ``!cmp. TotOrd cmp ==> good_cmp cmp``, 84 rw[TotOrd,good_cmp_thm] >> metis_tac[]) 85 86val _ = temp_overload_on ("invert", ``ternaryComparisons$invert_comparison``) 87 88val TO_inv_invert = store_thm("TO_inv_invert", 89 ``!c. TotOrd c ==> TO_inv c = CURRY (invert o UNCURRY c)``, 90 simp[FUN_EQ_THM,TO_inv] >> gen_tac >> strip_tac >> 91 map_every qx_gen_tac[`x`,`y`] >> 92 Cases_on`c x y`>>simp[]>> 93 fs[TotOrd] >> metis_tac[]) 94 95val option_cmp2_TO_inv = store_thm("option_cmp2_TO_inv", 96 ``!c. option_cmp2 c = TO_inv (option_cmp (TO_inv c))``, 97 simp[FUN_EQ_THM,TO_inv] >> 98 gen_tac >> Cases >> Cases >> 99 simp[option_cmp2_def,option_cmp_def,TO_inv]); 100 101val list_cmp_ListOrd = store_thm("list_cmp_ListOrd", 102 ``!c. TotOrd c ==> list_cmp c = ListOrd (TO c)``, 103 simp[FUN_EQ_THM,PULL_FORALL] >> 104 ho_match_mp_tac list_cmp_ind >> 105 simp[list_cmp_def,ListOrd,TO_of_LinearOrder, 106 StrongLinearOrder_of_TO,TO_apto_TO_ID,listorder] >> 107 rw[] >> 108 fs[GSYM TO_apto_TO_ID,TotOrd] >> 109 BasicProvers.CASE_TAC >> 110 metis_tac[cmp_thms]) 111 112val TotOrd_list_cmp = store_thm("TotOrd_list_cmp", 113 ``!c. TotOrd c ==> TotOrd (list_cmp c)``, 114 srw_tac[][] >> imp_res_tac list_cmp_ListOrd >> simp[TO_ListOrd]) 115 116val pair_cmp_lexTO = store_thm("pair_cmp_lexTO", 117 ``!R V. TotOrd R /\ TotOrd V ==> pair_cmp R V = R lexTO V``, 118 simp[FUN_EQ_THM,lexTO_thm,pair_cmp_def,pairTheory.FORALL_PROD]) 119 120val num_cmp_numOrd = store_thm("num_cmp_numOrd", 121 ``num_cmp = numOrd``, 122 simp[FUN_EQ_THM,num_cmp_def,numOrd,TO_of_LinearOrder]) 123 124val char_cmp_charOrd = store_thm("char_cmp_charOrd", 125 ``char_cmp = charOrd``, 126 simp[FUN_EQ_THM,char_cmp_def,charOrd,num_cmp_numOrd]) 127 128val string_cmp_stringto = store_thm("string_cmp_stringto", 129 ``string_cmp = apto stringto``, 130 simp[FUN_EQ_THM,stringto] >> 131 Induct >- ( Cases >> simp[aplistoto,string_cmp_def,list_cmp_def] ) >> 132 gen_tac >> Cases >> 133 simp[aplistoto,string_cmp_def,list_cmp_def,apcharto_thm,char_cmp_charOrd] >> 134 BasicProvers.CASE_TAC >> 135 simp[MATCH_MP list_cmp_ListOrd TO_charOrd,listoto,charto] >> 136 rpt AP_THM_TAC >> 137 match_mp_tac (GSYM TO_apto_TO_IMP) >> 138 simp[TO_ListOrd]) 139 140(* cmps are good *) 141 142val option_cmp_good = Q.store_thm ("option_cmp_good", 143`!cmp. good_cmp cmp ==> good_cmp (option_cmp cmp)`, 144 rw [good_cmp_def] >> 145 Cases_on `x` >> 146 TRY (Cases_on `y`) >> 147 TRY (Cases_on `z`) >> 148 metis_tac [option_cmp_def, comparison_distinct]); 149 150val option_cmp2_good = Q.store_thm ("option_cmp2_good", 151`!cmp. good_cmp cmp ==> good_cmp (option_cmp2 cmp)`, 152 rw [good_cmp_def] >> 153 Cases_on `x` >> 154 TRY (Cases_on `y`) >> 155 TRY (Cases_on `z`) >> 156 metis_tac [option_cmp2_def, comparison_distinct]); 157 158val list_cmp_good = Q.store_thm ("list_cmp_good", 159`!cmp. good_cmp cmp ==> good_cmp (list_cmp cmp)`, 160 simp [good_cmp_def] >> 161 rpt gen_tac >> 162 strip_tac >> 163 rpt conj_tac >> 164 Induct_on `x` >> 165 TRY (Cases_on `y`) >> 166 TRY (Cases_on `z`) >> 167 REWRITE_TAC [list_cmp_def] >> 168 rpt strip_tac >> 169 every_case_tac >> 170 metis_tac [list_cmp_def, comparison_distinct, comparison_case_def, comparison_nchotomy]); 171 172val pair_cmp_good = Q.store_thm ("pair_cmp_good", 173`!cmp1 cmp2. good_cmp cmp1 /\ good_cmp cmp2 ==> good_cmp (pair_cmp cmp1 cmp2)`, 174 simp [good_cmp_def] >> 175 rpt gen_tac >> 176 strip_tac >> 177 rpt conj_tac >> 178 TRY (Cases_on `x`) >> 179 TRY (Cases_on `y`) >> 180 TRY (Cases_on `z`) >> 181 REWRITE_TAC [pair_cmp_def] >> 182 rpt strip_tac >> 183 every_case_tac >> 184 metis_tac [pair_cmp_def, comparison_distinct, comparison_case_def, comparison_nchotomy]); 185 186val bool_cmp_good = Q.store_thm ("bool_cmp_good[simp]", 187`good_cmp bool_cmp`, 188 simp [good_cmp_def] >> 189 rpt conj_tac >> 190 TRY (Cases_on `x`) >> 191 TRY (Cases_on `y`) >> 192 TRY (Cases_on `z`) >> 193 REWRITE_TAC [bool_cmp_def] >> 194 every_case_tac >> 195 fs []); 196 197val num_cmp_good = Q.store_thm ("num_cmp_good[simp]", 198`good_cmp num_cmp`, 199 simp [good_cmp_def] >> 200 rpt conj_tac >> 201 TRY (Cases_on `x`) >> 202 TRY (Cases_on `y`) >> 203 TRY (Cases_on `z`) >> 204 REWRITE_TAC [num_cmp_def] >> 205 every_case_tac >> 206 full_simp_tac (srw_ss()++ARITH_ss) []); 207 208val char_cmp_good = Q.store_thm ("char_cmp_good[simp]", 209`good_cmp char_cmp`, 210 simp [good_cmp_def] >> 211 rpt conj_tac >> 212 TRY (Cases_on `x`) >> 213 TRY (Cases_on `y`) >> 214 TRY (Cases_on `z`) >> 215 REWRITE_TAC [char_cmp_def, num_cmp_def] >> 216 every_case_tac >> 217 full_simp_tac (srw_ss()++ARITH_ss) []); 218 219val string_cmp_good = Q.store_thm ("string_cmp_good[simp]", 220`good_cmp string_cmp`, 221 metis_tac [string_cmp_def, char_cmp_good, list_cmp_good]); 222 223val list_cmp_cong = Q.store_thm ("list_cmp_cong", 224`!cmp l1 l2 cmp' l1' l2'. 225 (l1 = l1') /\ 226 (l2 = l2') /\ 227 (!x x'. MEM x l1' /\ MEM x' l2' ==> cmp x x' = cmp' x x') 228 ==> 229 list_cmp cmp l1 l2 = list_cmp cmp' l1' l2'`, 230 ho_match_mp_tac list_cmp_ind >> 231 rw [list_cmp_def] >> 232 rw [list_cmp_def] >> 233 every_case_tac >> 234 rw []); 235 236val option_cmp_cong = Q.store_thm ("option_cmp_cong", 237`!cmp v1 v2 cmp' v1' v2'. 238 (v1 = v1') /\ 239 (v2 = v2') /\ 240 (!x x'. v1' = SOME x /\ v2' = SOME x' ==> cmp x x' = cmp' x x') 241 ==> 242 option_cmp cmp v1 v2 = option_cmp cmp' v1' v2'`, 243 ho_match_mp_tac ternaryComparisonsTheory.option_compare_ind >> 244 rw [option_cmp_def] >> 245 rw [option_cmp_def]); 246 247val option_cmp2_cong = Q.store_thm ("option_cmp2_cong", 248`!cmp v1 v2 cmp' v1' v2'. 249 (v1 = v1') /\ 250 (v2 = v2') /\ 251 (!x x'. v1' = SOME x /\ v2' = SOME x' ==> cmp x x' = cmp' x x') 252 ==> 253 option_cmp2 cmp v1 v2 = option_cmp2 cmp' v1' v2'`, 254 ho_match_mp_tac (fetch "-" "option_cmp2_ind") >> 255 rw [option_cmp2_def] >> 256 rw [option_cmp2_def]); 257 258val pair_cmp_cong = Q.store_thm ("pair_cmp_cong", 259`!cmp1 cmp2 v1 v2 cmp1' cmp2' v1' v2'. 260 (v1 = v1') /\ 261 (v2 = v2') /\ 262 (!a b c d. v1' = (a,b) /\ v2' = (c,d) ==> cmp1 a c = cmp1' a c) /\ 263 (!a b c d. v1' = (a,b) /\ v2' = (c,d) ==> cmp2 b d = cmp2' b d) 264 ==> 265 pair_cmp cmp1 cmp2 v1 v2 = pair_cmp cmp1' cmp2' v1' v2'`, 266 simp [pair_cmp_def, pairTheory.FORALL_PROD]); 267 268val _ = DefnBase.export_cong "list_cmp_cong"; 269val _ = DefnBase.export_cong "option_cmp_cong"; 270val _ = DefnBase.export_cong "option_cmp2_cong"; 271val _ = DefnBase.export_cong "pair_cmp_cong"; 272 273val good_cmp_trans = Q.store_thm ("good_cmp_trans", 274`!cmp. good_cmp cmp ==> transitive (\ (k,v) (k',v'). cmp k k' = Less)`, 275 rw [relationTheory.transitive_def] >> 276 Cases_on `x` >> 277 Cases_on `y` >> 278 Cases_on `z` >> 279 fs [] >> 280 metis_tac [cmp_thms]); 281 282val good_cmp_Less_trans = Q.store_thm ("good_cmp_Less_trans", 283`!cmp. good_cmp cmp ==> transitive (\k k'. cmp k k' = Less)`, 284 rw [relationTheory.transitive_def] >> 285 fs [] >> 286 metis_tac [cmp_thms]); 287 288val good_cmp_Less_irrefl_trans = Q.store_thm ("good_cmp_Less_irrefl_trans", 289`!cmp. good_cmp cmp ==> (irreflexive (\k k'. cmp k k' = Less) /\ 290 transitive (\k k'. cmp k k' = Less))`, 291 simp [good_cmp_Less_trans, relationTheory.irreflexive_def] >> 292 simp [cmp_thms]); 293 294val bool_cmp_antisym = Q.store_thm ("bool_cmp_antisym[simp]", 295`!x y. bool_cmp x y = Equal <=> x = y`, 296 rw [] >> 297 Cases_on `x` >> 298 Cases_on `y` >> 299 rw [bool_cmp_def]); 300 301val num_cmp_antisym = Q.store_thm ("num_cmp_antisym[simp]", 302`!x y. num_cmp x y = Equal <=> x = y`, 303 rw [num_cmp_def]); 304 305val char_cmp_antisym = Q.store_thm ("char_cmp_antisym[simp]", 306`!x y. char_cmp x y = Equal <=> x = y`, 307 rw [char_cmp_def, num_cmp_antisym] >> 308 rw [ORD_11]); 309 310val list_cmp_antisym = Q.store_thm ("list_cmp_antisym", 311`!cmp x y. (!x y. cmp x y = Equal <=> x = y) ==> (list_cmp cmp x y = Equal <=> x = y)`, 312 ho_match_mp_tac list_cmp_ind >> 313 rw [list_cmp_def] >> 314 every_case_tac >> 315 rw [] >> 316 metis_tac [comparison_distinct]); 317 318val string_cmp_antisym = Q.store_thm ("string_cmp_antisym[simp]", 319`!x y. string_cmp x y = Equal <=> x = y`, 320 metis_tac [string_cmp_def, char_cmp_antisym, list_cmp_antisym]); 321 322val pair_cmp_antisym = Q.store_thm ("pair_cmp_antisym", 323`!cmp1 cmp2 x y. 324 (!x y. cmp1 x y = Equal <=> x = y) /\ 325 (!x y. cmp2 x y = Equal <=> x = y) 326 ==> 327 (pair_cmp cmp1 cmp2 x y = Equal <=> x = y)`, 328 Cases_on `x` >> 329 Cases_on `y` >> 330 rw [pair_cmp_def] >> 331 every_case_tac >> 332 rw [] >> 333 metis_tac [comparison_distinct]); 334 335val option_cmp_antisym = Q.store_thm ("option_cmp_antisym", 336`!cmp x y. 337 (!x y. cmp x y = Equal <=> x = y) 338 ==> 339 (option_cmp cmp x y = Equal <=> x = y)`, 340 Cases_on `x` >> 341 Cases_on `y` >> 342 rw [option_cmp_def] >> 343 every_case_tac >> 344 rw [] >> 345 metis_tac [comparison_distinct]); 346 347val option_cmp2_antisym = Q.store_thm ("option_cmp2_antisym", 348`!cmp x y. 349 (!x y. cmp x y = Equal <=> x = y) 350 ==> 351 (option_cmp2 cmp x y = Equal <=> x = y)`, 352 Cases_on `x` >> 353 Cases_on `y` >> 354 rw [option_cmp2_def] >> 355 every_case_tac >> 356 rw [] >> 357 metis_tac [comparison_distinct]); 358 359val resp_equiv_def = Define ` 360resp_equiv cmp f <=> !k1 k2 v. cmp k1 k2 = Equal ==> f k1 v = f k2 v`; 361 362val resp_equiv2_def = Define ` 363resp_equiv2 cmp cmp2 f <=> (!k1 k2. cmp k1 k2 = Equal ==> cmp2 (f k1) (f k2) = Equal)`; 364 365val equiv_inj_def = Define ` 366equiv_inj cmp cmp2 f <=> (!k1 k2. cmp2 (f k1) (f k2) = Equal ==> cmp k1 k2 = Equal)`; 367 368val antisym_resp_equiv = Q.store_thm ("antisym_resp_equiv", 369`!cmp f. 370 (!x y. cmp x y = Equal ==> x = y) 371 ==> 372 resp_equiv cmp f /\ !cmp2. good_cmp cmp2 ==> resp_equiv2 cmp cmp2 f`, 373 rw [resp_equiv_def, resp_equiv2_def] >> 374 metis_tac [cmp_thms]); 375 376val list_cmp_equal_list_rel = Q.store_thm ("list_cmp_equal_list_rel", 377`!cmp l1 l2. 378 list_cmp cmp l1 l2 = Equal <=> LIST_REL (\x y. cmp x y = Equal) l1 l2`, 379 Induct_on `l1` >> 380 rw [] >> 381 Cases_on `l2` >> 382 fs [list_cmp_def] >> 383 every_case_tac >> 384 fs []); 385 386val TO_of_LinearOrder_LLEX = store_thm("TO_of_LinearOrder_LLEX", 387 ``!R. irreflexive R ==> (TO_of_LinearOrder (LLEX R) = list_cmp (TO_of_LinearOrder R))``, 388 srw_tac[][relationTheory.irreflexive_def] >> 389 simp[FUN_EQ_THM] >> 390 Induct >- ( 391 Cases >> simp[list_cmp_def,TO_of_LinearOrder] ) >> 392 gen_tac >> Cases >> 393 simp[list_cmp_def,TO_of_LinearOrder] >> 394 pop_assum(assume_tac o GSYM) >> simp[] >> 395 srw_tac[][TO_of_LinearOrder] >> full_simp_tac(srw_ss())[] >> rev_full_simp_tac(srw_ss())[]) 396 397val _ = export_theory (); 398