1(* File: tcTacs.sml. Author: F. Lockwood Morris. Begun 6 Aug 2013. *) 2 3(* Conversions culminating in TC_CONV, applicable to a term of the *) 4(* form (FMAP_TO_RELN (FMAPAL ... ))^+ (with ENUMERAL-sets as *) 5(* the map values), which it proves equal to one of the form *) 6(* (FMAP_TO_RELN (FMAPAL ......... )), alternatively applicable to a *) 7(* term of the form (FMAP_TO_RELN (fmap [(.,{...}); ... ]))^+, again *) 8(* proving it equal to a term of the same form without the ^+ . *) 9 10structure tcTacs :> tcTacs = 11struct 12(* comment out load before Holmaking *) 13(* app load ["pred_setTheory", "totoTacs", "enumTacs", "fmapalTacs", 14 "tcTheory"]; *) 15 16open Parse HolKernel boolLib bossLib; 17val _ = set_trace "Unicode" 0; 18 19open enumTacs fmapalTacs tcTheory; 20 21val AR = ASM_REWRITE_TAC []; 22fun ulist x = [x]; 23 24val ERR = mk_HOL_ERR "tcTacs"; 25 26(* A conversion to translate the most convenient explicit representation, 27 namely ``fmap [(a1, {v11; ... ; v1m1}); ... ; (an, {vn1; ... ; vnmn})]``, 28 of a set-valued fmap to an ENUMERAL-valued FMAPAL, given a conversion 29 for working out the total order on elements, and the name of the order. 30 FMAP_TO_RELN g, where g has the form of a result from ENUF_CONV, is our 31 standard explicit representation of a binary relation. *) 32 33fun ENUF_CONV keyconv keyord = 34RAND_CONV (MAP_ELEM_CONV (RAND_CONV 35 (TO_set_CONV NO_CONV THENC 36 set_TO_ENUMERAL_CONV keyconv keyord))) THENC 37fmap_TO_FMAPAL_CONV keyconv keyord; 38 39(* ******************************************************************** *) 40(* The main recursive workhorse will be TC_ITER_CONV, but there is *) 41(* set_up work to be done first; specifically we expect to have *) 42(* TC_CONV keyconv = PRE_TC_CONV keyconv THENC *) 43(* RAND_CONV (TC_ITER_CONV keyconv) . *) 44(* ******************************************************************** *) 45 46val EMPTY_UNION_EQN = prove (``!sd:'a set. sd = {} UNION sd``, 47REWRITE_TAC [pred_setTheory.UNION_EMPTY]); 48 49(* Catholic PRE_TC_CONV, works for fmap or FMAPAL terms. *) 50 51fun PRE_TC_CONV keyconv Aplus = 52let val A = rand Aplus; 53 val hypb = ISPEC A subTC_EMPTY; 54 val [elemty, elemsetty] = snd (dest_type (type_of (rand A))); 55 val fdomt = mk_comb (mk_const ("FDOM", 56 type_subst [alpha |-> elemty, beta |-> elemsetty] 57 ``:('a |-> 'b) -> 'a -> bool``), rand A); 58 val hypa = 59 SYM ((FDOM_CONV THENC 60 TO_set_CONV keyconv THENC 61 REWR_CONV EMPTY_UNION_EQN) fdomt) 62in MATCH_MP TC_ITER_THM (CONJ hypa hypb) end; 63 64fun TC_MOD_CONV keyconv = 65REWR_CONV TC_MOD THENC 66RATOR_CONV (RATOR_CONV (RAND_CONV (IN_CONV keyconv))) THENC COND_CONV THENC 67TRY_CONV (UNION_CONV keyconv); 68 69val [tc_iter_NIL, tc_iter_CONS] = CONJUNCTS TC_ITER; 70 71(* tc_iter_NIL = |- !r. TC_ITER [] r = r 72 tc_iter_CONS = 73 |- !x d r. TC_ITER (x::d) r = TC_ITER d (TC_MOD x (r ' x) o_f r) *) 74 75fun TC_ITER_CONV keyconv = 76let fun tci t = 77((REWR_CONV tc_iter_CONS THENC 78 RAND_CONV (LAND_CONV (RAND_CONV (FAPPLY_CONV keyconv)) THENC 79 o_f_CONV (TC_MOD_CONV keyconv)) THENC 80 tci) ORELSEC 81 REWR_CONV tc_iter_NIL) t 82in tci end; 83 84fun TC_CONV keyconv = PRE_TC_CONV keyconv THENC 85 RAND_CONV (TC_ITER_CONV keyconv); 86 87(* *** examples for debugging and timing: *** *) 88(* ****************************************** 89open numLib totoTacs; 90val cormenex = ``[(2, {4; 3}); (3, {2}); (4, {3; 1}); (1, {})]``; 91 ENUF_CONV numto_CONV ``numto`` 92 ``fmap [(2, set [4; 3]); (3, set [2]); (4, set [3; 1]); (1, set [])]``; 93val corfmap = rand (concl (ENUF_CONV numto_CONV ``numto`` ``fmap ^cormenex``)); 94 95 val Aplus = ``(FMAP_TO_RELN ^corfmap)^+``; 96 val keyconv = numto_CONV; 97 98 PRE_TC_CONV keyconv ``(FMAP_TO_RELN ^corfmap)^+``; 99 PRE_TC_CONV NO_CONV ``(FMAP_TO_RELN (fmap ^cormenex))^+``; 100 101 val s123 = rand (concl (DISPLAY_TO_ENUMERAL_CONV 102 numto_CONV ``numto`` ``{1; 2; 3}``)); 103 val s345 = rand (concl (DISPLAY_TO_ENUMERAL_CONV 104 numto_CONV ``numto`` ``{5; 4; 3}``)); 105 TC_MOD_CONV numto_CONV ``TC_MOD 5 ^s123 ^s345``; 106 TC_MOD_CONV numto_CONV ``TC_MOD 5 ^s345 ^s123``; 107 val t123 = ``{1; 2; 3}``; 108 val t345 = ``{5; 4; 3}``; 109 TC_MOD_CONV REDUCE_CONV ``TC_MOD 5 ^t123 ^t345``; 110 TC_MOD_CONV REDUCE_CONV ``TC_MOD 5 ^t345 ^t123``; 111 112 val tcit = 113 rand (rand (concl (PRE_TC_CONV keyconv ``(FMAP_TO_RELN ^corfmap)^+``))); 114 TC_ITER_CONV keyconv tcit; 115 val tins = rand (rand (concl (PRE_TC_CONV NO_CONV 116 ``(FMAP_TO_RELN (fmap ^cormenex))^+``))); 117 TC_ITER_CONV REDUCE_CONV tins; 118 119 Count.apply (TC_CONV numto_CONV) ``(FMAP_TO_RELN ^corfmap)^+``; 120 (*runtime: 0.036s, Prims: 7326*) 121 val one_to_ten = ``fmap [(1,{4}); (2,{6}); (3,{1}); (4,{5}); (5,{9}); 122 (6,{8}); (8,{10}); (9,{2}); (10,{7})]``; 123 val one_ten_chain = rand (concl ( 124 Count.apply (ENUF_CONV numto_CONV ``numto``) one_to_ten)); 125 (*runtime: 0.008s, Prims: 2741*) 126 127val small_tc = rand (concl ( 128 Count.apply (TC_CONV numto_CONV) ``(FMAP_TO_RELN ^one_ten_chain)^+``)); 129 (*runtime: 0.164s, Prims: 25411*) 130 131 Count.apply (TC_CONV REDUCE_CONV) ``(FMAP_TO_RELN ^one_to_ten)^+``; 132 (*runtime: 0.04400s, Prims: 17569*) 133 134val ls = rand (rand (concl (FMAPAL_TO_fmap_CONV numto_CONV (rand small_tc)))); 135 136rand (concl 137 (MAP_ELEM_CONV (RAND_CONV (ENUMERAL_TO_DISPLAY_CONV numto_CONV)) ls)); 138 139val beer_bottles = ``fmap 140[(99,{98}); (98,{97}); (97,{96}); (96,{95}); (95,{94}); 141 (94,{93}); (93,{92}); (92,{91}); (91,{90}); (90,{89}); 142 (89,{88}); (88,{87}); (87,{86}); (86,{85}); (85,{84}); 143 (84,{83}); (83,{82}); (82,{81}); (81,{80}); (80,{79}); 144 (79,{78}); (78,{77}); (77,{76}); (76,{75}); (75,{74}); 145 (74,{73}); (73,{72}); (72,{71}); (71,{70}); (70,{69}); 146 (69,{68}); (68,{67}); (67,{66}); (66,{65}); (65,{64}); 147 (64,{63}); (63,{62}); (62,{61}); (61,{60}); (60,{59}); 148 (59,{58}); (58,{57}); (57,{56}); (56,{55}); (55,{54}); 149 (54,{53}); (53,{52}); (52,{51}); (51,{50}); (50,{49}); 150 (49,{48}); (48,{47}); (47,{46}); (46,{45}); (45,{44}); 151 (44,{43}); (43,{42}); (42,{41}); (41,{40}); (40,{39}); 152 (39,{38}); (38,{37}); (37,{36}); (36,{35}); (35,{34}); 153 (34,{33}); (33,{32}); (32,{31}); (31,{30}); (30,{29}); 154 (29,{28}); (28,{27}); (27,{26}); (26,{25}); (25,{24}); 155 (24,{23}); (23,{22}); (22,{21}); (21,{20}); (20,{19}); 156 (19,{18}); (18,{17}); (17,{16}); (16,{15}); (15,{14}); 157 (14,{13}); (13,{12}); (12,{11}); (11,{10}); (10,{9}); (9,{8}); 158 (8,{7}); (7,{6}); (6,{5}); (5,{4}); (4,{3}); (3,{2}); (2,{1}); (1,{0})]``; 159 160val beer_chain = rand (concl ( 161 Count.apply (ENUF_CONV numto_CONV ``numto``) beer_bottles)); 162 (*runtime: 0.12s, Prims: 43892*) 163 164 val beer_tc_fmapal = rand (rand (concl ( 165 Count.apply (TC_CONV numto_CONV) ``(FMAP_TO_RELN ^beer_chain)^+``))); 166 (*runtime: 11.905s, Prims: 2800937*) 167 168 Count.apply (FMAPAL_TO_fmap_CONV numto_CONV) 169 beer_tc_fmapal; 170 (*runtime: 0.032s, Prims: 8280 *) 171rand (concl 172 (Count.apply (MAP_ELEM_CONV (RAND_CONV (ENUMERAL_TO_DISPLAY_CONV numto_CONV))) 173 (rand (rand (concl (FMAPAL_TO_fmap_CONV numto_CONV beer_tc_fmapal)))))); 174 (*runtime: 3.104s, Prims: 444149*) 175(* Unreasonable amount of work converting, but one can finally read the 176 output and see that it is correct. *) 177 178 Count.apply (FAPPLY_CONV numto_CONV) ``^beer_tc_fmapal ' 50``; 179 (*runtime: 0.004s, Prims: 307*) 180 181(* |- (FMAP_TO_RELN 182 (FMAPAL numto 183 (node 184 (node 185 (node (node nt (1,ENUMERAL numto (node nt 0 nt)) nt) 186 (2,ENUMERAL numto (node nt 1 nt)) 187 (node nt (3,ENUMERAL numto (node nt 2 nt)) nt)) 188 189... 190 (node 191 (node nt (97,ENUMERAL numto (node nt 96 nt)) 192 nt) (98,ENUMERAL numto (node nt 97 nt)) 193 (node nt (99,ENUMERAL numto (node nt 98 nt)) 194 nt)))))))))^+ = 195 FMAP_TO_RELN 196 (FMAPAL numto 197 (node 198 (node 199 (node (node nt (1,ENUMERAL numto (node nt 0 nt)) nt) 200 (2,ENUMERAL numto (node nt 0 (node nt 1 nt))) 201 (node nt 202 (3, 203 ENUMERAL numto 204 (node (node nt 0 nt) 1 (node nt 2 nt))) nt)) 205... 206 (node (node nt 92 nt) 93 207 (node nt 94 nt)) 95 208 (node (node nt 96 nt) 97 209 (node nt 98 nt)))))))) 210 nt)))))))) *) 211 212val beer_tc_fmap = rand (rand (concl (Count.apply (TC_CONV REDUCE_CONV) 213 ``(FMAP_TO_RELN ^beer_bottles)^+``))); 214 (*runtime: 42.143s,Prims:23897363*) 215 216(* |- (FMAP_TO_RELN 217 (fmap 218 [(99,{98}); (98,{97}); (97,{96}); (96,{95}); (95,{94}); 219 (94,{93}); (93,{92}); (92,{91}); (91,{90}); (90,{89}); 220... 221 (8,{7}); (7,{6}); (6,{5}); (5,{4}); (4,{3}); (3,{2}); (2,{1}); 222 (1,{0})]))^+ = 223 FMAP_TO_RELN 224 (fmap 225 [(99, 226 {98; 97; 96; 95; 94; 93; 92; 91; 90; 89; 88; 87; 86; 85; 84; 227 83; 82; 81; 80; 79; 78; 77; 76; 75; 74; 73; 72; 71; 70; 69; 228... 229 (5,{4; 3; 2; 1; 0}); (4,{3; 2; 1; 0}); (3,{2; 1; 0}); 230 (2,{1; 0}); (1,{0})]): *) 231 232Count.apply (FAPPLY_CONV REDUCE_CONV) ``^beer_tc_fmap ' 50``; 233 (*runtime: 0.016s, Prims: 4077*) 234 235**************************** *) 236end; 237