The variable `t` in your goal cannot be generalised, for the same reason
that you can't generalise variables that appear free in the assumptions of
a theorem.
I think the goalstack you showed is unproveable. But it looks like you
probably did an induction without using a general enough induction
hypothesis.
Perhaps show us your initial goal. The answer to "How can I apply GEN to
the assumption 0?" might be "generalise your induction hypothesis".
On Sat, Oct 19, 2013 at 11:53 AM, Domenico D. D. Masini <
domenico.mas...@gmail.com> wrote:
> Hello,
>
> I'm trying to learn hol, and one thing is not clear to me is how to mix
> forward proof in a goal directed proof while being in an active goal
> package session.
>
> One thing I was trying is to complete a proof with this current goalstack:
>
> ?v. R (t',v) /\ R (u,v)
> ------------------------------------
> 0. !u. R (t,u) ==> ?v. R (t,v) /\ R (u,v)
> 1. R (t',u)
>
> How can I apply GEN to the assumption 0 and then MP on the new 0 and 1?
>
> Thanks for any suggestion.
>
> Kind Regards,
> Domenico
>
>
> ------------------------------------------------------------------------------
> October Webinars: Code for Performance
> Free Intel webinars can help you accelerate application performance.
> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
> from
> the latest Intel processors and coprocessors. See abstracts and register >
> http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
