Ramana, Rob & Freek, thanks for explaining new_definition! I figured
it out myself last night by hours of trial and error, and this works:
parse_as_infix("seg_less",(12, "right"));;
let SegmentOrdering_DEF = new_definition
`s seg_less t <=>
? A B C D X. s = Segment A B /\ t = Segment C D /\
X IN open (C,D) /\ Segment A B === Segment C X`;;
I feel pretty dumb, as I'd already (by earlier trial and error) done
it correctly on 15 earlier uses of new_definitions, without realizing
the rule, which is: you can't specify the type of a variable twice!
BTW I would have preferred to call it seg<, to go with angle< later,
but HOL Light didn't let me do that. Does anyone know why?
Now I'm past 2000 lines in my paper's formalization
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar
I haven't yet checked the seg_less code, but I proved 2 thms using my
Hilbert segment congruence axioms (here with math characters):
C1IntervalUniqueness_THM : thm =
|- ∀ A B C. B ∈ open (A,C) ⇒ ¬(Segment A B ≡ Segment A C)
OrderedCongruentSegments_THM : thm =
|- ∀ A B C D F.
¬(A = C) ∧ ¬(D = F)
⇒ Segment A C ≡ Segment D F
⇒ B ∈ open (A,C)
⇒ (∃ E. E ∈ open (D,F) ∧ Segment A B ≡ Segment D E)
and with math characters, here's the seg_less definition:
SegmentOrdering_DEF : thm =
|- ∀s t.
s seg_less t ⇔
(∃A B C D X.
s = Segment A B ∧
t = Segment C D ∧
X ∈ open (C,D) ∧
Segment A B ≡ Segment C X)
I'm really happy, as this is serious set theory.
So the rule is that you can't type a variable twice. seg_less is
typed implicitly in this definition, so if I've already typed it with
new_constant, I'm going to get the not-too-helpful error message
Exception: Failure "new_basic_definition".
Can you guys tell me how you learned this? I don't believe the HOL
Light reference manual or tutorial explains it. I googled for
HOL Light Failure "new_basic_definition"
and only found Freek's paper arxiv.org/pdf/1103.3322, which says
In particular, in the existing HOL Light system it is not possible to
change the definition of a defined constant:
# let X0 = new_definition ‘X = 0‘;;
val ( X0 ) : thm = |- X = 0
# let X1 = new_definition ‘X = 1‘;;
Exception: Failure "new_basic_definition".
That's important, and relevant, but not quite my problem...
--
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
