src/Pure/proofterm.ML
changeset 36621 2fd4e2c76636
parent 36620 e6bb250402b5
child 36732 9c2ee10809b2
     1.1 --- a/src/Pure/proofterm.ML	Tue May 04 12:30:15 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue May 04 14:38:59 2010 +0200
     1.3 @@ -108,6 +108,8 @@
     1.4    val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
     1.5    val equal_intr: term -> term -> proof -> proof -> proof
     1.6    val equal_elim: term -> term -> proof -> proof -> proof
     1.7 +  val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     1.8 +    sort list -> proof -> proof
     1.9    val axm_proof: string -> term -> proof
    1.10    val oracle_proof: string -> term -> oracle * proof
    1.11    val promise_proof: theory -> serial -> term -> proof
    1.12 @@ -884,6 +886,22 @@
    1.13    equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
    1.14  
    1.15  
    1.16 +(**** sort hypotheses ****)
    1.17 +
    1.18 +fun strip_shyps_proof algebra present witnessed extra_sorts prf =
    1.19 +  let
    1.20 +    fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
    1.21 +    val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
    1.22 +    val replacements = present @ extra @ witnessed;
    1.23 +    fun replace T =
    1.24 +      if exists (fn (T', _) => T' = T) present then raise Same.SAME
    1.25 +      else
    1.26 +        (case get_first (get (Type.sort_of_atyp T)) replacements of
    1.27 +          SOME T' => T'
    1.28 +        | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
    1.29 +  in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
    1.30 +
    1.31 +
    1.32  (***** axioms and theorems *****)
    1.33  
    1.34  val proofs = Unsynchronized.ref 2;