On 28 May 2012, at 05:01, Bill Richter wrote:
> Rob, thank you very much for answering my questions! That was smart
> of you to notice this problem, which I have worried about:
>
> your axioms seem to be loose about whether `(A, B) same_side l`
> holds if A or B is on the line l.
>
> I like your EquivRelOn R P solution (thanks for the correction), or we
> can even define EquivRelOFF R I. I have two more questions.
>
> 1) Can you tell me why this didn't work?
>
> let SameSideEquivalenceRelation_THM = thm `;
> thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
> proof
> qed by SameSideReflexiveRelation_THM, SameSideTransitiveRelation_THM,
> SameSideTransitiveRelation_THM, Reflexive_relation_DEF,
> Symmetric_relation_DEF, Transitive_relation_DEF `;;
>
I don't know anything at all about miz3, I am afraid. However, I did have a
little play with your script and found the following fix:
let SameSideEquivalenceRelation_THM = thm `;
thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
proof
qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM,
SameSideTransitiveRelation_THM `;;
(You hadn't cited your theorem about symmetry, and you don't need to unwind any
definitions.)
>
> 2) I wrote a new definition I have a definition
>
> let InteriorAngle_DEF = new_definition
> `!A O B. int_angle(A, O, B) = if Collinear(A, O, B) then {} else
> {P | ~(P IN line(O, A)) /\ ~(P IN line(O, B)) /\
> P,B same_side line(O, A) /\ P,A same_side line(O, B)}`;;
>
> I don't if it's working yet, but I would like to simplify this with a
> variable declaration and then substitution
>
> a = line(O, A)
> b = line(O, B)
>
You can do local definitions with "let", like this:
let InteriorAngle_DEF = new_definition
`!A O B. int_angle(A, O, B) =
if Collinear(A, O, B) then {} else
let a = line(O, A) in
let b = line(O, B) in
{P | ~(P IN a) /\ ~(P IN b) /\
P,B same_side a /\ P,A same_side b}`;;
"let" is syntactic sugar supported by two object language definitions, LET_DEF
and LET_END_DEF.
Regards,
Rob.------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
