Re: [isabelle] Eisbach match drule



On Fri, 2016-07-22 at 17:22 +0800, Zhe Hou wrote:
> Dear Eisbach developers,

I'm not an Eisbach developer, but I'll try to answer as best I can!

> I ran into a problem when using drule in match. It seems that drule
> is not supported, but rule is. For example, let's first define a
> silly lemma here:
> 
> lemma dummy: "A â B â B"
> by auto
> 
> Then, when proving the following lemma, I try:
> 
> lemma "A â B â A â B"
> apply (match premises in "A â B" â âdrule dummyâ)
> 
> But Isabelle says "Failed to apply proof method". However, the
> following is ok:
> 
> lemma "A â B â A â B"
> apply (drule dummy)

This is not anything to do with drule in particular. Rather, it's
related to the subgoal focusing performed by the match method. You
might want to reread section 2.1 of the Eisbach user manual:

https://isabelle.in.tum.de/dist/Isabelle2016/doc/eisbach.pdf

In particular, drule is looking for an unstructured premise, but match
has removed these from the subgoal focus. Within the inner method, only
named premises are accessible.

> Is there a way to use drule inside match? Or, is there an alternative
> to drule?

One way to make drule work would be to explicitly re-insert the premise
of interest:

lemma "A â B â A â B"
 apply (match premises in H[thin]: "A â B" â
     âinsert H; drule conjunct2â)
 oops

Note that we had to name the matched premise to make it accessible.
I've also use the `thin` attribute to remove the original premise on
return from the match.

Perhaps this is a slight improvement:

lemma "A â B â A â B"
 apply (match premises in H[thin]: "A â B" â
  Â
  âinsert conjunct2[OF H]â)
 oops

> Thanks a lot,
> 
> Zhe
> 

You're welcome!

Matthew


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