'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;

--- a/NEWS	Sun Nov 20 17:32:27 2011 +0100
+++ b/NEWS	Sun Nov 20 17:44:41 2011 +0100
@@ -12,6 +12,12 @@
 the historic accident of dynamic re-evaluation in interpretations
 etc. was exploited.
 
+* Commands 'lemmas' and 'theorems' allow local variables using 'for'
+declaration, and results are standardized before being stored.  Thus
+old-style "standard" after instantiation or composition of facts
+becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
+indices of schematic variables.
+
 
 *** Pure ***
 

--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -1112,8 +1112,9 @@
   @{rail "
     @@{command axioms} (@{syntax axmdecl} @{syntax prop} +)
     ;
-    (@@{command lemmas} | @@{command theorems}) @{syntax target}?
+    (@@{command lemmas} | @@{command theorems}) @{syntax target}? \\
       (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+      (@'for' (@{syntax vars} + @'and'))?
   "}
 
   \begin{description}
@@ -1127,13 +1128,14 @@
   systems.  Everyday work is typically done the hard way, with proper
   definitions and proven theorems.
   
-  \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} retrieves and stores
-  existing facts in the theory context, or the specified target
-  context (see also \secref{sec:target}).  Typical applications would
-  also involve attributes, to declare Simplifier rules, for example.
-  
-  \item @{command "theorems"} is essentially the same as @{command
-  "lemmas"}, but marks the result as a different kind of facts.
+  \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def
+  "for"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"} evaluates given facts (with attributes) in
+  the current context, which may be augmented by local variables.
+  Results are standardized before being stored, i.e.\ schematic
+  variables are renamed to enforce index @{text "0"} uniformly.
+
+  \item @{command "theorems"} is the same as @{command "lemmas"}, but
+  marks the result as a different kind of facts.
 
   \end{description}
 *}

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 20 17:32:27 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 20 17:44:41 2011 +0100
@@ -1642,7 +1642,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{3}{}
+\rail@begin{6}{}
 \rail@bar
 \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[]
 \rail@nextbar{1}
@@ -1652,15 +1652,25 @@
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@plus
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextplus{2}
+\rail@nextplus{5}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
+\rail@bar
+\rail@nextbar{4}
+\rail@term{\isa{\isakeyword{for}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
+\rail@nextplus{5}
+\rail@cterm{\isa{\isakeyword{and}}}[]
+\rail@endplus
+\rail@endbar
 \rail@end
 \end{railoutput}
 
@@ -1676,12 +1686,13 @@
   systems.  Everyday work is typically done the hard way, with proper
   definitions and proven theorems.
   
-  \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} retrieves and stores
-  existing facts in the theory context, or the specified target
-  context (see also \secref{sec:target}).  Typical applications would
-  also involve attributes, to declare Simplifier rules, for example.
-  
-  \item \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts.
+  \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}~\indexdef{}{keyword}{for}\hypertarget{keyword.for}{\hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} evaluates given facts (with attributes) in
+  the current context, which may be augmented by local variables.
+  Results are standardized before being stored, i.e.\ schematic
+  variables are renamed to enforce index \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}} uniformly.
+
+  \item \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} is the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but
+  marks the result as a different kind of facts.
 
   \end{description}%
 \end{isamarkuptext}%

--- a/src/HOL/Auth/Guard/Extensions.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -455,7 +455,7 @@
 lemma knows_max_Cons: "knows_max A (ev#evs)
 = knows_max' A [ev] Un knows_max A evs"
 apply (simp add: knows_max_def del: knows_max'_def_Cons)
-apply (rule_tac evs1=evs in knows_max'_Cons_substI)
+apply (rule_tac evs=evs in knows_max'_Cons_substI)
 by blast
 
 lemmas knows_max_Cons_substI = knows_max_Cons [THEN ssubst]
@@ -619,6 +619,4 @@
 lemma used_sub_parts_used: "X:used (ev # evs) ==> X:parts {msg ev} Un used evs"
 by (induct ev, auto)
 
-
-
 end

--- a/src/HOL/Auth/Guard/Guard.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -202,7 +202,7 @@
 
 lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
-apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI)
+apply (erule_tac l=l and x=x in mem_cnb_minus_substI)
 apply simp
 done
 
@@ -299,7 +299,7 @@
 
 lemma Guard_invKey_keyset: "[| Nonce n:analz (G Un H); Guard n Ks G; finite G;
 keyset H |] ==> EX K. K:Ks & Key K:analz (G Un H)"
-apply (frule_tac P="%G. Nonce n:G" and G2=G in analz_keyset_substD, simp_all)
+apply (frule_tac P="%G. Nonce n:G" and G=G in analz_keyset_substD, simp_all)
 apply (drule_tac G="G Un (H Int keysfor G)" in Guard_invKey_finite)
 by (auto simp: Guard_def intro: analz_sub)
 

--- a/src/HOL/Auth/Guard/GuardK.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -198,7 +198,7 @@
 
 lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
-by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
+by (erule_tac l=l and x=x in mem_cnb_minus_substI, simp)
 
 lemma parts_cnb: "Z:parts (set l) ==>
 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -293,7 +293,7 @@
 
 lemma GuardK_invKey_keyset: "[| Key n:analz (G Un H); GuardK n Ks G; finite G;
 keyset H; Key n ~:H |] ==> EX K. K:Ks & Key K:analz (G Un H)"
