*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Eisbach match drule*From*: <Matthew.Brecknell at data61.csiro.au>*Date*: Sun, 24 Jul 2016 23:37:51 +0000*Accept-language*: en-AU, en-US*In-reply-to*: <SNT407-EAS1956D51DBCB1D5A8C7E2919E40A0@phx.gbl>*Ironport-phdr*: 9a23:AmUjVxOXRnGK072VDXYl6mtUPXoX/o7sNwtQ0KIMzox0KPn7rarrMEGX3/hxlliBBdydsKMczbSO+PmwASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+KyZrvnLnio9X6WEZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0o8VEFKThdq41SbhVSSk9PnouzMnqrgXYCwCG4z0VWSMLkUwbLRLC6USue57triv3qaxXwiSRPsv7SbQcVT2+5vkyDhTziT0AcTckpjKEwvdshb5W9Ury7yd0xJTZNdmY*References*: <SNT407-EAS1956D51DBCB1D5A8C7E2919E40A0@phx.gbl>*Thread-index*: AQHR5gRkodlRCPTtREm2TbRbd8MBhg==*Thread-topic*: [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

**References**:**[isabelle] Eisbach match drule***From:*Zhe Hou

- Previous by Date: Re: [isabelle] Defining an operation on a particular set and arguments of the definition command
- Next by Date: Re: [isabelle] Eisbach match drule
- Previous by Thread: [isabelle] Eisbach match drule
- Next by Thread: Re: [isabelle] Eisbach match drule
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list