Thanks, Ramana! I'll try to find Larry's book ($66.30 on Amazon). But since
it's ML code, uh, can't we read the sources and get a pretty good idea? Is
there an Isabelle doc version of this? Thanks for the feedback on my MP_TAC o
SPEC code, which I forgot to say is John's code
http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/LABEL_TAC.html
with FIRST_ASSUM replacing the label stuff. I'm really happy you taught me
some of the ML meaning of what had formerly been HOL black box magic. I
guessed later that my "types" were actually ML types, as you said, but I didn't
guess that when I posted.
BTW you were going to write some HOL documentation for mathematicians who sorta
understand ZFC...
Here's a nice example of how I taught myself a tactics proof via miz3. Here's
a very short proof of a vector version of John's 1-line tutorial theorem on p 67
let MOVE_INVARIANT = prove
(`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area; COLLINEAR_LEMMA;
vector_mul] THEN VEC2_TAC);;
using his new vector versions of the tutorial defs
let oriented_area = new_definition
`oriented_area (a:real^2,b:real^2,c:real^2) =
((b$1 - a$1) * (c$2 - a$2) - (c$1 - a$1) * (b$2 - a$2)) / &2`;;
let move = new_definition
`!A B C A' B' C':real^2. move (A,B,C) (A',B',C') <=>
~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
(B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
C = C' /\ A = A' /\ collinear {vec 0,A - C,B' - B} \/
A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;
and a version of VEC2_TAC of the p 183 tutorial cross product result VEC3_TAC.
But I couldn't do it until I'd written a 45-line miz3 proof which takes much
longer to run (and I'd sure like to know why!!!).
--
Best,
Bill
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
timeout := 50;;
needs "Multivariate/vectors.ml";;
let VEC2_TAC =
SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_2; SUM_2; DIMINDEX_2; VECTOR_2;
vector_add; vec; dot; orthogonal; basis;
vector_neg; vector_sub; vector_mul; ARITH] THEN
CONV_TAC REAL_RING;;
let oriented_area = new_definition
`oriented_area (a:real^2,b:real^2,c:real^2) =
((b$1 - a$1) * (c$2 - a$2) - (c$1 - a$1) * (b$2 - a$2)) / &2`;;
let move = new_definition
`!A B C A' B' C':real^2. move (A,B,C) (A',B',C') <=>
~collinear {A,B,C} /\ ~collinear {A',B',C'} /\
(B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
C = C' /\ A = A' /\ collinear {vec 0,A - C,B' - B} \/
A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;
let Noncollinear_3ImpliesDistinct = prove
(`~collinear {a,b,c} ==> ~(a = b) /\ ~(a = c) /\ ~(b = c)`,
MESON_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_REFL]);;
let MOVE_INVARIANT_THM = thm `;
!p p'. move p p' ==>
oriented_area p = oriented_area p'
proof
let p p' be real^2#real^2#real^2;
assume move p p' [H1];
consider A B C A' B' C' such that
p = (A,B,C) /\ p' = (A',B',C') [DefABC] by PAIR_SURJECTIVE;
~collinear {A,B,C} /\ ~collinear {A',B',C'} [ABCncol] by -, H1, move;
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(A' = B') /\ ~(A' = C') /\ ~(B' = C')
[Distinct] by -, Noncollinear_3ImpliesDistinct;
~(C - B = vec 0) /\ ~(A - C = vec 0) /\ ~(B - A = vec 0) [vecDistinct]
by -, VEC2_TAC;
cases by DefABC, H1, move;
suppose B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} [Case];
cases by -, vecDistinct, COLLINEAR_LEMMA;
suppose A' - A = vec 0;
A' = A by -, VECTOR_ARITH_TAC;
qed by -, Case, DefABC, oriented_area;
suppose ?c. A' - A = c % (C - B);
((B$1 - A$1) * (C$2 - A$2) - (C$1 - A$1) * (B$2 - A$2)) / &2 =
((B$1 - A'$1) * (C$2 - A'$2) - (C$1 - A'$1) * (B$2 - A'$2)) / &2 by
-, H1, VEC2_TAC;
qed by -, Case, DefABC, oriented_area;
end;
suppose C = C' /\ A = A' /\ collinear {vec 0,A - C,B' - B} [Case];
cases by -, vecDistinct, COLLINEAR_LEMMA;
suppose B' - B = vec 0;
B' = B by -, VECTOR_ARITH_TAC;
qed by -, Case, DefABC, oriented_area;
suppose ?c. B' - B = c % (A - C);
((B$1 - A$1) * (C$2 - A$2) - (C$1 - A$1) * (B$2 - A$2)) / &2 =
((B'$1 - A$1) * (C$2 - A$2) - (C$1 - A$1) * (B'$2 - A$2)) / &2 by
-, H1, VEC2_TAC;
qed by -, Case, DefABC, oriented_area;
end;
suppose A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C} [Case];
cases by -, vecDistinct, COLLINEAR_LEMMA;
suppose C' - C = vec 0;
C' = C by -, VECTOR_ARITH_TAC;
qed by -, Case, DefABC, oriented_area;
suppose ?c. C' - C = c % (B - A);
((B$1 - A$1) * (C$2 - A$2) - (C$1 - A$1) * (B$2 - A$2)) / &2 =
((B$1 - A$1) * (C'$2 - A$2) - (C'$1 - A$1) * (B$2 - A$2)) / &2 by
-, H1, VEC2_TAC;
qed by -, Case, DefABC, oriented_area;
end;
end;
`;;
let MOVE_INVARIANT = prove
(`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area; COLLINEAR_LEMMA;
vector_mul] THEN VEC2_TAC);;
(* non-collinear stuff not necessary: *)
let nove = new_definition
`!A B C A' B' C':real^2. nove (A,B,C) (A',B',C') <=>
(B = B' /\ C = C' /\ collinear {vec 0,C - B,A' - A} \/
C = C' /\ A = A' /\ collinear {vec 0,A - C,B' - B} \/
A = A' /\ B = B' /\ collinear {vec 0,B - A,C' - C})`;;
let NOVE_INVARIANT = prove
(`!p p'. nove p p' ==> oriented_area p = oriented_area p'`,
REWRITE_TAC[FORALL_PAIR_THM; nove; oriented_area; COLLINEAR_LEMMA;
vector_mul] THEN VEC2_TAC);;
------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnmore_123012
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