-apply (frule_tac P="%G. Key n:G" and G2=G in analz_keyset_substD, simp_all)
+apply (frule_tac P="%G. Key n:G" and G=G in analz_keyset_substD, simp_all)
 apply (drule_tac G="G Un (H Int keysfor G)" in GuardK_invKey_finite)
 apply (auto simp: GuardK_def intro: analz_sub)
 by (drule keyset_in, auto)

--- a/src/HOL/Deriv.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/HOL/Deriv.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -586,7 +586,7 @@
                 (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
          a \<le> b |]
       ==> P(a,b)"
-apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
+apply (rule Bolzano_nest_unique [where P=P, THEN exE], assumption+)
 apply (rule tendsto_minus_cancel)
 apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
 apply (rule ccontr)

--- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -1004,7 +1004,7 @@
                    {s. h \<le> (giv o sub i o client) s &
                        h pfixGe (ask o sub i o client) s}"
   apply (rule single_LeadsTo_I)
-  apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s"
+  apply (rule_tac k1 = h and x1 = "(sub i o allocAsk) s"
          in System_lemma2 [THEN LeadsTo_weaken])
   apply auto
   apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe)

--- a/src/HOL/UNITY/Comp/Priority.thy	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy	Sun Nov 20 17:44:41 2011 +0100
@@ -213,7 +213,7 @@
                leadsTo {s. above i s < x}"
 apply (rule leadsTo_UN)
 apply (rule single_leadsTo_I, clarify)
-apply (rule_tac x2 = "above i x" in above_decreases_lemma)
+apply (rule_tac x = "above i x" in above_decreases_lemma)
 apply (simp_all (no_asm_use) add: Highest_iff_above0)
 apply blast+
 done

--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 20 17:44:41 2011 +0100
@@ -257,7 +257,8 @@
 (* theorems *)
 
 fun theorems kind =
-  Parse_Spec.name_facts >> (fn args => #2 oo Specification.theorems_cmd kind args);
+  Parse_Spec.name_facts -- Parse.for_fixes
+    >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
 
 val _ =
   Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
@@ -267,8 +268,9 @@
 
 val _ =
   Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl
-    (Parse.and_list1 Parse_Spec.xthms1
-      >> (fn args => #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
+    (Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
+      >> (fn (facts, fixes) =>
+          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
 
 
 (* name space entry path *)

--- a/src/Pure/Isar/specification.ML	Sun Nov 20 17:32:27 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Nov 20 17:44:41 2011 +0100
@@ -52,9 +52,11 @@
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    (binding * typ option * mixfix) list ->
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorems_cmd: string ->
     (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
+    (binding * string option * mixfix) list ->
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
@@ -283,18 +285,30 @@
 
 (* fact statements *)
 
-fun gen_theorems prep_fact prep_att kind raw_facts int lthy =
+local
+
+fun gen_theorems prep_fact prep_att prep_vars
+    kind raw_facts raw_fixes int lthy =
   let
     val attrib = prep_att (Proof_Context.theory_of lthy);
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
-    val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts;
+    val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
+
+    val facts' = facts
+      |> Attrib.partial_evaluation ctxt'
+      |> Element.facts_map (Element.transform_ctxt (Proof_Context.export_morphism ctxt' lthy));
+    val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   in (res, lthy') end;
 
-val theorems = gen_theorems (K I) (K I);
-val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src;
+in
+
+val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src Proof_Context.read_vars;
+
+end;
 
 
 (* complex goal statements *)