Re: [isabelle] Using an assumption as a rule



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
> > 
> > 




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