# HG changeset patch # User wenzelm # Date 1321807481 -3600 # Node ID 1bbbac9a0cb03f777f837f0ca8db23fae9fcfe5d # Parent 5292435af7cf00d7f9521b82e6682239fc28a023 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing; diff -r 5292435af7cf -r 1bbbac9a0cb0 NEWS --- 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 *** diff -r 5292435af7cf -r 1bbbac9a0cb0 doc-src/IsarRef/Thy/Spec.thy --- 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 \ 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 \ b\<^sub>n"}~@{keyword_def + "for"}~@{text "x\<^sub>1 \ 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} *} diff -r 5292435af7cf -r 1bbbac9a0cb0 doc-src/IsarRef/Thy/document/Spec.tex --- 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}% diff -r 5292435af7cf -r 1bbbac9a0cb0 src/HOL/Auth/Guard/Extensions.thy --- 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 diff -r 5292435af7cf -r 1bbbac9a0cb0 src/HOL/Auth/Guard/Guard.thy --- 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 \ 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) diff -r 5292435af7cf -r 1bbbac9a0cb0 src/HOL/Auth/Guard/GuardK.thy --- 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 \ 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) diff -r 5292435af7cf -r 1bbbac9a0cb0 src/HOL/Deriv.thy --- 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 @@ (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)); a \ 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) diff -r 5292435af7cf -r 1bbbac9a0cb0 src/HOL/UNITY/Comp/Alloc.thy --- 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 \ (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) diff -r 5292435af7cf -r 1bbbac9a0cb0 src/HOL/UNITY/Comp/Priority.thy --- 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 diff -r 5292435af7cf -r 1bbbac9a0cb0 src/Pure/Isar/isar_syn.ML --- 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 *) diff -r 5292435af7cf -r 1bbbac9a0cb0 src/Pure/Isar/specification.ML --- 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 *)