--- 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 **)
--- 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 =