src/Pure/proofterm.ML
changeset 36620 e6bb250402b5
parent 36619 deadcd0ec431
child 36621 2fd4e2c76636
     1.1 --- a/src/Pure/proofterm.ML	Tue May 04 11:02:50 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue May 04 12:30:15 2010 +0200
     1.3 @@ -58,8 +58,10 @@
     1.4    val strip_combt: proof -> proof * term option list
     1.5    val strip_combP: proof -> proof * proof list
     1.6    val strip_thm: proof_body -> proof_body
     1.7 -  val map_proof_terms_option: (term -> term option) -> (typ -> typ option) -> proof -> proof
     1.8 +  val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
     1.9 +  val map_proof_types_same: typ Same.operation -> proof Same.operation
    1.10    val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
    1.11 +  val map_proof_types: (typ -> typ) -> proof -> proof
    1.12    val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
    1.13    val maxidx_proof: proof -> int -> int
    1.14    val size_of_proof: proof -> int
    1.15 @@ -273,10 +275,8 @@
    1.16  val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
    1.17  fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
    1.18  
    1.19 -fun map_proof_terms_option f g =
    1.20 +fun map_proof_same term typ ofclass =
    1.21    let
    1.22 -    val term = Same.function f;
    1.23 -    val typ = Same.function g;
    1.24      val typs = Same.map typ;
    1.25  
    1.26      fun proof (Abst (s, T, prf)) =
    1.27 @@ -292,22 +292,23 @@
    1.28            (proof prf1 %% Same.commit proof prf2
    1.29              handle Same.SAME => prf1 %% proof prf2)
    1.30        | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
    1.31 -      | proof (OfClass (T, c)) = OfClass (typ T, c)
    1.32 +      | proof (OfClass T_c) = ofclass T_c
    1.33        | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
    1.34        | proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
    1.35        | proof (PThm (i, ((a, prop, SOME Ts), body))) =
    1.36            PThm (i, ((a, prop, SOME (typs Ts)), body))
    1.37        | proof _ = raise Same.SAME;
    1.38 -  in Same.commit proof end;
    1.39 +  in proof end;
    1.40 +
    1.41 +fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
    1.42 +fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
    1.43  
    1.44  fun same eq f x =
    1.45    let val x' = f x
    1.46    in if eq (x, x') then raise Same.SAME else x' end;
    1.47  
    1.48 -fun map_proof_terms f g =
    1.49 -  map_proof_terms_option
    1.50 -   (fn t => SOME (same (op =) f t) handle Same.SAME => NONE)
    1.51 -   (fn T => SOME (same (op =) g T) handle Same.SAME => NONE);
    1.52 +fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
    1.53 +fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
    1.54  
    1.55  fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
    1.56    | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
    1.57 @@ -696,17 +697,17 @@
    1.58  (***** generalization *****)
    1.59  
    1.60  fun generalize (tfrees, frees) idx =
    1.61 -  map_proof_terms_option
    1.62 -    (Term_Subst.generalize_option (tfrees, frees) idx)
    1.63 -    (Term_Subst.generalizeT_option tfrees idx);
    1.64 +  Same.commit (map_proof_terms_same
    1.65 +    (Term_Subst.generalize_same (tfrees, frees) idx)
    1.66 +    (Term_Subst.generalizeT_same tfrees idx));
    1.67  
    1.68  
    1.69  (***** instantiation *****)
    1.70  
    1.71  fun instantiate (instT, inst) =
    1.72 -  map_proof_terms_option
    1.73 -    (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
    1.74 -    (Term_Subst.instantiateT_option instT);
    1.75 +  Same.commit (map_proof_terms_same
    1.76 +    (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
    1.77 +    (Term_Subst.instantiateT_same instT));
    1.78  
    1.79  
    1.80  (***** lifting *****)
    1.81 @@ -757,9 +758,8 @@
    1.82    end;
    1.83  
    1.84  fun incr_indexes i =
    1.85 -  map_proof_terms_option
    1.86 -    (Same.capture (Logic.incr_indexes_same ([], i)))
    1.87 -    (Same.capture (Logic.incr_tvar_same i));
    1.88 +  Same.commit (map_proof_terms_same
    1.89 +    (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
    1.90  
    1.91  
    1.92  (***** proof by assumption *****)