Hi everyone,
Who knows the means of “ITSET” and “SUM_IMAGE” (they were in the
pred_setTheory)?
val ITSET_def =
let open TotalDefn
in
tDefine "ITSET"
`ITSET (s:'a->bool) (b:'b) =
if FINITE s then
if s={} then b
else ITSET (REST s) (f (CHOICE s) b)
else ARB`
(WF_REL_TAC `measure (CARD o FST)` THEN
METIS_TAC [CARD_PSUBSET, REST_PSUBSET])
end;
What does the variables “b” stand for?
How can I use the definition of “ITSET”?
Could anyone give me an example?
val SUM_IMAGE_DEF = new_definition(
"SUM_IMAGE_DEF",
``SUM_IMAGE f s = ITSET (\e acc. f e + acc) s 0``);
What does the variables “e” and “acc” stand for?
I really appreciate your help!
best wishes,
Amy
------------------------------------------------------------------------------
Beautiful is writing same markup. Internet Explorer 9 supports
standards for HTML5, CSS3, SVG 1.1, ECMAScript5, and DOM L2 & L3.
Spend less time writing and rewriting code and more time creating great
experiences on the web. Be a part of the beta today
http://p.sf.net/sfu/msIE9-sfdev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
