Re: [isabelle] Using an assumption as a rule



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.