My old definition of ray OK. The problem was int_angle, where I needed this
clumsy looking usage, with the useless and "unsettling" first line of the proof
let InteriorWellDefined_THM = thm `;
let A O B X P be point;
assume P IN int_angle A O B [H1];
assume X IN ray O B DELETE O [H2];
thus P IN int_angle A O X
proof
int_angle A O B P by H1, IN;
consider a b such that
~Collinear A O B /\
Line a /\ O IN a /\ A IN a /\ P NOTIN a /\
Line b /\ O IN b /\ B IN b /\ P NOTIN b /\
P,B same_side a /\ P,A same_side b [def_int] by -, InteriorAngle_DEF;
[...]
With my new code, it looks much better:
let InteriorWellDefined_THM = thm `;
let A O B X P be point;
assume P IN int_angle A O B [H1];
assume X IN ray O B DELETE O [H2];
thus P IN int_angle A O X
proof
consider a b such that
~Collinear A O B /\
Line a /\ O IN a /\ A IN a /\ P NOTIN a /\
Line b /\ O IN b /\ B IN b /\ P NOTIN b /\
P,B same_side a /\ P,A same_side b [def_int] by -, IN_InteriorAngle;
[...]
The fixed comes from the set abstraction definition and sets.ml-type theorem
let InteriorAngle_DEF = new_definition
`∀ A O B P.
int_angle A O B = {P:point | ¬Collinear A O B ∧ ∃ a b.
Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b}`;;
let IN_InteriorAngle = prove
(`∀ A O B P:point. P ∈ int_angle A O B ⇔
¬Collinear A O B ∧ ∃ a b.
Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b`,
REWRITE_TAC[IN_ELIM_THM; InteriorAngle_DEF]);;
I think it's fine for me to write `IN_ELIM_THM' HOL Light code in my miz3 code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
that I don't understand, because `IN_ELIM_THM' code of this sort fills sets.ml,
which I'm making heavy use of. It would be nice to understand my own code, but
that's no higher a priority than understanding sets.ml. Still, it would be nice
to rewrite the parts of sets.ml I use in miz3, including this.
--
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
