60 (term list list * (string * typ) list list) * Proof.context |
60 (term list list * (string * typ) list list) * Proof.context |
61 val nonzero_string_of_int: int -> string |
61 val nonzero_string_of_int: int -> string |
62 |
62 |
63 val strip_typeN: int -> typ -> typ list * typ |
63 val strip_typeN: int -> typ -> typ list * typ |
64 |
64 |
|
65 val mk_predT: typ list -> typ |
|
66 val mk_pred1T: typ -> typ |
|
67 val mk_pred2T: typ -> typ -> typ |
65 val mk_optionT: typ -> typ |
68 val mk_optionT: typ -> typ |
66 val mk_relT: typ * typ -> typ |
69 val mk_relT: typ * typ -> typ |
67 val dest_relT: typ -> typ * typ |
70 val dest_relT: typ -> typ * typ |
68 val mk_sumT: typ * typ -> typ |
71 val mk_sumT: typ * typ -> typ |
69 |
72 |
120 val o_apply: thm |
123 val o_apply: thm |
121 val mk_sym: thm -> thm |
124 val mk_sym: thm -> thm |
122 val mk_trans: thm -> thm -> thm |
125 val mk_trans: thm -> thm -> thm |
123 val mk_unabs_def: int -> thm -> thm |
126 val mk_unabs_def: int -> thm -> thm |
124 |
127 |
|
128 val fold_defs: Proof.context -> thm list -> thm -> thm |
|
129 val unfold_defs: Proof.context -> thm list -> thm -> thm |
|
130 |
125 val mk_permute: ''a list -> ''a list -> 'b list -> 'b list |
131 val mk_permute: ''a list -> ''a list -> 'b list -> 'b list |
126 val find_indices: ''a list -> ''a list -> int list |
132 val find_indices: ''a list -> ''a list -> int list |
127 |
133 |
128 val certifyT: Proof.context -> typ -> ctyp |
134 val certifyT: Proof.context -> typ -> ctyp |
129 val certify: Proof.context -> term -> cterm |
135 val certify: Proof.context -> term -> cterm |
314 |
320 |
315 (** Types **) |
321 (** Types **) |
316 |
322 |
317 fun strip_typeN 0 T = ([], T) |
323 fun strip_typeN 0 T = ([], T) |
318 | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T |
324 | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T |
319 | strip_typeN n T = raise TYPE ("strip_typeN", [T], []); |
325 | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []); |
320 |
326 |
|
327 fun mk_predT Ts = Ts ---> HOLogic.boolT; |
|
328 fun mk_pred1T T = mk_predT [T]; |
|
329 fun mk_pred2T T U = mk_predT [T, U]; |
321 fun mk_optionT T = Type (@{type_name option}, [T]); |
330 fun mk_optionT T = Type (@{type_name option}, [T]); |
322 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; |
331 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; |
323 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; |
332 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; |
324 fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]); |
333 fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]); |
325 fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT; |
334 fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT; |