1(* An alternative approach to creating finite sets as a quotient of lists.  *)
2(* This takes the extensionality principle as the definition of equivalence.*)
3(* Composed and contributed by Michael Norrish.                             *)
4(* June 24, 2005.                                                           *)
5
6open HolKernel Parse boolLib bossLib BasicProvers listTheory quotientLib
7
8val _ = new_theory "ext_finite_set";
9
10fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before
11                         export_rewrites [n]
12
13val leq_def = Define`leq x y = !e:'a. MEM e x = MEM e y`
14
15val leq_refl = Store_Thm(
16  "leq_refl",
17  ``!x :'a list. leq x x``,
18  SRW_TAC [] [leq_def]);
19
20val leq_sym = Store_Thm(
21  "leq_sym",
22  ``!x y :'a list. leq x y ==> leq y x``,
23  SRW_TAC [] [leq_def]);
24
25val leq_trans = Store_Thm(
26  "leq_trans",
27  ``!x y z :'a list. leq x y /\ leq y z ==> leq x z``,
28  SRW_TAC [] [leq_def]);
29
30(* functions on representatives *)
31
32(* insertion is represented by :: *)
33val NOT_NIL_EQUIV_CONS = store_thm(
34  "NOT_NIL_EQUIV_CONS",
35  ``~(leq [] ((a:'a)::A))``,
36  SRW_TAC [boolSimps.DNF_ss] [leq_def]);
37
38val NIL_RSP = store_thm(
39  "NIL_RSP",
40  ``leq ([]:'a list) []``,
41  SRW_TAC [] [leq_def]);
42
43val CONS_RSP = store_thm(
44  "CONS_RSP",
45  ``!x:'a A B. leq A B ==> leq (x::A) (x::B)``,
46  SRW_TAC [] [leq_def]);
47
48(* membership is represented by MEM *)
49val MEM_RSP = store_thm(
50  "MEM_RSP",
51  ``!X Y x:'a. leq X Y ==> (MEM x X = MEM x Y)``,
52  SRW_TAC [] [leq_def]);
53
54val NO_MEM_NIL = Store_Thm(
55  "NO_MEM_NIL",
56  ``!A. (!a:'a. ~(MEM a A)) = (A = [])``,
57  Induct_on `A` THEN SRW_TAC [] [] THEN PROVE_TAC []);
58
59val NONE_MEM_NIL = store_thm(
60  "NONE_MEM_NIL",
61  ``!A. (!a:'a. ~(MEM a A)) = (leq A [])``,
62  SRW_TAC [] [leq_def]);
63
64val MEM_CONS = store_thm(
65  "MEM_CONS",
66  ``!A (a:'a). MEM a A ==> leq (a :: A) A``,
67  SRW_TAC [] [leq_def] THEN PROVE_TAC []);
68
69val CONS_LEFT_COMM = prove(
70  ``!A x y:'a. leq (x::y::A) (y::x::A)``,
71  SRW_TAC [] [leq_def] THEN PROVE_TAC []);
72
73val CONS_LEFT_IDEM = prove(
74  ``!A x:'a. leq (x::x::A) (x::A)``,
75  SRW_TAC [] [leq_def] THEN PROVE_TAC []);
76
77val finite_set1_strong_cases = store_thm(
78  "finite_set1_strong_cases",
79  ``!X. (X = []) \/ ?(a:'a) Y. ~MEM a Y /\ leq X (a::Y)``,
80  Induct THEN FULL_SIMP_TAC (srw_ss()) [leq_def] THEN
81  METIS_TAC [MEM]);
82
83(* Delete1 *)
84val Delete1_def = Define
85   `($Delete1 [] x = [])  /\
86    ($Delete1 ((a:'a) :: A) x = if a = x then $Delete1 A x
87                                     else a :: ($Delete1 A x))`;
88val _ = export_rewrites ["Delete1_def"]
89
90val _ = add_infix ("Delete1", 500, HOLgrammars.LEFT);
91
92val MEM_Delete1 = store_thm (
93  "MEM_Delete1",
94  ``!A (a:'a) x. MEM x (A Delete1 a) = MEM x A /\ ~(x = a)``,
95  Induct THEN SRW_TAC[][] THEN PROVE_TAC []);
96
97val MEM_Delete1_IDENT = Store_Thm(
98  "MEM_Delete1_IDENT",
99  ``!A (a:'a). ~(MEM a (A Delete1 a))``,
100  Induct_on `A` THEN SRW_TAC [][]);
101
102val NOT_MEM_Delete1_IDENT = store_thm(
103  "NOT_MEM_Delete1_IDENT",
104  ``!A (b:'a). ~MEM b A ==> (A Delete1 b = A)``,
105  Induct_on `A` THEN SRW_TAC [][]);
106
107val Delete1_RSP = store_thm(
108  "Delete1_RSP",
109  ``!A B (a:'a). leq A B ==> (leq (A Delete1 a) (B Delete1 a))``,
110  SRW_TAC [] [leq_def,MEM_Delete1]);
111
112val CONS_Delete1 = store_thm(
113  "CONS_Delete1",
114  ``!A (a:'a). leq (a :: (A Delete1 a)) (if MEM a A then A else a::A)``,
115  SRW_TAC [] [leq_def, MEM_Delete1] THEN PROVE_TAC []);
116
117val MEM_CONS_Delete1 = store_thm
118   ("MEM_CONS_Delete1",
119    ``!A (a:'a). MEM a A ==> leq (a :: (A Delete1 a)) A``,
120    PROVE_TAC [CONS_Delete1]
121   );
122
123val finite_set1_Delete1_cases1 = store_thm
124   ("finite_set1_Delete1_cases1",
125    ``!X. (X = []) \/ ?a:'a. leq X (a :: (X Delete1 a))``,
126    Cases THEN SRW_TAC [][leq_def, MEM_Delete1] THEN METIS_TAC []);
127
128val finite_set1_Delete1_cases = store_thm
129   ("finite_set1_Delete1_cases",
130    ``!X. (X = []) \/
131            ?a:'a. MEM a X /\ leq X (a :: (X Delete1 a))``,
132    PROVE_TAC[finite_set1_Delete1_cases1,MEM,MEM_RSP]
133   );
134
135(* Card1 *)
136
137val Card1_def = Define
138   `(Card1 ([]) = 0)  /\
139    (Card1 ((a:'a) :: A) = if MEM a A then Card1 A else SUC (Card1 A))`;
140val _ = export_rewrites ["Card1_def"]
141
142val NOT_MEM_Card1 = store_thm
143   ("NOT_MEM_Card1",
144    ``!A:'a list a. ~(MEM a A) ==>
145             (Card1 (a :: A) = SUC (Card1 A))``,
146    RW_TAC std_ss [Card1_def]
147   );
148
149val Card1_SUC = store_thm (
150  "Card1_SUC",
151  ``!A n. (Card1 A = SUC n) ==>
152          ?(a:'a) B. ~(MEM a B) /\ leq A (a :: B)``,
153  Induct THEN SRW_TAC [][] THENL [
154    PROVE_TAC [MEM_CONS, leq_trans, leq_sym],
155    PROVE_TAC [leq_refl]
156  ]);
157
158val MEM_Card1_NOT_0 = store_thm(
159  "MEM_Card1_NOT_0",
160  ``!A a. MEM (a:'a) A ==> ~(Card1 A = 0)``,
161  Induct_on `A` THEN SRW_TAC [][] THEN PROVE_TAC []);
162
163val Card1_CONS_GT_0 = store_thm (
164  "Card1_CONS_GT_0",
165  ``!A (a:'a). 0 < Card1 (a :: A)``,
166  METIS_TAC [MEM, arithmeticTheory.NOT_ZERO_LT_ZERO,
167             MEM_Card1_NOT_0]);
168
169val Card1_Delete1 = store_thm(
170  "Card1_Delete1",
171  ``!A (a:'a).
172      Card1 (A Delete1 a) = if MEM a A then Card1 A - 1 else Card1 A``,
173  Induct_on `A` THEN SRW_TAC [][MEM_Delete1] THEN SRW_TAC [][] THEN
174  PROVE_TAC [MEM_Card1_NOT_0, DECIDE ``~(x = 0) ==> (SUC (x - 1) = x)``]);
175
176val Card1_RSP = store_thm (
177  "Card1_RSP",
178  ``!A B:'a list. leq A B ==> (Card1 A = Card1 B)``,
179  SIMP_TAC (srw_ss()) [leq_def] THEN Induct THEN SRW_TAC [][] THENL [
180    PROVE_TAC [],
181    `MEM h B /\ ~(Card1 B = 0)` by PROVE_TAC [MEM_Card1_NOT_0] THEN
182    Q_TAC SUFF_TAC `Card1 A = Card1 (B Delete1 h)`
183          THEN1 SRW_TAC [numSimps.ARITH_ss][Card1_Delete1] THEN
184    FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][MEM_Delete1] THEN
185    PROVE_TAC []
186  ]);
187
188val Card1_0 = store_thm(
189  "Card1_0",
190  ``!A:'a list. (Card1 A = 0) = (A = [])``,
191  Induct_on `A` THEN SRW_TAC [][] THEN PROVE_TAC [NO_MEM_NIL]);
192
193(* list2set *)
194val list2set_thm = prove(
195  ``(LIST_TO_SET ([]:'a list) = {}) /\
196    (!h:'a t. LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)``,
197  SRW_TAC [][pred_setTheory.EXTENSION]);
198
199val list2set_RSP = store_thm(
200  "list2set_RSP",
201  ``!A B:'a list. leq A B ==> (LIST_TO_SET A = LIST_TO_SET B)``,
202  SRW_TAC [][leq_def, pred_setTheory.EXTENSION]);
203
204(* fold *)
205
206val Fold1_def = Define`
207  (Fold1 f (z:'b) [] = z) /\
208  (Fold1 f z ((a:'a)::A) =
209     if (!u v w. f u (f v w) = f v (f u w)) then
210       if MEM a A then Fold1 f z A
211       else f a (Fold1 f z A)
212     else z)
213` ;
214
215val MEM_lcommuting_Fold1 = store_thm(
216  "MEM_lcommuting_Fold1",
217  ``!B f (z:'b) (h:'a).
218     (!u v w. f u (f v w) = f v (f u w)) /\ MEM h B ==>
219     (Fold1 f z B = f h (Fold1 f z (B Delete1 h)))``,
220  Induct_on `B` THEN SRW_TAC [][Fold1_def, MEM_Delete1] THENL [
221    PROVE_TAC [],
222    PROVE_TAC [NOT_MEM_Delete1_IDENT],
223    PROVE_TAC []
224  ]);
225
226val Fold1_RSP = store_thm(
227  "Fold1_RSP",
228  ``!A B:'a list f (z:'b). leq A B ==> (Fold1 f z A = Fold1 f z B)``,
229  REWRITE_TAC [leq_def] THEN Induct THEN SRW_TAC [][Fold1_def] THENL [
230    PROVE_TAC [],
231    `MEM h B` by PROVE_TAC [] THEN
232    `Fold1 f z B = f h (Fold1 f z (B Delete1 h))`
233       by PROVE_TAC [MEM_lcommuting_Fold1] THEN
234    SRW_TAC [][] THEN AP_TERM_TAC THEN
235    FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][MEM_Delete1] THEN
236    PROVE_TAC [],
237    Cases_on `B` THEN SRW_TAC [][Fold1_def]
238  ]);
239
240val APPEND_RSP = store_thm(
241  "APPEND_RSP",
242  ``!A1 A2 B1 B2:'a list. leq A1 A2 /\ leq B1 B2 ==>
243                          leq (APPEND A1 B1) (APPEND A2 B2)``,
244  SRW_TAC [][leq_def]);
245
246val Inter1_def = Define
247   `($Inter1 ([]) B = [])  /\
248    ($Inter1 ((a:'a) :: A) B = if MEM a B then a :: ($Inter1 A B)
249                                          else $Inter1 A B)`;
250
251val _ = add_infix ("Inter1", 600, HOLgrammars.LEFT);
252
253val MEM_Inter1 = store_thm
254   ("MEM_Inter1",
255    ``!A B (x:'a).
256           MEM x (A Inter1 B) = MEM x A /\ MEM x B``,
257    Induct
258    THEN SRW_TAC [][Inter1_def]
259    THEN PROVE_TAC []
260   );
261
262val Inter1_RSP = store_thm
263   ("Inter1_RSP",
264    ``!A1 A2 B1 B2:'a list.
265           leq A1 A2 /\ leq B1 B2 ==>
266           leq (A1 Inter1 B1) (A2 Inter1 B2)``,
267    SRW_TAC [][leq_def, MEM_Inter1]);
268
269(* do the quotient *)
270val leq_equiv = save_thm("leq_equiv",
271    refl_sym_trans_equiv leq_refl leq_sym leq_trans);
272
273val equivs = [leq_equiv];
274
275
276val fnlist =
277    [{def_name="Empty_def",
278      fname="Empty",
279      func= ``[] :'a list``,
280      fixity=NONE},
281
282     {def_name="Insert_def",
283      fname="Insert",
284      func= ``CONS :'a -> 'a list -> 'a list``,
285      fixity=SOME(Infixr 490)},
286
287(* if desired, a membership constant for finite sets can be defined in
288   terms of fset2set:
289
290     fmem x s = x ��� fset2set s                        (UOK)
291
292   Alternatively, fmem could just be overloaded to a term of this form, as
293   is done in the finite_set version of this example.
294
295   The following doesn't work because MEM is not a constant (since f42df6bf5)
296
297     {def_name="In_def",
298      fname="In",
299      func= ``MEM :'a -> 'a list -> bool``,
300      fixity=SOME(Infix(NONASSOC,425))},
301*)
302
303     {def_name="Card_def",
304      fname="Card",
305      func= ``Card1 :'a list -> num``,
306      fixity=NONE},
307
308     {def_name="Delete_def",
309      fname="Delete",
310      func= ``$Delete1 :'a list -> 'a -> 'a list``,
311      fixity=SOME(Infixl 500)},
312
313     {def_name="Union_def",
314      fname="Union",
315      func= ``APPEND :'a list -> 'a list -> 'a list``,
316      fixity=SOME(Infixl 500)},
317
318     {def_name="Inter_def",
319      fname="Inter",
320      func= ``$Inter1 :'a list -> 'a list -> 'a list``,
321      fixity=SOME(Infixl 600)},
322
323     {def_name="Fold_def",
324      fname="Fold",
325      func= ``Fold1 :('a -> 'b -> 'b) -> 'b -> 'a list -> 'b``,
326      fixity=NONE},
327
328     {def_name="fset2set_def",
329      fname="fset2set",
330      func= ``LIST_TO_SET :'a list -> 'a -> bool``,
331      fixity=NONE}
332    ];
333
334
335(* ==================================================== *)
336(*   LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS   *)
337(* ==================================================== *)
338
339val _ = quotient.chatting := true;   (* Causes display of quotient as built *)
340
341
342val  [finite_set_cases, Insert_LEFT_COMM, Insert_LEFT_IDEM,
343      In, NONE_In_Empty, In_Insert, finite_set_strong_cases,
344      Card, NOT_In_Card, Card_SUC, Card_Insert_GT_0,
345      In_Card_NOT_0, NOT_Empty_Insert,
346      Delete_def, In_Delete, Card_Delete,
347      Insert_Delete, In_Insert_Delete, finite_set_Delete_cases,
348      Union, In_Union, Inter, In_Inter,
349      Fold, fset2set, finite_set_EXTENSION, finite_set_INDUCT
350     ] =
351
352    define_quotient_types
353
354    {types = [{name = "finite_set", equiv = leq_equiv}],
355     defs = fnlist,
356     tyop_equivs = [],
357     tyop_quotients = [FUN_QUOTIENT],
358     tyop_simps = [FUN_REL_EQ, FUN_MAP_I],
359     respects = [NIL_RSP, CONS_RSP, Card1_RSP, Delete1_RSP,
360                 APPEND_RSP, Inter1_RSP, Fold1_RSP, list2set_RSP],
361     poly_preserves = [FORALL_PRS, EXISTS_PRS, COND_PRS],
362     poly_respects = [RES_FORALL_RSP, RES_EXISTS_RSP, COND_RSP],
363     old_thms = [list_CASES, CONS_LEFT_COMM, CONS_LEFT_IDEM,
364                 MEM, NONE_MEM_NIL, MEM_CONS, finite_set1_strong_cases,
365                 Card1_def, NOT_MEM_Card1, Card1_SUC, Card1_CONS_GT_0,
366                 MEM_Card1_NOT_0, NOT_NIL_EQUIV_CONS,
367                 Delete1_def, MEM_Delete1, Card1_Delete1,
368                 CONS_Delete1, MEM_CONS_Delete1, finite_set1_Delete1_cases,
369                 APPEND, MEM_APPEND, Inter1_def, MEM_Inter1,
370                 Fold1_def, list2set_thm, leq_def, list_INDUCT]
371   };
372
373val _ = map save_thm
374    [("finite_set_cases",finite_set_cases),
375     ("Insert_LEFT_COMM",Insert_LEFT_COMM),
376     ("Insert_LEFT_IDEM",Insert_LEFT_IDEM),
377     ("In",In),
378     ("NONE_In_Empty",NONE_In_Empty),
379     ("In_Insert",In_Insert),
380     ("finite_set_strong_cases",finite_set_strong_cases),
381     ("Card",Card),
382     ("NOT_In_Card",NOT_In_Card),
383     ("Card_SUC",Card_SUC),
384     ("Card_Insert_GT_0",Card_Insert_GT_0),
385     ("In_Card_NOT_0",In_Card_NOT_0),
386     ("NOT_Empty_Insert",NOT_Empty_Insert),
387     ("Delete_def",Delete_def),
388     ("In_Delete",In_Delete),
389     ("Card_Delete",Card_Delete),
390     ("Insert_Delete",Insert_Delete),
391     ("In_Insert_Delete",In_Insert_Delete),
392     ("finite_set_Delete_cases",finite_set_Delete_cases),
393     ("Union",Union),
394     ("In_Union",In_Union),
395     ("Inter",Inter),
396     ("In_Inter",In_Inter),
397     ("Fold",Fold),
398     ("fset2set",fset2set),
399     ("finite_set_EXTENSION",finite_set_EXTENSION),
400     ("finite_set_INDUCT",finite_set_INDUCT)
401    ];
402
403val _ = export_theory();
404
405val _ = html_theory "ext_finite_set";
406