--- a/NEWS Tue Mar 24 11:53:18 2015 +0100
+++ b/NEWS Tue Mar 24 15:57:51 2015 +0100
@@ -66,6 +66,10 @@
these variables become schematic in the instantiated theorem. This
behaviour is analogous to 'for' in attributes "where" and "of".
+* Explicit instantiation via attributes "where", "of", and proof methods
+"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
+("_") that stand for anonymous local variables.
+
* Command "class_deps" takes optional sort arguments constraining
the search space.
--- a/src/Pure/Tools/rule_insts.ML Tue Mar 24 11:53:18 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Tue Mar 24 15:57:51 2015 +0100
@@ -68,18 +68,18 @@
else error_var "Bad sort for instantiation of type variable: " (xi, pos)
end;
-fun read_terms ctxt ss Ts =
+fun read_terms ss Ts ctxt =
let
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
- val ts = map2 parse Ts ss;
+ val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt;
val ts' =
map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
- |> Syntax.check_terms ctxt
- |> Variable.polymorphic ctxt;
+ |> Syntax.check_terms ctxt'
+ |> Variable.polymorphic ctxt';
val Ts' = map Term.fastype_of ts';
val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
- in (ts', tyenv') end;
+ in ((ts', tyenv'), ctxt') end;
fun make_instT f v =
let
@@ -95,7 +95,7 @@
in
-fun read_insts ctxt mixed_insts thm =
+fun read_insts thm mixed_insts ctxt =
let
val (type_insts, term_insts) =
List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
@@ -110,7 +110,7 @@
(*term instantiations*)
val (xs, ss) = split_list term_insts;
val Ts = map (the_type vars1) xs;
- val (ts, inferred) = read_terms ctxt ss Ts;
+ val ((ts, inferred), ctxt') = read_terms ss Ts ctxt;
(*implicit type instantiations*)
val instT2 = Term_Subst.instantiateT inferred;
@@ -121,7 +121,7 @@
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
val inst_vars = map_filter (make_inst inst2) vars2;
- in (inst_tvars, inst_vars) end;
+ in ((inst_tvars, inst_vars), ctxt') end;
end;
@@ -134,13 +134,13 @@
val ctxt' = ctxt
|> Variable.declare_thm thm
|> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
- val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm;
+ val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt';
in
thm
|> Drule.instantiate_normalize
- (map (apply2 (Thm.ctyp_of ctxt) o apfst TVar) inst_tvars,
- map (apply2 (Thm.cterm_of ctxt) o apfst Var) inst_vars)
- |> singleton (Variable.export ctxt' ctxt)
+ (map (apply2 (Thm.ctyp_of ctxt'') o apfst TVar) inst_tvars,
+ map (apply2 (Thm.cterm_of ctxt'') o apfst Var) inst_vars)
+ |> singleton (Variable.export ctxt'' ctxt)
|> Rule_Cases.save thm
end;
@@ -225,7 +225,7 @@
val (fixed, fixes_ctxt) = param_ctxt
|> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes;
- val (inst_tvars, inst_vars) = read_insts fixes_ctxt mixed_insts thm;
+ val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
(* lift and instantiate rule *)
@@ -238,14 +238,14 @@
(Logic.incr_indexes (fixed, paramTs, inc) t);
val inst_tvars' = inst_tvars
- |> map (apply2 (Thm.ctyp_of fixes_ctxt o Logic.incr_tvar inc) o apfst TVar);
+ |> map (apply2 (Thm.ctyp_of inst_ctxt o Logic.incr_tvar inc) o apfst TVar);
val inst_vars' = inst_vars
- |> map (fn (v, t) => apply2 (Thm.cterm_of fixes_ctxt) (lift_var v, lift_term t));
+ |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
val thm' =
Drule.instantiate_normalize (inst_tvars', inst_vars')
(Thm.lift_rule cgoal thm)
- |> singleton (Variable.export fixes_ctxt param_ctxt);
+ |> singleton (Variable.export inst_ctxt param_ctxt);
in
compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
end) i st;
--- a/src/Pure/variable.ML Tue Mar 24 11:53:18 2015 +0100
+++ b/src/Pure/variable.ML Tue Mar 24 15:57:51 2015 +0100
@@ -52,15 +52,16 @@
val add_fixes: string list -> Proof.context -> string list * Proof.context
val add_fixes_direct: string list -> Proof.context -> Proof.context
val auto_fixes: term -> Proof.context -> Proof.context
+ val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
val variant_fixes: string list -> Proof.context -> string list * Proof.context
val dest_fixes: Proof.context -> (string * string) list
- val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
val export_terms: Proof.context -> Proof.context -> term list -> term list
val exportT_terms: Proof.context -> Proof.context -> term list -> term list
val exportT: Proof.context -> Proof.context -> thm list -> thm list
val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
+ val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
val import_inst: bool -> term list -> Proof.context ->
(((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
@@ -460,11 +461,21 @@
|> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []))
|> declare_term t;
-fun invent_types Ss ctxt =
- let
- val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
- val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
- in (tfrees, ctxt') end;
+
+(* dummy patterns *)
+
+fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt =
+ let val ([x], ctxt') = add_fixes [Name.uu_] ctxt
+ in (Free (x, T), ctxt') end
+ | fix_dummy_patterns (Abs (x, T, b)) ctxt =
+ let val (b', ctxt') = fix_dummy_patterns b ctxt
+ in (Abs (x, T, b'), ctxt') end
+ | fix_dummy_patterns (t $ u) ctxt =
+ let
+ val (t', ctxt') = fix_dummy_patterns t ctxt;
+ val (u', ctxt'') = fix_dummy_patterns u ctxt';
+ in (t' $ u', ctxt'') end
+ | fix_dummy_patterns a ctxt = (a, ctxt);
@@ -541,6 +552,12 @@
(** import -- fix schematic type/term variables **)
+fun invent_types Ss ctxt =
+ let
+ val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
+ val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
+ in (tfrees, ctxt') end;
+
fun importT_inst ts ctxt =
let
val tvars = rev (fold Term.add_tvars ts []);