[isabelle] Using an assumption as a rule

[Edward Pierzchalski]

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

[Simon Wimmer]

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

[Edward Pierzchalski]

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.

[Peter Lammich]

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

[Makarius]

On 06/10/16 14:16, Peter Lammich wrote:
>
> 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
> "!!_.[|_|] ==> _".

I just want to point out that the 'subgoal' command has no overhead: on
the contrary, it allows to check proofs compositionally and thus in
parallel. The explicit proof structure is also an advantage for
maintainability.

In some situations, 'subgoal' cannot be used, though. One example are
schematic goal states. Then one really needs to go back to old-style
tactical means.


Makarius

[Peter Lammich]

I just want to point out that the 'subgoal' command has no overhead:

Sorry, I meant textual overhead (boilerplate), not computational
overhead.

--
  Peter