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;;