[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

On Thu, Oct 6, 2016 at 11:51 AM Edward Pierzchalski <

Post by Edward Pierzchalski
Hi all,
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

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

Post by 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
On Thu, Oct 6, 2016 at 11:51 AM Edward Pierzchalski <
Hi all,
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

[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

Post by 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.

Post by 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
On Thu, Oct 6, 2016 at 11:51 AM Edward Pierzchalski <
Hi all,
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

[Makarius]

Post by Peter Lammich
for exactly this usecase (induction proofs), I use a custom method
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

Post by Makarius
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