Sorry, I want to use SPEC not GEN in the step 1).
Kind Regards,
Domenico
2013/10/20 Domenico D. D. Masini <domenico.mas...@gmail.com>
> Hello,
>
> thanks for the reply but the goal to me seems trivial from the current
> assumptions in the goalstack.
>
> I want to generalize 'u' (not 't')
>
> 1) from the assumption 0: '!u. (R (t,u) ==> ?v. R (t,v) /\ R (u,v))' to
> obtain R (t,u) ==> ?v. R (t,v) /\ R (u,v), then
> 2) with MP from the new 0: R (t,u) ==> ?v. R (t,v) /\ R (u,v) and the
> assumption 1: R (t',u), obtain ?v. R (t',v) /\ R (u,v) which is just the
> goal.
>
> The problem is that I want to generalize on the assumption and not the
> goal.
>
> Kind Regards,
> Domenico
>
>
>
>
>
> 2013/10/19 Ramana Kumar <ram...@member.fsf.org>
>
>> 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
