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:

  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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.