# HG changeset patch # User ballarin # Date 1113809123 -7200 # Node ID b901a127ac73c829397aa70d6f08592cc06f82d6 # Parent 13d1ec61bc891983d8a1fb48ec6e3d57ecd16eea Interpretation supports statically scoped attributes; documentation. diff -r 13d1ec61bc89 -r b901a127ac73 NEWS --- a/NEWS Sun Apr 17 19:40:43 2005 +0200 +++ b/NEWS Mon Apr 18 09:25:23 2005 +0200 @@ -163,6 +163,7 @@ do not occur in proof obligations, neither are instantiated theorems stored in duplicate. Use print_interps to inspect active interpretations of a particular locale. + For details, see the Isar Reference manual. * Locales: proper static binding of attribute syntax -- i.e. types / terms / facts mentioned as arguments are always those of the locale diff -r 13d1ec61bc89 -r b901a127ac73 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Sun Apr 17 19:40:43 2005 +0200 +++ b/doc-src/IsarRef/generic.tex Mon Apr 18 09:25:23 2005 +0200 @@ -180,7 +180,7 @@ specifications included here, e.g.\ a local $simp$ rule. \item [$\INCLUDES{c}$] copies the specified context in a statically scoped - manner. + manner. Only available in the long goal format of \S\ref{sec:goals}. In contrast, the initial $import$ specification of a locale expression maintains a dynamic relation to the locales being referenced (benefiting @@ -224,6 +224,79 @@ \end{descr} +\subsubsection{Interpretation of locales} + +Locale expressions (more precisely, \emph{context expressions}) may be +instantiated, and the instantiated facts added to the current context. +This requires a proof of the instantiated specification and is called +\emph{locale interpretation}. Interpretation is possible in theories +($\isarcmd{interpretation}$) and proof contexts +($\isarcmd{interpret}$). + +\indexisarcmd{interpretation}\indexisarcmd{interpret} +\indexisarcmd{print-interps} +\begin{matharray}{rcl} + \isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\ + \isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + \isarcmd{print_interps}^* & : & \isarkeep{theory~|~proof} \\ +\end{matharray} + +\indexouternonterm{interp} + +\railalias{printinterps}{print\_interps} +\railterm{printinterps} + +\begin{rail} + 'interpretation' interp + ; + 'interpret' interp + ; + printinterps name + ; + interp: thmdecl? contextexpr ('[' (inst+) ']')? + ; +\end{rail} + +\begin{descr} + +\item [$\isarcmd{interpretation}~expr~insts$] + interprets $expr$ in the theory. The instantiation is positional. + All parameters must receive an instantiation term --- with the + exception of defined parameters. These are, if omitted, derived + from the defining equation and other instantiations. Use ``\_'' to + omit an instantiation term. Free variables are automatically + generalized. + + The context expression may be preceded by a name and/or attributes. + These take effect in the post-processing of facts. The name is used + to prefix fact names, for example to avoid accidental hiding of + other facts. Attributes are applied after attributes of the + interpreted facts. + + The command is aware of interpretations already active in the + theory. No proof obligations are generated for those, neither is + post-processing applied to their facts. This avoids duplication of + interpreted facts, in particular. Note that, in the case of a + locale with import, parts of the interpretation may already be + active. The command will only generate proof obligations and add + facts for new parts. + + Adding facts to locales has the + effect of adding interpreted facts to the theory for all active + interpretations also. + +\item [$\isarcmd{interpret}~expr~insts$] + interprets $expr$ in the proof context and is otherwise similar to + the previous command. Free variables in instantiations are not + generalized, however. + +\item [$\isarcmd{print_interps}~loc$] + prints the interpretations of a particular locale $loc$ that are + active in the current context, either theory or proof context. + +\end{descr} + + \section{Derived proof schemes} \subsection{Generalized elimination}\label{sec:obtain} diff -r 13d1ec61bc89 -r b901a127ac73 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Sun Apr 17 19:40:43 2005 +0200 +++ b/src/FOL/ex/LocaleTest.thy Mon Apr 18 09:25:23 2005 +0200 @@ -53,14 +53,12 @@ interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro) - (* both X and Y get type 'b since 'b is the internal type of parameter b, - not wanted, but put up with for now. *) print_interps A (* possible accesses *) thm p1.a.asm_A thm LocaleTest.p1.a.asm_A -thm LocaleTest.asm_A thm p1.asm_A +thm p1.asm_A thm LocaleTest.p1.asm_A (* without prefix *) diff -r 13d1ec61bc89 -r b901a127ac73 src/HOL/Algebra/CRing.thy --- a/src/HOL/Algebra/CRing.thy Sun Apr 17 19:40:43 2005 +0200 +++ b/src/HOL/Algebra/CRing.thy Mon Apr 18 09:25:23 2005 +0200 @@ -574,28 +574,10 @@ locale ring_hom_cring = cring R + cring S + var h + assumes homh [simp, intro]: "h \ ring_hom R S" -(* notes hom_closed [simp, intro] = ring_hom_closed [OF homh] and hom_mult [simp] = ring_hom_mult [OF homh] and hom_add [simp] = ring_hom_add [OF homh] and hom_one [simp] = ring_hom_one [OF homh] -*) - -lemma (in ring_hom_cring) hom_closed [simp, intro]: - "x \ carrier R ==> h x \ carrier S" - by (simp add: ring_hom_closed [OF homh]) - -lemma (in ring_hom_cring) hom_mult [simp]: - "[| x \ carrier R; y \ carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" - by (simp add: ring_hom_mult [OF homh]) - -lemma (in ring_hom_cring) hom_add [simp]: - "[| x \ carrier R; y \ carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" - by (simp add: ring_hom_add [OF homh]) - -lemma (in ring_hom_cring) hom_one [simp]: - "h \ = \\<^bsub>S\<^esub>" - by (simp add: ring_hom_one [OF homh]) lemma (in ring_hom_cring) hom_zero [simp]: "h \ = \\<^bsub>S\<^esub>" diff -r 13d1ec61bc89 -r b901a127ac73 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Sun Apr 17 19:40:43 2005 +0200 +++ b/src/HOL/Algebra/Group.thy Mon Apr 18 09:25:23 2005 +0200 @@ -470,8 +470,8 @@ done text{*This alternative proof of the previous result demonstrates interpret. - It uses @{text Prod.inv_equality} (available after instantiation) instead of - @{text "group.inv_equality [OF DirProd_group]"}. *} + It uses @{text Prod.inv_equality} (available after @{text interpret}) + instead of @{text "group.inv_equality [OF DirProd_group]"}. *} lemma includes group G + group H assumes g: "g \ carrier G" @@ -542,19 +542,8 @@ @{term H}, with a homomorphism @{term h} between them*} locale group_hom = group G + group H + var h + assumes homh: "h \ hom G H" -(* notes hom_mult [simp] = hom_mult [OF homh] and hom_closed [simp] = hom_closed [OF homh] -CB: late binding problem? -*) - -lemma (in group_hom) hom_mult [simp]: - "[| x \ carrier G; y \ carrier G |] ==> h (x \ y) = h x \\<^bsub>H\<^esub> h y" - by (simp add: hom_mult [OF homh]) - -lemma (in group_hom) hom_closed [simp]: - "x \ carrier G ==> h x \ carrier H" - by (simp add: hom_closed [OF homh]) lemma (in group_hom) one_closed [simp]: "h \ \ carrier H" diff -r 13d1ec61bc89 -r b901a127ac73 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Sun Apr 17 19:40:43 2005 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Mon Apr 18 09:25:23 2005 +0200 @@ -1474,7 +1474,6 @@ by (simp del: monom_mult (* eval.hom_mult eval.hom_pow, delayed inst! *) add: monom_mult [THEN sym] monom_pow) also - (* from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring *) from R S eval_monom1 have "... = h r \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" by (simp add: eval_const) finally show ?thesis . @@ -1487,9 +1486,6 @@ assume S: "s \ carrier S" and R: "r \ carrier R" and P: "p \ carrier P" from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"] by - (rule ring_hom_cring.axioms, assumption)+ -(* - from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring -*) from S R P show ?thesis by (simp add: monom_mult_is_smult [THEN sym] eval_const) qed @@ -1571,11 +1567,15 @@ by (fast intro: UP_univ_propI INTEG_cring id_ring_hom) text {* - An instantiation mechanism would now import all theorems and lemmas + Interpretation allows now to import all theorems and lemmas valid in the context of homomorphisms between @{term INTEG} and @{term "UP INTEG"} globally. *} +interpretation INTEG: UP_univ_prop [INTEG INTEG id] + using INTEG_id_eval + by - (rule UP_univ_prop.axioms, assumption)+ + lemma INTEG_closed [intro, simp]: "z \ carrier INTEG" by (unfold INTEG_def) simp @@ -1589,6 +1589,6 @@ by (induct n) (simp_all add: INTEG_def nat_pow_def) lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500" - by (simp add: UP_univ_prop.eval_monom [OF INTEG_id_eval]) + by (simp add: INTEG.eval_monom) end diff -r 13d1ec61bc89 -r b901a127ac73 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun Apr 17 19:40:43 2005 +0200 +++ b/src/Pure/Isar/locale.ML Mon Apr 18 09:25:23 2005 +0200 @@ -351,8 +351,12 @@ in (case loc_regs of NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") - | SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":") - (map prt_inst (Termlisttab.dest r))) + | SOME r => let + val r' = Termlisttab.dest r; + val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; + in Pretty.big_list ("Interpretations in " ^ msg ^ ":") + (map prt_inst r'') + end) |> Pretty.writeln end; @@ -540,7 +544,6 @@ fun tinst_tab_elem sg tinst = map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst); - (* instantiate TFrees and Frees *) fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst @@ -589,8 +592,8 @@ (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) end; -fun inst_tab_elem sg inst = - map_values (tinst_tab_type (#2 inst)) (inst_tab_term inst) (inst_tab_thm sg inst); +fun inst_tab_elem sg (inst as (_, tinst)) = + map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst); fun inst_tab_elems sign inst ((n, ps), elems) = ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems); @@ -1923,7 +1926,8 @@ disch (prfx, atts) (thy_ctxt, Notes facts) = let val reg_atts = map (attrib thy_ctxt) atts; - val facts = map_attrib_facts (attrib thy_ctxt) facts; + (* discharge hyps in attributes *) + val facts = map_attrib_facts (attrib thy_ctxt o Args.map_values I I I disch) facts; val facts' = map (apfst (apsnd (fn a => a @ reg_atts))) facts; (* discharge hyps *) val facts'' = map (apsnd (map (apfst (map disch)))) facts';