Re: [isabelle] A tricky problem with Isabelle locales



Hallo,

first of all, I cannot quite see the purpose of declaring the second
lemma as "in dummy".

The reason why you cannot simply unfold the definition of f in your
second lemma is that the definition lemma dummy.f_def is conditional:
Try "thm dummy.f_def" and you'll get:

    dummy ?x ⟹ dummy.f ?x ≡ ∀y. y ∨ ?x

i.e. your definition of is is conditional; it only exists inside the
locale, and therefore you must first prove that the assumptions of the
locale hold, i.e. "dummy True" in your case, since you want to show that
"dummy.f True" holds; "True" is the parameter x that you give to the
locale. Your proof could then look like this:

What you can do is this:

lemma "dummy.f True"
proof-
  have "dummy True" by (unfold_locales, rule)
  from dummy.f_def[OF this] show "dummy.f True" by simp
qed


Cheers,
Manuel


On 18/03/13 21:59, W. Li wrote:
> 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.