fold_proof_terms: canonical arguments;
authorwenzelm
Tue Jul 18 20:01:42 2006 +0200 (2006-07-18)
changeset 201477aa076a45cb4
parent 20146 d8cf6eb9baf9
child 20148 8a5fa86994c7
fold_proof_terms: canonical arguments;
removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue Jul 18 20:01:41 2006 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Jul 18 20:01:42 2006 +0200
     1.3 @@ -42,10 +42,7 @@
     1.4    val strip_thm : proof -> proof
     1.5    val map_proof_terms_option : (term -> term option) -> (typ -> typ option) -> proof -> proof
     1.6    val map_proof_terms : (term -> term) -> (typ -> typ) -> proof -> proof
     1.7 -  val fold_proof_terms : (term * 'a -> 'a) -> (typ * 'a -> 'a) -> 'a * proof -> 'a
     1.8 -  val add_prf_names : string list * proof -> string list
     1.9 -  val add_prf_tfree_names : string list * proof -> string list
    1.10 -  val add_prf_tvar_ixns : indexname list * proof -> indexname list
    1.11 +  val fold_proof_terms : (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
    1.12    val maxidx_of_proof : proof -> int
    1.13    val size_of_proof : proof -> int
    1.14    val change_type : typ list option -> proof -> proof
    1.15 @@ -299,24 +296,19 @@
    1.16     (fn t => SOME (same f t) handle SAME => NONE)
    1.17     (fn T => SOME (same g T) handle SAME => NONE);
    1.18  
    1.19 -fun fold_proof_terms f g (a, Abst (_, SOME T, prf)) = fold_proof_terms f g (g (T, a), prf)
    1.20 -  | fold_proof_terms f g (a, Abst (_, NONE, prf)) = fold_proof_terms f g (a, prf)
    1.21 -  | fold_proof_terms f g (a, AbsP (_, SOME t, prf)) = fold_proof_terms f g (f (t, a), prf)
    1.22 -  | fold_proof_terms f g (a, AbsP (_, NONE, prf)) = fold_proof_terms f g (a, prf)
    1.23 -  | fold_proof_terms f g (a, prf % SOME t) = f (t, fold_proof_terms f g (a, prf))
    1.24 -  | fold_proof_terms f g (a, prf % NONE) = fold_proof_terms f g (a, prf)
    1.25 -  | fold_proof_terms f g (a, prf1 %% prf2) = fold_proof_terms f g
    1.26 -      (fold_proof_terms f g (a, prf1), prf2)
    1.27 -  | fold_proof_terms _ g (a, PThm (_, _, _, SOME Ts)) = foldr g a Ts
    1.28 -  | fold_proof_terms _ g (a, PAxm (_, prop, SOME Ts)) = foldr g a Ts
    1.29 -  | fold_proof_terms _ _ (a, _) = a;
    1.30 +fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
    1.31 +  | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
    1.32 +  | fold_proof_terms f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f g prf
    1.33 +  | fold_proof_terms f g (AbsP (_, NONE, prf)) = fold_proof_terms f g prf
    1.34 +  | fold_proof_terms f g (prf % SOME t) = fold_proof_terms f g prf #> f t
    1.35 +  | fold_proof_terms f g (prf % NONE) = fold_proof_terms f g prf
    1.36 +  | fold_proof_terms f g (prf1 %% prf2) =
    1.37 +      fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
    1.38 +  | fold_proof_terms _ g (PThm (_, _, _, SOME Ts)) = fold g Ts  (* FIXME prop? *)
    1.39 +  | fold_proof_terms _ g (PAxm (_, prop, SOME Ts)) = fold g Ts  (* FIXME prop? *)
    1.40 +  | fold_proof_terms _ _ _ = I;
    1.41  
    1.42 -val add_prf_names = fold_proof_terms add_term_names ((uncurry K) o swap);
    1.43 -val add_prf_tfree_names = fold_proof_terms add_term_tfree_names add_typ_tfree_names;
    1.44 -val add_prf_tvar_ixns = fold_proof_terms add_term_tvar_ixns (add_typ_ixns o swap);
    1.45 -
    1.46 -fun maxidx_of_proof prf = fold_proof_terms
    1.47 -  (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); 
    1.48 +fun maxidx_of_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf ~1;
    1.49  
    1.50  fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
    1.51    | size_of_proof (AbsP (_, t, prf)) = 1 + size_of_proof prf
    1.52 @@ -509,7 +501,7 @@
    1.53    let
    1.54      val n = length args;
    1.55      fun subst (PBound i) Plev tlev =
    1.56 - 	 (if i < Plev then raise SAME    (*var is locally bound*)
    1.57 +         (if i < Plev then raise SAME    (*var is locally bound*)
    1.58            else incr_pboundvars Plev tlev (List.nth (args, i-Plev))
    1.59                   handle Subscript => PBound (i-n)  (*loose: change it*))
    1.60        | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
    1.61 @@ -559,13 +551,13 @@
    1.62  fun freeze_thaw_prf prf =
    1.63    let
    1.64      val (fs, Tfs, vs, Tvs) = fold_proof_terms
    1.65 -      (fn (t, (fs, Tfs, vs, Tvs)) =>
    1.66 +      (fn t => fn (fs, Tfs, vs, Tvs) =>
    1.67           (add_term_frees (t, fs), add_term_tfree_names (t, Tfs),
    1.68            add_term_vars (t, vs), add_term_tvar_ixns (t, Tvs)))
    1.69 -      (fn (T, (fs, Tfs, vs, Tvs)) =>
    1.70 +      (fn T => fn (fs, Tfs, vs, Tvs) =>
    1.71           (fs, add_typ_tfree_names (T, Tfs),
    1.72            vs, add_typ_ixns (Tvs, T)))
    1.73 -            (([], [], [], []), prf);
    1.74 +      prf ([], [], [], []);
    1.75      val fs' = map (fst o dest_Free) fs;
    1.76      val vs' = map (fst o dest_Var) vs;
    1.77      val names = vs' ~~ Name.variant_list fs' (map fst vs');
    1.78 @@ -715,9 +707,9 @@
    1.79            if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
    1.80  
    1.81      fun lift Us bs i j (Const ("==>", _) $ A $ B) =
    1.82 -	    AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
    1.83 +            AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
    1.84        | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
    1.85 -	    Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
    1.86 +            Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
    1.87        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
    1.88              map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
    1.89                (i + k - 1 downto i));
    1.90 @@ -993,9 +985,9 @@
    1.91            else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))),
    1.92              (ixn, t) :: insts)
    1.93        | (Free (a, T), Free (b, U)) =>
    1.94 -	  if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.95 +          if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.96        | (Const (a, T), Const (b, U))  =>
    1.97 -	  if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.98 +          if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.99        | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
   1.100        | (Bound i, Bound j) => if i=j then instsp else raise PMatch
   1.101        | _ => raise PMatch