Update from HH
[hl193./.git] / Multivariate / wlog.ml
1 (* ========================================================================= *)
2 (* Geometric "without loss of generality" tactics to pick convenient coords. *)
3 (* ========================================================================= *)
4
5 needs "Multivariate/determinants.ml";;
6 needs "Multivariate/convex.ml";;
7
8 (* ------------------------------------------------------------------------- *)
9 (* Flyspeck definition of plane, and its invariance theorems.                *)
10 (* ------------------------------------------------------------------------- *)
11
12 let plane = new_definition
13   `plane x = (?u v w. ~(collinear {u,v,w}) /\ x = affine hull {u,v,w})`;;
14
15 let PLANE_TRANSLATION_EQ = prove
16  (`!a:real^N s. plane(IMAGE (\x. a + x) s) <=> plane s`,
17   REWRITE_TAC[plane] THEN GEOM_TRANSLATE_TAC[]);;
18
19 let PLANE_TRANSLATION = prove
20  (`!a:real^N s. plane s ==> plane(IMAGE (\x. a + x) s)`,
21   REWRITE_TAC[PLANE_TRANSLATION_EQ]);;
22
23 add_translation_invariants [PLANE_TRANSLATION_EQ];;
24
25 let PLANE_LINEAR_IMAGE_EQ = prove
26  (`!f:real^M->real^N p.
27         linear f /\ (!x y. f x = f y ==> x = y)
28         ==> (plane(IMAGE f p) <=> plane p)`,
29   REPEAT STRIP_TAC THEN REWRITE_TAC[plane] THEN
30   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
31    `?u. u IN IMAGE f (:real^M) /\
32         ?v. v IN IMAGE f (:real^M) /\
33             ?w. w IN IMAGE (f:real^M->real^N) (:real^M) /\
34                 ~collinear {u, v, w} /\ IMAGE f p = affine hull {u, v, w}` THEN
35   CONJ_TAC THENL
36    [REWRITE_TAC[RIGHT_AND_EXISTS_THM; IN_IMAGE; IN_UNIV] THEN
37     REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
38     EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
39     SUBGOAL_THEN `{u,v,w} SUBSET IMAGE (f:real^M->real^N) p` MP_TAC THENL
40      [ASM_REWRITE_TAC[HULL_SUBSET]; SET_TAC[]];
41     REWRITE_TAC[EXISTS_IN_IMAGE; IN_UNIV] THEN
42     REWRITE_TAC[SET_RULE `{f a,f b,f c} = IMAGE f {a,b,c}`] THEN
43     ASM_SIMP_TAC[AFFINE_HULL_LINEAR_IMAGE] THEN
44     REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN BINOP_TAC THENL
45      [ASM_MESON_TAC[COLLINEAR_LINEAR_IMAGE_EQ]; ASM SET_TAC[]]]);;
46
47 let PLANE_LINEAR_IMAGE = prove
48  (`!f:real^M->real^N p.
49         linear f /\ plane p /\ (!x y. f x = f y ==> x = y)
50         ==> plane(IMAGE f p)`,
51   MESON_TAC[PLANE_LINEAR_IMAGE_EQ]);;
52
53 add_linear_invariants [PLANE_LINEAR_IMAGE_EQ];;
54
55 (* ------------------------------------------------------------------------- *)
56 (* Rotating and translating so a given plane in R^3 becomes {x | x$3 = &0}.  *)
57 (* ------------------------------------------------------------------------- *)
58
59 let ROTATION_PLANE_HORIZONTAL = prove
60  (`!s. plane s
61        ==>  ?a f. orthogonal_transformation f /\ det(matrix f) = &1 /\
62                   IMAGE f (IMAGE (\x. a + x) s) = {z:real^3 | z$3 = &0}`,
63   let lemma = prove
64    (`span {z:real^3 | z$3 = &0} = {z:real^3 | z$3 = &0}`,
65     REWRITE_TAC[SPAN_EQ_SELF; subspace; IN_ELIM_THM] THEN
66     SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT;
67              DIMINDEX_3; ARITH] THEN REAL_ARITH_TAC) in
68   REPEAT STRIP_TAC THEN
69   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [plane]) THEN
70   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
71   MAP_EVERY X_GEN_TAC [`a:real^3`; `b:real^3`; `c:real^3`] THEN
72   MAP_EVERY (fun t ->
73     ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
74                            ALL_TAC])
75    [`a:real^3 = b`; `a:real^3 = c`; `b:real^3 = c`] THEN
76   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC) THEN
77   ASM_SIMP_TAC[AFFINE_HULL_INSERT_SPAN; IN_INSERT; NOT_IN_EMPTY] THEN
78   EXISTS_TAC `--a:real^3` THEN
79   REWRITE_TAC[SET_RULE `IMAGE (\x:real^3. --a + x) {a + x | x | x IN s} =
80                         IMAGE (\x. --a + a + x) s`] THEN
81   REWRITE_TAC[VECTOR_ARITH `--a + a + x:real^3 = x`; IMAGE_ID] THEN
82   REWRITE_TAC[SET_RULE `{x - a:real^x | x = b \/ x = c} = {b - a,c - a}`] THEN
83   MP_TAC(ISPEC `span{b - a:real^3,c - a}`
84     ROTATION_LOWDIM_HORIZONTAL) THEN
85   REWRITE_TAC[DIMINDEX_3] THEN ANTS_TAC THENL
86    [MATCH_MP_TAC LET_TRANS THEN
87     EXISTS_TAC `CARD{b - a:real^3,c - a}` THEN
88     SIMP_TAC[DIM_SPAN; DIM_LE_CARD; FINITE_RULES] THEN
89     SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC;
90     ALL_TAC] THEN
91   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f:real^3->real^3` THEN
92   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
93   FIRST_ASSUM(ASSUME_TAC o MATCH_MP ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
94   ASM_SIMP_TAC[GSYM SPAN_LINEAR_IMAGE] THEN
95   GEN_REWRITE_TAC RAND_CONV [GSYM lemma] THEN
96   MATCH_MP_TAC DIM_EQ_SPAN THEN CONJ_TAC THENL
97    [ASM_MESON_TAC[IMAGE_SUBSET; SPAN_INC; SUBSET_TRANS]; ALL_TAC] THEN
98   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2` THEN CONJ_TAC THENL
99    [MP_TAC(ISPECL [`{z:real^3 | z$3 = &0}`; `(:real^3)`] DIM_EQ_SPAN) THEN
100     REWRITE_TAC[SUBSET_UNIV; DIM_UNIV; DIMINDEX_3; lemma] THEN
101     MATCH_MP_TAC(TAUT `~r /\ (~p ==> q) ==> (q ==> r) ==> p`) THEN
102     REWRITE_TAC[ARITH_RULE `~(x <= 2) <=> 3 <= x`] THEN
103     REWRITE_TAC[EXTENSION; SPAN_UNIV; IN_ELIM_THM] THEN
104     DISCH_THEN(MP_TAC o SPEC `vector[&0;&0;&1]:real^3`) THEN
105     REWRITE_TAC[IN_UNIV; VECTOR_3] THEN REAL_ARITH_TAC;
106     ALL_TAC] THEN
107   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `dim {b - a:real^3,c - a}` THEN
108   CONJ_TAC THENL
109    [ALL_TAC; ASM_MESON_TAC[LE_REFL; DIM_INJECTIVE_LINEAR_IMAGE;
110              ORTHOGONAL_TRANSFORMATION_INJECTIVE]] THEN
111   MP_TAC(ISPEC `{b - a:real^3,c - a}` INDEPENDENT_BOUND_GENERAL) THEN
112   SIMP_TAC[CARD_CLAUSES; FINITE_RULES; IN_SING; NOT_IN_EMPTY] THEN
113   ASM_REWRITE_TAC[VECTOR_ARITH `b - a:real^3 = c - a <=> b = c`; ARITH] THEN
114   DISCH_THEN MATCH_MP_TAC THEN
115   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE (RAND_CONV o RAND_CONV)
116     [SET_RULE `{a,b,c} = {b,a,c}`]) THEN
117   REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN
118   REWRITE_TAC[independent; CONTRAPOS_THM; dependent] THEN
119   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; RIGHT_OR_DISTRIB] THEN
120   REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2] THEN
121   ASM_SIMP_TAC[SET_RULE `~(a = b) ==> {a,b} DELETE b = {a}`;
122                SET_RULE `~(a = b) ==> {a,b} DELETE a = {b}`;
123                VECTOR_ARITH `b - a:real^3 = c - a <=> b = c`] THEN
124   REWRITE_TAC[SPAN_BREAKDOWN_EQ; SPAN_EMPTY; IN_SING] THEN
125   ONCE_REWRITE_TAC[VECTOR_SUB_EQ] THEN MESON_TAC[COLLINEAR_LEMMA; INSERT_AC]);;
126
127 let ROTATION_HORIZONTAL_PLANE = prove
128  (`!p. plane p
129        ==>  ?a f. orthogonal_transformation f /\ det(matrix f) = &1 /\
130                   IMAGE (\x. a + x) (IMAGE f {z:real^3 | z$3 = &0}) = p`,
131   REPEAT STRIP_TAC THEN
132   FIRST_X_ASSUM(MP_TAC o MATCH_MP ROTATION_PLANE_HORIZONTAL) THEN
133   DISCH_THEN(X_CHOOSE_THEN `a:real^3`
134    (X_CHOOSE_THEN `f:real^3->real^3` STRIP_ASSUME_TAC)) THEN
135   FIRST_ASSUM(X_CHOOSE_THEN `g:real^3->real^3` STRIP_ASSUME_TAC o MATCH_MP
136     ORTHOGONAL_TRANSFORMATION_INVERSE) THEN
137   MAP_EVERY EXISTS_TAC [`--a:real^3`; `g:real^3->real^3`] THEN
138   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
139   ASM_REWRITE_TAC[GSYM IMAGE_o; o_DEF; IMAGE_ID;
140                   VECTOR_ARITH `--a + a + x:real^3 = x`] THEN
141   MATCH_MP_TAC(REAL_RING `!f. f * g = &1 /\ f = &1 ==> g = &1`) THEN
142   EXISTS_TAC `det(matrix(f:real^3->real^3))` THEN
143   REWRITE_TAC[GSYM DET_MUL] THEN
144   ASM_SIMP_TAC[GSYM MATRIX_COMPOSE; ORTHOGONAL_TRANSFORMATION_LINEAR] THEN
145   ASM_REWRITE_TAC[o_DEF; MATRIX_ID; DET_I]);;
146
147 (* ------------------------------------------------------------------------- *)
148 (* Apply plane rotation to a goal.                                           *)
149 (* ------------------------------------------------------------------------- *)
150
151 let GEOM_HORIZONTAL_PLANE_RULE =
152   let ifn = MATCH_MP
153    (TAUT `(p ==> (x <=> x')) /\ (~p ==> (x <=> T)) ==> (x' ==> x)`)
154   and pth = prove
155    (`!a f. orthogonal_transformation (f:real^N->real^N)
156            ==> ((!P. (!x. P x) <=> (!x. P (a + f x))) /\
157                 (!P. (?x. P x) <=> (?x. P (a + f x))) /\
158                 (!Q. (!s. Q s) <=> (!s. Q (IMAGE (\x. a + x) (IMAGE f s)))) /\
159                 (!Q. (?s. Q s) <=> (?s. Q (IMAGE (\x. a + x) (IMAGE f s))))) /\
160                (!P. {x | P x} =
161                     IMAGE (\x. a + x) (IMAGE f {x | P(a + f x)}))`,
162     REPEAT GEN_TAC THEN DISCH_TAC THEN
163     MP_TAC(ISPEC `(\x. a + x) o (f:real^N->real^N)`
164       QUANTIFY_SURJECTION_THM) THEN REWRITE_TAC[o_THM; IMAGE_o] THEN
165     DISCH_THEN MATCH_MP_TAC THEN
166     ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_SURJECTIVE;
167                   VECTOR_ARITH `a + (x - a:real^N) = x`])
168   and cth = prove
169    (`!a f. {} = IMAGE (\x:real^3. a + x) (IMAGE f {})`,
170     REWRITE_TAC[IMAGE_CLAUSES])
171   and oth = prove
172    (`!f:real^3->real^3.
173         orthogonal_transformation f /\ det(matrix f) = &1
174         ==> linear f /\
175             (!x y. f x = f y ==> x = y) /\
176             (!y. ?x. f x = y) /\
177             (!x. norm(f x) = norm x) /\
178             (2 <= dimindex(:3) ==> det(matrix f) = &1)`,
179     GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
180      [ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR];
181       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_INJECTIVE];
182       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_SURJECTIVE];
183       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION]])
184   and fth = MESON[]
185    `(!a f. q a f ==> (p <=> p' a f))
186     ==> ((?a f. q a f) ==> (p <=> !a f. q a f ==> p' a f))` in
187   fun tm ->
188     let x,bod = dest_forall tm in
189     let th1 = EXISTS_GENVAR_RULE
190       (UNDISCH(ISPEC x ROTATION_HORIZONTAL_PLANE)) in
191     let [a;f],tm1 = strip_exists(concl th1) in
192     let [th_orth;th_det;th_im] = CONJUNCTS(ASSUME tm1) in
193     let th2 = PROVE_HYP th_orth (UNDISCH(ISPECL [a;f] pth)) in
194     let th3 = (EXPAND_QUANTS_CONV(ASSUME(concl th2)) THENC
195                SUBS_CONV[GSYM th_im; ISPECL [a;f] cth]) bod in
196     let th4 = PROVE_HYP th2 th3 in
197     let th5 = TRANSLATION_INVARIANTS a in
198     let th6 = GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV)
199                 [ASSUME(concl th5)] th4 in
200     let th7 = PROVE_HYP th5 th6 in
201     let th8s = CONJUNCTS(MATCH_MP oth (CONJ th_orth th_det)) in
202     let th9 = LINEAR_INVARIANTS f th8s in
203     let th10 = GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV) [th9] th7 in
204     let th11 = if intersect (frees(concl th10)) [a;f] = []
205                then PROVE_HYP th1 (itlist SIMPLE_CHOOSE [a;f] th10)
206                else MP (MATCH_MP fth (GENL [a;f] (DISCH_ALL th10))) th1 in
207     let th12 = REWRITE_CONV[ASSUME(mk_neg(hd(hyp th11)))] bod in
208     let th13 = ifn(CONJ (DISCH_ALL th11) (DISCH_ALL th12)) in
209     let th14 = MATCH_MP MONO_FORALL (GEN x th13) in
210     GEN_REWRITE_RULE (TRY_CONV o LAND_CONV) [FORALL_SIMP] th14;;
211
212 let GEOM_HORIZONTAL_PLANE_TAC p =
213   W(fun (asl,w) ->
214         let avs,bod = strip_forall w
215         and avs' = subtract (frees w) (freesl(map (concl o snd) asl)) in
216         let avs,bod = strip_forall w in
217         MAP_EVERY X_GEN_TAC avs THEN
218         MAP_EVERY (fun t -> SPEC_TAC(t,t)) (rev(subtract (avs@avs') [p])) THEN
219         SPEC_TAC(p,p) THEN
220         W(MATCH_MP_TAC o GEOM_HORIZONTAL_PLANE_RULE o snd));;
221
222 (* ------------------------------------------------------------------------- *)
223 (* Injection from real^2 -> real^3 plane with zero last coordinate.          *)
224 (* ------------------------------------------------------------------------- *)
225
226 let pad2d3d = new_definition
227  `(pad2d3d:real^2->real^3) x = lambda i. if i < 3 then x$i else &0`;;
228
229 let FORALL_PAD2D3D_THM = prove
230  (`!P. (!y:real^3. y$3 = &0 ==> P y) <=> (!x. P(pad2d3d x))`,
231   GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
232    [FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[pad2d3d] THEN
233     SIMP_TAC[LAMBDA_BETA; DIMINDEX_3; ARITH; LT_REFL];
234     FIRST_X_ASSUM(MP_TAC o SPEC `(lambda i. (y:real^3)$i):real^2`) THEN
235     MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
236     SIMP_TAC[CART_EQ; pad2d3d; DIMINDEX_3; ARITH; LAMBDA_BETA; DIMINDEX_2;
237              ARITH_RULE `i < 3 <=> i <= 2`] THEN
238     REWRITE_TAC[ARITH_RULE `i <= 3 <=> i <= 2 \/ i = 3`] THEN
239     ASM_MESON_TAC[]]);;
240
241 let QUANTIFY_PAD2D3D_THM = prove
242  (`(!P. (!y:real^3. y$3 = &0 ==> P y) <=> (!x. P(pad2d3d x))) /\
243    (!P. (?y:real^3. y$3 = &0 /\ P y) <=> (?x. P(pad2d3d x)))`,
244   REWRITE_TAC[MESON[] `(?y. P y) <=> ~(!x. ~P x)`] THEN
245   REWRITE_TAC[GSYM FORALL_PAD2D3D_THM] THEN MESON_TAC[]);;
246
247 let LINEAR_PAD2D3D = prove
248  (`linear pad2d3d`,
249   REWRITE_TAC[linear; pad2d3d] THEN
250   SIMP_TAC[CART_EQ; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
251            LAMBDA_BETA; DIMINDEX_2; DIMINDEX_3; ARITH;
252            ARITH_RULE `i < 3 ==> i <= 2`] THEN
253   REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
254   REAL_ARITH_TAC);;
255
256 let INJECTIVE_PAD2D3D = prove
257  (`!x y. pad2d3d x = pad2d3d y ==> x = y`,
258   SIMP_TAC[CART_EQ; pad2d3d; LAMBDA_BETA; DIMINDEX_3; DIMINDEX_2] THEN
259   REWRITE_TAC[ARITH_RULE `i < 3 <=> i <= 2`] THEN
260   MESON_TAC[ARITH_RULE `i <= 2 ==> i <= 3`]);;
261
262 let NORM_PAD2D3D = prove
263  (`!x. norm(pad2d3d x) = norm x`,
264   SIMP_TAC[NORM_EQ; DOT_2; DOT_3; pad2d3d; LAMBDA_BETA;
265            DIMINDEX_2; DIMINDEX_3; ARITH] THEN
266   REAL_ARITH_TAC);;
267
268 (* ------------------------------------------------------------------------- *)
269 (* Apply 3D->2D conversion to a goal. Take care to preserve variable names.  *)
270 (* ------------------------------------------------------------------------- *)
271
272 let PAD2D3D_QUANTIFY_CONV =
273   let gv = genvar `:real^2` in
274   let pth = CONV_RULE (BINOP_CONV(BINDER_CONV(RAND_CONV(GEN_ALPHA_CONV gv))))
275                       QUANTIFY_PAD2D3D_THM in
276   let conv1 = GEN_REWRITE_CONV I [pth]
277   and dest_quant tm = try dest_forall tm with Failure _ -> dest_exists tm in
278   fun tm ->
279     let th = conv1 tm in
280     let name = fst(dest_var(fst(dest_quant tm))) in
281     let ty = snd(dest_var(fst(dest_quant(rand(concl th))))) in
282     CONV_RULE(RAND_CONV(GEN_ALPHA_CONV(mk_var(name,ty)))) th;;
283
284 let PAD2D3D_TAC =
285   let pad2d3d_tm = `pad2d3d`
286   and pths = [LINEAR_PAD2D3D; INJECTIVE_PAD2D3D; NORM_PAD2D3D]
287   and cth = prove
288    (`{} = IMAGE pad2d3d {} /\
289      vec 0 = pad2d3d(vec 0)`,
290     REWRITE_TAC[IMAGE_CLAUSES] THEN MESON_TAC[LINEAR_PAD2D3D; LINEAR_0]) in
291   let lasttac =
292     GEN_REWRITE_TAC REDEPTH_CONV [LINEAR_INVARIANTS pad2d3d_tm pths] in
293   fun gl -> (GEN_REWRITE_TAC ONCE_DEPTH_CONV [cth] THEN
294              CONV_TAC(DEPTH_CONV PAD2D3D_QUANTIFY_CONV) THEN
295              lasttac) gl;;
296
297 (* ------------------------------------------------------------------------- *)
298 (* Rotating so a given line from the origin becomes the x-axis.              *)
299 (* ------------------------------------------------------------------------- *)
300
301 let ROTATION_HORIZONTAL_LINE = prove
302  (`!a:real^N.
303         ?b f. orthogonal_transformation f /\ det(matrix f) = &1 /\ f b = a /\
304               (!k. 1 < k /\ k <= dimindex(:N) ==> b$k = &0)`,
305   GEN_TAC THEN ASM_CASES_TAC `dimindex(:N) = 1` THENL
306    [MAP_EVERY EXISTS_TAC [`a:real^N`; `\x:real^N. x`] THEN
307     ASM_SIMP_TAC[DET_I; MATRIX_ID; ORTHOGONAL_TRANSFORMATION_ID; LTE_ANTISYM];
308     EXISTS_TAC `norm(a:real^N) % (basis 1):real^N` THEN
309     SIMP_TAC[VECTOR_MUL_COMPONENT; LT_IMP_LE; BASIS_COMPONENT] THEN
310     SIMP_TAC[ARITH_RULE `1 < k ==> ~(k = 1)`; REAL_MUL_RZERO] THEN
311     MATCH_MP_TAC ROTATION_EXISTS THEN
312     SIMP_TAC[NORM_MUL; NORM_BASIS; LE_REFL; DIMINDEX_GE_1] THEN
313     REWRITE_TAC[REAL_ABS_NORM; REAL_MUL_RID] THEN
314     MATCH_MP_TAC(ARITH_RULE `~(n = 1) /\ 1 <= n ==> 2 <= n`) THEN
315     ASM_REWRITE_TAC[DIMINDEX_GE_1]]);;
316
317 let GEOM_HORIZONTAL_LINE_RULE =
318   let pth = prove
319    (`!f. orthogonal_transformation (f:real^N->real^N)
320          ==> (vec 0 = f(vec 0) /\ {} = IMAGE f {}) /\
321              ((!P. (!x. P x) <=> (!x. P (f x))) /\
322               (!P. (?x. P x) <=> (?x. P (f x))) /\
323               (!Q. (!s. Q s) <=> (!s. Q (IMAGE f s))) /\
324               (!Q. (?s. Q s) <=> (?s. Q (IMAGE f s)))) /\
325              (!P. {x | P x} = IMAGE f {x | P(f x)})`,
326     REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IMAGE_CLAUSES] THEN
327     CONJ_TAC THENL
328      [FIRST_X_ASSUM(MP_TAC o MATCH_MP ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
329       MESON_TAC[LINEAR_0];
330       MATCH_MP_TAC QUANTIFY_SURJECTION_THM THEN
331       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_SURJECTIVE]])
332   and oth = prove
333    (`!f:real^N->real^N.
334         orthogonal_transformation f /\ det(matrix f) = &1
335         ==> linear f /\
336             (!x y. f x = f y ==> x = y) /\
337             (!y. ?x. f x = y) /\
338             (!x. norm(f x) = norm x) /\
339             (2 <= dimindex(:N) ==> det(matrix f) = &1)`,
340     GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
341      [ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR];
342       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_INJECTIVE];
343       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_SURJECTIVE];
344       ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION]])
345     and sth = prove
346    (`((!k. 1 < k /\ k <= dimindex(:2) ==> b$k = &0) <=> b$2 = &0) /\
347      ((!k. 1 < k /\ k <= dimindex(:3) ==> b$k = &0) <=> b$2 = &0 /\ b$3 = &0)`,
348     REWRITE_TAC[DIMINDEX_2; DIMINDEX_3;
349                 ARITH_RULE `k <= 3 <=> k = 3 \/ k <= 2`;
350                 ARITH_RULE `k <= 2 <=> k = 2 \/ ~(1 < k)`] THEN
351     MESON_TAC[ARITH_RULE `1 < 2 /\ 1 < 3`]) in
352   let sfn = GEN_REWRITE_RULE ONCE_DEPTH_CONV [sth] in
353   fun tm ->
354     let x,bod = dest_forall tm in
355     let th1 = EXISTS_GENVAR_RULE
356      (sfn(ISPEC x ROTATION_HORIZONTAL_LINE)) in
357     let [a;f],tm1 = strip_exists(concl th1) in
358     let th_orth,th2 = CONJ_PAIR(ASSUME tm1) in
359     let th_det,th2a = CONJ_PAIR th2 in
360     let th_works,th_zero = CONJ_PAIR th2a in
361     let thc,thq = CONJ_PAIR(PROVE_HYP th2 (UNDISCH(ISPEC f pth))) in
362     let th3 = CONV_RULE(RAND_CONV(SUBS_CONV(GSYM th_works::CONJUNCTS thc)))
363                (EXPAND_QUANTS_CONV(ASSUME(concl thq)) bod) in
364     let th4 = PROVE_HYP thq th3 in
365     let thps = CONJUNCTS(MATCH_MP oth (CONJ th_orth th_det)) in
366     let th5 = LINEAR_INVARIANTS f thps in
367     let th6 = PROVE_HYP th_orth
368      (GEN_REWRITE_RULE (RAND_CONV o REDEPTH_CONV) [th5] th4) in
369     let ntm = mk_forall(a,mk_imp(concl th_zero,rand(concl th6))) in
370     let th7 = MP(SPEC a (ASSUME ntm)) th_zero in
371     let th8 = DISCH ntm (EQ_MP (SYM th6) th7) in
372     if intersect (frees(concl th8)) [a;f] = [] then
373       let th9 = PROVE_HYP th1 (itlist SIMPLE_CHOOSE [a;f] th8) in
374       let th10 = DISCH ntm (GEN x (UNDISCH th9)) in
375       CONV_RULE(LAND_CONV (GEN_ALPHA_CONV x)) th10
376     else
377       let mtm = list_mk_forall([a;f],mk_imp(hd(hyp th8),rand(concl th6))) in
378       let th9 = EQ_MP (SYM th6) (UNDISCH(SPECL [a;f] (ASSUME mtm))) in
379       let th10 = itlist SIMPLE_CHOOSE [a;f] (DISCH mtm th9) in
380       let th11 = GEN x (PROVE_HYP th1 th10) in
381       MATCH_MP MONO_FORALL th11;;
382
383 let GEOM_HORIZONTAL_LINE_TAC l (asl,w as gl) =
384   let avs,bod = strip_forall w
385   and avs' = subtract (frees w) (freesl(map (concl o snd) asl)) in
386   (MAP_EVERY X_GEN_TAC avs THEN
387    MAP_EVERY (fun t -> SPEC_TAC(t,t)) (rev(subtract (avs@avs') [l])) THEN
388    SPEC_TAC(l,l) THEN
389    W(MATCH_MP_TAC o GEOM_HORIZONTAL_LINE_RULE o snd)) gl;;