equal
deleted
inserted
replaced
30 |
30 |
31 val supp_ty: typ -> typ |
31 val supp_ty: typ -> typ |
32 val supp_const: typ -> term |
32 val supp_const: typ -> term |
33 val mk_supp_ty: typ -> term -> term |
33 val mk_supp_ty: typ -> term -> term |
34 val mk_supp: term -> term |
34 val mk_supp: term -> term |
|
35 |
|
36 val supports_const: typ -> term |
|
37 val mk_supports_ty: typ -> term -> term -> term |
|
38 val mk_supports: term -> term -> term |
35 |
39 |
36 val mk_equiv: thm -> thm |
40 val mk_equiv: thm -> thm |
37 val safe_mk_equiv: thm -> thm |
41 val safe_mk_equiv: thm -> thm |
38 |
42 |
39 val mk_diff: term * term -> term |
43 val mk_diff: term * term -> term |
41 val mk_union: term * term -> term |
45 val mk_union: term * term -> term |
42 val fold_union: term list -> term |
46 val fold_union: term list -> term |
43 val mk_conj: term * term -> term |
47 val mk_conj: term * term -> term |
44 val fold_conj: term list -> term |
48 val fold_conj: term list -> term |
45 |
49 |
|
50 (* fresh arguments for a term *) |
|
51 val fresh_args: Proof.context -> term -> term list |
|
52 |
46 (* datatype operations *) |
53 (* datatype operations *) |
47 type cns_info = (term * typ * typ list * bool list) list |
54 type cns_info = (term * typ * typ list * bool list) list |
48 |
55 |
49 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
56 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
50 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
57 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
112 fun supp_ty ty = ty --> @{typ "atom set"}; |
119 fun supp_ty ty = ty --> @{typ "atom set"}; |
113 fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty) |
120 fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty) |
114 fun mk_supp_ty ty t = supp_const ty $ t; |
121 fun mk_supp_ty ty t = supp_const ty $ t; |
115 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
122 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
116 |
123 |
|
124 fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool}); |
|
125 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; |
|
126 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; |
117 |
127 |
118 fun mk_equiv r = r RS @{thm eq_reflection}; |
128 fun mk_equiv r = r RS @{thm eq_reflection}; |
119 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
129 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
120 |
130 |
121 |
131 |
139 fun mk_conj (t1, @{term "True"}) = t1 |
149 fun mk_conj (t1, @{term "True"}) = t1 |
140 | mk_conj (@{term "True"}, t2) = t2 |
150 | mk_conj (@{term "True"}, t2) = t2 |
141 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
151 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
142 |
152 |
143 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
153 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
|
154 |
|
155 |
|
156 (* produces fresh arguments for a term *) |
|
157 |
|
158 fun fresh_args ctxt f = |
|
159 f |> fastype_of |
|
160 |> binder_types |
|
161 |> map (pair "z") |
|
162 |> Variable.variant_frees ctxt [f] |
|
163 |> map Free |
|
164 |
|
165 |
144 |
166 |
145 (** datatypes **) |
167 (** datatypes **) |
146 |
168 |
147 (* constructor infos *) |
169 (* constructor infos *) |
148 type cns_info = (term * typ * typ list * bool list) list |
170 type cns_info = (term * typ * typ list * bool list) list |