1structure pred_setSyntax :> pred_setSyntax =
2struct
3
4local open pred_setTheory in end;
5
6open HolKernel Abbrev;
7
8val ERR = mk_HOL_ERR "pred_setSyntax"
9
10(*---------------------------------------------------------------------------*)
11(* Types                                                                     *)
12(*---------------------------------------------------------------------------*)
13
14fun mk_set_type ty = ty --> bool
15
16fun dest_set_type ty =
17   case total dom_rng ty of
18      SOME (ty1, ty2) =>
19         if ty2 = Type.bool
20            then ty1
21         else raise ERR "dest_set_type" "not an instance of 'a -> bool"
22    | NONE => raise ERR "dest_set_type" "not an instance of 'a -> bool"
23
24val is_set_type  = Lib.can dest_set_type
25
26(*---------------------------------------------------------------------------*)
27(* Get the type of the elements of a set                                     *)
28(*---------------------------------------------------------------------------*)
29
30fun eltype tm = dest_set_type (type_of tm)
31
32(*---------------------------------------------------------------------------*)
33(* Set constants. Note that "IN" is alredy defined in boolTheory.            *)
34(*---------------------------------------------------------------------------*)
35
36val t1 = HolKernel.syntax_fns1 "pred_set"
37val t2 = HolKernel.syntax_fns2 "pred_set"
38val t3 = HolKernel.syntax_fns3 "pred_set"
39
40fun syn s = HolKernel.syntax_fns s "pred_set"
41val s1 = syn {n = 2, dest = HolKernel.dest_monop, make = HolKernel.mk_monop}
42val s2 = syn {n = 3, dest = HolKernel.dest_binop, make = HolKernel.mk_binop}
43
44val (in_tm, mk_in, dest_in, is_in) = HolKernel.syntax_fns2 "bool" "IN"
45val (insert_tm, mk_insert, dest_insert, is_insert) = s2 "INSERT"
46val (inter_tm, mk_inter, dest_inter, is_inter) = s2 "INTER"
47val (union_tm, mk_union, dest_union, is_union) = s2 "UNION"
48val (diff_tm, mk_diff, dest_diff, is_diff) = s2 "DIFF"
49val (delete_tm, mk_delete, dest_delete, is_delete) = s2 "DELETE"
50val (gspec_tm, mk_gspec, dest_gspec, is_gspec) = s1 "GSPEC"
51val (compl_tm, mk_compl, dest_compl, is_compl) = s1 "COMPL"
52val (card_tm, mk_card, dest_card, is_card) = t1 "CARD"
53val (image_tm, mk_image, dest_image, is_image) = s2 "IMAGE"
54val (finite_tm, mk_finite, dest_finite, is_finite) = t1 "FINITE"
55val (sing_tm, mk_sing, dest_sing, is_sing) = t1 "SING"
56val (subset_tm, mk_subset, dest_subset, is_subset) = t2 "SUBSET"
57val (psubset_tm, mk_psubset, dest_psubset, is_psubset) = t2 "PSUBSET"
58val (pow_tm, mk_pow, dest_pow, is_pow) = s1 "POW"
59val (disjoint_tm, mk_disjoint, dest_disjoint, is_disjoint) = t2 "DISJOINT"
60val (bigunion_tm, mk_bigunion, dest_bigunion, is_bigunion) = s1 "BIGUNION"
61val (biginter_tm, mk_biginter, dest_biginter, is_biginter) = s1 "BIGINTER"
62val (cross_tm, mk_cross, dest_cross, is_cross) = s2 "CROSS"
63val (count_tm, mk_count, dest_count, is_count) = s1 "count"
64val (max_set_tm, mk_max_set, dest_max_set, is_max_set) = t1 "MAX_SET"
65val (min_set_tm, mk_min_set, dest_min_set, is_min_set) = t1 "MIN_SET"
66val (sum_image_tm, mk_sum_image, dest_sum_image, is_sum_image) = t2 "SUM_IMAGE"
67val (sum_set_tm, mk_sum_set, dest_sum_set, is_sum_set) = t1 "SUM_SET"
68val (choice_tm, mk_choice, dest_choice, is_choice) = t1 "CHOICE"
69val (rest_tm, mk_rest, dest_rest, is_rest) = s1 "REST"
70val (inj_tm, mk_inj, dest_inj, is_inj) = t3 "INJ"
71val (surj_tm, mk_surj, dest_surj, is_surj) = t3 "SURJ"
72val (bij_tm, mk_bij, dest_bij, is_bij) = t3 "BIJ"
73val (linv_tm, mk_linv, dest_linv, is_linv) = t3 "LINV"
74val (rinv_tm, mk_rinv, dest_rinv, is_rinv) = t3 "RINV"
75
76(*---------------------------------------------------------------------------*)
77(* Empty set                                                                 *)
78(*---------------------------------------------------------------------------*)
79
80val empty_tm = prim_mk_const {Name = "EMPTY", Thy = "pred_set"}
81
82fun mk_empty ty =
83   inst [alpha |-> ty] empty_tm
84   handle HOL_ERR _ => raise ERR "mk_empty" ""
85
86fun dest_empty tm =
87   if same_const tm empty_tm
88      then type_of tm
89   else raise ERR "dest_empty" "not the empty set"
90
91val is_empty = Lib.can dest_empty
92
93(*---------------------------------------------------------------------------*)
94(* Unversal set                                                              *)
95(*---------------------------------------------------------------------------*)
96
97val univ_tm = prim_mk_const {Name = "UNIV", Thy = "pred_set"}
98
99fun mk_univ ty =
100   inst [alpha |-> ty] univ_tm
101   handle HOL_ERR _ => raise ERR "mk_univ" ""
102
103fun dest_univ tm =
104   if same_const tm univ_tm
105      then type_of tm
106   else raise ERR "dest_univ" "not the universal set"
107
108val is_univ = Lib.can dest_univ
109
110(*---------------------------------------------------------------------------*)
111(* Infiniteness                                                              *)
112(*---------------------------------------------------------------------------*)
113
114fun mk_infinite tm =
115   boolSyntax.mk_neg (mk_finite tm)
116   handle HOL_ERR _ => raise ERR "mk_infinite" "not a set?"
117
118fun dest_infinite t =
119   let
120      val t' = boolSyntax.dest_neg t
121   in
122      dest_finite t'
123   end
124   handle HOL_ERR _ =>
125          raise ERR "dest_infinite" "not an application of INFINITE"
126
127val is_infinite = Lib.can dest_infinite
128
129(*---------------------------------------------------------------------------*)
130(* Finitely iterated insertion                                               *)
131(*---------------------------------------------------------------------------*)
132
133fun prim_mk_set (l, ty) =
134   itlist (curry mk_insert) l (mk_empty ty)
135   handle HOL_ERR _ => raise ERR "prim_mk_set" ""
136
137fun mk_set [] = raise ERR "mk_set" "empty set"
138  | mk_set (els as (h::_)) =
139      itlist (curry mk_insert) els (mk_empty (type_of h))
140      handle HOL_ERR _ => raise ERR "mk_set" ""
141
142val strip_set =
143   let
144      fun strip tm =
145         let
146            val (h, t) = dest_insert tm
147         in
148            h::strip t
149         end
150         handle HOL_ERR _ =>
151                if same_const tm empty_tm
152                   then []
153                else raise ERR "strip_set" "not an enumerated set"
154   in
155      strip
156   end
157
158(*---------------------------------------------------------------------------*)
159(* Set comprehensions                                                        *)
160(*---------------------------------------------------------------------------*)
161
162fun prim_mk_set_spec (tm1, tm2, sharedvars) =
163   let
164      val tuple = pairSyntax.list_mk_pair sharedvars
165   in
166      mk_comb (inst [alpha |-> type_of tm1, beta |-> type_of tuple] gspec_tm,
167               pairSyntax.mk_pabs (tuple, pairSyntax.mk_pair (tm1, tm2)))
168   end
169   handle HOL_ERR _ => raise ERR "prim_mk_set_spec" ""
170
171fun mk_set_spec (tm1, tm2) =
172   let
173      val shared = intersect (free_vars_lr tm1) (free_vars_lr tm2)
174   in
175      prim_mk_set_spec (tm1, tm2, shared)
176   end
177   handle e as HOL_ERR _ => raise wrap_exn "mk_set_spec" "" e
178
179fun dest_set_spec tm =
180   case total dest_comb tm of
181      SOME (c, M) =>
182         if same_const c gspec_tm
183            then pairSyntax.dest_pair (snd (pairSyntax.dest_pabs M))
184         else raise ERR "dest_set_spec" "not a set comprehension"
185    | NONE => raise ERR "dest_set_spec" "not a set comprehension"
186
187val is_set_spec = Lib.can dest_set_spec
188
189(*---------------------------------------------------------------------------*)
190(* Big union                                                                 *)
191(*---------------------------------------------------------------------------*)
192
193fun list_mk_bigunion sets = mk_bigunion (mk_set sets)
194fun strip_bigunion tm = strip_set (dest_bigunion tm)
195
196(*---------------------------------------------------------------------------*)
197(* Big intersection                                                          *)
198(*---------------------------------------------------------------------------*)
199
200fun list_mk_biginter sets = mk_biginter (mk_set sets)
201fun strip_biginter tm = strip_set (dest_biginter tm)
202
203end
204