Re: [isabelle] Using an assumption as a rule



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.