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