Freek, that's very interesting! To get a decent comparison between
the miz3 HOLBY prover and actual Mizar in my Tarski geometry code, I
have to get rid of infixes and switch to currying, as you said here:
> a,b equal_line c,d
The "HOL style" way of defining this would be a "Curried"
_non_-infix function "equal_line" that you write like
equal_line a b c d
So I got rid of all my infixes in my almost 1000 lines of miz3 code of
http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
There's not a single comma in the code of the curried version
http://www.math.northwestern.edu/~richter/TarskiAxiomGeometryCurry.ml
The improvement is significant but not overwhelming. I had five
5-digit `solved at' numbers, and now have only one, in a simple proof:
[...]..solved at 12994
val LineEqTrans_THM : thm =
|- !a b c d e f.
~(a = b) /\ ~(c = d) /\ ~(e = f)
==> equal_line a b c d
==> equal_line c d e f
==> equal_line a b e f
let LineEqTrans_THM = thm `;
let a b c d e f be point;
assume ~(a = b) /\ ~(c = d) /\ ~(e = f) [H1];
assume equal_line a b c d [H2];
assume equal_line c d e f [H3];
thus equal_line a b e f
proof
(! y . on_line y a b <=> on_line y c d) /\
(! y . on_line y c d <=> on_line y e f) [X2] by H2, H3, LineEq_DEF;
(! y . on_line y a b <=> on_line y e f) by -;
qed by -, H1, LineEq_DEF`;;
As you explained to me, the `solved at' numbers mean that HOLBY has
quit and MESON has taken over. Why is MESON working so hard???
This isn't the only time MESON works hard. I also have six 4-digit
`solved at' numbers.
This might be a HOL Light bug, as it didn't work:
new_type("point",0);;
new_constant("===",`:point->point->point->point->bool`);;
new_constant("Between",`:point->point->point->bool`);;
let cong_DEF = new_definition
`cong a b c x y z <=>
=== a b x y /\ === a c x z /\ === b c y z`;;
The cong_DEF earns me an error message:
# Exception: Failure "term after binary operator expected".
It worked fine when I change === to EquiV:
# val cong_DEF : thm =
|- !a x b c y z.
cong a b c x y z <=> EquiV a b x y /\ EquiV a c x z /\ EquiV b c y z
--
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
