[isabelle] Interpretations and lemmas



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 at 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.







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