Hi Ada,
You need to search for suitable theorems.
In this case
> apropos ``TAKE 0`` ;
<<HOL message: inventing new type variable names: 'a>>
val it =
[(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)),
so from the initial goal
e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ;
This should work but doesn't - when all else fails, look at the types:
show_types := true ;
and you see that they are different.
Do it this way instead.
e (ASM_REWRITE_TAC [listTheory.TAKE_0, listTheory.LENGTH_EQ_NUM_compute]) ;
then you're almost there.
If you didn't have the theorem TAKE_0 you would have to use the
definition of TAKE, namely listTheory.TAKE_def, and use
Cases_on `p`
Cheers,
Jeremy
On 15/12/15 14:27, Ada wrote:
> Hey guys,
>
> I am learning to use HOL4. There is a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
> When I was proving one property of TAKE, I find an interesting thing. As
> follows:
> - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
>> val it =
> TAKE 0 p = p
> ------------------------------------
> LENGTH p = 0
> : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
> > val it =
> TAKE 0 p = p
> ------------------------------------
> 0. LENGTH p = 0
> 1. !l. (LENGTH l = 0) <=> (l = [])
> 2. !l n.
> (LENGTH l = NUMERAL (BIT1 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
> 3. !l n.
> (LENGTH l = NUMERAL (BIT2 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
> 4. !l n1 n2.
> (LENGTH l = n1 + n2) <=>
> ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
> : proof
> The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove
> that. Could anyone prove it?
> Thanks! --Wish.
>
>
> ------------------------------------------------------------------------------
>
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
