It's a bit confusing. The expressions you enter in the session are not
actually in HOL - they are in the functional programming language ML.
This is the language used to implement HOL4. You are in an ML toplevel
(also called "read-eval-print loop" or "REPL"), with HOL4 already
incorporated. ML expressions that you enter in the session get
evaluated by the toplevel. These may include standard library functions
that are provided by ML, or functions provided by HOL4, or a mixture of
both. This is a very powerful paradigm, and allows the user to extend
the theorem prover as much as they like with their own facilities.
You are able to input HOL expressions (called "terms") by surrounding
them with two backquote characters at the start and end, like this:
`` FST (1,2) ``;
which results in:
val it = ``FST (1,2)``: term
Inference rules are provided by HOL4 as ML functions that return
theorems, for example 'REWRITE_CONV':
REWRITE_CONV [pairTheory.FST] ``FST (1,2)``;
results in:
val it = |- FST (1,2) = 1: thm
As Ramana says, there happens to be an ML function called 'fst', which
directly corresponds to the HOL function 'FST'. But when you enter the
following into the ML session:
fst (1,2);
to result in
val it = 1: int
you are not doing theorem proving, you are just doing functional
programming.
Hope this makes sense.
Mark.
On 22/06/2016 09:24, Ramana Kumar wrote:
> FST is a function in logic, not in ML.
>
> In this case, there does happen to be a similar function, called fst, in ML.
>
> Are you trying to specify/prove something in logic? Or are you trying to
> write an ML program?
>
> On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote:
>
>> Hi,guys
>> I am working with HOL4.
>> FST is in pairTheory, its definition is
>>
>> [FST] Theorem
>>
>> |- ∀x y. FST (x,y) = x
>>
>> But, When I use it like following:
>>
>> val n = FST (1,2);
>>
>> It responses:
>>
>> ! Toplevel input:
>> ! val n = FST (1,2);
>> ! ^^^
>> ! Type clash: expression of type
>> ! thm
>> ! cannot have type
>> ! 'a -> 'b
>>
>> What is the reason? Does anyone know how to use it?
>>
>> Thanks!
>> ------------------------------------------------------------------------------
>> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
>> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
>> present their vision of the future. This family event has something for
>> everyone, including kids. Get more information and register today.
>> http://sdm.link/attshape
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>
> ------------------------------------------------------------------------------
> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
