Thanks, John! We need to get rid of the new_axiom biz at some point,
I think, but our code sure looks nice. Thanks again! I have two miz3
comments for Freek and you:
1) I was wrong about comments: you can use
::
for comments inside a proof, just as in Mizar. That's almost
explained in Freek's pdf, but it ought to be clearer. BUT (and I
think this is a bug) you can't have ` in the comment.
2) Here's a miz3 problem I had that I couldn't solve, and the error
message doesn't help me. There's only one error message, so I'll just
send the miz3 Exception: Mizar_error, which contains this:
cases by X1, X2;
:: #2
:: 2: inference time-out
Mizar thought that was fine. So I rewrote the code to say first
cases by X1;
and then
cases by X2;
and it didn't help. So I don't think it's a cases problem. I think
there's some other error I made which isn't getting reported.
Exception:
Mizar_error
(`;
let a b x be point;
assume ~(a = b) [H1];
assume ~(a = x) [H2];
assume on_line(x,a,b) [H3];
thus ! c .
on_line(c,a,b) ==> on_line(c,a,x)
proof
let c be point;
assume on_line(c,a,b) [H4];
Between (a,b,x) \/ Between (b,x,a) \/ Between (x,a,b) by H3, Line_DEF;
Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) [X1]
by -, Bsymmetry_THM;
Between (a,b,c) \/ Between (b,c,a) \/ Between (c,a,b) by H4, Line_DEF;
Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) [X2]
by -, Bsymmetry_THM;
x = b \/ b = c \/ (~(x = b) /\ ~(b = c));
cases by -;
suppose x = b [Case1];
on_line(c,a,x) by -, H4;
qed by -;
suppose b = c [Case3];
Between (a,c,x) \/ Between (c,x,a) \/ Between (x,a,c) by -, H3,
Line_DEF;
Between (x,c,a) \/ Between (a,x,c) \/ Between (c,a,x) by -,
Bsymmetry_THM;
on_line(c,a,x) by -, H2, Line_DEF;
qed by -;
suppose ~(x = b) /\ ~(b = c) [Case2];
Between (a,x,c) \/ Between (a,c,x) \/ Between (x,a,c)
proof
cases by X1, X2;
:: #2
:: 2: inference time-out
suppose Between (a,b,x) /\ Between (a,b,c) [X3];
Between (b,x,c) \/ Between (b,c,x) by -, H1, Gupta_THM;
is_ordered (a,b,x,c) \/ is_ordered (a,b,c,x) by -, Case2, X3,
BTransitivityOrdered_THM;
qed by -, is_ordered_DEF;
suppose Between (a,b,x) /\ Between (a,c,b);
is_ordered (a,c,b,x) by -, B123and134Ordered_THM;
qed by -, is_ordered_DEF;
suppose Between (a,b,x) /\ Between (c,a,b);
is_ordered (c,a,b,x) by -, H1, BTransitivityOrdered_THM;
Between (c,a,x) by -, is_ordered_DEF;
qed by -, Bsymmetry_THM;
suppose Between (a,x,b) /\ Between (a,b,c);
is_ordered (a,x,b,c) by -, B123and134Ordered_THM;
qed by -, is_ordered_DEF;
suppose Between (a,x,b) /\ Between (a,c,b) [X4];
consider m such that
Between (b,a,m) /\ a,m === a,b [X5] by -, A4;
~(a = m) [X6] by H1, X5, EquivSymmetric, A3;
Between (m,a,b) by X5, Bsymmetry_THM;
Between (m,a,c) /\ Between (m,a,x) by -, X4, B124and234then123_THM;
Between (a,c,x) \/ Between (a,x,c) by -, X6, Gupta_THM;
qed by -;
suppose Between (a,x,b) /\ Between (c,a,b);
Between (c,a,x) by -, B124and234then123_THM;
qed by -, Bsymmetry_THM;
suppose Between (x,a,b) /\ Between (a,b,c);
is_ordered (x,a,b,c) by -, H1, BTransitivityOrdered_THM;
qed by -, is_ordered_DEF;
suppose Between (x,a,b) /\ Between (a,c,b);
qed by -, B124and234then123_THM;
suppose Between (x,a,b) /\ Between (c,a,b);
Between (b,a,x) /\ Between (b,a,c) by -, Bsymmetry_THM;
Between (a,x,c) \/ Between (a,c,x) by -, H1, Gupta_THM;
qed by -;
end;
Between (a,x,c) \/ Between (x,c,a) \/ Between (c,a,x) by -,
Bsymmetry_THM;
qed by -, H2, Line_DEF;
end
;`,
(0, 1, 0)).
#
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
