Hi Vladimir,
* It could be that types are different in lemma5_8 and
in your goal. If you try
MATCH_MP_TAC lemma5_8
and it fails, this is probably the case. Then you
should set
show_types := true
and have a look at the types in the goal and the theorem.
* Try METIS_TAC instead of PROVE_TAC, as it
can be more effective in some cases.
Konrad.
On Nov 5, 2008, at 3:46 PM, Vladimir Timashov wrote:
> Hello,
>
> I again need your help in some beginner questions.
>
> I have a theorem proved:
>
> - lemma5_8;
> > val it =
> |- (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) /\
> ((!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>
> (access t2 (k + 1) = access t1 (k + 1))) /\
> ((!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>
> (access t2 k = access t1 k)) /\
> access t1 k <= access t1 (k + 1) ==>
> access t2 k <= access t2 (k + 1) : thm
>
> I need to prove a theorem. After some intermediate transformations
> I get the following subgoal:
>
> Current goal:
> access t2 k <= access t2 (k + 1)
> ------------------------------------
> 0. !k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)
> 1. (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>
> (access t2 (k + 1) = access t1 (k + 1))
> 2. (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==>
> (access t2 k = access t1 k)
> 3. access t1 k <= access t1 (k + 1)
>
> You can see that even names of variables and order of assumptions
> are the same for lemma and subgoal. But I was not able to prove
> this. For example:
> e(PROVE_TAC[lemma5_8]);
>
> fails with "Too deep" exception with 287320 inferences on the 30-th
> step.
>
> Am I correct that "assumptions" and "goal" is in fact an
> implication of conjunctions and goal and my theorems are equal?
>
> So could you please advice how I should prove the theorem using lemma?
>
>
> Thank you.
>
> --
>
> Sincerely yours,
> Vladimir Yu. Timashov
> ICQ: 334366950
> ----------------------------------------------------------------------
> ---
> This SF.Net email is sponsored by the Moblin Your Move Developer's
> challenge
> Build the coolest Linux based applications with Moblin SDK & win
> great prizes
> Grand prize is a trip for two to an Open Source event anywhere in
> the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
