# HG changeset patch
# User wenzelm
# Date 1427717985 -7200
# Node ID 4039d8aecda44d841d4adb5afac8a004a093b80f
# Parent  f339ff48a6ee85dc4b3c94e87fb459824fe76134
more uniform syntax for named instantiations;

diff -r f339ff48a6ee -r 4039d8aecda4 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Mar 30 10:52:54 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Mar 30 14:19:45 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}
     ;
diff -r f339ff48a6ee -r 4039d8aecda4 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Mar 30 10:52:54 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Mar 30 14:19:45 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
diff -r f339ff48a6ee -r 4039d8aecda4 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Mon Mar 30 10:52:54 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Mar 30 14:19:45 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}
diff -r f339ff48a6ee -r 4039d8aecda4 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Mon Mar 30 10:52:54 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Mon Mar 30 14:19:45 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