I think you shouldn't use new_constant and new_definition. Just the latter
should be enough to create the new constant with its definition. The former
creates a constant without a definition (it's like new_axiom in that it
should be avoided)
On Jun 26, 2012 2:18 AM, "Bill Richter" <[email protected]>
wrote:
> I need help with `new_definition' for my Hilbert paper formalization,
> for order relations on segments and angles, both defined as sets. At
> the end is what I really want, but this is a simple relevant bomb:
>
> new_type("point",0);;
> new_constant("doubleton",`:(point->bool)->bool`);;
>
> let Doubleton_DEF = new_definition
> `!s:point->bool. doubleton s <=>
> ?A:point B:point. s = {A, B}`;;
>
> (* I get the error message
> Exception: Failure "new_basic_definition".
>
> This doesn't seem like a typing problem, and of course that's not my
> error message anyway, but let's check, and it all looks right:
>
> type_of `{A:point, B:point}`;;
> => hol_type = `:point->bool`
>
> type_of `doubleton`;;
> => hol_type = `:(point->bool)->bool`
>
> type_of `doubleton (s:point->bool)`;;
> => hol_type = `:bool`
>
> I'm wondering if the problem is that HOL Light thinks I'm trying to
> redefine =. I'm not. I'm trying to define the predicate doubleton: s
> is a doubleton iff there exist points A and B such that s = {A, B}.
>
> Note that sets are really predicates, as explained in sets.ml, and as
> explained in the tutorial, {A, B} is syntactic sugar for
> A INSERT {B}
> or more precisely
> A INSERT B INSERT EMPTY
> as we see by evaluating
> `A INSERT {B}`;;
> `A INSERT B INSERT EMPTY`;;
>
> These are indeed functions, as we see from sets.ml:
>
> let IN = new_definition
> `!P:A->bool. !x. x IN P <=> P x`;;
>
> let INSERT_DEF = new_definition
> `x INSERT s = \y:A. y IN s \/ (y = x)`;;
>
> let EMPTY = new_definition
> `EMPTY = (\x:A. F)`;;
>
> I'd like to know where the syntactic sugar is defined.
>
> What I really want is the following, which makes sense after loading in
> my 1900 line miz3 file HilbertAxiom.ml
>
> http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar
> *)
>
> new_constant("seg_less",`:(point->bool)->(point->bool)->bool`);;
> let SegmentLess_DEF = new_definition
> `! s t. seg_less s t <=>
> ? A B C D. ~(A = B) /\ ~(C = D) /\
> s = Segment A B /\ t = Segment C D /\
> ? E. E IN open (C,D) /\ Segment A B === Segment C E`;;
>
> (* I get the same error message:
> Exception: Failure "new_basic_definition".
>
> --
> Best,
> Bill *)
>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
