[isabelle] A tricky problem with Isabelle locales



Dear Isabelle pros,

I have encountered a tricky problem with Isabelle locales. Is there anyone kind enough to help?

Suppose we have a dummy locale and a definition:
 locale dummy = fixes x::bool assumes x_true:x
 definition (in dummy) f::bool where "f ≡ ∀y::bool. y∨x"

We can show the following lemma by unfolding 'f' first:
 lemma (in dummy) f
 proof (unfold f_def,rule)
fix y show "y∨x" using x_true by auto
 qed

However, when trying to prove a similar lemma, I don't know how to unfold 'f' :(
 lemma (in dummy) "dummy.f True"

Any help is highly appreciated.
Best regards,
Wenda Li




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