Email Gateway (Aug 18 2022 at 09:50): Email Gateway (Aug 18 2022 at 09:50):From: "Dr. Brendan Patrick Mahony" <Brendan.Mahony@dsto.defence.gov.au>
Is this a bug in the locale mechanism?
theory test = Main:
locale Double =
fixes x :: "nat" and y :: "nat"
assumes double: "x = 2*y"
lemma (in Double) z1:
assumes "z = x"
shows "z = 2*y"
by (auto ! intro: double)
print_locale! Double (* z1 appears + un-named copy *)
lemma (in Double) z2:
"z = x ==> z = 2*y"
by (auto ! intro: double)
print_locale! Double (* no un-named copy of z2 *)
lemmas (in Double) z3 = z1 z2
interpretation i0: Double ["4" "2"]
by (auto simp add: Double_def)
lemmas (in Double) z1' = z1
lemmas (in Double) z2' = z2
lemmas (in Double) z4 = z1 z2
this last fails with
*** Match
*** At command "lemmas".
Dr Brendan Mahony
Information Networks Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
Email Gateway (Aug 18 2022 at 09:50):From: Clemens Ballarin <ballarin@in.tum.de>
Which version of Isabelle are you refering to? The exception is no
longer present in the current repository version.
Clemens
Email Gateway (Aug 18 2022 at 09:51):From: Makarius <makarius@sketis.net>
On Mon, 30 Oct 2006, Dr. Brendan Patrick Mahony wrote:
Is this a bug in the locale mechanism?
theory test = Main:
locale Double =
fixes x :: "nat" and y :: "nat"
assumes double: "x = 2*y"interpretation i0: Double ["4" "2"]
by (auto simp add: Double_def)lemmas (in Double) z4 = z1 z2
this last fails with
*** Match
*** At command "lemmas".
The problem here is that in Isabelle2005 the interpretation command
chooses to fail for lemma collections where the RHS mentions multiple
facts. Here is a shorter example to reproduce the problem:
locale foo
interpretation foo .
lemmas (in foo) foo = refl refl
We have fixed that in recent development snapshots, although this won't
help you for the actual Isabelle2005 release.
lemma (in Double) z1:
assumes "z = x"
shows "z = 2*y"
by (auto ! intro: double)print_locale! Double (* z1 appears + un-named copy *)
This is merely due to the multiple views on a complex statements, which is
in general as follows:
lemma a: fixes ... assumes ... shows b: ...
This results in separate facts named a, b etc.
Some further (unrelated) notes:
* The old theory header ``theory test = Main:'' will no longer work
after Isabelle2005.
* Capitalized names are normally used for theories only; better use
plain lower-case for locales. (Otherwise it is easy to run into
unexpected effects with name space accesses.)
Makarius
Last updated: May 03 2024 at 04:19 UTC