src/Pure/proofterm.ML
changeset 13744 2241191a3c54
parent 13662 1f8ddc4b371e
child 13749 6844c38d74df
     1.1 --- a/src/Pure/proofterm.ML	Mon Dec 09 10:38:56 2002 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Tue Dec 10 10:40:32 2002 +0100
     1.3 @@ -47,6 +47,7 @@
     1.4    val add_prf_tfree_names : string list * proof -> string list
     1.5    val add_prf_tvar_ixns : indexname list * proof -> indexname list
     1.6    val maxidx_of_proof : proof -> int
     1.7 +  val size_of_proof : proof -> int
     1.8    val change_type : typ list option -> proof -> proof
     1.9    val prf_abstract_over : term -> proof -> proof
    1.10    val prf_incr_bv : int -> int -> int -> int -> proof -> proof
    1.11 @@ -271,6 +272,14 @@
    1.12  fun maxidx_of_proof prf = fold_proof_terms
    1.13    (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); 
    1.14  
    1.15 +fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
    1.16 +  | size_of_proof (AbsP (_, t, prf)) =
    1.17 +      if_none (apsome size_of_term t) 1 + size_of_proof prf
    1.18 +  | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
    1.19 +  | size_of_proof (prf % t) =
    1.20 +      if_none (apsome size_of_term t) 1 + size_of_proof prf
    1.21 +  | size_of_proof _ = 1;
    1.22 +
    1.23  fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs)
    1.24    | change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
    1.25    | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)