Re: [isabelle] Interpretations and lemmas
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:
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
* 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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and