src/Pure/drule.ML
changeset 6435 154b88d2b62e
parent 6390 5d58c100ca3f
child 6930 4b40fb299f9f
     1.1 --- a/src/Pure/drule.ML	Thu Apr 15 18:10:49 1999 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri Apr 16 14:42:44 1999 +0200
     1.3 @@ -74,6 +74,8 @@
     1.4    val swap_prems_rl     : thm
     1.5    val equal_intr_rule   : thm
     1.6    val instantiate'	: ctyp option list -> cterm option list -> thm -> thm
     1.7 +  val incr_indexes	: int -> thm -> thm
     1.8 +  val incr_indexes_wrt	: int list -> ctyp list -> cterm list -> thm list -> thm -> thm
     1.9  end;
    1.10  
    1.11  signature DRULE =
    1.12 @@ -669,6 +671,27 @@
    1.13    in instantiate' [] frees thm end;
    1.14  
    1.15  
    1.16 +(* increment var indexes *)
    1.17 +
    1.18 +fun incr_indexes 0 thm = thm
    1.19 +  | incr_indexes inc thm =
    1.20 +      let
    1.21 +        val sign = Thm.sign_of_thm thm;
    1.22 +
    1.23 +        fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
    1.24 +        fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
    1.25 +      in instantiate' (map inc_tvar (tvars_of thm)) (map inc_var (vars_of thm)) thm end;
    1.26 +
    1.27 +fun incr_indexes_wrt is cTs cts thms =
    1.28 +  let
    1.29 +    val maxidx =
    1.30 +      foldl Int.max (~1, is @
    1.31 +        map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @
    1.32 +        map (#maxidx o Thm.rep_cterm) cts @
    1.33 +        map (#maxidx o Thm.rep_thm) thms);
    1.34 +  in incr_indexes (maxidx + 1) end;
    1.35 +
    1.36 +
    1.37  (* mk_triv_goal *)
    1.38  
    1.39  (*make an initial proof state, "PROP A ==> (PROP A)" *)