Hi Naeem,
1. "op" is not the keyword to use. Instead, use either
the "dollar" notation (thus, "$+" or "arithmetic$+"), or the
"paren" notation "(+)", which is also supported.
2. FOLD on sets is already defined: it is called ITSET.
See the Description (page 102) for a short description.
3. Your SETSUM is a simple instance of SUM_IMAGE,
which is also defined in pred_set.
Cheers,
Konrad.
On Dec 7, 2008, at 1:54 PM, [EMAIL PROTECTED] wrote:
> Hello,
>
> I am trying to define a function named SETSUM which uses another
> function FOLD:
> (****FOLD****)
> - val FOLD_defn = Defn.Hol_defn
> "FOLD"
> `FOLD (f:'a->'a->'a) (g:'b->'a) (z:'a)
> (A:'a->bool) =
> if FINITE A then if A={} then z else FOLD f g (CHOICE A) (REST A)
> else ARB`;
>> val FOLD_defn =
> HOL function definition (recursive)
>
> Equation(s) :
> [..]
> |- FOLD f g z A =
> (if FINITE A then
> (if A = {} then z else FOLD f g (CHOICE A) (REST A))
> else
> ARB)
>
> Induction :
> [..]
> |- !P.
> (!f g z A.
> (FINITE A /\ ~(A = {}) ==> P f g (CHOICE A) (REST A)) ==>
> P f g z A) ==>
> !v v1 v2 v3. P v v1 v2 v3
>
> Termination conditions :
> 0. !z g f A.
> FINITE A /\ ~(A = {}) ==> R (f,g,CHOICE A,REST A)
> (f,g,z,A)
> 1. WF R : defn
>
> The definition of setsum is as follows:
>
> val SETSUM_defn = Defn.Hol_defn
> "SETSUM"
> `SETSUM (f:'b->real) (A:real->bool) = if FINITE A
> then FOLD (op +) f 0 A else 0`;
>
> on line 16, characters 82-85:
> No rule for [+]
>
> Exception raised at Parse.Absyn:
> at line 16, character 88:
> Parse failed
> ! Uncaught exception:
> ! HOL_ERR
> -
>
>
>
> I am not sure why I am getting this error message, Am I using "op"
> correctly, can some please help?
>
> Naeem
>
>
> ----------------------------------------------------------------------
> --------
> SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas,
> Nevada.
> The future of the web can't happen without you. Join us at MIX09
> to help
> pave the way to the Next Web now. Learn more and register at
> http://ad.doubleclick.net/clk;208669438;13503038;i?http://
> 2009.visitmix.com/
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas, Nevada.
The future of the web can't happen without you. Join us at MIX09 to help
pave the way to the Next Web now. Learn more and register at
http://ad.doubleclick.net/clk;208669438;13503038;i?http://2009.visitmix.com/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
