1 needs "Multivariate/vectors.ml";;
3 needs "Examples/solovay.ml";;
5 g `orthogonal (A - B) (C - B)
6 ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`;;
9 e(CONV_TAC REAL_RING);;
11 g`!x y:real^N. x dot y <= norm x * norm y`;;
12 e SOLOVAY_VECTOR_TAC;;
14 (**** Needs external SDP solver
15 needs "Examples/sos.ml";;
17 e(CONV_TAC REAL_SOS);;
20 (`!a x y:real^N. (y - x) dot (a - y) >= &0 ==> norm(y - a) <= norm(x - a)`,
21 SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
27 let EXAMPLE_10 = prove
31 !v. &0 < v /\ v <= u ==> norm(v % y - x) < norm x`,
32 SOLOVAY_VECTOR_TAC THEN
33 W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
34 CONV_TAC REAL_QELIM_CONV);;
39 (`(!i. 1 <= i /\ i <= 3 ==> P i) <=> P 1 /\ P 2 /\ P 3`,
40 MESON_TAC[ARITH_RULE `1 <= i /\ i <= 3 <=> (i = 1) \/ (i = 2) \/ (i = 3)`]);;
43 (`!t. sum(1..3) t = t(1) + t(2) + t(3)`,
44 REWRITE_TAC[num_CONV `3`; num_CONV `2`; SUM_CLAUSES_NUMSEG] THEN
45 REWRITE_TAC[SUM_SING_NUMSEG; ARITH; REAL_ADD_ASSOC]);;
48 (`(vector [x;y;z] :real^3)$1 = x /\
49 (vector [x;y;z] :real^3)$2 = y /\
50 (vector [x;y;z] :real^3)$3 = z`,
51 SIMP_TAC[vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
52 REWRITE_TAC[num_CONV `2`; num_CONV `1`; EL; HD; TL]);;
54 let DOT_VECTOR = prove
55 (`(vector [x1;y1;z1] :real^3) dot (vector [x2;y2;z2]) =
56 x1 * x2 + y1 * y2 + z1 * z2`,
57 REWRITE_TAC[dot; DIMINDEX_3; SUM_3; VECTOR_3]);;
59 let VECTOR_ZERO = prove
60 (`(vector [x;y;z] :real^3 = vec 0) <=> x = &0 /\ y = &0 /\ z = &0`,
61 SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]);;
63 let ORTHOGONAL_VECTOR = prove
64 (`orthogonal (vector [x1;y1;z1] :real^3) (vector [x2;y2;z2]) =
65 (x1 * x2 + y1 * y2 + z1 * z2 = &0)`,
66 REWRITE_TAC[orthogonal; DOT_VECTOR]);;
68 parse_as_infix("cross",(20,"right"));;
70 let cross = new_definition
71 `(a:real^3) cross (b:real^3) =
72 vector [a$2 * b$3 - a$3 * b$2;
73 a$3 * b$1 - a$1 * b$3;
74 a$1 * b$2 - a$2 * b$1] :real^3`;;
77 SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
78 vector_add; vec; dot; cross; orthogonal; basis; ARITH] THEN
81 let VEC3_RULE tm = prove(tm,VEC3_TAC);;
83 let ORTHOGONAL_CROSS = VEC3_RULE
84 `!x y. orthogonal (x cross y) x /\ orthogonal (x cross y) y /\
85 orthogonal x (x cross y) /\ orthogonal y (x cross y)`;;
87 let LEMMA_0 = VEC3_RULE
88 `~(basis 1 :real^3 = vec 0) /\
89 ~(basis 2 :real^3 = vec 0) /\
90 ~(basis 3 :real^3 = vec 0)`;;
92 let LEMMA_1 = VEC3_RULE `!u v. u dot (u cross v) = &0`;;
94 let LEMMA_2 = VEC3_RULE `!u v. v dot (u cross v) = &0`;;
96 let LEMMA_3 = VEC3_RULE `!u:real^3. vec 0 dot u = &0`;;
98 let LEMMA_4 = VEC3_RULE `!u:real^3. u dot vec 0 = &0`;;
100 let LEMMA_5 = VEC3_RULE `!x. x cross x = vec 0`;;
102 let LEMMA_6 = VEC3_RULE
104 ==> ~(u cross basis 1 = vec 0) \/
105 ~(u cross basis 2 = vec 0) \/
106 ~(u cross basis 3 = vec 0)`;;
108 let LEMMA_7 = VEC3_RULE
109 `!u v w. (u cross v = vec 0) ==> (u dot (v cross w) = &0)`;;
111 let NORMAL_EXISTS = prove
112 (`!u v:real^3. ?w. ~(w = vec 0) /\ orthogonal u w /\ orthogonal v w`,
113 REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
114 [`u:real^3 = vec 0`; `v:real^3 = vec 0`; `u cross v = vec 0`] THEN
115 ASM_REWRITE_TAC[orthogonal] THEN
116 ASM_MESON_TAC[LEMMA_0; LEMMA_1; LEMMA_2; LEMMA_3; LEMMA_4;
117 LEMMA_5; LEMMA_6; LEMMA_7]);;