34 val exists_const: typ -> term |
34 val exists_const: typ -> term |
35 val Collect_const: typ -> term |
35 val Collect_const: typ -> term |
36 val mk_eq: term * term -> term |
36 val mk_eq: term * term -> term |
37 val dest_eq: term -> term * term |
37 val dest_eq: term -> term * term |
38 val mk_all: string * typ * term -> term |
38 val mk_all: string * typ * term -> term |
|
39 val list_all: (string * typ) list * term -> term |
39 val mk_exists: string * typ * term -> term |
40 val mk_exists: string * typ * term -> term |
40 val mk_Collect: string * typ * term -> term |
41 val mk_Collect: string * typ * term -> term |
41 val mk_mem: term * term -> term |
42 val mk_mem: term * term -> term |
42 val dest_mem: term -> term * term |
43 val dest_mem: term -> term * term |
43 val mk_UNIV: typ -> term |
44 val mk_UNIV: typ -> term |
137 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs) |
138 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs) |
138 | dest_eq t = raise TERM ("dest_eq", [t]) |
139 | dest_eq t = raise TERM ("dest_eq", [t]) |
139 |
140 |
140 fun all_const T = Const ("All", [T --> boolT] ---> boolT); |
141 fun all_const T = Const ("All", [T --> boolT] ---> boolT); |
141 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P); |
142 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P); |
|
143 val list_all = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)); |
142 |
144 |
143 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT); |
145 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT); |
144 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P); |
146 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P); |
145 |
147 |
146 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T); |
148 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T); |