If you put exactly what you typed into HOL4, then you were using "first"
from ML rather than the one in the logic.
To do evaluation in the logic, try:
EVAL ``first [1;2;3;4] 3``
On Mon, Nov 30, 2015 at 5:29 PM, Waqar Ahmad <12phdwah...@seecs.edu.pk>
wrote:
>
>
> On Mon, Nov 30, 2015 at 12:42 PM, Ada <ada.k...@qq.com> wrote:
>
>> Hey guys,
>>
>> I am learning to use HOL4. I defined a function named "first" in HOL4.
>> This function can get the first n elements in a list. As follows:
>>
>> - val first_def = Define`(first [] n = [] )
>> /\ (first (p::pl) 0 = [] )
>> /\ (first (p::pl) n = HD (p::pl) :: first (TL
>> (p::pl)) (n-1)) `;
>> <<HOL message: inventing new type variable names: 'a>>
>> Equations stored under "first_def".
>> Induction stored under "first_ind".
>> > val first_def =
>> |- (!n. first [] n = []) /\ (!pl p. first (p::pl) 0 = []) /\
>> !v4 pl p.
>> first (p::pl) (SUC v4) =
>> HD (p::pl)::first (TL (p::pl)) (SUC v4 - 1) : thm
>> In which, I saw HD and TL had been defined in listTheory. HD gets the
>> first element in a list, TL gets the last.
>>
>>
> You can use TAKE function already defined in the HOL4 list theory, which
> returns the first 'n' element of the given list... Also, you may find many
> usefull properties of the TAKE function in the list theory...
>
> |- (∀n. TAKE n [] = []) ∧
> ∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs
>
>
> But , when I tried to use "first", failed. As followes:
>>
>> - first ([0,1,0,1,0],3);
>> ! Toplevel input:
>> ! first ([0,1,0,1,0],3);
>> ! ^^^^^
>> ! Type clash: expression of type
>> ! ('a -> bool) -> 'a list -> 'a
>> ! cannot have type
>> ! 'b * 'c -> 'a list -> 'a
>>
>> - first [0,1,0,1,0] 3;
>> ! Toplevel input:
>> ! first [0,1,0,1,0] 3;
>> ! ^^^^^^^^^^
>> ! Type clash: expression of type
>> ! 'a list
>> ! cannot have type
>> ! 'b -> bool
>>
>>
> Use first [0;1;0;1;0] 3;
> Hopefully it will work....
>
>
> I was wondering why it failed. Could anyone find the reasion?
>>
>> Thanks! --Wish.
>>
>>
>> ------------------------------------------------------------------------------
>> Go from Idea to Many App Stores Faster with Intel(R) XDK
>> Give your users amazing mobile app experiences with Intel(R) XDK.
>> Use one codebase in this all-in-one HTML5 development environment.
>> Design, debug & build mobile apps & 2D/3D high-impact games for multiple
>> OSs.
>> http://pubads.g.doubleclick.net/gampad/clk?id=254741551&iu=/4140
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
>
> --
> Thanks and best regards,
>
> Waqar Ahmed
> Ph.D Candidate,
> School of Electrical Engineering and Computer Science (SEECS),
> National University of Science and Technology (NUST), H-12, Islamabad,
> Pakistan
>
>
>
> ------------------------------------------------------------------------------
> Go from Idea to Many App Stores Faster with Intel(R) XDK
> Give your users amazing mobile app experiences with Intel(R) XDK.
> Use one codebase in this all-in-one HTML5 development environment.
> Design, debug & build mobile apps & 2D/3D high-impact games for multiple
> OSs.
> http://pubads.g.doubleclick.net/gampad/clk?id=254741551&iu=/4140
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741551&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
