1 needs "Tutorial/Vectors.ml";;
3 let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir")
4 (MESON[LEMMA_0] `?x:real^3. ~(x = vec 0)`);;
6 parse_as_infix("||",(11,"right"));;
7 parse_as_infix("_|_",(11,"right"));;
9 let perpdir = new_definition
10 `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
12 let pardir = new_definition
13 `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
15 let DIRECTION_CLAUSES = prove
16 (`((!x. P(dest_dir x)) <=> (!x. ~(x = vec 0) ==> P x)) /\
17 ((?x. P(dest_dir x)) <=> (?x. ~(x = vec 0) /\ P x))`,
18 MESON_TAC[direction_tybij]);;
20 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
22 (!x y. x || y <=> y || x) /\
23 (!x y z. x || y /\ y || z ==> x || z)`,
24 REWRITE_TAC[pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
26 let DIRECTION_AXIOM_1 = prove
27 (`!p p'. ~(p || p') ==> ?l. p _|_ l /\ p' _|_ l /\
28 !l'. p _|_ l' /\ p' _|_ l' ==> l' || l`,
29 REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN REPEAT STRIP_TAC THEN
30 MP_TAC(SPECL [`p:real^3`; `p':real^3`] NORMAL_EXISTS) THEN
31 MATCH_MP_TAC MONO_EXISTS THEN
32 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
34 let DIRECTION_AXIOM_2 = prove
35 (`!l l'. ?p. p _|_ l /\ p _|_ l'`,
36 REWRITE_TAC[perpdir; DIRECTION_CLAUSES] THEN
37 MESON_TAC[NORMAL_EXISTS; ORTHOGONAL_SYM]);;
39 let DIRECTION_AXIOM_3 = prove
41 ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
42 ~(?l. p _|_ l /\ p' _|_ l /\ p'' _|_ l)`,
43 REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN
44 MAP_EVERY (fun t -> EXISTS_TAC t THEN REWRITE_TAC[LEMMA_0])
45 [`basis 1 :real^3`; `basis 2 : real^3`; `basis 3 :real^3`] THEN
48 let CROSS_0 = VEC3_RULE `x cross vec 0 = vec 0 /\ vec 0 cross x = vec 0`;;
50 let DIRECTION_AXIOM_4_WEAK = prove
51 (`!l. ?p p'. ~(p || p') /\ p _|_ l /\ p' _|_ l`,
52 REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN REPEAT STRIP_TAC THEN
54 `orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 2) l /\
55 ~((l cross basis 1) cross (l cross basis 2) = vec 0) \/
56 orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 3) l /\
57 ~((l cross basis 1) cross (l cross basis 3) = vec 0) \/
58 orthogonal (l cross basis 2) l /\ orthogonal (l cross basis 3) l /\
59 ~((l cross basis 2) cross (l cross basis 3) = vec 0)`
60 MP_TAC THENL [POP_ASSUM MP_TAC THEN VEC3_TAC; MESON_TAC[CROSS_0]]);;
62 let ORTHOGONAL_COMBINE = prove
63 (`!x a b. a _|_ x /\ b _|_ x /\ ~(a || b)
64 ==> ?c. c _|_ x /\ ~(a || c) /\ ~(b || c)`,
65 REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN
66 REPEAT STRIP_TAC THEN EXISTS_TAC `a + b:real^3` THEN
67 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
69 let DIRECTION_AXIOM_4 = prove
70 (`!l. ?p p' p''. ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
71 p _|_ l /\ p' _|_ l /\ p'' _|_ l`,
72 MESON_TAC[DIRECTION_AXIOM_4_WEAK; ORTHOGONAL_COMBINE]);;
74 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
76 let PERPDIR_WELLDEF = prove
77 (`!x y x' y'. x || x' /\ y || y' ==> (x _|_ y <=> x' _|_ y')`,
78 REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
81 lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
82 "perpl" PERPDIR_WELLDEF;;
84 let line_lift_thm = lift_theorem line_tybij
85 (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
87 let LINE_AXIOM_1 = line_lift_thm DIRECTION_AXIOM_1;;
88 let LINE_AXIOM_2 = line_lift_thm DIRECTION_AXIOM_2;;
89 let LINE_AXIOM_3 = line_lift_thm DIRECTION_AXIOM_3;;
90 let LINE_AXIOM_4 = line_lift_thm DIRECTION_AXIOM_4;;
92 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
93 (prove(`?x:line. T`,REWRITE_TAC[]));;
95 parse_as_infix("on",(11,"right"));;
97 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
99 let POINT_CLAUSES = prove
100 (`((p = p') <=> (dest_point p = dest_point p')) /\
101 ((!p. P (dest_point p)) <=> (!l. P l)) /\
102 ((?p. P (dest_point p)) <=> (?l. P l))`,
103 MESON_TAC[point_tybij]);;
105 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
108 (`!p p'. ~(p = p') ==> ?l. p on l /\ p' on l /\
109 !l'. p on l' /\ p' on l' ==> (l' = l)`,
110 POINT_TAC LINE_AXIOM_1);;
113 (`!l l'. ?p. p on l /\ p on l'`,
114 POINT_TAC LINE_AXIOM_2);;
117 (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
118 ~(?l. p on l /\ p' on l /\ p'' on l)`,
119 POINT_TAC LINE_AXIOM_3);;
122 (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
123 p on l /\ p' on l /\ p'' on l`,
124 POINT_TAC LINE_AXIOM_4);;