Re: [isabelle] Using an assumption as a rule



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






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