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
