--- a/src/Doc/Isar_Ref/Generic.thy Mon Mar 30 11:36:30 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Mar 30 14:32:41 2015 +0200
@@ -301,9 +301,7 @@
@{rail \<open>
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
@@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
- ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
- ;
- dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') @{syntax for_fixes}
+ (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
;
@@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
;
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Mar 30 11:36:30 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Mar 30 14:32:41 2015 +0200
@@ -290,9 +290,8 @@
@{syntax_def prop}: @{syntax term}
\<close>}
- Positional instantiations are indicated by giving a sequence of
- terms, or the placeholder ``@{text _}'' (underscore), which means to
- skip a position.
+ Positional instantiations are specified as a sequence of terms, or the
+ placeholder ``@{text _}'' (underscore), which means to skip a position.
@{rail \<open>
@{syntax_def inst}: '_' | @{syntax term}
@@ -300,6 +299,19 @@
@{syntax_def insts}: (@{syntax inst} *)
\<close>}
+ Named instantiations are specified as pairs of assignments @{text "v =
+ t"}, which refer to schematic variables in some theorem that is
+ instantiated. Both type and terms instantiations are admitted, and
+ distinguished by the usual syntax of variable names.
+
+ @{rail \<open>
+ @{syntax_def named_inst}: variable '=' (type | term)
+ ;
+ @{syntax_def named_insts}: (named_inst @'and' +)
+ ;
+ variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}
+ \<close>}
+
Type declarations and definitions usually refer to @{syntax
typespec} on the left-hand side. This models basic type constructor
application at the outer syntax level. Note that only plain postfix
--- a/src/Doc/Isar_Ref/Proof.thy Mon Mar 30 11:36:30 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Mar 30 14:32:41 2015 +0200
@@ -740,9 +740,7 @@
;
@@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
;
- @@{attribute "where"}
- ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
- (@{syntax type} | @{syntax term}) * @'and') \<newline> @{syntax for_fixes}
+ @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}
\<close>}
\begin{description}
--- a/src/Pure/Tools/rule_insts.ML Mon Mar 30 11:36:30 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML Mon Mar 30 14:32:41 2015 +0200
@@ -104,16 +104,19 @@
val t' = Syntax.check_term ctxt' t;
in (t', ctxt') end;
-fun read_insts thm mixed_insts ctxt =
+fun read_insts thm raw_insts raw_fixes ctxt =
let
val (type_insts, term_insts) =
- List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
+ List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
- (*thm context*)
- val ctxt1 = Variable.declare_thm thm ctxt;
val tvars = Thm.fold_terms Term.add_tvars thm [];
val vars = Thm.fold_terms Term.add_vars thm [];
+ (*eigen-context*)
+ val ctxt1 = ctxt
+ |> Variable.declare_thm thm
+ |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+
(*explicit type instantiations*)
val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);
val vars1 = map (apsnd instT1) vars;
@@ -140,16 +143,15 @@
(** forward rules **)
-fun where_rule ctxt mixed_insts fixes thm =
+fun where_rule ctxt raw_insts raw_fixes thm =
let
- val ctxt' = ctxt |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
- val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt';
+ val ((inst_tvars, inst_vars), ctxt') = read_insts thm raw_insts raw_fixes 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;
@@ -173,12 +175,14 @@
(* where: named instantiation *)
+val parse_insts =
+ Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
+ -- Parse.for_fixes;
+
val _ = Theory.setup
(Attrib.setup @{binding "where"}
- (Scan.lift
- (Parse.and_list (Parse.position Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))
- -- Parse.for_fixes) >> (fn (insts, fixes) =>
- Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
+ (Scan.lift parse_insts >> (fn (insts, fixes) =>
+ Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
"named instantiation of theorem");
@@ -225,7 +229,7 @@
(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
-fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
+fun bires_inst_tac bires_flag ctxt raw_insts raw_fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
let
(* goal context *)
@@ -235,10 +239,7 @@
(* instantiation context *)
- val ((inst_tvars, inst_vars), inst_ctxt) = goal_ctxt
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
- |> read_insts thm mixed_insts;
-
+ val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm raw_insts raw_fixes goal_ctxt;
val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []);
@@ -309,10 +310,7 @@
fun method inst_tac tac =
Args.goal_spec --
- Scan.optional (Scan.lift
- (Parse.and_list1
- (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --
- Parse.for_fixes --| Args.$$$ "in")) ([], []) --
+ Scan.optional (Scan.lift (parse_insts --| Args.$$$ "in")) ([], []) --
Attrib.thms >>
(fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
if null insts andalso null fixes