*To*: Edward Pierzchalski <e.a.pierzchalski at gmail.com>, Simon Wimmer <wimmersimon at gmail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Using an assumption as a rule*From*: Peter Lammich <lammich at in.tum.de>*Date*: Thu, 06 Oct 2016 14:16:46 +0200*In-reply-to*: <CADBMsp+HYoZcbbmTipP=d9k2if+OqSzmC46-7C1Gh_yo3Z+UsA@mail.gmail.com>*References*: <CADBMsp+9iPT620WVfyDhz-Hmzu2RJVwBu4ddV6WyA+8F4+vmww@mail.gmail.com> <CAASQnwNE0hTq4Hm8-9vX2cATbOMwTJGnYMUNtHRJXKUCOb6MPw@mail.gmail.com> <CADBMsp+HYoZcbbmTipP=d9k2if+OqSzmC46-7C1Gh_yo3Z+UsA@mail.gmail.com>

Hi, for exactly this usecase (induction proofs), I use a custom method rprems: Â apply rprems also does what you want, without the subgoal overhead. It resolves the conclusion with the first premise, even if this premise is of form "!!_.[|_|] ==> _". It's currently in $AFP/Automatic_Refinement/Lib/Refine_Util, but if more people find this useful, maybe one could move it to Isabelle? -- Â Peter On Do, 2016-10-06 at 10:12 +0000, Edward Pierzchalski wrote: > Thanks for the tip, Simon! That worked quite nicely. > > The reason I have intro-like rules is because I'm inside some simple > induction proofs in apply mode, where the overhead from doing it > "properly" > in Isar just isn't worth it. > > On Thu, 6 Oct 2016 at 21:05 Simon Wimmer <wimmersimon at gmail.com> > wrote: > > > > > Hi Ed, > > > > I'm not sure if you really want the rule to appear in your goal > > anyways. > > However, you could use something like > > > > subgoal premises prems > > Â apply (rule prems(2)) > > > > to apply the rule in apply-style. > > > > Simon > > > > On Thu, Oct 6, 2016 at 11:51 AM Edward Pierzchalski < > > e.a.pierzchalski at gmail.com> wrote: > > > > Hi all, > > > > Say my current goal looks like: > > > > A v ==> > > (!! x. B x ==> C x) ==> > > C v > > > > Here, I have an assumption that I could easily use as an > > introduction rule > > for my conclusion, resulting in the new goal > > > > A v ==> > > B v ==> > > C v > > > > If I were in Isar mode, the rule-shaped assumption would have a > > name that I > > could apply using the rule tactic. Is there an easy way to do this > > in apply > > mode? At the moment I'm repeatedly using meta_allE (my case has a > > few more > > bound variables), but this seems dirty. > > > > Regards, > > --Ed > > > >

**Follow-Ups**:**Re: [isabelle] Using an assumption as a rule***From:*Makarius

**References**:**[isabelle] Using an assumption as a rule***From:*Edward Pierzchalski

**Re: [isabelle] Using an assumption as a rule***From:*Simon Wimmer

**Re: [isabelle] Using an assumption as a rule***From:*Edward Pierzchalski

- Previous by Date: Re: [isabelle] Using an assumption as a rule
- Next by Date: Re: [isabelle] Using an assumption as a rule
- Previous by Thread: Re: [isabelle] Using an assumption as a rule
- Next by Thread: Re: [isabelle] Using an assumption as a rule
- Cl-isabelle-users October 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