# HG changeset patch # User ballarin # Date 1124878020 -7200 # Node ID 165c97f9bb63152a9f5807ef06e8e237f26e7a12 # Parent ad4c98fd367bd7ad1d6bc3f398ccb4da91afca94 Printing of interpretations: option to show witness theorems; diff -r ad4c98fd367b -r 165c97f9bb63 NEWS --- a/NEWS Wed Aug 24 12:05:48 2005 +0200 +++ b/NEWS Wed Aug 24 12:07:00 2005 +0200 @@ -215,7 +215,7 @@ instantiation of terms from the current context. This is applied to specifications and theorems of the interpreted expression. Interpretation in locales only permits parameter renaming through the locale expression. -Interpretation is smart in that interpretation that are active already +Interpretation is smart in that interpretations that are active already 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. diff -r ad4c98fd367b -r 165c97f9bb63 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Wed Aug 24 12:05:48 2005 +0200 +++ b/doc-src/IsarRef/generic.tex Wed Aug 24 12:07:00 2005 +0200 @@ -260,7 +260,7 @@ ; 'interpret' interp ; - printinterps name + printinterps '!'? name ; interp: thmdecl? contextexpr ('[' (inst+) ']')? ; @@ -314,7 +314,7 @@ become part of locale $name$ as \emph{derived} context elements and are available when the context $name$ is subsequently entered. Note that, like import, this is dynamic: facts added to a locale - part of $expr$ after the interpretation become also available in + part of $expr$ after interpretation become also available in $name$. Like facts of renamed context elements, facts obtained by interpretation may be accessed by prefixing with the parameter renaming (where the parameters @@ -330,6 +330,11 @@ are considered by interpretation. This enables circular interpretations. + If interpretations of $name$ exist in the current theory, the + command adds interpretations for $expr$ as well, with the same + prefix and attributes, although only for fragments of $expr$ that + are not interpreted in the theory already. + \item [$\isarcmd{interpret}~expr~insts$] interprets $expr$ in the proof context and is otherwise similar to interpretation in theories. Free variables in instantiations are not @@ -337,7 +342,11 @@ \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. + active in the current context, either theory or proof context. The + exclamation point argument causes triggers printing of + \emph{witness} theorems justifying interpretations. These are + normally omitted from the output. + \end{descr} @@ -356,7 +365,7 @@ in the first place. The locale package does not attempt to remove subsumed interpretations. This situation is normally harmless, but note that $blast$ gets confused by the presence of multiple axclass - instances a rule. + instances of a rule. \end{warn} diff -r ad4c98fd367b -r 165c97f9bb63 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Wed Aug 24 12:05:48 2005 +0200 +++ b/src/FOL/ex/LocaleTest.thy Wed Aug 24 12:07:00 2005 +0200 @@ -17,6 +17,20 @@ ML {* set show_hyps *} ML {* set show_sorts *} +ML {* + fun check_thm name = let + val thy = the_context (); + val thm = get_thm thy (Name name); + val {prop, hyps, ...} = rep_thm thm; + val prems = Logic.strip_imp_prems prop; + val _ = if null hyps then () + else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^ + "Consistency check of locales package failed."); + val _ = if null prems then () + else error ("Theorem " ^ quote name ^ " has premises.\n" ^ + "Consistency check of locales package failed."); + in () end; +*} section {* Context Elements and Locale Expressions *} @@ -98,6 +112,7 @@ thm i1.a.asm_A thm LocaleTest.i1.a.asm_A thm i1.asm_A thm LocaleTest.i1.asm_A +ML {* check_thm "i1.a.asm_A" *} (* without prefix *) @@ -111,6 +126,7 @@ (* possible accesses *) thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C +ML {* check_thm "asm_C" *} interpretation i2: ID [X "Y::i" "Y = X"] by (simp add: eq_commute) @@ -144,14 +160,20 @@ thm i2.th_x thm i3.th_x +ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *} + lemma (in ID) th_y: "d == (a = b)" . thm i2.th_y thm i3.th_y +ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *} + lemmas (in ID) th_z = th_y thm i2.th_z +ML {* check_thm "i2.th_z" *} + subsection {* Interpretation in Proof Contexts *} @@ -194,6 +216,8 @@ thm i7.e_def2 (* has no premise *) +ML {* check_thm "i7.e_def2" *} + locale IE' = fixes e defines e_def: "e == (%x. x & x)" notes e_def2 = e_def @@ -201,6 +225,8 @@ thm i7'.e_def2 +ML {* check_thm "i7'.e_def2" *} + (* Definition involving free variable in assm *) locale (open) IG = fixes g assumes asm_G: "g --> x" @@ -210,6 +236,8 @@ thm i8.asm_G2 +ML {* check_thm "i8.asm_G2" *} + text {* Locale without assumptions *} locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]] @@ -581,6 +609,8 @@ thm Rbool.new_cancel (* additional prems discharged!! *) +ML {* check_thm "Rbool.new_cancel" *} + lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel) @@ -617,6 +647,15 @@ then show "y = z" by (simp add: rone rinv) qed simp +interpretation Rqrgrp < Rprgrp +proof - + show "Rpsemi(op **)" + apply (rule Rpsemi.intro) apply (rule assoc) done +next + show "Rprgrp_axioms(op **, one, inv)" + apply (rule Rprgrp_axioms.intro) apply (rule rone) apply (rule rinv) done +qed + interpretation R2: Rqlgrp ["op #" "rone" "rinv"] proof - apply_end (rule Rqsemi.intro) @@ -633,6 +672,8 @@ print_interps Rqsemi print_interps Rqlgrp +print_interps Rplgrp (* no interpretations yet *) + interpretation Rqlgrp < Rqrgrp proof (rule Rqrgrp_axioms.intro) @@ -650,6 +691,15 @@ } qed +print_interps! Rqrgrp +print_interps! Rpsemi (* witness must not have meta hyps *) +print_interps! Rprgrp (* witness must not have meta hyps *) +print_interps! Rplgrp (* witness must not have meta hyps *) +thm R2.rcancel +thm R2.lcancel + +ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *} + subsection {* Generation of Witness Theorems for Transitive Interpretations *} @@ -734,10 +784,3 @@ apply (rule r_assoc) done end - -(* Known problems: -- var vs. fixes in locale to be interpreted (interpretation in locale) - (implicit locale expressions generated by multiple registrations) -- reprocess registrations in theory (after qed)? -- current finish_global adds unwanted lemmas to theory/locale -*) diff -r ad4c98fd367b -r 165c97f9bb63 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Aug 24 12:05:48 2005 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Wed Aug 24 12:07:00 2005 +0200 @@ -49,7 +49,7 @@ val print_locales: Toplevel.transition -> Toplevel.transition val print_locale: Locale.expr * Locale.element list -> Toplevel.transition -> Toplevel.transition - val print_registrations: string -> Toplevel.transition -> Toplevel.transition + val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition val print_attributes: Toplevel.transition -> Toplevel.transition val print_simpset: Toplevel.transition -> Toplevel.transition val print_rules: Toplevel.transition -> Toplevel.transition @@ -231,9 +231,9 @@ fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) import body); -fun print_registrations name = Toplevel.unknown_context o - Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name) - (Locale.print_local_registrations name o Proof.context_of)); +fun print_registrations show_wits name = Toplevel.unknown_context o + Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations show_wits name) + (Locale.print_local_registrations show_wits name o Proof.context_of)); val print_attributes = Toplevel.unknown_theory o Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); diff -r ad4c98fd367b -r 165c97f9bb63 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Aug 24 12:05:48 2005 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Aug 24 12:07:00 2005 +0200 @@ -648,7 +648,8 @@ val print_registrationsP = OuterSyntax.improper_command "print_interps" "print interpretations of named locale" K.diag - (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); + (Scan.optional (P.$$$ "!" >> K true) false -- P.xname >> + (Toplevel.no_timing oo uncurry IsarCmd.print_registrations)); val print_attributesP = OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag diff -r ad4c98fd367b -r 165c97f9bb63 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed Aug 24 12:05:48 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed Aug 24 12:07:00 2005 +0200 @@ -465,7 +465,7 @@ val (propss, after_qed) = Locale.prep_global_registration (prfx, atts) expr insts thy; in - multi_theorem_i Drule.internalK (fst #> after_qed) ProofContext.export_plain + multi_theorem_i Drule.internalK (after_qed o fst) ProofContext.export_plain ("", []) [] (map (fn ((n, _), props) => ((NameSpace.base n, []), map (fn prop => (prop, ([], []))) props)) propss) int thy @@ -491,7 +491,7 @@ val (propss, after_qed) = Locale.prep_registration_in_locale target expr thy; in - locale_multi_theorem_i Drule.internalK (fst #> after_qed) + locale_multi_theorem_i Drule.internalK (after_qed o fst) ProofContext.export_plain target ("",[]) [] (map (fn ((n, _), props) => ((NameSpace.base n, []),