src/Pure/drule.ML
changeset 14081 6c0f67e2f8d5
parent 13659 3cf622f6b0b2
child 14340 bc93ffa674cc
     1.1 --- a/src/Pure/drule.ML	Sun Jun 29 21:27:28 2003 +0200
     1.2 +++ b/src/Pure/drule.ML	Sun Jun 29 21:28:13 2003 +0200
     1.3 @@ -120,6 +120,8 @@
     1.4    val vars_of_terms: term list -> (indexname * typ) list
     1.5    val tvars_of: thm -> (indexname * sort) list
     1.6    val vars_of: thm -> (indexname * typ) list
     1.7 +  val rename_bvars: (string * string) list -> thm -> thm
     1.8 +  val rename_bvars': string option list -> thm -> thm
     1.9    val unvarifyT: thm -> thm
    1.10    val unvarify: thm -> thm
    1.11    val tvars_intr_list: string list -> thm -> thm * (string * indexname) list
    1.12 @@ -849,6 +851,44 @@
    1.13      end;
    1.14  
    1.15  
    1.16 +
    1.17 +(** renaming of bound variables **)
    1.18 +
    1.19 +(* replace bound variables x_i in thm by y_i *)
    1.20 +(* where vs = [(x_1, y_1), ..., (x_n, y_n)]  *)
    1.21 +
    1.22 +fun rename_bvars [] thm = thm
    1.23 +  | rename_bvars vs thm =
    1.24 +    let
    1.25 +      val {sign, prop, ...} = rep_thm thm;
    1.26 +      fun ren (Abs (x, T, t)) = Abs (if_none (assoc (vs, x)) x, T, ren t)
    1.27 +        | ren (t $ u) = ren t $ ren u
    1.28 +        | ren t = t;
    1.29 +    in equal_elim (reflexive (cterm_of sign (ren prop))) thm end;
    1.30 +
    1.31 +
    1.32 +(* renaming in left-to-right order *)
    1.33 +
    1.34 +fun rename_bvars' xs thm =
    1.35 +  let
    1.36 +    val {sign, prop, ...} = rep_thm thm;
    1.37 +    fun rename [] t = ([], t)
    1.38 +      | rename (x' :: xs) (Abs (x, T, t)) =
    1.39 +          let val (xs', t') = rename xs t
    1.40 +          in (xs', Abs (if_none x' x, T, t')) end
    1.41 +      | rename xs (t $ u) =
    1.42 +          let
    1.43 +            val (xs', t') = rename xs t;
    1.44 +            val (xs'', u') = rename xs' u
    1.45 +          in (xs'', t' $ u') end
    1.46 +      | rename xs t = (xs, t);
    1.47 +  in case rename xs prop of
    1.48 +      ([], prop') => equal_elim (reflexive (cterm_of sign prop')) thm
    1.49 +    | _ => error "More names than abstractions in theorem"
    1.50 +  end;
    1.51 +
    1.52 +
    1.53 +
    1.54  (* unvarify(T) *)
    1.55  
    1.56  (*assume thm in standard form, i.e. no frees, 0 var indexes*)