# HG changeset patch
# User wenzelm
# Date 1428503062 -7200
# Node ID bcccad156236076c11d462399f0ee1e1966c9829
# Parent  d69dc7a133e76c8109e3d1a136f727cfcfaacf5c
explicitly checked alpha conversion -- actual renaming happens outside kernel;

diff -r d69dc7a133e7 -r bcccad156236 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Apr 08 15:06:43 2015 +0200
+++ b/src/Pure/more_thm.ML	Wed Apr 08 16:24:22 2015 +0200
@@ -68,6 +68,8 @@
   val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
   val close_derivation: thm -> thm
+  val rename_params_rule: string list * int -> thm -> thm
+  val rename_boundvars: term -> term -> thm -> thm
   val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
   val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
@@ -392,6 +394,38 @@
   else thm;
 
 
+(* user renaming of parameters in a subgoal *)
+
+(*The names, if distinct, are used for the innermost parameters of subgoal i;
+  preceding parameters may be renamed to make all parameters distinct.*)
+fun rename_params_rule (names, i) st =
+  let
+    val (_, Bs, Bi, C) = Thm.dest_state (st, i);
+    val params = map #1 (Logic.strip_params Bi);
+    val short = length params - length names;
+    val names' =
+      if short < 0 then error "More names than parameters in subgoal!"
+      else Name.variant_list names (take short params) @ names;
+    val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
+    val Bi' = Logic.list_rename_params names' Bi;
+  in
+    (case duplicates (op =) names of
+      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); st)
+    | [] =>
+      (case inter (op =) names free_names of
+        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); st)
+      | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st))
+  end;
+
+
+(* preservation of bound variable names *)
+
+fun rename_boundvars pat obj th =
+  (case Term.rename_abs pat obj (Thm.prop_of th) of
+    NONE => th
+  | SOME prop' => Thm.renamed_prop prop' th);
+
+
 
 (** specification primitives **)
 
diff -r d69dc7a133e7 -r bcccad156236 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 08 15:06:43 2015 +0200
+++ b/src/Pure/thm.ML	Wed Apr 08 16:24:22 2015 +0200
@@ -34,6 +34,7 @@
   val maxidx_of_cterm: cterm -> int
   val global_cterm_of: theory -> term -> cterm
   val cterm_of: Proof.context -> term -> cterm
+  val renamed_term: term -> cterm -> cterm
   val dest_comb: cterm -> cterm * cterm
   val dest_fun: cterm -> cterm
   val dest_arg: cterm -> cterm
@@ -81,6 +82,7 @@
   val cprop_of: thm -> cterm
   val cprem_of: thm -> int -> cterm
   val transfer: theory -> thm -> thm
+  val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
@@ -125,14 +127,13 @@
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
+  val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
   val assumption: Proof.context option -> int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm
   val rotate_rule: int -> int -> thm -> thm
   val permute_prems: int -> int -> thm -> thm
-  val rename_params_rule: string list * int -> thm -> thm
-  val rename_boundvars: term -> term -> thm -> thm
   val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
     bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
@@ -195,6 +196,10 @@
 
 val cterm_of = global_cterm_of o Proof_Context.theory_of;
 
+fun renamed_term t' (Cterm {thy, t, T, maxidx, sorts}) =
+  if t aconv t' then Cterm {thy = thy, t = t', T = T, maxidx = maxidx, sorts = sorts}
+  else raise TERM ("renamed_term: terms disagree", [t, t']);
+
 fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) =
   Theory.merge (thy1, thy2);
 
@@ -416,6 +421,13 @@
         prop = prop})
   end;
 
+(*implicit alpha-conversion*)
+fun renamed_prop prop' (Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
+  if prop aconv prop' then
+    Thm (der, {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
+      hyps = hyps, tpairs = tpairs, prop = prop'})
+  else raise TERM ("renamed_prop: props disagree", [prop, prop']);
+
 fun make_context NONE thy = Context.Theory thy
   | make_context (SOME ctxt) thy =
       if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
@@ -1426,56 +1438,6 @@
   end;
 
 
-(** User renaming of parameters in a subgoal **)
-
-(*Calls error rather than raising an exception because it is intended
-  for top-level use -- exception handling would not make sense here.
-  The names in cs, if distinct, are used for the innermost parameters;
-  preceding parameters may be renamed to make all params distinct.*)
-fun rename_params_rule (cs, i) state =
-  let
-    val Thm (der, {thy, tags, maxidx, shyps, hyps, ...}) = state;
-    val (tpairs, Bs, Bi, C) = dest_state (state, i);
-    val iparams = map #1 (Logic.strip_params Bi);
-    val short = length iparams - length cs;
-    val newnames =
-      if short < 0 then error "More names than abstractions!"
-      else Name.variant_list cs (take short iparams) @ cs;
-    val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
-    val newBi = Logic.list_rename_params newnames Bi;
-  in
-    (case duplicates (op =) cs of
-      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
-    | [] =>
-      (case inter (op =) cs freenames of
-        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
-      | [] =>
-        Thm (der,
-         {thy = thy,
-          tags = tags,
-          maxidx = maxidx,
-          shyps = shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = Logic.list_implies (Bs @ [newBi], C)})))
-  end;
-
-
-(*** Preservation of bound variable names ***)
-
-fun rename_boundvars pat obj (thm as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
-  (case Term.rename_abs pat obj prop of
-    NONE => thm
-  | SOME prop' => Thm (der,
-      {thy = thy,
-       tags = tags,
-       maxidx = maxidx,
-       hyps = hyps,
-       shyps = shyps,
-       tpairs = tpairs,
-       prop = prop'}));
-
-
 (* strip_apply f B A strips off all assumptions/parameters from A
    introduced by lifting over B, and applies f to remaining part of A*)
 fun strip_apply f =