--- 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.
--- 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}
--- 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
-*)
--- 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);
--- 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
--- 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, []),