1(*****************************************************************************) 2(* Encoding and decoding of finite maps to lists and then s-expressions *) 3(* *) 4(*****************************************************************************) 5 6(*****************************************************************************) 7(* Load theories *) 8(*****************************************************************************) 9 10(* 11load "finite_mapTheory"; 12load "sortingTheory"; 13load "translateTheory"; 14open finite_mapTheory sortingTheory pred_setTheory listTheory pred_setLib; 15*) 16 17(*****************************************************************************) 18(* Boilerplate needed for compilation: open HOL4 systems modules. *) 19(*****************************************************************************) 20 21open HolKernel Parse boolLib bossLib; 22 23(*****************************************************************************) 24(* Theories for compilation *) 25(*****************************************************************************) 26 27open finite_mapTheory pred_setTheory listTheory pred_setLib sortingTheory; 28 29(*****************************************************************************) 30(* Start new theory "fmap_encode" *) 31(*****************************************************************************) 32 33val _ = new_theory "fmap_encode"; 34 35val PULL_CONV = REPEATC (DEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC AND_IMP_INTRO_CONV)); 36val PULL_RULE = CONV_RULE PULL_CONV; 37 38val IND_STEP_TAC = PAT_ASSUM ``!y. P ==> Q`` (MATCH_MP_TAC o PULL_RULE); 39 40(*****************************************************************************) 41(* fold for finite maps *) 42(*****************************************************************************) 43 44val fold_def = TotalDefn.tDefine "fold" `fold f v map = 45 if map = FEMPTY 46 then v 47 else let x = (@x. x IN FDOM map) 48 in (f (x, map ' x) (fold f v (map \\ x)))` 49 (WF_REL_TAC `measure (FCARD o SND o SND)` THEN 50 RW_TAC std_ss [FDOM_FUPDATE,FCARD_DEF,FDOM_DOMSUB,CARD_DELETE,FDOM_FINITE] THEN 51 METIS_TAC [FDOM_F_FEMPTY1,CARD_EQ_0,FDOM_EQ_EMPTY,FDOM_FINITE,arithmeticTheory.NOT_ZERO_LT_ZERO]); 52 53(*****************************************************************************) 54(* Encoding and decoding to lists *) 55(* *) 56(* Note: M2L, like SET_TO_LIST, is non-deterministic, so we cannot prove *) 57(* M2L (L2M x) = x for any x. *) 58(* *) 59(*****************************************************************************) 60 61val M2L_def = Define `M2L = fold CONS []`; 62 63val L2M_def = Define `L2M = FOLDR (combin$C FUPDATE) FEMPTY`; 64 65val L2M = store_thm("L2M", 66 ``(L2M [] = FEMPTY) /\ (!a b. L2M (a::b) = L2M b |+ a)``, 67 RW_TAC std_ss [L2M_def,FOLDR]); 68 69(*****************************************************************************) 70(* Definitions to capture the properties that a list or a set representing *) 71(* a finite map would have. *) 72(*****************************************************************************) 73 74val uniql_def = 75 Define `uniql l = !x y y'. MEM (x,y) l /\ MEM (x,y') l ==> (y = y')`; 76 77val uniqs_def = 78 Define `uniqs s = !x y y'. (x,y) IN s /\ (x,y') IN s ==> (y = y')`; 79 80(*****************************************************************************) 81(* Theorems about uniqs and l *) 82(*****************************************************************************) 83 84val uniqs_cons = prove(``uniqs (a INSERT b) ==> uniqs b``, 85 RW_TAC std_ss [uniqs_def,IN_INSERT] THEN METIS_TAC []); 86 87val uniql_cons = prove(``!a h. uniql (h::a) ==> uniql a``, 88 Induct THEN RW_TAC std_ss [uniql_def, MEM] THEN METIS_TAC []); 89 90val uniqs_eq = prove(``!a. FINITE a ==> (uniqs a = uniql (SET_TO_LIST a))``, 91 HO_MATCH_MP_TAC FINITE_INDUCT THEN 92 RW_TAC std_ss [SET_TO_LIST_THM, FINITE_EMPTY, uniql_def, uniqs_def, MEM, NOT_IN_EMPTY] THEN 93 EQ_TAC THEN RW_TAC std_ss [] THEN 94 FIRST_ASSUM MATCH_MP_TAC THEN 95 Q.EXISTS_TAC `x` THEN 96 METIS_TAC [SET_TO_LIST_IN_MEM, FINITE_INSERT]); 97 98val uniql_eq = prove(``!x. uniql x = uniqs (set x)``, 99 RW_TAC std_ss [uniql_def, uniqs_def, IN_LIST_TO_SET]); 100 101val uniql_filter = prove(``!x. uniql x ==> uniql (FILTER P x)``, 102 METIS_TAC [MEM_FILTER, uniql_def]); 103 104val uniq_double = prove(``!a. uniql a ==> (uniql (SET_TO_LIST (set a)))``, 105 Induct THEN 106 RW_TAC std_ss [uniql_def, SET_TO_LIST_THM, LIST_TO_SET_THM, FINITE_EMPTY, 107 MEM_SET_TO_LIST, MEM, NOT_IN_EMPTY, FINITE_LIST_TO_SET, IN_INSERT, IN_LIST_TO_SET]); 108 109val uniql_empty = prove(``uniql []``, RW_TAC std_ss [MEM, uniql_def]); 110 111(*****************************************************************************) 112(* L2M_EQ: Lists representing maps give the same maps *) 113(* !l1 l2. uniql l1 /\ uniql l2 /\ (set l1 = set l2) ==> (L2M l1 = L2M l2) *) 114(*****************************************************************************) 115 116val delete_l2m = prove(``!a b. L2M a \\ b = L2M (FILTER ($~ o $= b o FST) a)``, 117 Induct THEN TRY Cases THEN REPEAT (RW_TAC std_ss [L2M, FILTER, DOMSUB_FEMPTY, DOMSUB_FUPDATE_NEQ, DOMSUB_FUPDATE])); 118 119val update_filter = prove(``!a b. L2M a |+ b = L2M (FILTER ($~ o $= (FST b) o FST) a) |+ b``, 120 GEN_TAC THEN Cases THEN RW_TAC std_ss [] THEN METIS_TAC [FUPDATE_PURGE, delete_l2m]); 121 122val length_filter = prove(``!a P. LENGTH (FILTER P a) <= LENGTH a``, 123 Induct THEN RW_TAC std_ss [LENGTH, FILTER] THEN METIS_TAC [DECIDE ``a <= b ==> a <= SUC b``]); 124 125val seteq_mem = prove(``!l1 l2. (set l1 = set l2) ==> (?h. MEM h l1 /\ MEM h l2) \/ (l1 = []) /\ (l2 = [])``, 126 Induct THEN RW_TAC std_ss [LENGTH, MEM, LIST_TO_SET_THM, LIST_TO_SET_EQ_EMPTY] THEN 127 METIS_TAC [IN_LIST_TO_SET, IN_INSERT]); 128 129val l2m_update = prove(``!l h. uniql l /\ MEM h l ==> (L2M l = L2M l |+ h)``, 130 Induct THEN TRY Cases THEN TRY (Cases_on `h'`) THEN RW_TAC std_ss [MEM,L2M] THEN RW_TAC std_ss [FUPDATE_EQ] THEN 131 REVERSE (Cases_on `q' = q`) THEN RW_TAC std_ss [FUPDATE_COMMUTES, FUPDATE_EQ] THEN1 METIS_TAC [FUPDATE_COMMUTES,uniql_cons] THEN 132 FULL_SIMP_TAC std_ss [uniql_def] THEN METIS_TAC [MEM]); 133 134val length_filter_mem = prove(``!l P. (?x. MEM x l /\ ~(P x)) ==> (LENGTH (FILTER P l) < LENGTH l)``, 135 Induct THEN RW_TAC std_ss [FILTER,LENGTH,MEM] THEN 136 METIS_TAC [length_filter, DECIDE ``a <= b ==> a < SUC b``]); 137 138val L2M_EQ = store_thm("L2M_EQ", 139 ``!l1 l2. uniql l1 /\ uniql l2 /\ (set l1 = set l2) ==> (L2M l1 = L2M l2)``, 140 REPEAT GEN_TAC THEN completeInduct_on `LENGTH l1 + LENGTH l2` THEN REPEAT STRIP_TAC THEN 141 PAT_ASSUM ``!y. P`` (ASSUME_TAC o CONV_RULE (REPEATC (DEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC AND_IMP_INTRO_CONV)))) THEN 142 IMP_RES_TAC seteq_mem THEN FULL_SIMP_TAC std_ss [L2M] THEN 143 IMP_RES_TAC l2m_update THEN ONCE_ASM_REWRITE_TAC [] THEN 144 ONCE_REWRITE_TAC [update_filter] THEN 145 AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 146 RW_TAC std_ss [GSYM LENGTH_APPEND, GSYM rich_listTheory.FILTER_APPEND, uniql_filter, LIST_TO_SET_FILTER] THEN 147 MATCH_MP_TAC length_filter_mem THEN 148 Q.EXISTS_TAC `h` THEN RW_TAC std_ss [MEM_APPEND]); 149 150(*****************************************************************************) 151(* L2M_DOUBLE: *) 152(* `!a. uniql a ==> (L2M (SET_TO_LIST (set a)) = L2M a)` *) 153(*****************************************************************************) 154 155val L2M_DOUBLE = prove(``!a. uniql a ==> (L2M (SET_TO_LIST (set a)) = L2M a)``, 156 METIS_TAC [uniq_double, L2M_EQ, FINITE_LIST_TO_SET, SET_TO_LIST_INV]); 157 158(*****************************************************************************) 159(* EXISTS_MEM_M2L: *) 160(* `!x a. (?y. MEM (a,y) (M2L x)) = a IN FDOM x` *) 161(*****************************************************************************) 162 163val not_fempty_eq = prove(``!x. ~(x = FEMPTY) = (?y. y IN FDOM x)``, 164 HO_MATCH_MP_TAC fmap_INDUCT THEN 165 RW_TAC std_ss [FDOM_FUPDATE, IN_INSERT, FDOM_FEMPTY, NOT_IN_EMPTY, NOT_EQ_FEMPTY_FUPDATE] THEN 166 PROVE_TAC []); 167 168val fcard_less = prove(``!y x. y IN FDOM x ==> FCARD (x \\ y) < FCARD x``, 169 RW_TAC std_ss [FCARD_DEF, FDOM_DOMSUB, CARD_DELETE, FDOM_FINITE] THEN 170 METIS_TAC [CARD_EQ_0, DECIDE ``0 < a = ��(a = 0:num)``, NOT_IN_EMPTY, FDOM_FINITE]); 171 172val uniql_rec = prove(``!x y. uniql x /\ ��(?z. MEM (y,z) x) ==> (uniql ((y,z)::x))``, 173 Induct THEN RW_TAC std_ss [uniql_def, MEM] THEN METIS_TAC []); 174 175val INSERT_SING = prove(``(a INSERT b = {a}) = (b = {}) \/ (b = {a})``, 176 ONCE_REWRITE_TAC [INSERT_SING_UNION] THEN RW_TAC std_ss [UNION_DEF,SET_EQ_SUBSET, SUBSET_DEF] THEN 177 RW_TAC (std_ss ++ PRED_SET_ss) [] THEN METIS_TAC []); 178 179val fold_FEMPTY = store_thm("fold_FEMPTY",``(!f v. fold f v FEMPTY = v)``, 180 ONCE_REWRITE_TAC [fold_def] THEN RW_TAC std_ss []); 181 182val infdom_lemma = prove(``!a b. ��(a = b) /\ a IN FDOM x ==> (b IN FDOM x = b IN FDOM (x \\ a))``, 183 RW_TAC (std_ss ++ PRED_SET_ss) [FDOM_DOMSUB, IN_DELETE]); 184 185val EXISTS_MEM_M2L = store_thm("EXISTS_MEM_M2L", 186 ``!x a. (?y. MEM (a,y) (M2L x)) = a IN FDOM x``, 187 GEN_TAC THEN completeInduct_on `FCARD x` THEN REPEAT STRIP_TAC THEN 188 PAT_ASSUM ``!y. P`` (ASSUME_TAC o CONV_RULE (REPEATC (DEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC AND_IMP_INTRO_CONV)))) THEN 189 FULL_SIMP_TAC std_ss [M2L_def] THEN 190 ONCE_REWRITE_TAC [fold_def] THEN REPEAT (CHANGED_TAC (RW_TAC std_ss [MEM, FDOM_FEMPTY, NOT_IN_EMPTY])) THEN 191 Cases_on `(a = x')` THEN RW_TAC std_ss [] THEN FULL_SIMP_TAC std_ss [] THEN 192 METIS_TAC [fcard_less, infdom_lemma, not_fempty_eq]); 193 194(*****************************************************************************) 195(* UNIQL_M2L: *) 196(* `!x. uniql (M2L x)` *) 197(*****************************************************************************) 198 199val UNIQL_M2L = store_thm("UNIQL_M2L", ``!x. uniql (M2L x)``, 200 GEN_TAC THEN completeInduct_on `FCARD x` THEN RW_TAC std_ss [M2L_def] THEN 201 ONCE_REWRITE_TAC [fold_def] THEN RW_TAC std_ss [uniql_empty,GSYM M2L_def] THEN 202 MATCH_MP_TAC uniql_rec THEN `x' IN FDOM x` by METIS_TAC [not_fempty_eq] THEN 203 RW_TAC std_ss [fcard_less] THEN 204 `��(x' IN FDOM (x \\ x'))` by RW_TAC std_ss [FDOM_DOMSUB, IN_DELETE] THEN 205 METIS_TAC [infdom_lemma,EXISTS_MEM_M2L]); 206 207(*****************************************************************************) 208(* MEM_M2L: *) 209(* `!x y z. MEM (y,z) (M2L x) = y IN FDOM x /\ (z = x ' y)` *) 210(*****************************************************************************) 211 212val MEM_M2L = store_thm("MEM_M2L", 213 ``!x y z. MEM (y,z) (M2L x) = y IN FDOM x /\ (z = x ' y)``, 214 GEN_TAC THEN completeInduct_on `FCARD x` THEN REPEAT STRIP_TAC THEN Cases_on `x = FEMPTY` THEN RW_TAC std_ss [M2L_def] THEN 215 ONCE_REWRITE_TAC [fold_def] THEN RW_TAC std_ss [GSYM M2L_def, MEM, FDOM_FEMPTY, NOT_IN_EMPTY] THEN 216 Cases_on `y = x'` THEN RW_TAC std_ss [MEM] THEN1 217 METIS_TAC [not_fempty_eq, EXISTS_MEM_M2L, IN_DELETE, FDOM_DOMSUB] THEN 218 PAT_ASSUM ``!y. P`` (ASSUME_TAC o CONV_RULE (REPEATC (DEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC AND_IMP_INTRO_CONV)))) THEN 219 FULL_SIMP_TAC std_ss [] THEN 220 `FCARD (x \\ x') < FCARD x` by METIS_TAC [fcard_less, not_fempty_eq] THEN 221 RW_TAC std_ss [FDOM_DOMSUB, DOMSUB_FAPPLY_NEQ, IN_DELETE]); 222 223(*****************************************************************************) 224(* L2M_M2L_SETLIST *) 225(* `!x. L2M (M2L x) = L2M (SET_TO_LIST (set (M2L x)))` *) 226(*****************************************************************************) 227 228val L2M_M2L_SETLIST = store_thm("L2M_M2L_SETLIST", 229 ``!x. L2M (M2L x) = L2M (SET_TO_LIST (set (M2L x)))``, 230 GEN_TAC THEN HO_MATCH_MP_TAC L2M_EQ THEN 231 RW_TAC std_ss [UNIQL_M2L, GSYM uniqs_eq, FINITE_LIST_TO_SET, GSYM uniql_eq, SET_TO_LIST_INV]); 232 233(*****************************************************************************) 234(* SET_M2L_FUPDATE: *) 235(* `!x y. set (M2L (x |+ y)) = set (y :: M2L (x \\ FST y))` *) 236(*****************************************************************************) 237 238val MEM_M2L_FUPDATE = prove(``!x y z. MEM (y,z) (M2L (x |+ (y,z)))``, 239 RW_TAC std_ss [MEM_M2L, FDOM_FUPDATE, FAPPLY_FUPDATE, IN_INSERT]); 240 241val MEM_M2L_PAIR = prove(``!x y. MEM y (M2L x) = (FST y) IN FDOM x /\ (SND y = x ' (FST y))``, 242 GEN_TAC THEN Cases THEN RW_TAC std_ss [MEM_M2L]); 243 244val SET_M2L_FUPDATE = store_thm("SET_M2L_FUPDATE", 245 ``!x y. set (M2L (x |+ y)) = set (y :: M2L (x \\ FST y))``, 246 RW_TAC std_ss [SET_EQ_SUBSET, SUBSET_DEF, LIST_TO_SET_THM, IN_INSERT, IN_LIST_TO_SET, MEM_M2L_PAIR, MEM] THEN 247 TRY (Cases_on `x'`) THEN TRY (Cases_on `y`) THEN Cases_on `q = q'` THEN 248 FULL_SIMP_TAC std_ss [FDOM_FUPDATE, IN_INSERT, FAPPLY_FUPDATE, FDOM_DOMSUB, IN_DELETE, DOMSUB_FAPPLY, DOMSUB_FAPPLY_NEQ, NOT_EQ_FAPPLY]); 249 250(*****************************************************************************) 251(* FDOM_L2M: *) 252(* `!x y. y IN FDOM (L2M x) = ?z. MEM (y,z) x` *) 253(*****************************************************************************) 254 255val FDOM_L2M = store_thm("FDOM_L2M", 256 ``!x y. y IN FDOM (L2M x) = ?z. MEM (y,z) x``, 257 Induct THEN TRY (Cases_on `h`) THEN 258 RW_TAC std_ss [L2M,MEM,FDOM_FEMPTY,NOT_IN_EMPTY,FDOM_FUPDATE,IN_INSERT] THEN 259 METIS_TAC []); 260 261(*****************************************************************************) 262(* FDOM_L2M_M2L *) 263(* `!x. FDOM (L2M (M2L x)) = FDOM x` *) 264(*****************************************************************************) 265 266val FDOM_L2M_M2L = prove(``!x. FDOM (L2M (M2L x)) = FDOM x``, 267 RW_TAC std_ss [SET_EQ_SUBSET, SUBSET_DEF, FDOM_L2M, MEM_M2L]); 268 269(*****************************************************************************) 270(* L2M_APPLY: *) 271(* `!x y z. uniql x /\ MEM (y,z) x ==> (L2M x ' y = z)` *) 272(*****************************************************************************) 273 274val L2M_APPLY = store_thm("L2M_APPLY", 275 ``!x y z. uniql x /\ MEM (y,z) x ==> (L2M x ' y = z)``, 276 Induct THEN TRY (Cases_on `h`) THEN RW_TAC std_ss [MEM,L2M] THEN 277 Cases_on `q = y` THEN RW_TAC std_ss [FAPPLY_FUPDATE,NOT_EQ_FAPPLY] THEN 278 REPEAT (POP_ASSUM MP_TAC) THEN REWRITE_TAC [MEM, uniql_def] THEN 279 METIS_TAC []); 280 281(*****************************************************************************) 282(* L2M_APPLY_MAP_EQ: *) 283(* `!x f g y. ONE_ONE f /\ (?z. MEM (y,z) x) ==> *) 284(* (L2M (MAP (f ## g) x) ' (f y) = g (L2M x ' y)) *) 285(*****************************************************************************) 286 287val L2M_APPLY_MAP_EQ = store_thm("L2M_APPLY_MAP_EQ", 288 ``!x f g y. ONE_ONE f /\ (?z. MEM (y,z) x) ==> (L2M (MAP (f ## g) x) ' (f y) = g (L2M x ' y))``, 289 Induct THEN NTAC 2 (RW_TAC std_ss [L2M, MAP, MEM,FAPPLY_FUPDATE_THM,pairTheory.PAIR_MAP]) THEN 290 FULL_SIMP_TAC std_ss [] THEN 291 Cases_on `h` THEN RW_TAC std_ss [FAPPLY_FUPDATE_THM] THEN 292 METIS_TAC [pairTheory.FST,ONE_ONE_THM]); 293 294(*****************************************************************************) 295(* APPLY_L2M_M2L *) 296(* `y IN FDOM x ==> (L2M (M2L x) ' y = x ' y)` *) 297(*****************************************************************************) 298 299val APPLY_L2M_M2L = store_thm("APPLY_L2M_M2L", 300 ``!x y. y IN FDOM x ==> (L2M (M2L x) ' y = x ' y)``, 301 METIS_TAC [L2M_APPLY, UNIQL_M2L, MEM_M2L, FDOM_L2M_M2L, FDOM_L2M]); 302 303(*****************************************************************************) 304(* L2M_M2L: *) 305(* `!x. L2M (M2L x) = x` *) 306(*****************************************************************************) 307 308val L2M_M2L = store_thm("L2M_M2L", 309 ``!x. L2M (M2L x) = x``, 310 REWRITE_TAC [GSYM SUBMAP_ANTISYM, SUBMAP_DEF, FDOM_L2M_M2L] THEN 311 RW_TAC std_ss [APPLY_L2M_M2L]); 312 313(*****************************************************************************) 314(* SETEQ *) 315(*****************************************************************************) 316 317val SETEQ_def = Define `SETEQ l1 l2 = !x. MEM x l1 = MEM x l2`; 318 319val SETEQ_TRANS = store_thm("SETEQ_TRANS", 320 ``!l1 l2 l3. SETEQ l1 l2 /\ SETEQ l2 l3 ==> SETEQ l1 l3``, 321 RW_TAC std_ss [SETEQ_def]); 322 323val SETEQ_SYM = store_thm("SETEQ_SYM", 324 ``!l. SETEQ l l``, 325 RW_TAC std_ss [SETEQ_def]); 326 327(*****************************************************************************) 328(* M2L_L2M_SETEQ: *) 329(* `!x. uniql x ==> SETEQ x (M2L (L2M x))` *) 330(*****************************************************************************) 331 332val lemma1 = prove(``!x y z. uniql (y::x) ==> !z. MEM (FST y,z) x ==> (z = SND y)``, 333 REPEAT (Cases ORELSE GEN_TAC) THEN REWRITE_TAC [uniql_def,MEM] THEN METIS_TAC []); 334 335val M2L_L2M_SETEQ = store_thm("M2L_L2M_SETEQ", 336 ``!x. uniql x ==> SETEQ x (M2L (L2M x))``, 337 Induct THEN RW_TAC std_ss [L2M, M2L_def, fold_FEMPTY, SETEQ_def,MEM] THEN 338 IMP_RES_TAC uniql_cons THEN 339 Cases_on `x' = h` THEN Cases_on `MEM x' x` THEN Cases_on `x'` THEN 340 RW_TAC std_ss [GSYM M2L_def,GSYM IN_LIST_TO_SET, SET_M2L_FUPDATE] THEN 341 RW_TAC std_ss [IN_LIST_TO_SET, MEM, MEM_M2L, FDOM_DOMSUB, DOMSUB_FAPPLY_THM, IN_DELETE, FDOM_L2M, L2M_APPLY] THEN 342 METIS_TAC [lemma1,pairTheory.PAIR, L2M_APPLY, uniql_def]); 343 344(*****************************************************************************) 345(* M2L_L2M_MAP_SETEQ: *) 346(* `!l f g. ONE_ONE f ==> *) 347(* SETEQ (M2L (L2M (MAP (f ## g) l))) (MAP (f ## g) (M2L (L2M l)))` *) 348(*****************************************************************************) 349 350val M2L_L2M_MAP_SETEQ = store_thm("M2L_L2M_MAP_SETEQ", 351 ``!l f g. ONE_ONE f ==> SETEQ (M2L (L2M (MAP (f ## g) l))) (MAP (f ## g) (M2L (L2M l)))``, 352 RW_TAC std_ss [SETEQ_def] THEN EQ_TAC THEN Cases_on `x` THEN 353 RW_TAC std_ss [pairTheory.PAIR_MAP, MEM_MAP,pairTheory.EXISTS_PROD, MEM_M2L,FDOM_L2M] THEN 354 TRY (Q.EXISTS_TAC `p_1`) THEN RW_TAC std_ss [] THEN 355 METIS_TAC [L2M_APPLY_MAP_EQ]); 356 357(*****************************************************************************) 358(* *) 359(*****************************************************************************) 360 361val SORTSET_def = Define `SORTSET sort relation = sort relation o SET_TO_LIST o set`; 362val SORTEDSET_def = Define `SORTEDSET r l = SORTED r l /\ ALL_DISTINCT l`; 363val MAPSET_def = Define `MAPSET r l = SORTED r l /\ ALL_DISTINCT (MAP FST l)`; 364 365local 366val not = ``$~ : bool -> bool``; 367in 368val RFILTER_EQ_NIL = 369 CONJ (REWRITE_RULE [] (AP_TERM not (SPEC_ALL FILTER_NEQ_NIL))) 370 (CONV_RULE (REWRITE_CONV [] THENC LAND_CONV SYM_CONV) (AP_TERM not (SPEC_ALL FILTER_NEQ_NIL))) 371end 372 373val ALL_DISTINCT_THM = ALL_DISTINCT_FILTER; 374 375(*****************************************************************************) 376(* PERM_S2L_L2S: *) 377(* `!l. ALL_DISTINCT l ==> PERM (SET_TO_LIST (set l)) l` *) 378(*****************************************************************************) 379 380val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS", 381 ``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``, 382 RW_TAC std_ss [ALL_DISTINCT_THM,FILTER,MEM] THEN 383 PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`) THEN RW_TAC std_ss [FILTER_NEQ_NIL] THEN 384 FIRST_ASSUM ACCEPT_TAC); 385 386val IN_FILTER_SET = prove(``!x y. FINITE x /\ y IN x ==> (FILTER ($= y) (SET_TO_LIST x) = [y])``, 387 GEN_TAC THEN completeInduct_on `CARD x` THEN 388 RW_TAC std_ss [SET_TO_LIST_THM, FILTER, FINITE_EMPTY, CHOICE_DEF] THEN 389 POP_ASSUM MP_TAC THEN RW_TAC std_ss [CHOICE_NOT_IN_REST, FINITE_REST, MEM_SET_TO_LIST, NOT_IN_EMPTY, RFILTER_EQ_NIL] THEN 390 PAT_ASSUM ``!y. P`` (MATCH_MP_TAC o CONV_RULE (REPEATC (DEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC AND_IMP_INTRO_CONV)))) THEN 391 Q.EXISTS_TAC `CARD (REST x)` THEN RW_TAC std_ss [FINITE_REST, REST_DEF, CARD_DELETE, CHOICE_DEF, IN_DELETE, GSYM arithmeticTheory.NOT_ZERO_LT_ZERO,CARD_EQ_0]); 392 393val NOT_IN_FILTER_SET = prove(``!x y. FINITE x /\ ~(y IN x) ==> (FILTER ($= y) (SET_TO_LIST x) = [])``, 394 RW_TAC std_ss [REWRITE_RULE [] (AP_TERM ``$~:bool -> bool`` (SPEC_ALL FILTER_NEQ_NIL)), MEM_SET_TO_LIST]); 395 396val FILTER_SET = store_thm("FILTER_SET", 397 ``!x. FINITE x ==> (!y. FILTER ($= y) (SET_TO_LIST x) = if y IN x then [y] else [])``, 398 METIS_TAC [IN_FILTER_SET, NOT_IN_FILTER_SET]); 399 400val PERM_S2L_L2S = store_thm("PERM_S2L_L2S", 401 ``!l. ALL_DISTINCT l ==> PERM (SET_TO_LIST (set l)) l``, 402 REPEAT (RW_TAC std_ss [PERM_DEF, FILTER_SET, FINITE_LIST_TO_SET, RFILTER_EQ_NIL, IN_LIST_TO_SET, ALL_DISTINCT_THM])); 403 404val NO_MEM_EMPTY = prove(``!l. (!x. ��(MEM x l)) = (l = [])``, 405 Induct THEN RW_TAC std_ss [MEM] THEN METIS_TAC []); 406 407val SORTED_APPEND = prove(``!a b r. transitive r /\ SORTED r (a ++ b) ==> !x y. MEM x a /\ MEM y b ==> r x y``, 408 Induct THEN METIS_TAC [APPEND,MEM,SORTED_EQ,MEM_APPEND]); 409 410val MEM_PERM = store_thm("MEM_PERM", 411 ``!l1 l2. PERM l1 l2 ==> (!a. MEM a l1 = MEM a l2)``, 412 METIS_TAC [Q.SPEC `$= a` MEM_FILTER, PERM_DEF]); 413 414val PERM_CONS_IFF2 = store_thm( 415 "PERM_CONS_IFF2", 416 ``PERM (h1::t1) (h2::t1) <=> (h1 = h2)``, 417 `!x:'a y. x::y = [x] ++ y` by SRW_TAC [][] THEN 418 POP_ASSUM (fn th => ONCE_REWRITE_TAC [th]) THEN 419 ASM_REWRITE_TAC [PERM_APPEND_IFF] THEN SRW_TAC [][] THEN METIS_TAC []); 420 421val PERM_SORTED_EQ = store_thm( 422 "PERM_SORTED_EQ", 423 ``!l1 l2 r. 424 (irreflexive r \/ antisymmetric r) /\ transitive r /\ PERM l1 l2 /\ 425 SORTED r l1 /\ SORTED r l2 ==> (l1 = l2)``, 426 REPEAT GEN_TAC THEN completeInduct_on `LENGTH l1 + LENGTH l2` THEN 427 MAP_EVERY Q.X_GEN_TAC [`l1`, `l2`] THEN 428 `(l1 = []) \/ ?h1 t1. l1 = h1::t1` by (Cases_on `l1` THEN METIS_TAC []) THEN 429 `(l2 = []) \/ ?h2 t2. l2 = h2::t2` by (Cases_on `l2` THEN METIS_TAC []) THEN 430 TRY (SRW_TAC [][] THEN NO_TAC) THEN 431 REPEAT BasicProvers.VAR_EQ_TAC THEN 432 SIMP_TAC (srw_ss()) [] THEN STRIP_TAC THEN BasicProvers.VAR_EQ_TAC THEN 433 DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN 434 `t1 = t2` 435 by (IND_STEP_TAC THEN 436 REPEAT (Q.PAT_ASSUM `SORTED r X` MP_TAC) THEN 437 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [SORTED_EQ] THEN 438 Q.PAT_ASSUM `PERM X Y` MP_TAC THEN 439 ASM_SIMP_TAC (srw_ss()) [PERM_CONS_EQ_APPEND] THEN 440 DISCH_THEN (Q.X_CHOOSE_THEN `M` MP_TAC) THEN 441 `(M = []) \/ ?h0 t0. M = h0::t0` 442 by (Cases_on `M` THEN SRW_TAC [][]) THEN 443 ASM_SIMP_TAC (srw_ss()) [] THEN 444 DISCH_THEN (Q.X_CHOOSE_THEN `N` STRIP_ASSUME_TAC) THEN 445 REPEAT BasicProvers.VAR_EQ_TAC THEN REPEAT STRIP_TAC THEN 446 `h0 = h1` by 447 METIS_TAC [MEM_PERM, MEM, MEM_APPEND, SORTED_APPEND, 448 relationTheory.irreflexive_def, 449 relationTheory.antisymmetric_def, 450 relationTheory.transitive_def] THEN 451 BasicProvers.VAR_EQ_TAC THEN 452 Q_TAC SUFF_TAC `PERM (t0 ++ [h0] ++ N) (h0::(t0 ++ N))` 453 THEN1 METIS_TAC [PERM_TRANS, PERM_SYM] THEN 454 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 455 `h0::(t0 ++ N) = [h0] ++ t0 ++ N` by SRW_TAC [][] THEN 456 POP_ASSUM SUBST1_TAC THEN 457 REWRITE_TAC [PERM_APPEND_IFF, PERM_APPEND]) THEN 458 POP_ASSUM SUBST_ALL_TAC THEN 459 FULL_SIMP_TAC (srw_ss()) [PERM_CONS_IFF2]); 460 461val SORTSET_SORTEDSET = store_thm("SORTSET_SORTEDSET", 462 ``!l. transitive R /\ (irreflexive R \/ antisymmetric R) /\ SORTS sort R /\ SORTEDSET R l ==> (SORTSET sort R l = l)``, 463 RW_TAC std_ss [SORTEDSET_def,SORTSET_def, SETEQ_def, SORTS_DEF] THEN 464 `PERM (sort R (SET_TO_LIST (set l))) l` by METIS_TAC [PERM_SYM, PERM_TRANS, PERM_S2L_L2S] THEN 465 METIS_TAC [PERM_SORTED_EQ]); 466 467val ALL_DISTINCT_M2L = store_thm("ALL_DISTINCT_M2L", 468 ``!s. ALL_DISTINCT (M2L s)``, 469 completeInduct_on `FCARD s` THEN REPEAT STRIP_TAC THEN 470 REWRITE_TAC [M2L_def] THEN ONCE_REWRITE_TAC [fold_def] THEN 471 NTAC 2 (RW_TAC std_ss [ALL_DISTINCT, GSYM M2L_def,MEM_M2L,FDOM_DOMSUB,IN_DELETE]) THEN 472 IND_STEP_TAC THEN 473 METIS_TAC [fcard_less, not_fempty_eq]); 474 475val ALL_DISTINCT_MAPFST_M2L = store_thm("ALL_DISTINCT_MAPFST_M2L", 476 ``!s. ALL_DISTINCT (MAP FST (M2L s))``, 477 completeInduct_on `FCARD s` THEN REPEAT STRIP_TAC THEN 478 REWRITE_TAC [M2L_def] THEN ONCE_REWRITE_TAC [fold_def] THEN 479 NTAC 2 (RW_TAC std_ss [ALL_DISTINCT, GSYM M2L_def,MEM_M2L,FDOM_DOMSUB,IN_DELETE,MAP,MEM_MAP]) THEN 480 (IND_STEP_TAC ORELSE Cases_on `y` THEN RW_TAC std_ss [ALL_DISTINCT, GSYM M2L_def,MEM_M2L,FDOM_DOMSUB,IN_DELETE,MAP,MEM_MAP]) THEN 481 METIS_TAC [fcard_less, not_fempty_eq]); 482 483val PERM_DISTINCT = sortingTheory.ALL_DISTINCT_PERM 484 485val SORTSET_SORT = prove(``!l R. (antisymmetric R \/ irreflexive R) /\ transitive R /\ SORTS sort R /\ ALL_DISTINCT l ==> (SORTSET sort R l = sort R l)``, 486 RW_TAC std_ss [SORTS_DEF,SORTSET_def] THEN 487 `PERM l (sort R (SET_TO_LIST (set l)))` by METIS_TAC [PERM_S2L_L2S, PERM_DISTINCT, PERM_TRANS, PERM_SYM] THEN 488 MATCH_MP_TAC PERM_SORTED_EQ THEN RW_TAC std_ss [] THEN 489 Q.EXISTS_TAC `R` THEN RW_TAC std_ss [] THEN 490 METIS_TAC [PERM_S2L_L2S, PERM_DISTINCT, PERM_TRANS, PERM_SYM]); 491 492val PERM_S2L_L2S_EQ = prove(``!l1 l2. SETEQ l1 l2 ==> PERM (SET_TO_LIST (set l1)) (SET_TO_LIST (set l2))``, 493 RW_TAC std_ss [PERM_DEF, FILTER_SET, FINITE_LIST_TO_SET,IN_LIST_TO_SET,SETEQ_def]); 494 495val PERM_SETEQ = store_thm("PERM_SETEQ", 496 ``!l1 l2. PERM l1 l2 ==> SETEQ l1 l2``, 497 Induct THEN RW_TAC std_ss [PERM_CONS_EQ_APPEND, PERM_NIL,SETEQ_def] THEN 498 Cases_on `x = h` THEN ASM_REWRITE_TAC [MEM, MEM_APPEND] THEN EQ_TAC THEN 499 RES_TAC THEN FULL_SIMP_TAC std_ss [SETEQ_def, MEM_APPEND]); 500 501val SETEQ_THM = store_thm("SETEQ_THM", 502 ``!l1 l2. SETEQ l1 l2 = (set l1 = set l2)``, 503 RW_TAC std_ss [pred_setTheory.EXTENSION, SETEQ_def, IN_LIST_TO_SET]); 504 505val SORTSET_EQ = prove(``!l1 l2 R. SORTS sort R /\ (irreflexive R \/ antisymmetric R) /\ transitive R /\ SETEQ l1 l2 ==> (SORTSET sort R l1 = SORTSET sort R l2)``, 506 RW_TAC std_ss [SORTSET_def, SORTS_DEF] THEN 507 MATCH_MP_TAC PERM_SORTED_EQ THEN Q.EXISTS_TAC `R` THEN RW_TAC std_ss [] THEN 508 METIS_TAC [PERM_S2L_L2S_EQ,PERM_TRANS,PERM_SYM, PERM_SETEQ]); 509 510val MAPSET_IMP_SORTEDSET = prove(``!l R. transitive R ==> (MAPSET R l ==> SORTEDSET R l)``, 511 Induct THEN RW_TAC std_ss [MAPSET_def, SORTEDSET_def, ALL_DISTINCT, MAP, MEM_MAP] THEN 512 METIS_TAC [MAPSET_def, SORTEDSET_def, SORTED_EQ]); 513 514val SORTED_CONS = store_thm("SORTED_CONS", 515 ``!a b R. SORTED R (a::b) ==> SORTED R b``, 516 GEN_TAC THEN Cases THEN RW_TAC std_ss [SORTED_DEF]); 517 518val MAPSET_CONS = store_thm("MAPSET_CONS", 519 ``!a b R. MAPSET R (a::b) ==> MAPSET R b``, 520 RW_TAC std_ss [MAPSET_def, MAP, ALL_DISTINCT, SORTED_CONS] THEN 521 METIS_TAC [SORTED_CONS]); 522 523val MAPSET_UNIQ = store_thm("MAPSET_UNIQ", 524 ``!a R. MAPSET R a ==> uniql a``, 525 Induct THEN REPEAT STRIP_TAC THEN IMP_RES_TAC MAPSET_CONS THEN RES_TAC THEN 526 FULL_SIMP_TAC std_ss [uniql_def, MEM, uniql_def, MAPSET_def, MAP, ALL_DISTINCT, MEM_MAP] THEN 527 Cases_on `h` THEN RW_TAC std_ss [] THENL [ 528 PAT_ASSUM ``!y. P \/ Q`` (MP_TAC o Q.SPEC `(q,y')`), 529 PAT_ASSUM ``!y. P \/ Q`` (MP_TAC o Q.SPEC `(q,y)`), 530 ALL_TAC] THEN 531 ASM_REWRITE_TAC [] THEN METIS_TAC []); 532 533val ALL_DISTINCT_MAPFST = store_thm("ALL_DISTINCT_MAPFST", 534 ``!l. ALL_DISTINCT (MAP FST l) ==> ALL_DISTINCT l``, 535 Induct THEN RW_TAC std_ss [ALL_DISTINCT,MAP,MEM_MAP] THEN 536 METIS_TAC []); 537 538val MAPSET_DISTINCT = store_thm("MAPSET_DISTINCT", 539 ``MAPSET R x ==> ALL_DISTINCT x``, 540 METIS_TAC [MAPSET_def,ALL_DISTINCT_MAPFST]); 541 542val TOTAL_LEX = store_thm("TOTAL_LEX",``!R R'. total R /\ total R' ==> total (R LEX R')``, 543 RW_TAC std_ss [pairTheory.LEX_DEF,relationTheory.total_def] THEN 544 Cases_on `x` THEN Cases_on `y` THEN RW_TAC std_ss [] THEN 545 METIS_TAC []); 546 547val TRANSITIVE_LEX = store_thm("TRANSITIVE_LEX", 548 ``!R R'. transitive R /\ transitive R' ==> transitive (R LEX R')``, 549 RW_TAC std_ss [pairTheory.LEX_DEF,relationTheory.transitive_def] THEN 550 Cases_on `x` THEN Cases_on `y` THEN Cases_on `z` THEN RW_TAC std_ss [] THEN 551 FULL_SIMP_TAC std_ss [] THEN 552 METIS_TAC []); 553 554val SORTED_LEX = store_thm("SORTED_LEX", 555 ``!R1 R2. total R1 /\ transitive R1 /\ transitive R2 ==> !x. SORTED (R1 LEX R2) x ==> SORTED R1 (MAP FST x)``, 556 NTAC 3 STRIP_TAC THEN Induct THEN TRY Cases THEN RW_TAC std_ss [SORTED_EQ,MAP,SORTED_DEF,TRANSITIVE_LEX,MEM_MAP,pairTheory.LEX_DEF] THEN 557 RES_TAC THEN Cases_on `y'` THEN FULL_SIMP_TAC std_ss [] THEN 558 METIS_TAC [relationTheory.transitive_def, relationTheory.total_def]); 559 560val filter_first = prove(``!l x y. (FILTER ($= x) (MAP FST l) = [x]) /\ (x = FST y) /\ MEM y l ==> (FILTER ($= x o FST) l = [y])``, 561 Induct THEN RW_TAC std_ss [FILTER,MEM,RFILTER_EQ_NIL] THEN 562 FULL_SIMP_TAC std_ss [MAP,FILTER,list_11,RFILTER_EQ_NIL, MEM_MAP] THEN 563 FIRST [PAT_ASSUM ``a = b`` MP_TAC, METIS_TAC []] THEN 564 RW_TAC std_ss [RFILTER_EQ_NIL, MEM_MAP] THEN METIS_TAC []); 565 566val MAP_FST_DISTINCT_EQ = store_thm("MAP_FST_DISTINCT_EQ", 567 ``!l1 l2. (MAP FST l1 = MAP FST l2) /\ ALL_DISTINCT (MAP FST l1) /\ PERM l1 l2 ==> (l1 = l2)``, 568 REPEAT STRIP_TAC THEN MATCH_MP_TAC LIST_EQ THEN RW_TAC std_ss [PERM_LENGTH,pairTheory.PAIR_FST_SND_EQ] THEN 569 `FST (EL x l1) = FST (EL x l2)` by METIS_TAC [EL_MAP, PERM_LENGTH] THEN 570 FULL_SIMP_TAC std_ss [ALL_DISTINCT_FILTER] THEN 571 `MEM (FST (EL x l2)) (MAP FST l2) /\ MEM (FST (EL x l1)) (MAP FST l1)` by METIS_TAC [MEM_MAP, rich_listTheory.EL_IS_EL,PERM_LENGTH] THEN 572 MAP_EVERY (fn x => x by (MATCH_MP_TAC filter_first THEN METIS_TAC [filter_first, rich_listTheory.EL_IS_EL, PERM_LENGTH, MEM_PERM])) [ 573 `FILTER ($= (FST (EL x l2)) o FST) l2 = [EL x l2]`, 574 `FILTER ($= (FST (EL x l2)) o FST) l2 = [EL x l1]`] THEN 575 METIS_TAC [pairTheory.PAIR,list_11]); 576 577 578val SETEQ_PERM = store_thm("SETEQ_PERM", 579 ``!l1 l2. SETEQ l1 l2 /\ ALL_DISTINCT l1 /\ ALL_DISTINCT l2 ==> PERM l1 l2``, 580 RW_TAC std_ss [SETEQ_def, ALL_DISTINCT_FILTER, PERM_DEF] THEN 581 Cases_on `MEM x l1` THEN1 METIS_TAC [FILTER_NEQ_NIL] THEN 582 MAP_EVERY (fn x => x by RW_TAC std_ss [RFILTER_EQ_NIL]) 583 [`FILTER ($= x) l1 = []`, `FILTER ($= x) l2 = []`] THEN 584 METIS_TAC []); 585 586(*****************************************************************************) 587(* M2L_L2M: *) 588(*`!R R' sort. total R /\ transitive R /\ transitive R' /\ antisymmetric R *) 589(* /\ SORTS sort (R LEX R') *) 590(* ==> !l. MAPSET (R LEX R') l *) 591(* ==> (sort (R LEX R') (M2L (L2M l)) = l)` *) 592(*****************************************************************************) 593 594val M2L_L2M = store_thm("M2L_L2M", 595 ``!sort R R'. total R /\ antisymmetric R /\ transitive R /\ transitive R' /\ 596 SORTS sort (R LEX R') ==> !l. MAPSET (R LEX R') l 597 ==> (sort (R LEX R') (M2L (L2M l)) = l)``, 598 REPEAT STRIP_TAC THEN 599 CONV_TAC SYM_CONV THEN MATCH_MP_TAC MAP_FST_DISTINCT_EQ THEN 600 IMP_RES_TAC MAPSET_def THEN 601 REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [SORTS_DEF] THEN 602 TRY ( 603 MATCH_MP_TAC PERM_SORTED_EQ THEN Q.EXISTS_TAC `R` THEN REPEAT CONJ_TAC THEN TRY (MATCH_MP_TAC (PULL_RULE SORTED_LEX) THEN METIS_TAC []) THEN 604 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC PERM_MAP) THEN 605 MATCH_MP_TAC SETEQ_PERM THEN 606 RW_TAC std_ss [ALL_DISTINCT_MAPFST] THEN 607 REPEAT (MAP_FIRST MATCH_MP_TAC [PERM_SETEQ, PERM_TRANS]) THEN 608 TRY (Q.EXISTS_TAC `M2L (L2M l)`) THEN RW_TAC std_ss [] THEN 609 TRY (MATCH_MP_TAC SETEQ_PERM) THEN 610 METIS_TAC [M2L_L2M_SETEQ, MAPSET_UNIQ, ALL_DISTINCT_PERM, ALL_DISTINCT_M2L, ALL_DISTINCT_MAPFST]); 611 612(*****************************************************************************) 613(* Other ordering theorems.... *) 614(*****************************************************************************) 615 616val TRANS_INV = store_thm("TRANS_INV", 617 ``!R f. transitive R ==> transitive (inv_image R f)``, 618 RW_TAC std_ss [relationTheory.transitive_def,relationTheory.inv_image_def] THEN 619 METIS_TAC []); 620 621val TOTAL_INV = store_thm("TOTAL_INV", 622 ``!R f. total R ==> total (inv_image R f)``, 623 RW_TAC std_ss [relationTheory.total_def,relationTheory.inv_image_def] THEN 624 METIS_TAC []); 625 626val IRREFL_INV = store_thm("IRREFL_INV", 627 ``!R f. irreflexive R ==> irreflexive (inv_image R f)``, 628 RW_TAC std_ss [relationTheory.irreflexive_def,relationTheory.inv_image_def] THEN 629 METIS_TAC []); 630 631val ANTISYM_INV = store_thm("ANTISYM_INV", 632 ``!R f. ONE_ONE f /\ antisymmetric R ==> antisymmetric (inv_image R f)``, 633 RW_TAC std_ss [relationTheory.antisymmetric_def,relationTheory.inv_image_def, ONE_ONE_DEF]); 634 635val COM_LT_TRANS = prove(``!a b c. a < b /\ b < c ==> a < c : complex_rational``, 636 REPEAT Cases THEN RW_TAC std_ss [complex_rationalTheory.COMPLEX_LT_def] THEN 637 METIS_TAC [ratTheory.RAT_LES_TRANS]); 638 639val COM_LT_REFL = prove(``!a. ~(a < a : complex_rational)``, 640 REPEAT Cases THEN RW_TAC std_ss [complex_rationalTheory.COMPLEX_LT_def] THEN 641 METIS_TAC [ratTheory.RAT_LES_REF]); 642 643val COM_LT_TOTAL = prove(``!a b. a < b \/ b < a \/ (a = b : complex_rational)``, 644 REPEAT Cases THEN RW_TAC std_ss [complex_rationalTheory.COMPLEX_LT_def] THEN 645 METIS_TAC [ratTheory.RAT_LES_TOTAL]); 646 647(*****************************************************************************) 648(* SEXP Ordering theorems *) 649(*****************************************************************************) 650 651val SEXP_LE_def = Define `SEXP_LE a b = |= lexorder a b`; 652 653val _ = overload_on ("<=", ``SEXP_LE``); 654 655val lexorder_def = hol_defaxiomsTheory.lexorder_def; 656 657val sym_rwr = prove(`` 658 (!a b c. lexorder (sym a b) (chr c) = nil) /\ 659 (!a b c d. lexorder (sym a b) (cons c d) = t) /\ 660 (!a b c. lexorder (sym a b) (str c) = nil) /\ 661 (!a b c. lexorder (chr a) (sym b c) = t) /\ 662 (!a b c d. lexorder (cons a b) (sym c d) = nil) /\ 663 (!a b c. lexorder (str a) (sym b c) = t)``, 664 ONCE_REWRITE_TAC [lexorder_def] THEN RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def]); 665 666val bool_rwr = prove(``!a. bool a = if a then t else nil``,Cases THEN RW_TAC std_ss [translateTheory.bool_def]); 667 668val LIST_LEX_ORDER_NIL = store_thm( 669 "LIST_LEX_ORDER_NIL", 670 ``(LIST_LEX_ORDER R [] x = x <> []) /\ (LIST_LEX_ORDER R x [] = F)``, 671 Cases_on `x` THEN SRW_TAC [][sexpTheory.LIST_LEX_ORDER_def]); 672 673val EXPLODE_I = prove( 674 ``EXPLODE s = s``, 675 Induct_on `s` THEN SRW_TAC [][]); 676 677val consp_list_to_sexp = store_thm( 678 "consp_list_to_sexp", 679 ``((consp (list_to_sexp f b) = nil) <=> (b = [])) /\ 680 ((consp (list_to_sexp f b) = sym "COMMON-LISP" "NIL") <=> (b = []))``, 681 Induct_on `b` THEN 682 SRW_TAC [][sexpTheory.list_to_sexp_def, hol_defaxiomsTheory.ACL2_SIMPS]); 683 684val sexp_str_lt_l1 = prove( 685 ``!a b c. 686 (string_less_l (list_to_sexp chr a) (list_to_sexp chr b) (int c) = nil) = 687 ~STRING_LESS a b``, 688 Induct THEN (GEN_TAC THEN Cases ORELSE Cases) THEN 689 ONCE_REWRITE_TAC [hol_defaxiomsTheory.string_less_l_def] THEN 690 RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def, 691 sexpTheory.coerce_string_to_list_def, 692 EXPLODE_I, sexpTheory.list_to_sexp_def, 693 sexpTheory.STRING_LESS_IRREFLEXIVE, 694 GSYM translateTheory.INT_LT, integerTheory.INT_LT_CALCULATE, 695 bool_rwr, sexpTheory.STRING_LESS_def, 696 sexpTheory.LIST_LEX_ORDER_def, MAP, stringTheory.ORD_11, 697 sexpTheory.cpx_def, LIST_LEX_ORDER_NIL, MAP_EQ_NIL] THEN 698 REPEAT (POP_ASSUM MP_TAC) THEN 699 RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS] THEN 700 FULL_SIMP_TAC std_ss [GSYM sexpTheory.cpx_def, translateTheory.COM_THMS, GSYM sexpTheory.int_def, GSYM translateTheory.INT_THMS,integerTheory.INT_ADD_REDUCE, sexpTheory.STRING_LESS_def] THEN 701 RW_TAC std_ss [sexpTheory.int_def,sexpTheory.cpx_def, EXPLODE_I] THEN 702 FULL_SIMP_TAC (srw_ss()) [consp_list_to_sexp]); 703 704val len_not_nil = prove(``!a. ~(len a = nil)``, 705 Cases THEN ONCE_REWRITE_TAC [hol_defaxiomsTheory.len_def] THEN RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.nat_def, sexpTheory.int_def, sexpTheory.cpx_def] THEN 706 Cases_on `len s0` THEN RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.nat_def, sexpTheory.int_def]); 707 708val STRING_LESS_EQ_THM = prove( 709 ``(STRING_LESS_EQ "" x = T) /\ 710 (STRING_LESS_EQ x "" = (x = "")) /\ 711 (STRING_LESS_EQ (STRING c1 s1) (STRING c2 s2) = 712 ORD c1 < ORD c2 \/ (c1 = c2) /\ STRING_LESS_EQ s1 s2)``, 713 SRW_TAC [][sexpTheory.STRING_LESS_EQ_def, sexpTheory.STRING_LESS_def, 714 sexpTheory.LIST_LEX_ORDER_def, EXPLODE_I, 715 LIST_LEX_ORDER_NIL, stringTheory.ORD_11] THEN 716 METIS_TAC []); 717 718fun Prove(t,tac) = let val th = prove(t,tac) 719 in augment_srw_ss[rewrites [th]]; th end; 720 721val not_nil = store_thm( 722 "not_nil", 723 ``not nil = t``, 724 SRW_TAC [][hol_defaxiomsTheory.not_def, sexpTheory.ite_def]); 725 726val ite_rewrites = store_thm( 727 "ite_rewrites", 728 ``(ite nil a b = b) /\ (ite t a b = a)``, 729 REWRITE_TAC [translateTheory.TRUTH_REWRITES]); 730 731val t_neq_nil = Prove( 732 ``t <> nil``, 733 SRW_TAC [][sexpTheory.t_def, sexpTheory.nil_def]); 734 735val equal_str = Prove( 736 ``equal (str x) (str y) = bool (x = y)``, 737 SRW_TAC [][sexpTheory.equal_def, translateTheory.bool_def]); 738 739val ite_bool = prove( 740 ``ite (bool p) x y = if p then x else y``, 741 SRW_TAC [][sexpTheory.ite_def] THEN 742 FULL_SIMP_TAC (srw_ss()) [translateTheory.bool_def, t_neq_nil]); 743 744val _ = augment_srw_ss [rewrites [sexpTheory.consp_def, not_nil, 745 sexpTheory.rationalp_def, 746 sexpTheory.complex_rationalp_def, 747 sexpTheory.characterp_def, 748 sexpTheory.stringp_def, 749 sexpTheory.andl_def, 750 ite_rewrites, sexpTheory.equal_def]]; 751 752val bool_ite = Prove( 753 ``((ite x t nil = nil) = (x = nil)) /\ 754 ((ite x t nil = t) = x <> nil)``, 755 SRW_TAC [][sexpTheory.ite_def]); 756 757val alphorder_str = Prove( 758 ``alphorder (str x) (str y) = ite (string_less_equal (str x) (str y)) t nil``, 759 SRW_TAC [][hol_defaxiomsTheory.alphorder_def, sexpTheory.itel_def]); 760 761val STRING_LESS_EQ_REFL = store_thm( 762 "STRING_LESS_EQ_REFL", 763 ``STRING_LESS_EQ x x``, 764 REWRITE_TAC [sexpTheory.STRING_LESS_EQ_def]); 765val _ = augment_srw_ss [rewrites [STRING_LESS_EQ_REFL]] 766 767val int_not_nil = Prove( 768 ``int i <> nil``, 769 SRW_TAC [][sexpTheory.nil_def, sexpTheory.int_def, sexpTheory.cpx_def]); 770 771val nat_not_nil = Prove( 772 ``nat x <> nil``, 773 SRW_TAC [][sexpTheory.nat_def]); 774 775val list_eq_list_to_sexp = Prove( 776 ``list f x = list_to_sexp f x``, 777 Induct_on `x` THEN 778 SRW_TAC [][translateTheory.list_def, sexpTheory.list_to_sexp_def]); 779 780val lexorder_str_string = prove( 781 ``!a b. lexorder (str a) (str b) = if STRING_LESS_EQ a b then t else nil``, 782 SRW_TAC [][Once lexorder_def, sexpTheory.itel_def, 783 hol_defaxiomsTheory.atom_def, hol_defaxiomsTheory.not_def, 784 hol_defaxiomsTheory.alphorder_def, ite_bool, 785 hol_defaxiomsTheory.string_less_equal_def, 786 hol_defaxiomsTheory.string_less_def, 787 sexp_str_lt_l1, GSYM translateTheory.STRING_THMS, 788 sexpTheory.COMMON_LISP_def, sexpTheory.STRING_LESS_EQ_def, 789 GSYM sexpTheory.int_def, EXPLODE_I] THEN 790 FULL_SIMP_TAC (srw_ss()) []); 791 792val lexorder_char = prove(``!a b. lexorder (chr a) (chr b) = if ORD a <= ORD b then t else nil``, 793 ONCE_REWRITE_TAC [lexorder_def] THEN RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def] THEN 794 REPEAT (CHANGED_TAC (REPEAT (POP_ASSUM MP_TAC) THEN 795 RW_TAC std_ss [GSYM translateTheory.INT_THMS, translateTheory.bool_def, integerTheory.INT_GT_CALCULATE, integerTheory.INT_LT_CALCULATE, hol_defaxiomsTheory.ACL2_SIMPS, bool_rwr])) THEN 796 FULL_SIMP_TAC std_ss [GSYM stringTheory.ORD_11] THEN 797 DECIDE_TAC); 798 799val string_less_l_nil = prove(``!a b. string_less_l (str a) (str b) (int 0) = nil``, 800 ONCE_REWRITE_TAC [hol_defaxiomsTheory.string_less_l_def] THEN 801 RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def, sexpTheory.coerce_string_to_list_def, 802 stringTheory.EXPLODE_def, sexpTheory.list_to_sexp_def, 803 sexpTheory.STRING_LESS_IRREFLEXIVE, GSYM translateTheory.INT_LT, integerTheory.INT_LT_CALCULATE, 804 bool_rwr, sexpTheory.STRING_LESS_def, sexpTheory.LIST_LEX_ORDER_def, MAP, stringTheory.ORD_11, sexpTheory.cpx_def]); 805 806(*---------------------------------------------------------------------------*) 807(* In the good old days, strings were a separate type. Now the string type *) 808(* is an abbreviation for :char list. As a consequence, EXPLODE is the *) 809(* identity function. I am not sure if one should prove this fact in *) 810(* stringTheory. YES: because it is true; NO: because one would like strings *) 811(* to be an abstract entity characterized by some operations. *) 812(*---------------------------------------------------------------------------*) 813 814val EXPLODE_ID_LEM = prove 815(``!s. EXPLODE s = s``, Induct THEN SRW_TAC [] []); 816 817 818val lexorder_sym = prove( 819``lexorder (sym a b) (sym c d) = 820 if ~(a = "") /\ (BASIC_INTERN b a = sym a b) 821 then if ~(c = "") /\ (BASIC_INTERN d c = sym c d) 822 then if STRING_LESS b d \/ (b = d) /\ STRING_LESS_EQ a c then t else nil 823 else t 824 else if ~(c = "") /\ (BASIC_INTERN d c = sym c d) 825 then nil 826 else if STRING_LESS a c \/ (a = c) /\ STRING_LESS_EQ b d then t else nil``, 827 ONCE_REWRITE_TAC [lexorder_def] THEN 828 REWRITE_TAC [sexpTheory.coerce_string_to_list_def, 829 hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def, 830 sexpTheory.SEXP_SYM_LESS_EQ_def,sexpTheory.SEXP_SYM_LESS_def] THEN 831 REPEAT (CHANGED_TAC (REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC (std_ss ++ boolSimps.LET_ss) 832 [GSYM sexpTheory.int_def, hol_defaxiomsTheory.ACL2_SIMPS, 833 sexpTheory.coerce_string_to_list_def, 834 REWRITE_RULE [sexpTheory.nil_def] sexp_str_lt_l1, 835 string_less_l_nil, sexpTheory.COMMON_LISP_def])) THEN 836 METIS_TAC [sexpTheory.STRING_LESS_TRANS, 837 sexpTheory.STRING_LESS_TRANS_NOT, 838 EXPLODE_ID_LEM, 839 sexpTheory.STRING_LESS_TRICHOTOMY, 840 sexpTheory.STRING_LESS_EQ_TRANS, 841 sexpTheory.STRING_LESS_EQ_def, 842 sexpTheory.STRING_LESS_EQ_ANTISYM, 843 sexpTheory.STRING_LESS_IRREFLEXIVE]); 844 845 846val vars1 = [``num (com a b)``, ``sym a b``, ``str a``, ``chr a``, ``cons a b``]; 847val vars2 = [``num (com c d)``, ``sym c d``, ``str c``, ``chr c``, ``cons c d``]; 848 849val lexorder_terms = flatten (map (fn y => (map (fn x => mk_comb(mk_comb(``lexorder``, x), y)) vars1)) vars2); 850val lexorder_thms = map (REWRITE_CONV [lexorder_str_string, lexorder_char, lexorder_sym] THENC ONCE_REWRITE_CONV [lexorder_def] THENC 851 REWRITE_CONV [hol_defaxiomsTheory.ACL2_SIMPS,sexpTheory.itel_def, sym_rwr, 852 sexpTheory.SEXP_SYM_LESS_EQ_def, sexpTheory.SEXP_SYM_LESS_def]) lexorder_terms; 853 854val SEXP_LE_RWRS = LIST_CONJ (hol_defaxiomsTheory.ACL2_SIMPS::bool_rwr:: 855 METIS_PROVE [] ``((if a then b else c) = d) = (a /\ (b = d) \/ ~a /\ (c = d))``::lexorder_thms); 856 857fun ALL_CASES f (a,g) = 858let val v = filter (fn x => f x handle _ => false) (free_vars g) 859in (NTAC (length a) (POP_ASSUM MP_TAC) THEN 860 MAP_EVERY (fn b => SPEC_TAC (b,b)) v THEN 861 REPEAT Cases THEN 862 NTAC (length a) DISCH_TAC) (a,g) 863end; 864 865val SEXP_LE = REWRITE_RULE [hol_defaxiomsTheory.ACL2_SIMPS] SEXP_LE_def; 866 867fun rattac (a,goal) = 868let val rats = filter (curry op= ``:rat`` o type_of) (free_vars goal) 869 val zrats = filter (mem #"0" o explode o fst o dest_var) rats 870in 871 (MAP_EVERY (fn x => STRIP_ASSUME_TAC (SPEC (mk_eq(x, ``rat_0``)) EXCLUDED_MIDDLE)) zrats) (a,goal) 872end; 873 874fun droptac (a,goal) = 875 (if free_in ``lexorder s0 s0'`` goal 876 then ALL_TAC 877 else REPEAT (POP_ASSUM (K ALL_TAC))) (a,goal); 878 879val SEXP_LE_ANTISYMMETRIC = time store_thm("SEXP_LE_ANTISYMMETRIC", 880 ``antisymmetric SEXP_LE``, 881 REWRITE_TAC [relationTheory.antisymmetric_def, SEXP_LE] THEN 882 completeInduct_on `sexp_size x + sexp_size y` THEN 883 REPEAT Cases THEN ALL_CASES (curry op= ``:complex_rational`` o type_of) THEN 884 REWRITE_TAC [SEXP_LE_RWRS, sexpTheory.sexp_size_def, complex_rationalTheory.complex_rational_11, DE_MORGAN_THM] THEN 885 STRIP_TAC THEN droptac THEN TRY STRIP_TAC THEN 886 PROVE_TAC [ 887 sexpTheory.STRING_LESS_EQ_SYM, sexpTheory.STRING_LESS_IRREFLEXIVE, sexpTheory.STRING_LESS_SYM, 888 stringTheory.ORD_11, arithmeticTheory.LESS_EQUAL_ANTISYM, 889 ratTheory.RAT_LEQ_ANTISYM, ratTheory.RAT_LEQ_LES, ratTheory.RAT_LES_ANTISYM, 890 DECIDE ``a + b < 1n + (a + a') + (1 + (b + b'))``, 891 DECIDE ``a' + b' < 1n + (a + a') + (1 + (b + b'))``]); 892 893val sexp_le_antirewrite = REWRITE_RULE [hol_defaxiomsTheory.ACL2_SIMPS,relationTheory.antisymmetric_def,SEXP_LE_def] SEXP_LE_ANTISYMMETRIC; 894 895val SEXP_LE_TRANSITIVE = time store_thm ("SEXP_LE_TRANSITIVE", 896 ``transitive SEXP_LE``, 897 REWRITE_TAC [relationTheory.transitive_def, SEXP_LE] THEN 898 completeInduct_on `sexp_size x + sexp_size y + sexp_size z` THEN 899 REPEAT Cases THEN ALL_CASES (curry op= ``:complex_rational`` o type_of) THEN 900 REWRITE_TAC [SEXP_LE_RWRS, sexpTheory.sexp_size_def, complex_rationalTheory.complex_rational_11, DE_MORGAN_THM] THEN 901 STRIP_TAC THEN droptac THEN rattac THEN ASM_REWRITE_TAC [] THEN TRY STRIP_TAC THEN 902 PROVE_TAC [sexpTheory.STRING_LESS_EQ_def, sexpTheory.STRING_LESS_TRANS, sexpTheory.STRING_LESS_EQ_TRANS, 903 ratTheory.RAT_LES_TRANS, ratTheory.RAT_LES_REF, ratTheory.RAT_LEQ_TRANS, ratTheory.RAT_LEQ_LES, 904 arithmeticTheory.LESS_TRANS, arithmeticTheory.LESS_EQ_TRANS, 905 sexp_le_antirewrite, 906 DECIDE ``a + b + c < 1n + (a + a') + (1 + (b + b')) + (1 + (c + c'))``, 907 DECIDE ``a' + b' + c' < 1n + (a + a') + (1 + (b + b')) + (1 + (c + c'))``, sexpTheory.sexp_distinct]); 908 909val SEXP_LE_TOTAL = store_thm("SEXP_LE_TOTAL", ``total SEXP_LE``, 910 REWRITE_TAC [relationTheory.total_def, SEXP_LE_def, hol_defaxiomsTheory.ACL2_SIMPS] THEN 911 completeInduct_on `sexp_size x + sexp_size y` THEN 912 REPEAT Cases THEN ALL_CASES (curry op= ``:complex_rational`` o type_of) THEN 913 REWRITE_TAC [SEXP_LE_RWRS, sexpTheory.sexp_size_def, DE_MORGAN_THM] THEN 914 METIS_TAC [ratTheory.RAT_LEQ_LES,ratTheory.rat_leq_def, sexpTheory.STRING_LESS_TRICHOTOMY, arithmeticTheory.LESS_CASES, 915 arithmeticTheory.LESS_OR_EQ,stringTheory.ORD_11, ratTheory.RAT_LES_TOTAL, sexpTheory.STRING_LESS_EQ_def, 916 DECIDE ``a + c < 1n + (a + b) + (1 + (c + d))``, DECIDE ``b + d < 1n + (a + b) + (1 + (c + d))``]); 917 918val SEXP_LT_def = Define `SEXP_LT a b = ~(a = b) /\ SEXP_LE a b`; 919 920val _ = overload_on ("<", ``SEXP_LT``); 921 922val SEXP_LT_IRREFLEXIVE = store_thm("SEXP_LT_IRREFLEXIVE", 923 ``irreflexive SEXP_LT``, 924 METIS_TAC [SEXP_LT_def, relationTheory.irreflexive_def]); 925 926val SEXP_LT_TRANSITIVE = store_thm("SEXP_LT_TRANSITIVE", 927 ``transitive SEXP_LT``, 928 REWRITE_TAC [relationTheory.transitive_def, SEXP_LT_def] THEN 929 METIS_TAC (map (REWRITE_RULE [relationTheory.transitive_def,relationTheory.antisymmetric_def]) 930 [SEXP_LE_TRANSITIVE, SEXP_LE_ANTISYMMETRIC])); 931 932val TOTAL_K = store_thm("TOTAL_K", 933 ``total (K (K T))``, RW_TAC std_ss [relationTheory.total_def]); 934 935val TRANSITIVE_K = store_thm("TRANSITIVE_K", 936 ``transitive (K (K T))``, RW_TAC std_ss [relationTheory.transitive_def]); 937 938(*****************************************************************************) 939(* Encoding definitions *) 940(*****************************************************************************) 941 942val map_fmap_def = Define `map_fmap m1 m2 = L2M o MAP (m1 ## m2) o M2L`; 943 944val all_fmap_def = Define `all_fmap p1 p2 = EVERY (all_pair p1 p2) o M2L`; 945 946val fix_fmap_def = Define `fix_fmap f1 f2 = list (pair I I) o 947 QSORT3 ($<= LEX (K (K T))) o M2L o L2M o sexp_to_list (sexp_to_pair I I) o fix_list (fix_pair f1 f2)`; 948 949val encode_fmap_def = Define `encode_fmap fenc tenc = list (pair fenc tenc) o QSORT3 ((inv_image $<= fenc) LEX (K (K T))) o M2L`; 950 951val decode_fmap_def = Define `decode_fmap fdec tdec = L2M o sexp_to_list (sexp_to_pair fdec tdec)`; 952 953val detect_fmap_def = Define `detect_fmap fdet tdet x = 954 (MAPSET ($<= LEX (K (K T))) o sexp_to_list (sexp_to_pair I I)) x /\ 955 (listp (pairp fdet tdet) x)`; 956 957(*****************************************************************************) 958(* Encoding proofs *) 959(*****************************************************************************) 960 961val o_split = prove(``((a o sexp_to_list f) o list g = a o (sexp_to_list f o list g)) /\ 962 (sexp_to_list f o (list g o b) = (sexp_to_list f o list g) o b)``, 963 METIS_TAC [combinTheory.o_DEF]); 964 965val UNIQL_MAP = store_thm("UNIQL_MAP", ``!f g l. ONE_ONE f /\ uniql l ==> uniql (MAP (f ## g) l)``, 966 RW_TAC std_ss [uniql_def,MAP,MEM,pairTheory.PAIR_MAP,MEM_MAP,ONE_ONE_THM] THEN 967 METIS_TAC [pairTheory.PAIR]); 968 969val PERM_UNIQL = store_thm("PERM_UNIQL", ``!l1 l2. PERM l1 l2 ==> (uniql l1 = uniql l2)``, 970 RW_TAC std_ss [uniql_def,MAP,MEM,ONE_ONE_THM] THEN 971 METIS_TAC [pairTheory.PAIR, MEM_PERM]); 972 973val ONE_ONE_RING = store_thm("ONE_ONE_RING", 974 ``!f g. ONE_ONE (f o g) ==> ONE_ONE g``, 975 RW_TAC std_ss [ONE_ONE_DEF]); 976 977val ONE_ONE_I = store_thm("ONE_ONE_I", 978 ``ONE_ONE I``, RW_TAC std_ss [ONE_ONE_DEF]); 979 980val o_assoc = prove( 981 ``(f o g) o h = f o g o h``, METIS_TAC [combinTheory.o_DEF]); 982 983(*****************************************************************************) 984(* ENCDECMAP_FMAP: encode then decode equals map *) 985(*****************************************************************************) 986 987val ENCDECMAP_FMAP = store_thm("ENCDECMAP_FMAP", 988 ``!fdec tdec fenc tenc. ONE_ONE (fdec o fenc) ==> (decode_fmap fdec tdec o encode_fmap fenc tenc = map_fmap (fdec o fenc) (tdec o tenc))``, 989 REWRITE_TAC [decode_fmap_def, encode_fmap_def, o_assoc, map_fmap_def] THEN 990 REWRITE_TAC [o_split, translateTheory.ENCDECMAP_LIST, combinTheory.I_o_ID, quotient_listTheory.LIST_MAP_I, translateTheory.ENCDECMAP_PAIR] THEN 991 RW_TAC std_ss [FUN_EQ_THM] THEN 992 MATCH_MP_TAC L2M_EQ THEN REPEAT CONJ_TAC THEN 993 METIS_TAC [L2M_EQ, UNIQL_MAP, PERM_MAP, PERM_UNIQL, UNIQL_M2L, PERM_QSORT3, UNIQL_MAP, PERM_SETEQ, SETEQ_THM, PERM_SYM]); 994 995(*****************************************************************************) 996(* DECENCFIX_FMAP: decode then encode equals fix *) 997(*****************************************************************************) 998 999val RWR = REWRITE_RULE [FUN_EQ_THM, combinTheory.o_THM]; 1000 1001val map_lemma = prove(``!l f g. MAP FST (MAP (f ## g) l) = MAP f (MAP FST l)``, 1002 Induct THEN RW_TAC std_ss [MAP, pairTheory.PAIR_MAP]); 1003 1004val map_eq_sing = prove(``!l f x. (MAP f l = [x]) = ?h. (l = [h]) /\ (x = f h)``, 1005 Induct THEN RW_TAC std_ss [MAP, MAP_EQ_NIL] THEN PROVE_TAC []); 1006 1007val one_one_lemma = prove(``!f. ONE_ONE f ==> !y. $= (f y) o f = $= y``, 1008 RW_TAC std_ss [ONE_ONE_THM,FUN_EQ_THM] THEN METIS_TAC []); 1009 1010val ALL_DISTINCT_MAP = store_thm("ALL_DISTINCT_MAP", 1011 ``!l f. ONE_ONE f /\ ALL_DISTINCT l ==> ALL_DISTINCT (MAP f l)``, 1012 NTAC 2 (RW_TAC std_ss [ALL_DISTINCT_FILTER, rich_listTheory.FILTER_MAP, map_eq_sing, MEM_MAP, one_one_lemma])); 1013 1014val M2L_L2M_MAP = store_thm("M2L_L2M_MAP", 1015 ``!l f g. ONE_ONE f ==> PERM (M2L (L2M (MAP (f ## g) l))) (MAP (f ## g) (M2L (L2M l)))``, 1016 METIS_TAC [ALL_DISTINCT_MAPFST_M2L,ALL_DISTINCT_MAP, map_lemma, ALL_DISTINCT_MAPFST, SETEQ_PERM, M2L_L2M_MAP_SETEQ, ALL_DISTINCT_M2L]); 1017 1018val QSORT3_M2L_L2M_MAP_INV = store_thm("QSORT3_M2L_L2M_MAP_INV", 1019 ``!l f g h. ONE_ONE f /\ ONE_ONE h ==> (QSORT3 (inv_image $<= h LEX K (K T)) (M2L (L2M (MAP (f ## g) l))) = QSORT3 (inv_image $<= h LEX (K (K T))) (MAP (f ## g) (M2L (L2M l))))``, 1020 REPEAT STRIP_TAC THEN MATCH_MP_TAC MAP_FST_DISTINCT_EQ THEN 1021 REPEAT CONJ_TAC THEN 1022 TRY (MATCH_MP_TAC PERM_SORTED_EQ) THEN 1023 TRY (Q.EXISTS_TAC `inv_image $<= h`) THEN 1024 `total (inv_image $<= h)` by METIS_TAC [SEXP_LE_TOTAL, TOTAL_INV] THEN 1025 TRY (METIS_TAC [M2L_L2M_MAP, PERM_QSORT3, PERM_TRANS,PERM_SYM, PERM_MAP, QSORT3_SORTS, SEXP_LE_TOTAL, 1026 SEXP_LE_TRANSITIVE, TRANSITIVE_K, TOTAL_K, TRANSITIVE_LEX, TOTAL_LEX, SORTS_DEF, SORTED_LEX, 1027 ANTISYM_INV, TRANS_INV, IRREFL_INV, TOTAL_INV, 1028 SEXP_LE_ANTISYMMETRIC, ALL_DISTINCT_PERM, ALL_DISTINCT_MAPFST_M2L])); 1029 1030val INVIMAGE_I = store_thm("INVIMAGE_I", 1031 ``inv_image R I = R``, 1032 RW_TAC std_ss [relationTheory.inv_image_def] THEN METIS_TAC []); 1033 1034val QSORT3_M2L_L2M_MAP = save_thm("QSORT3_M2L_L2M_MAP", 1035 REWRITE_RULE [INVIMAGE_I,ONE_ONE_I] (Q.ISPEC `I:sexp->sexp` (Q.GEN `h` (SPEC_ALL QSORT3_M2L_L2M_MAP_INV)))); 1036 1037val MAP_EQ_LENGTH = store_thm("MAP_EQ_LENGTH", 1038 ``!l1 l2. (MAP f l1 = MAP g l2) ==> (LENGTH l1 = LENGTH l2)``, 1039 METIS_TAC [LENGTH_MAP]); 1040 1041val MEM_EL_FILTER = store_thm("MEM_EL_FILTER", 1042 ``!f l x. MEM x l ==> ?y. y < LENGTH (FILTER ($= (f x) o f) l) /\ (EL y (FILTER ($= (f x) o f) l) = x)``, 1043 GEN_TAC THEN Induct THEN RW_TAC std_ss [FILTER, rich_listTheory.EL_CONS, MEM] THEN RES_TAC THENL [ 1044 Q.EXISTS_TAC `0`, Q.EXISTS_TAC `SUC y`,ALL_TAC] THEN 1045 RW_TAC arith_ss [LENGTH,EL,HD,TL] THEN 1046 METIS_TAC []); 1047 1048val EL_MAP_FILTER = store_thm("EL_MAP_FILTER", 1049 ``!f x. (MAP f l1 = MAP f l2) /\ x < LENGTH l1 /\ (FILTER ($= (f (EL x l1)) o f) l1 = FILTER ($= (f (EL x l2)) o f) l2) ==> (EL x l1 = EL x l2)``, 1050 completeInduct_on `LENGTH l1 + LENGTH l2` THEN REPEAT Cases THEN 1051 RW_TAC std_ss [LENGTH, rich_listTheory.EL_CONS, MEM, MAP, FILTER] THEN 1052 Cases_on `x` THEN FULL_SIMP_TAC std_ss [rich_listTheory.EL_CONS, EL, HD, TL, list_11] THEN 1053 POP_ASSUM MP_TAC THEN RW_TAC std_ss [list_11] THEN 1054 IND_STEP_TAC THEN RW_TAC std_ss [] THEN Q.EXISTS_TAC `f` THEN RW_TAC arith_ss [] THEN METIS_TAC [EL_MAP, LENGTH_MAP]); 1055 1056val MAP_FST_SND_EQ = store_thm("MAP_FST_SND_EQ", 1057 ``!l1 l2. (MAP FST l1 = MAP FST l2) /\ (MAP SND l1 = MAP SND l2) ==> (l1 = l2)``, 1058 REPEAT GEN_TAC THEN completeInduct_on `LENGTH l1 + LENGTH l2` THEN REPEAT Cases THEN 1059 RW_TAC std_ss [LENGTH, rich_listTheory.EL_CONS, MEM, MAP, FILTER, pairTheory.PAIR_FST_SND_EQ] THEN 1060 IND_STEP_TAC THEN RW_TAC arith_ss []); 1061 1062val STABLE_FST_EQ = store_thm("STABLE_FST_EQ", 1063 ``!l1 l2. (MAP FST l1 = MAP FST l2) /\ (!x. FILTER ($= x o FST) l1 = FILTER ($= x o FST) l2) ==> (l1 = l2)``, 1064 METIS_TAC [EL_MAP_FILTER, EL_MAP, LENGTH_MAP, LIST_EQ_REWRITE,MAP_FST_SND_EQ]); 1065 1066val SORTED_MAP = store_thm("SORTED_MAP", 1067 ``!l f R. transitive R /\ SORTED (inv_image R f) l ==> SORTED R (MAP f l)``, 1068 Induct THEN RW_TAC std_ss [SORTED_EQ,SORTED_DEF,MAP,MEM_MAP] THEN 1069 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [SORTED_EQ, TRANS_INV, relationTheory.inv_image_def]); 1070 1071val INV_INV_IMAGE = store_thm("INV_INV_IMAGE", 1072 ``!h f. inv_image (inv_image R h) f = inv_image R (h o f)``, 1073 RW_TAC std_ss [relationTheory.inv_image_def]); 1074 1075local 1076val lemma 1077 = GSYM (GEN_ALL (PULL_RULE (DISCH_ALL (CONJUNCT2 (UNDISCH (SPEC_ALL (PULL_RULE (REWRITE_RULE [STABLE_DEF] QSORT3_STABLE)))))))); 1078val sorttac 1079 = RW_TAC std_ss [map_lemma, TRANSITIVE_K, SEXP_LE_ANTISYMMETRIC, SEXP_LE_TRANSITIVE, SEXP_LE_TOTAL, 1080 TOTAL_INV, TRANS_INV, ANTISYM_INV, IRREFL_INV, INV_INV_IMAGE, 1081 REWRITE_RULE [SORTS_DEF] QSORT3_SORTS, TOTAL_K, TOTAL_LEX, TRANSITIVE_LEX, TOTAL_INV, TRANS_INV] 1082in 1083val QSORT3_PAIRMAP_INV = store_thm("QSORT3_PAIRMAP_INV", 1084 ``!f h. ONE_ONE f /\ ONE_ONE h ==> 1085 !l g. QSORT3 (inv_image $<= h LEX K (K T)) (MAP (f ## g) l) = 1086 MAP (f ## g) (QSORT3 (inv_image $<= (h o f) LEX K (K T)) l)``, 1087 REPEAT STRIP_TAC THEN MATCH_MP_TAC STABLE_FST_EQ THEN REPEAT STRIP_TAC THENL [ 1088 MATCH_MP_TAC PERM_SORTED_EQ THEN 1089 Q.EXISTS_TAC `inv_image $<= h` THEN sorttac, 1090 MATCH_MP_TAC EQ_TRANS THEN 1091 Q.EXISTS_TAC `FILTER ($= x o FST) (MAP (f ## g) l)` THEN CONJ_TAC 1092 ] THEN1 METIS_TAC [PERM_QSORT3, PERM_MAP, PERM_SYM, PERM_TRANS, map_lemma] THEN 1093 REPEAT (FIRST [MATCH_MP_TAC (PULL_RULE SORTED_LEX) ORELSE MATCH_MP_TAC SORTED_MAP THEN RW_TAC std_ss [TRANS_INV,SEXP_LE_TRANSITIVE], 1094 MATCH_MP_TAC lemma ORELSE MATCH_MP_TAC (GSYM lemma) ORELSE (REWRITE_TAC [rich_listTheory.FILTER_MAP] THEN AP_TERM_TAC)]) THEN 1095 TRY (Q.EXISTS_TAC `K (K T)`) THEN sorttac THEN 1096 REPEAT (POP_ASSUM MP_TAC) THEN (fn (a,g) => MAP_EVERY (fn b => SPEC_TAC (b,b)) (free_vars g) (a,g)) THEN 1097 REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [pairTheory.LEX_DEF,relationTheory.inv_image_def, ONE_ONE_DEF]) 1098val QSORT3_PAIRMAP = save_thm("QSORT3_PAIRMAP", 1099 GEN_ALL (REWRITE_RULE [INVIMAGE_I,ONE_ONE_I] (Q.ISPEC `I:sexp->sexp` (Q.GEN `h` (SPEC_ALL QSORT3_PAIRMAP_INV))))) 1100end; 1101 1102val list_pair_map = prove(``!f g f' g' l. list (pair f g) (MAP (f' ## g') l) = list (pair (f o f') (g o g')) l``, 1103 NTAC 4 GEN_TAC THEN Induct THEN RW_TAC std_ss [translateTheory.list_def, translateTheory.pair_def, MAP, pairTheory.PAIR_MAP]); 1104 1105(*****************************************************************************) 1106(* DECENCFIX_FMAP: Decode then encode is fix. *) 1107(*****************************************************************************) 1108 1109val DECENCFIX_FMAP = store_thm("DECENCFIX_FMAP", 1110 ``!fdec tdec fenc tenc. ONE_ONE (fdec o fenc) ==> (encode_fmap fenc tenc o decode_fmap fdec tdec = fix_fmap (fenc o fdec) (tenc o tdec))``, 1111 RW_TAC std_ss [encode_fmap_def,decode_fmap_def,fix_fmap_def,FUN_EQ_THM,GSYM translateTheory.DECENCFIX_LIST,GSYM translateTheory.DECENCFIX_PAIR, 1112 RWR translateTheory.ENCDECMAP_LIST, translateTheory.ENCDECMAP_PAIR] THEN 1113 IMP_RES_TAC ONE_ONE_RING THEN 1114 RW_TAC std_ss [QSORT3_M2L_L2M_MAP, QSORT3_PAIRMAP, list_pair_map]); 1115 1116(*****************************************************************************) 1117(* MAPID_FMAP: Map identity. *) 1118(*****************************************************************************) 1119 1120val MAPID_FMAP = store_thm("MAPID_FMAP", 1121 ``map_fmap I I = I``, 1122 RW_TAC std_ss [FUN_EQ_THM, map_fmap_def, quotient_pairTheory.PAIR_MAP_I,quotient_listTheory.LIST_MAP_I, L2M_M2L]); 1123 1124(*****************************************************************************) 1125(* FIXID_FMAP: Fix identity. *) 1126(*****************************************************************************) 1127 1128val FIXID_FMAP = store_thm("FIXID_FMAP", 1129 ``(!x. p0 x ==> (f0 x = x)) ��� (!x. p1 x ==> (f1 x = x)) ==> !x. detect_fmap p0 p1 x ��� (fix_fmap f0 f1 x = x)``, 1130 RW_TAC std_ss [fix_fmap_def, detect_fmap_def, translateTheory.FIXID_LIST, translateTheory.FIXID_PAIR] THEN 1131 SUBGOAL_THEN ``fix_list (fix_pair f0 f1) x = x`` SUBST_ALL_TAC THENL [ALL_TAC, 1132 Q.ABBREV_TAC `m = sexp_to_list (sexp_to_pair I I) x` THEN 1133 `QSORT3 ($<= LEX K (K T)) (M2L (L2M m)) = m` by MATCH_MP_TAC (PULL_RULE M2L_L2M) THEN 1134 RW_TAC std_ss [SEXP_LE_TOTAL, SEXP_LE_TRANSITIVE, TRANSITIVE_K, SEXP_LE_ANTISYMMETRIC, QSORT3_SORTS, TRANSITIVE_LEX, TOTAL_LEX, TOTAL_K] THEN 1135 POP_ASSUM SUBST_ALL_TAC THEN 1136 Q.UNABBREV_TAC `m` THEN 1137 RW_TAC std_ss [RWR translateTheory.DECENCFIX_LIST, translateTheory.DECENCFIX_PAIR]] THEN 1138 MATCH_MP_TAC (GEN_ALL (PULL_RULE translateTheory.FIXID_LIST)) THEN 1139 Q.EXISTS_TAC `pairp p0 p1` THEN RW_TAC std_ss [] THEN MATCH_MP_TAC (GEN_ALL (PULL_RULE translateTheory.FIXID_PAIR)) THEN 1140 METIS_TAC [combinTheory.I_THM,combinTheory.K_THM, translateTheory.GENERAL_DETECT_PAIR]); 1141 1142val EVERY_PERM = store_thm("EVERY_PERM", ``!l1 l2. PERM l1 l2 ==> (EVERY P l1 = EVERY P l2)``, 1143 METIS_TAC [MEM_PERM, EVERY_MEM]); 1144 1145val INV_LEX_PAIRMAP = store_thm("INV_LEX_PAIRMAP", 1146 ``ONE_ONE f ==> (inv_image (R LEX R') (f ## g) = inv_image R f LEX inv_image R' g)``, 1147 RW_TAC std_ss [relationTheory.inv_image_def, pairTheory.LEX_DEF,pairTheory.PAIR_MAP, FUN_EQ_THM] THEN 1148 REPEAT (POP_ASSUM MP_TAC) THEN (fn (a,g) => MAP_EVERY (fn b => SPEC_TAC (b,b)) (free_vars g) (a,g)) THEN 1149 REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [] THEN 1150 METIS_TAC [ONE_ONE_THM]); 1151 1152val INVIMAGE_K = store_thm("INVIMAGE_K", 1153 ``inv_image (K (K T)) x = K (K T)``, 1154 RW_TAC std_ss [relationTheory.inv_image_def, pairTheory.LEX_DEF,pairTheory.PAIR_MAP, FUN_EQ_THM] THEN 1155 REPEAT (POP_ASSUM MP_TAC) THEN (fn (a,g) => MAP_EVERY (fn b => SPEC_TAC (b,b)) (free_vars g) (a,g)) THEN 1156 REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss []); 1157 1158(*****************************************************************************) 1159(* ENCDETALL_FMAP: Encoding then detecting equals every *) 1160(*****************************************************************************) 1161 1162val ENCDETALL_FMAP = store_thm("ENCDETALL_FMAP", 1163 ``!p0 p1 f0 f1. ONE_ONE f0 ==> (detect_fmap p0 p1 o encode_fmap f0 f1 = all_fmap (p0 o f0) (p1 o f1))``, 1164 RW_TAC std_ss [FUN_EQ_THM, detect_fmap_def, encode_fmap_def, all_fmap_def, RWR translateTheory.ENCDETALL_LIST, 1165 all_fmap_def, RWR translateTheory.ENCDECMAP_LIST, translateTheory.ENCDECMAP_PAIR, MAPSET_def, 1166 translateTheory.ENCDETALL_PAIR, map_lemma] THEN 1167 `!Q. EVERY Q (QSORT3 (inv_image $<= f0 LEX K (K T)) (M2L x)) = EVERY Q (M2L x)` by MATCH_MP_TAC EVERY_PERM THEN 1168 RW_TAC std_ss [PERM_QSORT3, PERM_SYM] THEN 1169 MATCH_MP_TAC (DECIDE ``!a b. a ==> (a /\ b = b)``) THEN REPEAT CONJ_TAC THEN 1170 MAP_FIRST MATCH_MP_TAC [SORTED_MAP, ALL_DISTINCT_MAP] THEN 1171 METIS_TAC [QSORT3_SORTS, SORTS_DEF, TRANSITIVE_LEX, TRANSITIVE_K, SEXP_LE_TRANSITIVE, TOTAL_LEX, TOTAL_K, SEXP_LE_TOTAL, 1172 TOTAL_INV, TRANS_INV, INV_LEX_PAIRMAP, 1173 INVIMAGE_K, ALL_DISTINCT_MAPFST_M2L, PERM_QSORT3, PERM_MAP, PERM_TRANS, PERM_SYM, ALL_DISTINCT_PERM]); 1174 1175(*****************************************************************************) 1176(* ALLID_FMAP: All identity *) 1177(*****************************************************************************) 1178 1179val ALLID_FMAP = store_thm("ALLID_FMAP", ``all_fmap (K T) (K T) = K T``, 1180 RW_TAC std_ss [all_fmap_def,translateTheory.ALLID_PAIR, translateTheory.ALLID_LIST]); 1181 1182(*****************************************************************************) 1183(* DETECT_DEAD: Detect nil is always true. *) 1184(*****************************************************************************) 1185 1186val DETECTDEAD_FMAP = store_thm("DETECTDEAD_FMAP", ``!p0 p1. detect_fmap p0 p1 nil``, 1187 RW_TAC std_ss [detect_fmap_def, translateTheory.sexp_to_list_def, sexpTheory.nil_def, MAPSET_def, 1188 SORTED_DEF, ALL_DISTINCT_THM, MAP, MEM, FILTER, translateTheory.listp_def,translateTheory.pairp_def]); 1189 1190val MAPSET_CONS = store_thm("MAPSET_CONS", 1191 ``!b a R. MAPSET ($<= LEX (K (K T))) (a::b) ==> MAPSET ($<= LEX (K (K T))) b``, 1192 RW_TAC std_ss [MAPSET_def, SORTED_EQ, SEXP_LE_TRANSITIVE, TRANSITIVE_LEX, TRANSITIVE_K, MAP, ALL_DISTINCT]); 1193 1194(*****************************************************************************) 1195(* DETECT_GENERAL_FMAP: An exact map implies any map *) 1196(*****************************************************************************) 1197 1198val DETECT_GENERAL_FMAP = store_thm("DETECT_GENERAL_FMAP", 1199 ``!p0 p1 x. detect_fmap p0 p1 x ==> detect_fmap (K T) (K T) x``, 1200 REWRITE_TAC [detect_fmap_def] THEN 1201 NTAC 2 GEN_TAC THEN Induct THEN RW_TAC std_ss [] THEN 1202 RW_TAC std_ss [translateTheory.listp_def, translateTheory.pairp_def] THEN 1203 FULL_SIMP_TAC std_ss [translateTheory.listp_def,translateTheory.pairp_def, translateTheory.sexp_to_list_def] THEN 1204 FIRST_ASSUM MATCH_MP_TAC THEN 1205 METIS_TAC [MAPSET_CONS]); 1206 1207val ONE_ONE_RING2 = store_thm("ONE_ONE_RING2", 1208 ``ONE_ONE a /\ ONE_ONE b ==> ONE_ONE (a o b)``, 1209 RW_TAC std_ss [ONE_ONE_DEF]); 1210 1211val PAIR_MAP_COMPOSE = store_thm("PAIR_MAP_COMPOSE", 1212 ``!a b c d. (a o b ## c o d) = (a ## c) o (b ## d)``, 1213 RW_TAC std_ss [FUN_EQ_THM,pairTheory.PAIR_MAP]); 1214 1215(*****************************************************************************) 1216(* MAP_COMPOSE: Composition of maps *) 1217(* `fmap_map f0 f1 o fmap_map g0 g1 = fmap_map (f0 o g0) (f1 o g1)` *) 1218(* Only needed for types based upon finite maps *) 1219(*****************************************************************************) 1220 1221val SETEQ_MAP = store_thm("SETEQ_MAP", 1222 ``SETEQ a b ==> SETEQ (MAP f a) (MAP f b)``, 1223 RW_TAC std_ss [SETEQ_def, MEM_MAP]); 1224 1225val SETEQ_COMM = save_thm("SETEQ_COMM", METIS_PROVE [SETEQ_THM] ``SETEQ a b = SETEQ b a``); 1226 1227val FMAP_MAP_COMPOSE = store_thm("FMAP_MAP_COMPOSE", 1228 ``ONE_ONE f0 /\ ONE_ONE g0 ==> (map_fmap f0 f1 o map_fmap g0 g1 = map_fmap (f0 o g0) (f1 o g1))``, 1229 RW_TAC std_ss [map_fmap_def, FUN_EQ_THM] THEN 1230 MATCH_MP_TAC L2M_EQ THEN 1231 RW_TAC std_ss [GSYM SETEQ_THM, UNIQL_M2L, UNIQL_MAP, ONE_ONE_RING2, PAIR_MAP_COMPOSE, MAP_o] THEN 1232 MATCH_MP_TAC SETEQ_MAP THEN 1233 MATCH_MP_TAC (ONCE_REWRITE_RULE [SETEQ_COMM] M2L_L2M_SETEQ) THEN 1234 PROVE_TAC [UNIQL_MAP, UNIQL_M2L]); 1235 1236(*****************************************************************************) 1237(* ENCMAPENC: Composition of encoding *) 1238(* `encode_fmap f0 f1 o map_fmap g0 g1 = encode_fmap (f0 o g0) (f1 o g1)` *) 1239(* Only needed for types based upon finite maps *) 1240(*****************************************************************************) 1241 1242val o_rule = REWRITE_RULE [FUN_EQ_THM,combinTheory.o_THM] 1243 1244val ENCMAPENC_FMAP = store_thm("ENCMAPENC_FMAP", 1245 ``ONE_ONE f0 /\ ONE_ONE g0 ==> (encode_fmap f0 f1 o map_fmap g0 g1 = encode_fmap (f0 o g0) (f1 o g1))``, 1246 RW_TAC std_ss [encode_fmap_def, map_fmap_def, FUN_EQ_THM, QSORT3_M2L_L2M_MAP_INV,L2M_M2L,QSORT3_PAIRMAP_INV, 1247 o_rule translateTheory.ENCMAPENC_LIST, translateTheory.ENCMAPENC_PAIR]); 1248 1249(*****************************************************************************) 1250(* Rewrite theorems: *) 1251(* -) sorted_car_rewrite *) 1252(*****************************************************************************) 1253 1254val sorted_car_def = TotalDefn.tDefine "sorted_car" ` 1255 sorted_car a = ite (andl [consp a ; consp (cdr a)]) 1256 (andl [not (equal (caar a) (caadr a)) ; lexorder (caar a) (caadr a) ; sorted_car (cdr a)]) 1257 t` 1258 (WF_REL_TAC `measure sexp_size` THEN Cases_on `a` THEN 1259 RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS]); 1260 1261val sexp_nil = REWRITE_RULE [hol_defaxiomsTheory.ACL2_SIMPS] ( 1262 prove(``!a f. (consp a = nil) ==> (sexp_to_list f a = []) /\ (car a = nil) /\ (cdr a = nil)``, 1263 Cases THEN RW_TAC std_ss [translateTheory.sexp_to_list_def, hol_defaxiomsTheory.ACL2_SIMPS])); 1264 1265val trans_rewrite = REWRITE_RULE [SEXP_LE_def, hol_defaxiomsTheory.ACL2_SIMPS, relationTheory.transitive_def] SEXP_LE_TRANSITIVE; 1266val sym_rewrite = REWRITE_RULE [SEXP_LE_def, hol_defaxiomsTheory.ACL2_SIMPS, relationTheory.antisymmetric_def] SEXP_LE_ANTISYMMETRIC; 1267 1268val lemma = prove( 1269 ``!x' x. ~(lexorder (car x) (car (car x')) = nil) /\ ~(car x = car (car x')) /\ (sorted_car x' = t) ==> ~MEM (car x) (MAP FST (sexp_to_list (sexp_to_pair I I) x'))``, 1270 Induct THEN ONCE_REWRITE_TAC [sorted_car_def] THEN 1271 REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS, translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def, MAP, ALL_DISTINCT, MEM] THEN 1272 RW_TAC std_ss [] THEN REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [] THEN 1273 Cases_on `x'` THEN 1274 FULL_SIMP_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def, MAP, ALL_DISTINCT, MEM] THEN 1275 RW_TAC std_ss [sexp_nil,MAP,MEM] THEN 1276 `~(car x = car (car x''))` by METIS_TAC [REWRITE_RULE [SEXP_LE_def, hol_defaxiomsTheory.ACL2_SIMPS, relationTheory.antisymmetric_def] SEXP_LE_ANTISYMMETRIC] THEN 1277 FIRST_ASSUM (fn x => MATCH_MP_TAC x THEN ASM_REWRITE_TAC [] THEN MATCH_MP_TAC trans_rewrite THEN METIS_TAC [])); 1278 1279val sorted_car_cons = prove(``!y x. sorted_car (cons x y) = ite (consp y) (andl [not (equal (car x) (caar y)) ; lexorder (car x) (caar y); sorted_car y]) t``, 1280 CONV_TAC (ONCE_DEPTH_CONV (LAND_CONV (REWR_CONV sorted_car_def))) THEN 1281 RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS]); 1282 1283val sorted_car_distinct = store_thm("sorted_car_distinct", 1284 ``!x. (sorted_car x = t) ==> ALL_DISTINCT (MAP FST (sexp_to_list (sexp_to_pair I I) x))``, 1285 Induct THEN ONCE_REWRITE_TAC [sorted_car_def] THEN 1286 REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS, translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def, MAP, ALL_DISTINCT, MEM] THEN 1287 RW_TAC std_ss [] THEN REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [] THEN 1288 Cases_on `x'` THEN 1289 FULL_SIMP_TAC std_ss [sorted_car_cons, hol_defaxiomsTheory.ACL2_SIMPS, translateTheory.sexp_to_list_def, 1290 translateTheory.sexp_to_pair_def, MAP, ALL_DISTINCT, MEM] THEN 1291 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [sexp_nil,MAP,MEM] THEN 1292 TRY (FIRST_ASSUM (STRIP_ASSUME_TAC o el 2 o CONJUNCTS o SPEC_ALL o MATCH_MP sexp_nil) THEN 1293 POP_ASSUM (CONV_TAC o DEPTH_CONV o REWR_CONV o GSYM)) THEN 1294 TRY (MATCH_MP_TAC lemma THEN ASM_REWRITE_TAC [SEXP_LT_def,hol_defaxiomsTheory.ACL2_SIMPS] THEN 1295 CONJ_TAC THEN1 (MATCH_MP_TAC trans_rewrite THEN Q.EXISTS_TAC `car s` THEN METIS_TAC []) THEN METIS_TAC [sym_rewrite]) THEN 1296 METIS_TAC [sym_rewrite, sexp_nil]); 1297 1298val slemma = prove(``!x l. SORTED (SEXP_LE LEX K (K T)) (x::l) = SORTED (SEXP_LE LEX K (K T)) l /\ ((l = []) \/ ((SEXP_LE LEX K (K T)) x (HD l)))``, 1299 GEN_TAC THEN Cases THEN RW_TAC std_ss [sortingTheory.SORTED_DEF,HD] THEN METIS_TAC []); 1300 1301val sorted_car_sorted = store_thm("sorted_car_sorted", 1302 ``!x. (sorted_car x = t) ==> SORTED (SEXP_LE LEX K (K T)) (sexp_to_list (sexp_to_pair I I) x)``, 1303 Induct THEN ONCE_REWRITE_TAC [sorted_car_def] THEN 1304 REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS, translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def, MAP, ALL_DISTINCT, 1305 sortingTheory.SORTED_DEF] THEN 1306 RW_TAC std_ss [slemma] THEN TRY (METIS_TAC [sexpTheory.t_def]) THEN 1307 REPEAT (POP_ASSUM MP_TAC) THEN TRY (Cases_on `x'`) THEN 1308 REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS, translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def, MAP, ALL_DISTINCT, 1309 sortingTheory.SORTED_DEF] THEN 1310 RW_TAC std_ss [HD, SEXP_LT_def,pairTheory.LEX_DEF, SEXP_LE_def, hol_defaxiomsTheory.ACL2_SIMPS] THEN 1311 METIS_TAC [sexp_nil]); 1312 1313val MAPSET_sortedcar = store_thm("MAPSET_sortedcar", 1314 ``!l. MAPSET (SEXP_LE LEX K (K T)) (sexp_to_list (sexp_to_pair I I) l) ==> (sorted_car l = t)``, 1315 Induct THEN ONCE_REWRITE_TAC [sorted_car_def] THEN TRY (REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS] THEN NO_TAC) THEN 1316 REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS,translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def] THEN 1317 RW_TAC std_ss [] THEN REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [MAPSET_def, slemma, MAP, ALL_DISTINCT, sexpTheory.t_def] THEN 1318 Cases_on `l'` THEN 1319 REWRITE_TAC [hol_defaxiomsTheory.ACL2_SIMPS,translateTheory.sexp_to_list_def, translateTheory.sexp_to_pair_def, 1320 MEM, ALL_DISTINCT, MAP, sortingTheory.SORTED_DEF] THEN 1321 FULL_SIMP_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS] THEN 1322 RW_TAC std_ss [HD, pairTheory.LEX_DEF, SEXP_LE_def,SEXP_LT_def, hol_defaxiomsTheory.ACL2_SIMPS] THEN 1323 METIS_TAC [sexp_nil]); 1324 1325val booleanp_sortedcar = store_thm("booleanp_sortedcar", ``!x. |= booleanp (sorted_car x)``, 1326 Induct THEN 1327 ONCE_REWRITE_TAC [sorted_car_def] THEN REPEAT ( 1328 RW_TAC std_ss [translateTheory.TRUTH_REWRITES, hol_defaxiomsTheory.booleanp_def,sexpTheory.ite_def, 1329 sexpTheory.equal_def, sexpTheory.andl_def, sexpTheory.consp_def, sexpTheory.car_def, sexpTheory.cdr_def] THEN 1330 REPEAT (POP_ASSUM MP_TAC))); 1331 1332val sorted_car_rewrite = store_thm("sorted_car_rewrite", 1333 ``!x. bool ((MAPSET (SEXP_LE LEX K (K T)) o sexp_to_list (sexp_to_pair I I)) x) = sorted_car x``, 1334 STRIP_TAC THEN Cases_on `sorted_car x = t` THEN RW_TAC std_ss [bool_rwr] THEN 1335 MAP_EVERY IMP_RES_TAC [sorted_car_sorted, sorted_car_distinct, MAPSET_sortedcar] THEN RW_TAC std_ss [] THEN 1336 ASSUME_TAC (Q.SPEC `x` booleanp_sortedcar) THEN 1337 FULL_SIMP_TAC std_ss [MAPSET_def] THEN 1338 POP_ASSUM MP_TAC THEN RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS]); 1339 1340(*****************************************************************************) 1341(* fdom_rewrite: bool (x IN FDOM y) *) 1342(*****************************************************************************) 1343 1344val assoc_list = store_thm("assoc_list", 1345 ``!y f g x. ONE_ONE f ==> (assoc (f x) (list (pair f g) y) = if (?z. MEM (x,z) y) then pair f g (HD (FILTER ($= x o FST) y)) else nil)``, 1346 Induct THEN ONCE_REWRITE_TAC [hol_defaxiomsTheory.assoc_def] THEN 1347 RW_TAC std_ss [MEM,translateTheory.list_def, hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def,bool_rwr, translateTheory.pair_def, FILTER, HD] THEN 1348 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [] THEN 1349 TRY (POP_ASSUM (ASSUME_TAC o REWRITE_RULE [pairTheory.PAIR_FST_SND_EQ] o Q.SPEC `SND h`)) THEN 1350 METIS_TAC [ONE_ONE_THM]); 1351 1352val not_pair_nil = prove(``!y f g. not (equal nil (pair f g y)) = t``, 1353 Cases THEN RW_TAC std_ss [translateTheory.pair_def,hol_defaxiomsTheory.ACL2_SIMPS]); 1354 1355val not_nil_nil = prove(``not (equal nil nil) = nil``, 1356 RW_TAC std_ss [translateTheory.pair_def,hol_defaxiomsTheory.ACL2_SIMPS]); 1357 1358val fdom_rewrite = store_thm("fdom_rewrite", 1359 ``!y x. ONE_ONE f ==> (bool (x IN FDOM y) = not (equal nil (assoc (f x) (encode_fmap f g y))))``, 1360 REWRITE_TAC [encode_fmap_def,combinTheory.o_THM, GSYM EXISTS_MEM_M2L, bool_rwr] THEN 1361 RW_TAC std_ss [assoc_list, not_pair_nil, translateTheory.TRUTH_REWRITES,not_nil_nil] THEN 1362 METIS_TAC [PERM_QSORT3, MEM_PERM]); 1363 1364(*****************************************************************************) 1365(* apply_rewrite: encode (y ' x) *) 1366(*****************************************************************************) 1367 1368val FILTER_EQ_SEXP_SORT = store_thm("FILTER_EQ_SEXP_SORT", 1369 ``!x l f. FILTER ($= x o FST) (QSORT3 (inv_image SEXP_LE f LEX K (K T)) l) = FILTER ($= x o FST) l``, 1370 REPEAT STRIP_TAC THEN MATCH_MP_TAC (GSYM (PULL_RULE (DISCH_ALL (CONJUNCT2 (MATCH_MP (fst (EQ_IMP_RULE (SPEC_ALL STABLE_DEF))) (UNDISCH (SPEC_ALL QSORT3_STABLE))))))) THEN 1371 REPEAT (RW_TAC std_ss [TRANS_INV, TRANSITIVE_LEX, TRANSITIVE_K, SEXP_LE_TRANSITIVE, TOTAL_INV, TOTAL_K, TOTAL_LEX, SEXP_LE_TOTAL, relationTheory.inv_image_def, pairTheory.LEX_DEF] THEN 1372 REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN ALL_CASES (K true))); 1373 1374val uniql_FILTER = prove(``!l. uniql l /\ MEM (x,y) l ==> (HD (FILTER ($= x o FST) l) = (x,y))``, 1375 Induct THEN REPEAT STRIP_TAC THEN IMP_RES_TAC uniql_cons THEN RW_TAC std_ss [uniql_def, FILTER, MEM, HD] THEN FULL_SIMP_TAC std_ss [MEM] THEN RES_TAC THEN 1376 FULL_SIMP_TAC std_ss [uniql_def,MEM] THEN RES_TAC THEN Cases_on `h` THEN FULL_SIMP_TAC std_ss []); 1377 1378val apply_rewrite = store_thm("apply_rewrite", 1379 ``!y x. ONE_ONE f /\ x IN FDOM y ==> (g (y ' x) = cdr (assoc (f x) (encode_fmap f g y)))``, 1380 REWRITE_TAC [encode_fmap_def,combinTheory.o_THM, GSYM EXISTS_MEM_M2L, bool_rwr] THEN 1381 RW_TAC std_ss [assoc_list, not_pair_nil, translateTheory.TRUTH_REWRITES,not_nil_nil, GSYM translateTheory.PAIR_THMS, FILTER_EQ_SEXP_SORT] THEN 1382 STRIP_ASSUME_TAC (Q.SPEC `y` UNIQL_M2L) THEN 1383 IMP_RES_TAC uniql_FILTER THEN 1384 RW_TAC std_ss [] THEN 1385 METIS_TAC [MEM_M2L, PERM_QSORT3, MEM_PERM]); 1386 1387val ains_def = 1388 TotalDefn.tDefine 1389 "ains" 1390 `ains a l = itel [(not (consp l), cons a nil) ; 1391 (equal (caar l) (car a), cons a (cdr l)) ; 1392 (lexorder (car a) (caar l), cons a l)] 1393 (cons (car l) (ains a (cdr l)))` 1394 (WF_REL_TAC `measure (sexp_size o SND)` THEN 1395 GEN_TAC THEN Cases THEN 1396 RW_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.sexp_size_def]); 1397 1398val insert_def = Define `(insert R (x,y) [] = [(x,y)]) /\ 1399 (insert R (x,y) ((hx,hy)::tl) = 1400 if hx = x then ((x,y)::tl) 1401 else if R x hx then ((x,y)::(hx,hy)::tl) 1402 else (hx,hy) :: insert R (x,y) tl)`; 1403 1404val ains_insert = store_thm("ains_insert", ``!l f g x y. ONE_ONE f ==> (ains (pair f g (x,y)) (list (pair f g) l) = list (pair f g) (insert (inv_image SEXP_LE f) (x,y) l))``, 1405 Induct THEN ONCE_REWRITE_TAC [ains_def] THEN TRY (Cases_on `h`) THEN 1406 RW_TAC std_ss [translateTheory.list_def, hol_defaxiomsTheory.ACL2_SIMPS, sexpTheory.itel_def, translateTheory.pair_def, insert_def, SEXP_LE_def, REWRITE_RULE [FUN_EQ_THM] relationTheory.inv_image_def] THEN 1407 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [translateTheory.pair_def] THEN METIS_TAC [ONE_ONE_THM]); 1408 1409val slemma = prove(``!x l. SORTED R (x::l) = SORTED R l /\ ((l = []) \/ (R x (HD l)))``, 1410 GEN_TAC THEN Cases THEN RW_TAC std_ss [sortingTheory.SORTED_DEF,HD] THEN METIS_TAC []); 1411 1412val SORTED_INSERT = store_thm("SORTED_INSERT", 1413 ``!R. total R ==> !l x y. SORTED (R LEX K (K T)) l ==> SORTED (R LEX K (K T)) (insert R (x,y) l)``, 1414 NTAC 2 STRIP_TAC THEN Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [slemma, SORTED_DEF, insert_def] THEN 1415 TRY (Cases_on `l`) THEN TRY (Cases_on `h`) THEN FULL_SIMP_TAC std_ss [pairTheory.LEX_DEF, HD, insert_def] THEN 1416 RW_TAC std_ss [HD] THEN 1417 METIS_TAC [relationTheory.total_def]); 1418 1419val MEM_MAPFST_INSERT = store_thm("MEM_MAPFST_INSERT", 1420 ``!l q x y. MEM q (MAP FST (insert R (x,y) l)) = (q = x) \/ MEM q (MAP FST l)``, 1421 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [MEM, MAP, insert_def] THEN 1422 PROVE_TAC []); 1423 1424val MEM_INSERT = store_thm("MEM_INSERT", 1425 ``!l a x y. MEM a (insert R (x,y) l) ==> (FST a = x) /\ (SND a = y) \/ MEM a l``, 1426 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [MEM, insert_def] THEN 1427 RES_TAC THEN FULL_SIMP_TAC std_ss [] THEN PROVE_TAC []); 1428 1429val INSERT_EQ = store_thm("INSERT_EQ", 1430 ``!l x y y'. antisymmetric R /\ transitive (R LEX R') /\ ALL_DISTINCT (MAP FST l) /\ SORTED (R LEX R') l /\ MEM (x,y) (insert R (x,y') l) ==> (y = y')``, 1431 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [MEM, insert_def,ALL_DISTINCT,MAP,MEM_MAP] THEN 1432 IMP_RES_TAC SORTED_EQ THEN FULL_SIMP_TAC std_ss [pairTheory.LEX_DEF] THEN METIS_TAC [relationTheory.antisymmetric_def,pairTheory.FST]); 1433 1434val INSERT_INSERTS = store_thm("INSERT_INSERTS", 1435 ``!l x y R. MEM (x,y) (insert R (x,y) l)``, 1436 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [insert_def, MEM]); 1437 1438val INSERT_MEM = store_thm("INSERT_MEM", 1439 ``!l x y q r R. MEM (x,y) l ==> MEM (x,y) (insert R (q,r) l) \/ (x = q)``, 1440 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [insert_def, MEM] THEN METIS_TAC []); 1441 1442 1443val ALL_DISTINCT_MAPFST_INSERT = store_thm("ALL_DISTINCT_MAPFST_INSERT", 1444 ``!l R x y. total R /\ antisymmetric R /\ transitive R /\ SORTED R (MAP FST l) /\ ALL_DISTINCT (MAP FST l) ==> ALL_DISTINCT (MAP FST (insert R (x,y) l))``, 1445 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [insert_def, MAP, ALL_DISTINCT, MEM, SORTED_EQ, MAP] THEN 1446 IMP_RES_TAC SORTED_EQ THEN 1447 METIS_TAC [relationTheory.transitive_def, relationTheory.antisymmetric_def, relationTheory.total_def, MEM_MAPFST_INSERT]); 1448 1449val INSERT_SET = store_thm("INSERT_SET", 1450 ``!l R R' x y. transitive R /\ antisymmetric R /\ total R /\ transitive (R LEX R') /\ SORTED (R LEX R') l /\ ALL_DISTINCT (MAP FST l) ==> 1451 (set (insert R (x,y) l) = (x,y) INSERT (set l DIFF {z | FST z = x}))``, 1452 Induct THEN REPEAT (Cases ORELSE GEN_TAC) THEN RW_TAC std_ss [insert_def, LIST_TO_SET_THM, EMPTY_DIFF, INSERT_DIFF, ALL_DISTINCT, MAP] THEN 1453 IMP_RES_TAC SORTED_EQ THEN 1454 RW_TAC (std_ss ++ pred_setLib.PRED_SET_ss) [INSERT_DEF, DIFF_DEF, SET_EQ_SUBSET,SUBSET_DEF, LIST_TO_SET_THM, insert_def, IN_LIST_TO_SET, MEM_MAP] THEN 1455 IMP_RES_TAC MEM_INSERT THEN 1456 FULL_SIMP_TAC (std_ss ++ pred_setLib.PRED_SET_ss) [MEM_MAP, INSERT_INSERTS] THEN 1457 TRY (Cases_on `x'`) THEN FULL_SIMP_TAC std_ss [] THENL [ 1458 ALL_TAC, RES_TAC THEN FULL_SIMP_TAC std_ss [pairTheory.LEX_DEF], 1459 ALL_TAC, ALL_TAC] THEN 1460 METIS_TAC [relationTheory.transitive_def, relationTheory.antisymmetric_def, relationTheory.total_def, INSERT_EQ, INSERT_MEM]); 1461 1462val EMPTY_SET = METIS_PROVE [SET_EQ_SUBSET, SUBSET_DEF, NOT_IN_EMPTY] ``({} = a) = !x. ~(x IN a)``; 1463 1464val M2L_RWR = prove(``!x y. MEM x (M2L y) = FST x IN FDOM y /\ (SND x = y ' (FST x))``, 1465 Cases THEN RW_TAC std_ss [MEM_M2L]); 1466 1467val SET_M2L_DOMSUB = store_thm("SET_M2L_DOMSUB", 1468 ``!m x. set (M2L (m \\ x)) = set (M2L m) DIFF {z | FST z = x}``, 1469 RW_TAC std_ss [SET_EQ_SUBSET, SUBSET_DEF, IN_DIFF, IN_LIST_TO_SET, M2L_RWR, FDOM_DOMSUB, IN_DELETE, DOMSUB_FAPPLY_THM] THEN 1470 FULL_SIMP_TAC (std_ss ++ PRED_SET_ss) []); 1471 1472 1473val INSERT_FUPDATE = store_thm("INSERT_FUPDATE", 1474 ``!x y R m. transitive R /\ antisymmetric R /\ total R ==> (QSORT3 (R LEX K (K T)) (M2L (m |+ (x,y))) = insert R (x,y) (QSORT3 (R LEX K (K T)) (M2L m)))``, 1475 REPEAT STRIP_TAC THEN MATCH_MP_TAC MAP_FST_DISTINCT_EQ THEN REPEAT STRIP_TAC THENL [ 1476 MATCH_MP_TAC PERM_SORTED_EQ THEN Q.EXISTS_TAC `R` THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THENL [ 1477 MATCH_MP_TAC PERM_MAP, 1478 METIS_TAC [SORTED_LEX, QSORT3_SORTS, SORTS_DEF, TRANSITIVE_LEX, TOTAL_LEX, TRANSITIVE_K, TOTAL_K, SORTED_INSERT], 1479 METIS_TAC [SORTED_LEX, QSORT3_SORTS, SORTS_DEF, TRANSITIVE_LEX, TOTAL_LEX, TRANSITIVE_K, TOTAL_K, SORTED_INSERT]], 1480 METIS_TAC [ALL_DISTINCT_MAPFST_M2L, PERM_DISTINCT, PERM_QSORT3, PERM_MAP], ALL_TAC] THEN 1481 MATCH_MP_TAC SETEQ_PERM THEN REPEAT CONJ_TAC THEN 1482 TRY (MATCH_MP_TAC SETEQ_TRANS THEN Q.EXISTS_TAC `M2L (m |+ (x,y))` THEN CONJ_TAC THEN1 METIS_TAC [PERM_SETEQ, PERM_QSORT3, PERM_SYM] THEN 1483 REWRITE_TAC [SETEQ_THM, SET_M2L_FUPDATE, LIST_TO_SET_THM] THEN 1484 Q.ABBREV_TAC `l = QSORT3 (R LEX K (K T)) (M2L m)` THEN 1485 REVERSE (`set (insert R (x,y) l) = (x,y) INSERT (set l DIFF {z | FST z = x})` by MATCH_MP_TAC INSERT_SET) THEN1 1486 (`set l = set (M2L m)` by METIS_TAC [PERM_SETEQ, SETEQ_THM, PERM_QSORT3] THEN ASM_REWRITE_TAC [SET_M2L_DOMSUB] THEN AP_TERM_TAC)) THEN 1487 METIS_TAC [PERM_MAP, ALL_DISTINCT_MAPFST_M2L, ALL_DISTINCT_PERM, ALL_DISTINCT_MAPFST_M2L, ALL_DISTINCT_MAPFST, PERM_QSORT3, SORTED_LEX, 1488 TRANSITIVE_K, QSORT3_SORTS, SORTS_DEF, TOTAL_K, TOTAL_LEX, TRANSITIVE_LEX, ALL_DISTINCT_MAPFST_INSERT]); 1489 1490val fupdate_rewrite = store_thm("fupdate_rewrite", 1491 ``!x f g m. ONE_ONE f ==> (encode_fmap f g (m |+ x) = ains (pair f g x) (encode_fmap f g m))``, 1492 Cases THEN RW_TAC std_ss [encode_fmap_def, ains_insert] THEN AP_TERM_TAC THEN 1493 MATCH_MP_TAC INSERT_FUPDATE THEN 1494 METIS_TAC [TRANS_INV, ANTISYM_INV, TOTAL_INV, SEXP_LE_TOTAL, SEXP_LE_TRANSITIVE, SEXP_LE_ANTISYMMETRIC]); 1495 1496val fempty_rewrite = store_thm("fempty_rewrite", 1497 ``!f g. encode_fmap f g FEMPTY = list (pair f g) []``, 1498 RW_TAC std_ss [encode_fmap_def,M2L_def] THEN 1499 ONCE_REWRITE_TAC [fold_def] THEN 1500 RW_TAC std_ss [sortingTheory.QSORT3_DEF]); 1501 1502val _ = export_theory(); 1503