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
