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