45 val fold_proof_terms : (term * 'a -> 'a) -> (typ * 'a -> 'a) -> 'a * proof -> 'a |
45 val fold_proof_terms : (term * 'a -> 'a) -> (typ * 'a -> 'a) -> 'a * proof -> 'a |
46 val add_prf_names : string list * proof -> string list |
46 val add_prf_names : string list * proof -> string list |
47 val add_prf_tfree_names : string list * proof -> string list |
47 val add_prf_tfree_names : string list * proof -> string list |
48 val add_prf_tvar_ixns : indexname list * proof -> indexname list |
48 val add_prf_tvar_ixns : indexname list * proof -> indexname list |
49 val maxidx_of_proof : proof -> int |
49 val maxidx_of_proof : proof -> int |
|
50 val size_of_proof : proof -> int |
50 val change_type : typ list option -> proof -> proof |
51 val change_type : typ list option -> proof -> proof |
51 val prf_abstract_over : term -> proof -> proof |
52 val prf_abstract_over : term -> proof -> proof |
52 val prf_incr_bv : int -> int -> int -> int -> proof -> proof |
53 val prf_incr_bv : int -> int -> int -> int -> proof -> proof |
53 val incr_pboundvars : int -> int -> proof -> proof |
54 val incr_pboundvars : int -> int -> proof -> proof |
54 val prf_loose_bvar1 : proof -> int -> bool |
55 val prf_loose_bvar1 : proof -> int -> bool |
268 val add_prf_tfree_names = fold_proof_terms add_term_tfree_names add_typ_tfree_names; |
269 val add_prf_tfree_names = fold_proof_terms add_term_tfree_names add_typ_tfree_names; |
269 val add_prf_tvar_ixns = fold_proof_terms add_term_tvar_ixns (add_typ_ixns o swap); |
270 val add_prf_tvar_ixns = fold_proof_terms add_term_tvar_ixns (add_typ_ixns o swap); |
270 |
271 |
271 fun maxidx_of_proof prf = fold_proof_terms |
272 fun maxidx_of_proof prf = fold_proof_terms |
272 (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); |
273 (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); |
|
274 |
|
275 fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf |
|
276 | size_of_proof (AbsP (_, t, prf)) = |
|
277 if_none (apsome size_of_term t) 1 + size_of_proof prf |
|
278 | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 |
|
279 | size_of_proof (prf % t) = |
|
280 if_none (apsome size_of_term t) 1 + size_of_proof prf |
|
281 | size_of_proof _ = 1; |
273 |
282 |
274 fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs) |
283 fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs) |
275 | change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) |
284 | change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) |
276 | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) |
285 | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) |
277 | change_type _ prf = prf; |
286 | change_type _ prf = prf; |