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