The rule you have learned is not quite right, but I can't point to exactly
what's wrong because I don't know what you mean by the verb "to type"
applied to a variable. I could take a guess at what you mean, but I think
it would be better if we had a shared understanding of what HOL theories
are, and in particular what it means to extend a theory, in the first place.
I'm not sure that we do. Did you read the HOL Logic manual as I suggested?
Anyway, the "rule" is that you can't have two different constants with the
same name and type. So if you already have a constant, HOL Light stops you
introducing it again via new_constant or new_definition. You would have to
delete it first. I'm actually not too sure how this all works in HOL Light,
but in HOL4 the mechanisms for definition automatically delete then add
constants if they are within the theory segment you are working on
(constants in other, closed theory segments can't be touched) and
invalidate any theorems involving the deleted constants. In HOL Light I
think there are no theory segments (or you could say there's one big one)
and I'm not sure whether constants can be deleted at all, or how past uses
get invalidated if they can be.
On Jun 27, 2012 8:10 AM, "Bill Richter" <[email protected]>
wrote:
> 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
>
------------------------------------------------------------------------------
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
