Update from HH

[Flyspeck/.git] / text_formalization / local / WJSCPRO.hl

\r
(* ========================================================================== *)\r
(* FLYSPECK - BOOK FORMALIZATION                                              *)\r
(*                                                                            *)\r
(* Chapter: Local Fan                                              *)\r
(* Author: Hoang Le Truong                                        *)\r
(* Date: 2012-04-01                                                           *)\r
(* ========================================================================= *)\r
\r
\r
\r
\r
module   Wjscpro = struct\r
\r
\r
\r
\r
\r
open Polyhedron;;\r
open Sphere;;\r
open Fan_defs;;\r
open Hypermap;;\r
open Vol1;;\r
open Fan;;\r
open Topology;;         \r
open Fan_misc;;\r
open Planarity;; \r
open Conforming;;\r
open Sphere;;\r
open Hypermap;;\r
open Fan;;\r
open Topology;;\r
open Prove_by_refinement;;\r
open Pack_defs;;\r
open Wrgcvdr_cizmrrh;;\r
open Local_lemmas;;\r
open Collect_geom;;\r
open Dih2k_hypermap;;\r
\r
\r
\r
let POWER_MOD_FUN=prove(`!n. 1<=n /\ 1<k ==> ((\i. ((1+i):num MOD k)) POWER n) i = (\i. ((n+i):num MOD k)) i`,\r
INDUCT_TAC\r
THENL[ARITH_TAC;\r
DISJ_CASES_TAC(ARITH_RULE`n=0 \/ 1<=n`)\r
THENL[\r
ASM_REWRITE_TAC[POWER;I_DEF;ARITH_RULE`SUC 0=1`;o_DEF];\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY")\r
THEN STRIP_TAC THEN STRIP_TAC\r
THEN REMOVE_THEN "THY" MP_TAC\r
THEN RESA_TAC\r
THEN ASM_REWRITE_TAC[COM_POWER;o_DEF;ADD1;MOD_ADD_MOD]\r
THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`)\r
THEN RESA_TAC\r
THEN MRESA_TAC MOD_LT[`1:num`;`k:num`]\r
THEN MRESAL_TAC MOD_ADD_MOD[`1`;`n+i:num`;`k:num`][ARITH_RULE`(n + 1) + i=1+n+i`]]]);;\r
\r
\r
\r
\r
let CLOSED_SY=prove_by_refinement(`\r
stable_system k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)\r
/\ 1< k /\ 2<k\r
==> \r
closed {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v /\ CONDITION2_SY v }`,\r
[REWRITE_TAC[CONDITION2_SY;CONDITION1_SY;stable_system]\r
THEN  REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN  REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist] \r
THEN REPEAT STRIP_TAC\r
THEN ASM_TAC\r
THEN DISCH_THEN(LABEL_TAC"THYGIANG2")\r
THEN DISCH_THEN(LABEL_TAC"THYGIANG")\r
THEN DISCH_THEN(LABEL_TAC"THYGIANG1")\r
THEN REPEAT STRIP_TAC\r
THEN EXISTS_TAC`vecmats (l:real^(M,3)finite_product)`\r
THEN SIMP_TAC[MATVEC_VECMATS_ID]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN   REWRITE_TAC[SKOLEM_THM]\r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN  DISCH_THEN(LABEL_TAC"THY1")\r
THEN  DISCH_THEN(LABEL_TAC"THY2")\r
THEN SUBGOAL_THEN`\r
!i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)\r
==>\r
((\n. row i (v n) - row j ((v:num->real^3^M) n)) --> row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product)))\r
 sequentially`ASSUME_TAC;\r
\r
SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]\r
THEN REPEAT STRIP_TAC\r
THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]\r
THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e/ &2:real`)\r
THEN POP_ASSUM MP_TAC\r
THEN  DISCH_THEN(LABEL_TAC"THY2")\r
THEN EXISTS_TAC`N:num`\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\  SUC(i-1)=i`)\r
THEN RESA_TAC\r
THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\  SUC(j-1)=j`)\r
THEN RESA_TAC\r
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`]\r
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[MATVEC_VECMATS_ID]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]\r
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`((v:num->real^3^M) n)`]\r
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`vecmats (l:real^(M,3)finite_product)`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[MATVEC_VECMATS_ID]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`j-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]\r
THEN MRESAL_TAC NORM_TRIANGLE[`row i ((v:num->real^3^M) n) - row i (vecmats (l:real^(M,3)finite_product))`;`--(row j ((v:num->real^3^M) n) - row j (vecmats (l:real^(M,3)finite_product)))`][NORM_NEG;VECTOR_ARITH`A+ --B=A-B:real^N` ]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
SUBGOAL_THEN`\r
!i. 1 <= i /\ i <= dimindex (:M) ==>\r
((\n. row i ((v:num->real^3^M) n)) --> row i (vecmats (l:real^(M,3)finite_product)))\r
 sequentially`ASSUME_TAC;\r
\r
SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]\r
THEN REPEAT STRIP_TAC\r
THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]\r
THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e:real`)\r
THEN POP_ASSUM MP_TAC\r
THEN  DISCH_THEN(LABEL_TAC"THY2")\r
THEN EXISTS_TAC`N:num`\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\  SUC(i-1)=i`)\r
THEN RESA_TAC\r
THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\  SUC(j-1)=j`)\r
THEN RESA_TAC\r
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`]\r
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[MATVEC_VECMATS_ID]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEU2")\r
THEN SUBGOAL_THEN`(!i j.\r
      1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)\r
      ==> (a:num#num->real) (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\\r
          norm (row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) <= (b:num#num->real) (i,j))` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC;\r
\r
MRESA_TAC LIM_NORM_LBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(a:num#num->real)(i,j)`]\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY];\r
\r
MRESA_TAC LIM_NORM_UBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(b:num#num->real)(i,j)`]\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY];\r
\r
ASM_REWRITE_TAC[]\r
THEN SUBGOAL_THEN`!i j.\r
          1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) /\ ~(i=j)\r
          ==> &2 <= norm (row i (vecmats (l:real^(M,3)finite_product)) - row j (vecmats l))` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY3")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY3"(fun th-> MRESA_TAC th[`i:num`;`j:num`])\r
THEN MATCH_MP_TAC(REAL_ARITH`a (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\ &2<= a(i,j)==> &2 <= norm (row i (vecmats l) - row j (vecmats l))`)\r
THEN MP_TAC(ARITH_RULE`i <= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`);\r
\r
RESA_TAC;\r
\r
MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`);\r
\r
RESA_TAC;\r
\r
REMOVE_THEN"THYGIANG"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`]);\r
\r
MP_TAC(ARITH_RULE`1<= i==> ~(i = 0)`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`])\r
THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`)\r
THEN RESA_TAC\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`];\r
\r
MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`);\r
\r
RESA_TAC;\r
\r
MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`)\r
THEN RESA_TAC\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`]);\r
\r
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th])\r
THEN SET_TAC[];\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY3")\r
THEN DISCH_THEN(LABEL_TAC"THY4")\r
THEN SUBGOAL_THEN`!i.\r
          1 <= i /\ i <= dimindex (:M)\r
          ==> norm (row i (vecmats (l:real^(M,3)finite_product)) - row (SUC (i MOD dimindex (:M))) (vecmats l))<= cstab` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN MP_TAC(ARITH_RULE`i<= dimindex (:M) ==> i< dimindex (:M) \/ i=dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
MP_TAC(ARITH_RULE`i< dimindex (:M) ==> i<= dimindex (:M) /\ i+1<=dimindex (:M) /\ i<= dimindex (:M)-1`)\r
THEN RESA_TAC\r
THEN MRESAL_TAC MOD_LT[`i:num`;`k:num`][ADD1]\r
THEN REMOVE_THEN "THY3"(fun th-> MRESAL_TAC th[`i:num`;`i+1:num`][ARITH_RULE`1<= i+1`])\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_THEN"THYGIANG1"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`0<= i:num`])\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`i+1:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`)\r
THEN RESA_TAC\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`i+1:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i+1`][ARITH_RULE`1*A=A`]\r
THEN STRIP_TAC\r
THEN ONCE_REWRITE_TAC[ARITH_RULE`A+1=1+A`]\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ SUC 0=1`]\r
THEN REMOVE_THEN "THY3"(fun th-> MRESAL_TAC th[`k:num`;`1:num`][ARITH_RULE`1<= 1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1])\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE` (1 <= dimindex (:M)) ==> 0 <= dimindex (:M) - 1` )\r
THEN SIMP_TAC[DIMINDEX_GE_1]\r
THEN STRIP_TAC\r
THEN REMOVE_THEN"THYGIANG1"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0<= 0:num/\ 0+1=1`;])\r
THEN POP_ASSUM MP_TAC\r
THEN MRESAL_TAC MOD_LT[`1:num`;`k:num`][ARITH_RULE`0<1`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k:num`;`1:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `] THEN\r
MRESAL_TAC th[`0:num`;`1:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`)\r
THEN RESA_TAC\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REAL_ARITH_TAC;\r
\r
SUBGOAL_THEN`(!i. 1 <= i /\ i <= dimindex (:M) ==> row i (vecmats (l:real^(M,3)finite_product)) IN ball_annulus)` ASSUME_TAC;\r
\r
MP_TAC COMPACT_BALL_ANNULUS\r
THEN ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED]\r
THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN  REWRITE_TAC[ IN_ELIM_THM; dist] \r
THEN   REWRITE_TAC[SKOLEM_THM]\r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEU")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`(\n. row i ((v:num->real^3^M) n)) `;` row i (vecmats (l:real^(M,3)finite_product))`])\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[];\r
\r
SUBGOAL_THEN`!i. 1 <= i /\ i <= dimindex (:M)\r
          ==> \r
              ~(row i (vecmats l) =\r
               row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))) `ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY5")\r
THEN REPEAT STRIP_TAC\r
THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`]\r
THEN REMOVE_THEN"THY5"(fun th-> MRESAL_TAC th[`i:num`;`SUC (i MOD dimindex (:M))`][VECTOR_ARITH`A-A = vec 0`;NORM_0])\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
ASM_REWRITE_TAC[convex_local_fan]\r
THEN ASM_REWRITE_TAC[local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN SUBGOAL_THEN `FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))`ASSUME_TAC;\r
\r
REWRITE_TAC[FAN]\r
THEN STRIP_TAC;\r
\r
REWRITE_TAC[SUBSET;UNIONS;E_SY;V_SY;IN_ELIM_THM;rows]\r
THEN REPEAT STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B \/ A=C`]\r
THEN STRIP_TAC;\r
\r
EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
STRIP_TAC;\r
\r
REWRITE_TAC[GRAPH;E_SY;IN_ELIM_THM]\r
THEN REPEAT STRIP_TAC\r
THEN ASM_REWRITE_TAC[HAS_SIZE]\r
THEN ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY           ;      IN_INSERT; NOT_IN_EMPTY]\r
THEN ARITH_TAC;\r
\r
STRIP_TAC;\r
\r
REWRITE_TAC[fan1;V_SY;rows]\r
THEN STRIP_TAC;\r
\r
MRESAL_TAC FINITE_IMAGE[`(\i. row i (vecmats (l:real^(M,3)finite_product)))`;`1..k`][IMAGE;IN_ELIM_THM;FINITE_NUMSEG;IN_NUMSEG]\r
THEN POP_ASSUM MP_TAC\r
THEN SUBGOAL_THEN`{y | ?x. (1 <= x /\ x <= dimindex (:M)) /\ y = row x (vecmats l)}={row i (vecmats (l:real^(M,3)finite_product)) | 1 <= i /\ i <= dimindex (:M)}`ASSUME_TAC;\r
\r
REWRITE_TAC[EXTENSION;IN_ELIM_THM];\r
\r
ASM_REWRITE_TAC[];\r
\r
REWRITE_TAC[SET_RULE`~(A SUBSET {})<=> ?a. a IN A`;IN_ELIM_THM]\r
THEN EXISTS_TAC`row 1(vecmats (l:real^(M,3)finite_product))`\r
THEN EXISTS_TAC`1`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1`;DIMINDEX_GE_1];\r
\r
STRIP_TAC;\r
\r
REWRITE_TAC[fan2;V_SY;IN_ELIM_THM;rows;NOT_EXISTS_THM;DE_MORGAN_THM]\r
THEN REPEAT STRIP_TAC\r
THEN DISJ_CASES_TAC(SET_RULE`~(1<= i) \/ 1<= i`);\r
\r
ASM_REWRITE_TAC[];\r
\r
DISJ_CASES_TAC(SET_RULE`~(i<= dimindex (:M)) \/ i<= dimindex (:M)`);\r
\r
ASM_REWRITE_TAC[];\r
\r
ASM_REWRITE_TAC[]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUEM")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"YEUEM"(fun th-> MRESAL1_TAC th `i:num`[ball_annulus;IN_ELIM_THM])\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIFF;IN_ELIM_THM;ball;DE_MORGAN_THM;dist;VECTOR_ARITH`vec 0- vec 0=vec 0`;NORM_0;REAL_ARITH`&0< &2`]);\r
\r
SUBGOAL_THEN`!i. (1 <= i /\ i <= dimindex (:M)) \r
                 ==> ~collinear ({vec 0} UNION {row i (vecmats l), row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))})`ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_REWRITE_TAC[]\r
THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS\r
THEN ASM_SIMP_TAC[]\r
THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`]\r
THEN ASM_SIMP_TAC[];\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`]\r
THEN REPEAT STRIP_TAC;\r
\r
REWRITE_TAC[fan6;E_SY;IN_ELIM_THM]\r
THEN REPEAT STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_REWRITE_TAC[]\r
THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS\r
THEN ASM_SIMP_TAC[]\r
THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`]\r
THEN ASM_SIMP_TAC[];\r
\r
REWRITE_TAC[fan7;]\r
THEN SUBGOAL_THEN`!i. 1 <= i /\ i <= dimindex (:M)\r
          ==> ~(vec 0= row i (vecmats l)) /\ ~(vec 0 = row (SUC (i MOD dimindex (:M)))(vecmats (l:real^(M,3)finite_product)))`ASSUME_TAC;\r
\r
STRIP_TAC\r
THEN STRIP_TAC\r
THEN MRESA_TAC th3[`(vec 0):real^3`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[];\r
\r
SUBGOAL_THEN`!u w.\r
     u IN V_SY (vecmats l) /\\r
     w IN V_SY (vecmats (l:real^(M,3)finite_product))\r
     ==> aff_ge {vec 0} {u} INTER aff_ge {vec 0} {w} =\r
         aff_ge {vec 0} ({u} INTER {w})`ASSUME_TAC;\r
\r
REWRITE_TAC[V_SY;IN_ELIM_THM;rows]\r
THEN REPEAT STRIP_TAC\r
THEN DISJ_CASES_TAC(SET_RULE`u=w:real^3 \/  {u} INTER {w}={}`);\r
\r
POP_ASSUM(fun th-> REWRITE_TAC[th;SET_RULE`A INTER A=A`]);\r
\r
ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_REWRITE_TAC[SET_RULE`{u} INTER {w} = {} <=> ~(u=w) `;EXTENSION; INTER;IN_ELIM_THM;IN_SING]\r
THEN REPEAT STRIP_TAC\r
THEN EQ_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN MATCH_MP_TAC (GEN_ALL VEC0_BALL_ANNULUS)\r
THEN EXISTS_TAC`u:real^3`\r
THEN EXISTS_TAC`w:real^3`\r
THEN DISJ_CASES_TAC(SET_RULE`i=i':num \/ ~(i=i')`);\r
\r
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN SET_TAC[]);\r
\r
ASM_SIMP_TAC[];\r
\r
REPEAT STRIP_TAC\r
THEN ASM_REWRITE_TAC[ENDS_IN_HALFLINE];\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY50")\r
THEN DISCH_THEN(LABEL_TAC"THY5")\r
THEN DISCH_THEN(LABEL_TAC"THY55")\r
THEN DISCH_THEN(LABEL_TAC"THY6")\r
THEN DISCH_THEN(LABEL_TAC"THY7")\r
THEN DISCH_THEN(LABEL_TAC"THY8")\r
THEN SUBGOAL_THEN`!e1 v.\r
     e1 IN E_SY (vecmats l) /\  v IN V_SY (vecmats (l:real^(M,3)finite_product))\r
     ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} {v} =\r
         aff_ge {vec 0} (e1 INTER {v})` ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN REPEAT STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"GIANG")\r
THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats \r
(l:real^(M,3)finite_product))`\r
THEN ASM_REWRITE_TAC[]\r
THEN DISJ_CASES_TAC(SET_RULE`y= v' \/ z= v' \/ (~(v'=y)/\ ~(v'=z:real^3))`);\r
\r
ASM_REWRITE_TAC[SET_RULE`{A,B} INTER {A}={A}`]\r
THEN REMOVE_THEN "THY6"(fun th-> MRESA1_TAC th`i:num`)\r
THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN SET_TAC[];\r
\r
POP_ASSUM MP_TAC\r
THEN STRIP_TAC;\r
\r
ASM_REWRITE_TAC[SET_RULE`{A,B} INTER {B}={B}`]\r
THEN REMOVE_THEN "THY6"(fun th-> MRESA1_TAC th`i:num`)\r
THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN SET_TAC[];\r
\r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN "THY6"(fun th-> MRESA1_TAC th`i:num`)\r
THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`v':real^3`] THEN MRESA_TAC th[`z:real^3`;`v':real^3`])\r
THEN MP_TAC(SET_RULE`~(y= v') /\ ~(z= v') ==> {y} INTER {v':real^3}={}/\ {z} INTER {v':real^3}={} /\ {y,z} INTER {v':real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_REWRITE_TAC[SET_RULE`(A UNION B UNION C) INTER D=(A INTER D) UNION (B INTER D) UNION (C INTER D)`;SET_RULE`A UNION A=A`]\r
THEN REMOVE_THEN "THY50"(fun th-> MRESA1_TAC th`i:num`)\r
THEN USE_THEN"GIANG" MP_TAC\r
THEN REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN STRIP_TAC\r
THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\\r
      SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN "THY5"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MRESA1_TAC th`(SUC (i MOD dimindex (:M))):num`)\r
THEN DISJ_CASES_TAC(SET_RULE`i= i' \/ ~(i= i':num)`);\r
\r
POP_ASSUM( fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC);\r
\r
DISJ_CASES_TAC(SET_RULE`i'= SUC (i MOD dimindex (:M)) \/ ~(i'= SUC (i MOD dimindex (:M)):num)`);\r
\r
POP_ASSUM( fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC);\r
\r
\r
\r
\r
\r
\r
\r
\r
\r
\r
\r
MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`]\r
THEN REMOVE_THEN"THY4"(fun th-> MRESA_TAC th[`i':num`;`i:num`] THEN  MRESA_TAC th[`i':num`;`SUC (i MOD dimindex (:M)):num`] THEN  MRESA_TAC th[`i:num`;`SUC (i MOD dimindex (:M)):num`])\r
THEN DISJ_CASES_TAC(SET_RULE`collinear{vec 0, y, v':real^3}\/ ~collinear{vec 0, y, v':real^3}`);\r
\r
POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.collinear_fan22)[`vec 0:real^3`;`v':real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`]\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THY7"(fun th-> MRESA1_TAC th`i':num`)\r
THEN MRESAL_TAC Planarity.sym_line_fan[`vec 0:real^3`;`v':real^3`;`y:real^3`][SET_RULE`DISJOINT {x} {y,z} <=> ~(x=y)/\ ~(x=z)`]\r
THEN MRESA_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{vec 0:real^3}`;`{v':real^3}`][SET_RULE`{A} UNION {B}={A,B}`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_REWRITE_TAC[aff]\r
THEN STRIP_TAC\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {v'} SUBSET affine hull {vec 0, v'}\r
 /\ affine hull {vec 0, v'} INTER aff_gt {vec 0} {y, z} = {}\r
==>    aff_gt {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {v'} = {}`)\r
THEN RESA_TAC\r
THEN SET_TAC[];\r
\r
DISJ_CASES_TAC(SET_RULE`collinear{vec 0, z, v':real^3}\/ ~collinear{vec 0, z, v':real^3}`);\r
\r
POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.collinear_fan22)[`vec 0:real^3`;`v':real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`]\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THY7"(fun th-> MRESA1_TAC th`i':num`)\r
THEN MRESAL_TAC Planarity.sym_line_fan[`vec 0:real^3`;`v':real^3`;`z:real^3`][SET_RULE`DISJOINT {x} {y,z} <=> ~(x=y)/\ ~(x=z)`]\r
THEN MRESA_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{vec 0:real^3}`;`{v':real^3}`][SET_RULE`{A} UNION {B}={A,B}`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_REWRITE_TAC[aff]\r
THEN STRIP_TAC\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {v'} SUBSET affine hull {vec 0, v'}\r
 /\ affine hull {vec 0, v'} INTER aff_gt {vec 0} {z,y} = {}\r
==>    aff_gt {vec 0} { z:real^3,y} INTER aff_ge {vec 0} {v'} = {}`)\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN SET_TAC[];\r
\r
MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`v':real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`v':real^3`]\r
THEN MRESA_TAC (GEN_ALL AFF_GE_INTER_AFF_GT_EQ_EMPTY)[`v':real^3`;`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN ASM_REWRITE_TAC[]\r
THEN SET_TAC[];\r
\r
SUBGOAL_THEN`!e1 e2.\r
     e1 IN E_SY (vecmats l)  /\\r
     e2 IN E_SY (vecmats (l:real^(M,3)finite_product)) /\ (e1 INTER e2={})\r
     ==> aff_gt {vec 0} e1 INTER aff_gt {vec 0} e2 = {}` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEU")\r
THEN REPEAT GEN_TAC\r
THEN DISCH_TAC\r
THEN POP_ASSUM (fun th-> MP_TAC th\r
THEN REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MP_TAC th\r
THEN STRIP_TAC)\r
THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`y1=row i' (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`z1=row (SUC (i' MOD dimindex (:M))) (vecmats \r
(l:real^(M,3)finite_product))`\r
THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y1, z1}) \/ aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y1, z1:real^3}={}`);\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[INTER;IN_ELIM_THM]\r
THEN STRIP_TAC\r
THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6"))\r
THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`v3:real^3`;]\r
THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`z:real^3`;`y:real^3`;`v3:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`v3:real^3`;]\r
THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`z1:real^3`;`y1:real^3`;`v3:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN DISJ_CASES_TAC(REAL_ARITH`(v3 cross y:real^3) dot y1 = &0 \/ &0< (v3 cross y) dot y1  \/ &0< --((v3 cross y) dot y1)`);\r
\r
MRESAL_TAC (GEN_ALL Local_lemmas.COPLANAR_IFF_CROSS_DOT)[`y:real^3`;`v3:real^3`;`y1:real^3`;`vec 0:real^3`;][VECTOR_ARITH`A- vec 0=A`]\r
THEN SUBGOAL_THEN`y1 IN aff {vec 0, v3,y:real^3}` ASSUME_TAC;\r
\r
ASM_SIMP_TAC[Conforming.aff_3_rep_cross_dot;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`];\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[aff; AFFINE_HULL_3;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))\r
THEN DISJ_CASES_TAC(REAL_ARITH`&0<= w\/ &0<= -- w`);\r
\r
SUBGOAL_THEN`y1 IN aff_ge {vec 0,v3} {y:real^3}` ASSUME_TAC;\r
\r
ASM_SIMP_TAC[AFF_GE_2_1;th3;IN_ELIM_THM]\r
THEN EXISTS_TAC`u:real`\r
THEN EXISTS_TAC`v':real`\r
THEN EXISTS_TAC`w:real`\r
THEN ASM_REWRITE_TAC[]\r
THEN VECTOR_ARITH_TAC;\r
\r
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v3:real^3`;`y:real^3`;`y1:real^3`];\r
\r
MRESA_TAC Planarity.aff_gt3_subset_aff_gt[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3;SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`y IN aff_gt {vec 0} {v3, y1} /\ aff_gt {vec 0} {v3, y1} SUBSET aff_gt {vec 0} {y1, z1} /\ aff_gt {vec 0} {y1, z1} SUBSET aff_ge {vec 0} {y1, z1}\r
==> y IN aff_ge {vec 0} {y1, z1:real^3}`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN STRIP_TAC\r
THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`y:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`y:real^3`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {y} SUBSET aff_ge {vec 0} {y1, z1}\r
==> aff_ge {vec 0} {y1, z1} INTER aff_ge {vec 0} {y} =aff_ge {vec 0} {y:real^3} `)\r
THEN RESA_TAC\r
THEN SUBGOAL_THEN`y IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;\r
\r
ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
MP_TAC(SET_RULE`y IN aff_gt {vec 0} {v3, y1}/\ aff_gt {vec 0} {v3, y1} SUBSET aff_gt {vec 0} {y1, z1:real^3} ==> y IN aff_gt {vec 0} {y1, z1}`)\r
THEN RESA_TAC\r
THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`y:real^3`;`y1:real^3`;`vec 0:real^3`]\r
THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`z1:real^3`;`y1:real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN RESA_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`z1:real^3`;`y:real^3`;`vec 0:real^3`]\r
THEN MP_TAC(SET_RULE`~(y = y1) /\ ~(z1=y)==> {y1,z1:real^3} INTER {y}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`y:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING];\r
\r
MP_TAC(SET_RULE`v3 IN aff_gt {vec 0} {y, z} /\ aff_gt {vec 0} {y, z} SUBSET aff_ge {vec 0} {y, z}\r
==> v3 IN aff_ge {vec 0} {y, z:real^3}`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN STRIP_TAC\r
THEN MRESA_TAC Planarity.aff_ge1_subset_aff_ge[`vec 0:real^3`;`z:real^3`;`y:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3;SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {v3, y} /\ aff_ge {vec 0} {v3, y} SUBSET aff_ge {vec 0} {y, z}\r
==> y1 IN aff_ge {vec 0} {y, z:real^3}`)\r
THEN RESA_TAC\r
THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`y1:real^3`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {y1} SUBSET aff_ge {vec 0} {y, z}\r
==> aff_ge {vec 0} {y, z} INTER aff_ge {vec 0} {y1} =aff_ge {vec 0} {y1:real^3} `)\r
THEN RESA_TAC\r
THEN SUBGOAL_THEN`y1 IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;\r
\r
ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[];\r
\r
MP_TAC(SET_RULE`{y,z} INTER {y1,z1:real^3}={}==> {y,z} INTER {y1}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING];\r
\r
SUBGOAL_THEN`y1 IN aff_ge {vec 0,v3} {z:real^3}` ASSUME_TAC;\r
\r
ASM_SIMP_TAC[AFF_GE_2_1;th3;IN_ELIM_THM]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;VECTOR_ARITH`v' % (t2 % y + t3 % z) + w % y= (v' * t2+w) % y + (v'*t3) % z /\\r
t2' % (t2 % y + t3 % z) + t3' % z = (t2' *t2) % y + (t2'*t3+t3') % z`])\r
THEN STRIP_TAC\r
THEN MP_TAC(REAL_ARITH`&0<t2/\ &0< t3==> ~(t2= &0) /\ &0<= t3 /\ &0<= t2`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_MUL_LINV`t2:real`\r
THEN EXISTS_TAC`&1- (v' * t2 + w)* inv t2 -(v' * t3 - (v' * t2 + w)* inv t2 * t3):real`\r
THEN EXISTS_TAC`(v' * t2 + w)* inv t2 :real`\r
THEN EXISTS_TAC`v' * t3 - (v' * t2 + w)* inv t2 * t3:real`\r
THEN ASM_REWRITE_TAC[REAL_ARITH`&1-A-B+A+B= &1/\ ((v' * t2 + w) * inv t2) * t3 + v' * t3 - (v' * t2 + w) * inv t2 * t3 =v' * t3 /\ (A*B)*C=A*(B*C) /\A * &1=A\r
/\ v' * t3 - (v' * t2 + w) * inv t2 * t3= (v' - v' * (inv t2 *t2)  - w* inv t2) * t3 /\ A-A -B*C= (--B)* C`;]\r
THEN MATCH_MP_TAC REAL_LE_MUL\r
THEN ASM_REWRITE_TAC[]\r
THEN MATCH_MP_TAC REAL_LE_MUL\r
THEN ASM_REWRITE_TAC[]\r
THEN MATCH_MP_TAC REAL_LE_INV\r
THEN ASM_REWRITE_TAC[];\r
\r
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v3:real^3`;`z:real^3`;`y1:real^3`];\r
\r
MRESA_TAC Planarity.aff_gt3_subset_aff_gt[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3;SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`z IN aff_gt {vec 0} {v3, y1} /\ aff_gt {vec 0} {v3, y1} SUBSET aff_gt {vec 0} {y1, z1} /\ aff_gt {vec 0} {y1, z1} SUBSET aff_ge {vec 0} {y1, z1}\r
==> z IN aff_ge {vec 0} {y1, z1:real^3}`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN STRIP_TAC\r
THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`z:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`z:real^3`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {z} SUBSET aff_ge {vec 0} {y1, z1}\r
==> aff_ge {vec 0} {y1, z1} INTER aff_ge {vec 0} {z} =aff_ge {vec 0} {z:real^3} `)\r
THEN RESA_TAC\r
THEN SUBGOAL_THEN`z IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;\r
\r
ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`(SUC (i MOD dimindex (:M))):num`\r
THEN ASM_REWRITE_TAC[]\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MP_TAC(SET_RULE`{y,z} INTER {y1,z1}={} ==> {y1, z1} INTER {z:real^3}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`z:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING];\r
\r
MP_TAC(SET_RULE`v3 IN aff_gt {vec 0} {y, z} /\ aff_gt {vec 0} {y, z} SUBSET aff_ge {vec 0} {y, z}\r
==> v3 IN aff_ge {vec 0} {y, z:real^3}`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN STRIP_TAC\r
THEN MRESA_TAC Planarity.aff_ge1_subset_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3;]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {v3, z} /\ aff_ge {vec 0} {v3, z} SUBSET aff_ge {vec 0} {y, z}\r
==> y1 IN aff_ge {vec 0} {y, z:real^3}`)\r
THEN RESA_TAC\r
THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`y1:real^3`]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`aff_ge {vec 0} {y1} SUBSET aff_ge {vec 0} {y, z}\r
==> aff_ge {vec 0} {y, z} INTER aff_ge {vec 0} {y1} =aff_ge {vec 0} {y1:real^3} `)\r
THEN RESA_TAC\r
THEN SUBGOAL_THEN`y1 IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;\r
\r
ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[];\r
\r
MP_TAC(SET_RULE`{y,z} INTER {y1,z1}={} ==> {y, z} INTER {y1:real^3}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING];\r
\r
POP_ASSUM MP_TAC\r
THEN STRIP_TAC;\r
\r
MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`y:real^3`;`y1:real^3`;`z1:real^3`][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN RESA_TAC\r
THEN SUBGOAL_THEN`&0<(z cross y) dot y1` ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`]\r
THEN REWRITE_TAC[DOT_LMUL]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t3:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z cross y) dot y1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`];\r
\r
SUBGOAL_THEN`&0< --((z cross y) dot z1)` ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`]\r
THEN REWRITE_TAC[DOT_LMUL;REAL_ARITH`--(A*B)=A*(--B)`]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t3:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * --((z cross y) dot z1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`];\r
\r
SUBGOAL_THEN`&0<(z1 cross y) dot y1` ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`t* &0 +A=A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t3:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z1 cross y) dot y1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`];\r
\r
MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`z1:real^3`;`y:real^3`;`z:real^3`][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN RESA_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW]\r
THEN REWRITE_TAC[DOT_LNEG]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ASM_REWRITE_TAC[REAL_ARITH`-- -- A=A`]\r
THEN STRIP_TAC\r
THEN SUBGOAL_THEN`&0< --((z1 cross z) dot y1)` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`A+t* &0 =A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL;REAL_ARITH`--(A*B)= A*(--B)`]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t2==> ~(t2= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t2:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t2:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t2`;`t2 * ((y1 cross z) dot z1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]\r
THEN ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE]\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW]\r
THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\\r
      SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\\r
      SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num`\r
THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))` THEN MRESA1_TAC th`SUC (i' MOD dimindex (:M))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2"))\r
THEN\r
MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`z:real^3`;`y:real^3`;`y1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< (z cross y) dot y1==> &0< ((z cross y) dot y1)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z cross y) dot y1)/ &4`)\r
THEN SUBGOAL_THEN`!n. N <= n\r
          ==> &0< (row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot\r
               row i' (v n) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row i' (v n)`;`(z cross y) dot y1`];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY1")\r
THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`z1:real^3`;`y:real^3`;`y1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< (z1 cross y) dot y1==> &0< ((z1 cross y) dot y1)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z1 cross y) dot y1)/ &4`)\r
THEN SUBGOAL_THEN`!n. N' <= n\r
          ==> &0< (row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot\r
               row i' (v n) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row i' (v n)`;`(z1 cross y) dot y1`];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY2")\r
THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`z:real^3`;`y:real^3`;`z1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< --((z cross y) dot z1)==> &0< --((z cross y) dot z1)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z cross y) dot z1)/ &4`)\r
THEN SUBGOAL_THEN`!n. N'' <= n\r
          ==> &0< --((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot\r
               row (SUC (i' MOD dimindex (:M))) (v n)) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row (SUC (i' MOD dimindex (:M))) (v n))`;`--((z cross y) dot z1)`]\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY3")\r
THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`z1:real^3`;`z:real^3`;`y1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< --((z1 cross z) dot y1)==> &0< --((z1 cross z) dot y1)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z1 cross z) dot y1)/ &4`)\r
THEN SUBGOAL_THEN`!n. N''' <= n\r
          ==> &0< --((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i MOD dimindex (:M))) (v n)) dot\r
               row i' (v n)) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i MOD dimindex (:M))) (v n)) dot row i' (v n))`;`--((z1 cross z) dot y1)`]\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG];\r
\r
MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N2:num. !n. N2<=n ==> ~( row (SUC (i MOD dimindex (:M))) (v n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`;\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`z:real^3`][o_DEF]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`z IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`)\r
THEN RESA_TAC;\r
\r
MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N3:num. !n. N3<=n ==> ~(row i ((v:num->real^3^M) n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`;\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row i ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`y:real^3`][o_DEF]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`y IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY4")\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY5")\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY6")\r
THEN ABBREV_TAC`N1=N+N'+N''+N'''+N2+N3:num`\r
THEN MP_TAC(ARITH_RULE`N+N'+N''+N'''+N2+N3= N1:num ==> N<= N1/\ N'<= N1 /\ N''<= N1/\ N'''<= N1 /\ N2<= N1/\ N3<=N1`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN "YEUTHY1"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY2"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY3"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY4"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY5"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY6"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN ABBREV_TAC`y'=row i ((v:num-> real^3^M) N1)`\r
THEN ABBREV_TAC`z'=row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) N1)`\r
THEN ABBREV_TAC`y1'=row i' ((v:num-> real^3^M) N1)`\r
THEN ABBREV_TAC`z1'=row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) N1)`\r
THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[convex_local_fan;local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[FAN;fan7;fan6]\r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY1")\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY2")\r
THEN SUBGOAL_THEN`{y',z'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`{y1',z1'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[];\r
\r
REMOVE_THEN "YEUTHY1"(fun th-> MRESAL1_TAC th`{y',z':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`]\r
THEN MRESAL1_TAC th`{y1',z1':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`])\r
THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`y':real^3`;`z':real^3`;`y1':real^3`;`z1':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`z1':real^3`;`y1':real^3`;`y':real^3`;`z':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ASM_REWRITE_TAC[]\r
THEN ABBREV_TAC`a=(y' cross z')`\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN ONCE_REWRITE_TAC[GSYM CROSS_LNEG]\r
THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW] \r
THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW]\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`--((y1' cross z1') cross a') IN aff_gt {vec 0} {y1', z1'}\r
/\ --((y1' cross z1') cross a') IN aff_gt {vec 0} {y', z'}\r
/\ aff_gt {vec 0} {y', z'} SUBSET aff_ge {vec 0} {y', z'}\r
/\ aff_gt {vec 0} {y1', z1'} SUBSET aff_ge {vec 0} {y1', z1'}\r
==> --((y1' cross z1') cross a') IN aff_ge {vec 0} {y', z'} INTER aff_ge {vec 0} {y1', z1'}`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MP_TAC(SET_RULE`~(y' IN {y1',z1'}) /\ ~(z' IN {y1',z1':real^3})==> ({y',z'}INTER{y1',z1'}={})`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"YEUTHY2"(fun th-> MRESAL_TAC th[`{y',z':real^3}`;`{y1',z1':real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)\r
THEN MRESA_TAC Planarity.origin_is_not_aff_gt_fan[`vec 0:real^3`;`y':real^3`;`z':real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3];\r
\r
POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW]\r
THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`y1:real^3`;`y:real^3`;`z:real^3`][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN RESA_TAC\r
THEN SUBGOAL_THEN`&0<(z1 cross y1) dot y` ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`]\r
THEN REWRITE_TAC[DOT_LMUL]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t3:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z1 cross y1) dot y)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`];\r
\r
SUBGOAL_THEN`&0< --((z1 cross y1) dot z)` ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`]\r
THEN REWRITE_TAC[DOT_LMUL;REAL_ARITH`--(A*B)=A*(--B)`]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t3:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * --((z1 cross y1) dot z)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`];\r
\r
SUBGOAL_THEN`&0<(z cross y1) dot y` ASSUME_TAC;\r
\r
REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`t* &0 +A=A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t3:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t3:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z cross y1) dot y)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`];\r
\r
MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`z:real^3`;`y1:real^3`;`z1:real^3`][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN RESA_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW]\r
THEN REWRITE_TAC[DOT_LNEG]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ASM_REWRITE_TAC[REAL_ARITH`-- -- A=A`]\r
THEN STRIP_TAC\r
THEN SUBGOAL_THEN`&0< --((z cross z1) dot y)` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3]\r
THEN STRIP_TAC\r
THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}`\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`])\r
THEN RESA_TAC\r
THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`A+t* &0 =A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL;REAL_ARITH`--(A*B)= A*(--B)`]\r
THEN RESA_TAC\r
THEN MP_TAC(REAL_ARITH`&0 < t2==> ~(t2= &0)`)\r
THEN RESA_TAC\r
THEN MRESA1_TAC REAL_LT_INV`t2:real`\r
THEN MRESA1_TAC REAL_MUL_LINV`t2:real`\r
THEN MRESAL_TAC REAL_LT_MUL[`inv t2`;`t2 * ((y cross z1) dot z)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]\r
THEN ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE]\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW]\r
THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\\r
      SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\\r
      SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num`\r
THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))` THEN MRESA1_TAC th`SUC (i' MOD dimindex (:M))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2"))\r
THEN\r
MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`z1:real^3`;`y1:real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< (z1 cross y1) dot y==> &0< ((z1 cross y1) dot y)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z1 cross y1) dot y)/ &4`)\r
THEN SUBGOAL_THEN`!n. N <= n\r
          ==> &0< (row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot\r
               row i (v n) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row i (v n)`;`(z1 cross y1) dot y`];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY1")\r
THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`z:real^3`;`y1:real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< (z cross y1) dot y==> &0< ((z cross y1) dot y)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z cross y1) dot y)/ &4`)\r
THEN SUBGOAL_THEN`!n. N' <= n\r
          ==> &0< (row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot\r
               row i (v n) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row i (v n)`;`(z cross y1) dot y`];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY2")\r
THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`z1:real^3`;`y1:real^3`;`z:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< --((z1 cross y1) dot z)==> &0< --((z1 cross y1) dot z)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z1 cross y1) dot z)/ &4`)\r
THEN SUBGOAL_THEN`!n. N'' <= n\r
          ==> &0< --((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot\r
               row (SUC (i MOD dimindex (:M))) (v n)) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row (SUC (i MOD dimindex (:M))) (v n))`;`--((z1 cross y1) dot z)`]\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY3")\r
THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`z:real^3`;`z1:real^3`;`y:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT]\r
THEN MP_TAC(REAL_ARITH`&0< --((z cross z1) dot y)==> &0< --((z cross z1) dot y)/ &4`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z cross z1) dot y)/ &4`)\r
THEN SUBGOAL_THEN`!n. N''' <= n\r
          ==> &0< --((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i' MOD dimindex (:M))) (v n)) dot\r
               row i (v n)) ` ASSUME_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"CHANGE")\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`)\r
THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i' MOD dimindex (:M))) (v n)) dot row i (v n))`;`--((z cross z1) dot y)`]\r
THEN POP_ASSUM MATCH_MP_TAC\r
THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG];\r
\r
MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N2:num. !n. N2<=n ==> ~( row (SUC (i MOD dimindex (:M))) (v n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`;\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`z:real^3`][o_DEF]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`z IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`)\r
THEN RESA_TAC;\r
\r
MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N3:num. !n. N3<=n ==> ~(row i ((v:num->real^3^M) n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`;\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF]\r
THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row i ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`y:real^3`][o_DEF]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[]\r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`y IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY4")\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY5")\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY6")\r
THEN ABBREV_TAC`N1=N+N'+N''+N'''+N2+N3:num`\r
THEN MP_TAC(ARITH_RULE`N+N'+N''+N'''+N2+N3= N1:num ==> N<= N1/\ N'<= N1 /\ N''<= N1/\ N'''<= N1 /\ N2<= N1/\ N3<=N1`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN "YEUTHY1"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY2"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY3"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY4"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY5"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_THEN "YEUTHY6"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN ABBREV_TAC`y'=row i ((v:num-> real^3^M) N1)`\r
THEN ABBREV_TAC`z'=row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) N1)`\r
THEN ABBREV_TAC`y1'=row i' ((v:num-> real^3^M) N1)`\r
THEN ABBREV_TAC`z1'=row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) N1)`\r
THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`N1:num`)\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[convex_local_fan;local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[FAN;fan7;fan6]\r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY1")\r
THEN DISCH_THEN(LABEL_TAC"YEUTHY2")\r
THEN SUBGOAL_THEN`{y',z'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`{y1',z1'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[];\r
\r
REMOVE_THEN "YEUTHY1"(fun th-> MRESAL1_TAC th`{y',z':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`]\r
THEN MRESAL1_TAC th`{y1',z1':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`])\r
THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`y1':real^3`;`z1':real^3`;`y':real^3`;`z':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`z':real^3`;`y':real^3`;`y1':real^3`;`z1':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ASM_REWRITE_TAC[]\r
THEN ABBREV_TAC`a=(y1' cross z1')`\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN ONCE_REWRITE_TAC[GSYM CROSS_LNEG]\r
THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW] \r
THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW]\r
THEN ONCE_REWRITE_TAC[CROSS_SKEW] \r
THEN STRIP_TAC\r
THEN MP_TAC(SET_RULE`--((y' cross z') cross a') IN aff_gt {vec 0} {y1', z1'}\r
/\ --((y' cross z') cross a') IN aff_gt {vec 0} {y', z'}\r
/\ aff_gt {vec 0} {y', z'} SUBSET aff_ge {vec 0} {y', z'}\r
/\ aff_gt {vec 0} {y1', z1'} SUBSET aff_ge {vec 0} {y1', z1'}\r
==> --((y' cross z') cross a') IN aff_ge {vec 0} {y', z'} INTER aff_ge {vec 0} {y1', z1'}`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MP_TAC(SET_RULE`~(y' IN {y1',z1'}) /\ ~(z' IN {y1',z1':real^3})==> ({y',z'}INTER{y1',z1'}={})`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"YEUTHY2"(fun th-> MRESAL_TAC th[`{y',z':real^3}`;`{y1',z1':real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)\r
THEN MRESA_TAC Planarity.origin_is_not_aff_gt_fan[`vec 0:real^3`;`y':real^3`;`z':real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ASM_SIMP_TAC[th3];\r
\r
ASM_REWRITE_TAC[];\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"MA1")\r
THEN DISCH_THEN(LABEL_TAC"MA2")\r
THEN REWRITE_TAC[UNION;IN_ELIM_THM]\r
THEN REPEAT STRIP_TAC;\r
\r
POP_ASSUM(fun th-> POP_ASSUM(fun th1-> MP_TAC th1 THEN \r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN REPEAT STRIP_TAC THEN ASSUME_TAC th1\r
)THEN MP_TAC th THEN \r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN REPEAT STRIP_TAC THEN ASSUME_TAC th)\r
THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats \r
(l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`y1=row i' (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`z1=row (SUC (i' MOD dimindex (:M))) (vecmats \r
(l:real^(M,3)finite_product))`\r
THEN DISJ_CASES_TAC(SET_RULE`{y,z}INTER {y1,z1:real^3}={} \/ {y,z} INTER {y1,z1}={y}\r
\/ {y,z} INTER {y1,z1}={z}\/ {y,z} INTER {y1,z1}={y,z}`);\r
\r
ASM_SIMP_TAC[]\r
THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6"))\r
THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y1:real^3`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]\r
THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[];\r
\r
REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`y1:real^3`] THEN MRESA_TAC th[`y:real^3`;`z1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y1:real^3`] THEN MRESA_TAC th[`z:real^3`;`z1:real^3`])\r
THEN MP_TAC(SET_RULE`{y, z} INTER {y1, z1} = {} ==> {y} INTER {y1:real^3}={}/\ {y} INTER {z1:real^3}={} /\ {z} INTER {z1:real^3}={} /\ {z} INTER {y1:real^3}={} /\ {y,z} INTER {y1:real^3}={} /\ {y,z} INTER {z1:real^3}={} /\ {z} INTER {y1:real^3,z1}={}/\ {y} INTER {y1:real^3,z1}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`y1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e1:real^3->bool`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`y:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`z:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`])\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN RESA_TAC\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN REMOVE_THEN"MA2"(fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN SET_TAC[];\r
\r
POP_ASSUM MP_TAC\r
THEN STRIP_TAC;\r
\r
ASM_SIMP_TAC[]\r
THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6"))\r
THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y1:real^3`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`];\r
\r
MP_TAC(SET_RULE`{y, z} INTER {y1, z1} = {y}==> y1=y \/ z1=y:real^3`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} \r
{y, z1}) \/ aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y, z1:real^3}={}`);\r
\r
POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`y:real^3`;`z:real^3`;`z1:real^3`;`v3:real^3`]\r
THEN \r
SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`z1:real^3`];\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`z:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`z IN aff_gt {vec 0} {y, z1} /\  aff_gt {vec 0} {y, z1} SUBSET\r
aff_ge {vec 0} {y, z1:real^3} /\  aff_ge {vec 0} {y, z1:real^3} INTER aff_ge {vec 0} {z} = aff_ge {vec 0} ({y, z1:real^3} INTER {z}) /\ z IN aff_ge {vec 0} {z}\r
==> z IN aff_ge {vec 0} ({y, z1} INTER {z})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {y, z1} = {y} ==> {y, z1} INTER {z:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`z1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z1:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z1:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`z1 IN aff_ge {vec 0} {y, z} /\  aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {z1} = aff_ge {vec 0} ({y, z:real^3} INTER {z1}) /\ z1 IN aff_ge {vec 0} {z1}\r
==> z1 IN aff_ge {vec 0} ({y, z} INTER {z1})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MRESA_TAC th3[`y:real^3`;`z1:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y=z1) /\ {y, z} INTER {y, z1} = {y} ==> {y, z} INTER {z1:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`z1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`z1:real^3`])\r
THEN MRESA_TAC th3[`y:real^3`;`z1:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`{y, z} INTER {y, z1} = {y} /\ ~(y=z) /\ ~(y=z1) ==> {y} INTER {z1:real^3}={} /\ {z} INTER {z1:real^3}={} /\ {z} INTER {y:real^3}={}  /\ {y,z} INTER {z1:real^3}={}  /\ {y,z1} INTER {z:real^3}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]  THEN MRESAL_TAC th[`e2:real^3->bool`;`z:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`])\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z1:real^3`][aff]\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z:real^3`][aff]\r
THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`y:real^3`]\r
THEN MP_TAC(SET_RULE`\r
affine hull {vec 0, y} INTER aff_gt {vec 0} {y, z1} = {}\r
/\ affine hull {vec 0, y} INTER aff_gt {vec 0} {y, z} = {}\r
/\ aff_ge {vec 0} {y} SUBSET affine hull {vec 0, y:real^3}\r
==> aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y}={}\r
/\ aff_ge {vec 0} {y} INTER aff_gt {vec 0} {y, z1}={}`)\r
THEN RESA_TAC\r
THEN ASM_REWRITE_TAC[SET_RULE`{} UNION A=A\r
/\ aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1} UNION\r
 (aff_ge {vec 0} {y} INTER aff_ge {vec 0} {y} UNION aff_ge {vec 0} {}) UNION\r
 aff_ge {vec 0} {}=\r
(aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1} UNION aff_ge {vec 0} {} UNION \r
aff_ge {vec 0} {}) UNION\r
 (aff_ge {vec 0} {y} INTER aff_ge {vec 0} {y} UNION aff_ge {vec 0} {}) \r
 `;]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING]\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]\r
THEN POP_ASSUM MP_TAC\r
THEN SET_TAC[];\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} \r
{y, y1}) \/ aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y, y1:real^3}={}`);\r
\r
POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`y:real^3`;`z:real^3`;`y1:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN \r
SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC;\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`z:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`z IN aff_gt {vec 0} {y1, y} /\  aff_gt {vec 0} {y1, y} SUBSET\r
aff_ge {vec 0} {y1, y:real^3} /\  aff_ge {vec 0} {y1, y:real^3} INTER aff_ge {vec 0} {z} = aff_ge {vec 0} ({y1, y:real^3} INTER {z}) /\ z IN aff_ge {vec 0} {z}\r
==> z IN aff_ge {vec 0} ({y1, y} INTER {z})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {y1, y} = {y} ==> {y, y1} INTER {z:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y1:real^3`;`y:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {y, z} /\  aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {y1} = aff_ge {vec 0} ({y, z:real^3} INTER {y1}) /\ y1 IN aff_ge {vec 0} {y1}\r
==> y1 IN aff_ge {vec 0} ({y, z} INTER {y1})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MRESA_TAC th3[`y1:real^3`;`y:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y=y1) /\ {y, z} INTER {y1, y} = {y} ==> {y, z} INTER {y1:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`y1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`y1:real^3`])\r
THEN MRESA_TAC th3[`y1:real^3`;`y:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`{y, z} INTER {y1, y} = {y} /\ ~(y=z) /\ ~(y=y1) ==> {y} INTER {y1:real^3}={} /\ {z} INTER {y1:real^3}={} /\ {z} INTER {y:real^3}={}  /\ {y,z} INTER {y1:real^3}={}  /\ {y1,y} INTER {z:real^3}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`y1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]  THEN MRESAL_TAC th[`e2:real^3->bool`;`z:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`])\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`y1:real^3`][aff]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z:real^3`][aff]\r
THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`y:real^3`]\r
THEN MP_TAC(SET_RULE`\r
affine hull {vec 0, y} INTER aff_gt {vec 0} {y, y1} = {}\r
/\ affine hull {vec 0, y} INTER aff_gt {vec 0} {y, z} = {}\r
/\ aff_ge {vec 0} {y} SUBSET affine hull {vec 0, y:real^3}\r
==> aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y}={}\r
/\ aff_ge {vec 0} {y} INTER aff_gt {vec 0} {y, y1}={}`)\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[SET_RULE`A UNION {}=A`;]\r
THEN SUBGOAL_THEN`aff_gt{vec 0} {y1,y}=aff_gt{vec 0} {y,y1:real^3}` ASSUME_TAC;\r
\r
ASSUME_TAC(SET_RULE`{y1,y}={y,y1:real^3}`)\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th]);\r
\r
ASM_REWRITE_TAC[SET_RULE`({} UNION aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1}) UNION\r
 ({} UNION\r
  aff_ge {vec 0} {} UNION\r
  aff_ge {vec 0} {y} INTER aff_ge {vec 0} {y}) UNION\r
 aff_ge {vec 0} {}\r
=(aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1} UNION aff_ge {vec 0} {}\r
 UNION\r
  aff_ge {vec 0} {}) UNION\r
  aff_ge {vec 0} {y}`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING]\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN SET_TAC[];\r
\r
ASM_SIMP_TAC[]\r
THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6"))\r
THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y1:real^3`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`];\r
\r
MP_TAC(SET_RULE`{y, z} INTER {y1, z1} = {z}==> y1=z \/ z1=z:real^3`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {z,y} INTER aff_gt {vec 0} \r
{z, z1}) \/ aff_gt {vec 0} {z,y} INTER aff_gt {vec 0} {z, z1:real^3}={}`);\r
\r
POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`z:real^3`;`y:real^3`;`z1:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN \r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`z:real^3`;`y:real^3`;`z1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC;\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`y:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`y IN aff_gt {vec 0} {z, z1} /\  aff_gt {vec 0} {z, z1} SUBSET\r
aff_ge {vec 0} {z, z1:real^3} /\  aff_ge {vec 0} {z, z1:real^3} INTER aff_ge {vec 0} {y} = aff_ge {vec 0} ({z, z1:real^3} INTER {y}) /\ y IN aff_ge {vec 0} {y}\r
==> y IN aff_ge {vec 0} ({z, z1} INTER {y})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {z, z1} = {z} ==> {z, z1} INTER {y:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`z1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`z:real^3`;`z1:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z1:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`z1 IN aff_ge {vec 0} {y, z} /\  aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {z1} = aff_ge {vec 0} ({y, z:real^3} INTER {z1}) /\ z1 IN aff_ge {vec 0} {z1}\r
==> z1 IN aff_ge {vec 0} ({y, z} INTER {z1})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MRESA_TAC th3[`z:real^3`;`z1:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(z=z1) /\ {y, z} INTER {z, z1} = {z} ==> {y, z} INTER {z1:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
POP_ASSUM MP_TAC\r
THEN SUBGOAL_THEN`aff_gt{vec 0} {z,y}=aff_gt{vec 0} {y,z:real^3}` ASSUME_TAC;\r
\r
ASSUME_TAC(SET_RULE`{z,y}={y,z:real^3}`)\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[th]);\r
\r
RESA_TAC\r
THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`z1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`z1:real^3`])\r
THEN MRESA_TAC th3[`z:real^3`;`z1:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`{y, z} INTER {z, z1} = {z} /\ ~(y=z) /\ ~(z=z1) ==> {y} INTER {z1:real^3}={} /\ {z} INTER {z1:real^3}={} /\ {z} INTER {y:real^3}={}  /\ {y,z} INTER {z1:real^3}={}  /\ {z,z1} INTER {y:real^3}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]  THEN MRESAL_TAC th[`e2:real^3->bool`;`y:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`])\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`z1:real^3`][aff]\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y:real^3`][aff]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`z:real^3`]\r
THEN MP_TAC(SET_RULE`\r
affine hull {vec 0, z} INTER aff_gt {vec 0} {z, z1} = {}\r
/\ affine hull {vec 0, z} INTER aff_gt {vec 0} {y, z} = {}\r
/\ aff_ge {vec 0} {z} SUBSET affine hull {vec 0, z:real^3}\r
==> aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z}={}\r
/\ aff_ge {vec 0} {z} INTER aff_gt {vec 0} {z, z1}={}`)\r
THEN RESA_TAC\r
THEN ASM_REWRITE_TAC[SET_RULE`({} UNION {} UNION aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1}) UNION\r
 aff_ge {vec 0} {} UNION\r
 {} UNION\r
 aff_ge {vec 0} {z} INTER aff_ge {vec 0} {z} UNION\r
 aff_ge {vec 0} {}=\r
(aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1} UNION aff_ge {vec 0} {} UNION \r
aff_ge {vec 0} {}) UNION\r
 ( aff_ge {vec 0} {z}) \r
 `;]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING]\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN SET_TAC[];\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {z, y} INTER aff_gt {vec 0} \r
{z, y1}) \/ aff_gt {vec 0} {z, y} INTER aff_gt {vec 0} {z, y1:real^3}={}`);\r
\r
POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`z:real^3`;`y:real^3`;`y1:real^3`;`v3:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN \r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`z:real^3`;`y:real^3`;`y1:real^3`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`y:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`y IN aff_gt {vec 0} {y1, z} /\  aff_gt {vec 0} {y1, z} SUBSET\r
aff_ge {vec 0} {y1, z:real^3} /\  aff_ge {vec 0} {y1, z:real^3} INTER aff_ge {vec 0} {y} = aff_ge {vec 0} ({y1, z:real^3} INTER {y}) /\ y IN aff_ge {vec 0} {y}\r
==> y IN aff_ge {vec 0} ({y1, z} INTER {y})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {y1, z} = {z} ==> { z,y1} INTER {y:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y1:real^3`;`z:real^3`]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING]\r
THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {y, z} /\  aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {y1} = aff_ge {vec 0} ({y, z:real^3} INTER {y1}) /\ y1 IN aff_ge {vec 0} {y1}\r
==> y1 IN aff_ge {vec 0} ({y, z} INTER {y1})`)\r
THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]\r
THEN MRESA_TAC th3[`y1:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(z=y1) /\ {y, z} INTER {y1, z} = {z} ==> {y, z} INTER {y1:real^3}={}`)\r
THEN RESA_TAC\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING];\r
\r
POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN STRIP_TAC\r
THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`SUC (i MOD dimindex (:M))`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i':num`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;\r
\r
REWRITE_TAC[IN_ELIM_THM;V_SY;rows]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`y1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`y1:real^3`])\r
THEN MRESA_TAC th3[`y1:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`{y, z} INTER {y1, z} = {z} /\ ~(y=z) /\ ~(z=y1) ==> {y} INTER {y1:real^3}={} /\ {z} INTER {y1:real^3}={} /\ {z} INTER {y:real^3}={}  /\ {y,z} INTER {y1:real^3}={}  /\ {y1,z} INTER {y:real^3}={}`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`y1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]  THEN MRESAL_TAC th[`e2:real^3->bool`;`y:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`])\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`]\r
THEN ASM_REWRITE_TAC[]\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y1:real^3`][aff]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y:real^3`][aff]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`z:real^3`]\r
THEN MP_TAC(SET_RULE`\r
affine hull {vec 0, z} INTER aff_gt {vec 0} {z, y1} = {}\r
/\ affine hull {vec 0, z} INTER aff_gt {vec 0} {z, y} = {}\r
/\ aff_ge {vec 0} {z} SUBSET affine hull {vec 0, z:real^3}\r
==> aff_gt {vec 0} {z, y} INTER aff_ge {vec 0} {z}={}\r
/\ aff_ge {vec 0} {z} INTER aff_gt {vec 0} {z, y1}={}`)\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[]\r
THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]\r
THEN ASM_REWRITE_TAC[SET_RULE`({} UNION aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1} UNION {}) UNION\r
 aff_ge {vec 0} {} UNION\r
 {} UNION\r
 aff_ge {vec 0} {} UNION\r
 aff_ge {vec 0} {z} INTER aff_ge {vec 0} {z}\r
= (aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1} UNION aff_ge {vec 0} {} UNION\r
 aff_ge {vec 0} {}) UNION\r
 aff_ge {vec 0} {z} `;]\r
THEN MRESA_TAC th3[`vec 0:real^3`;`y1:real^3`;`z:real^3`;]\r
THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING]\r
THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN SET_TAC[];\r
\r
ASM_SIMP_TAC[]\r
THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6"))\r
THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC th3[`y1:real^3`;`z1:real^3`;`vec 0:real^3`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]\r
THEN RESA_TAC\r
THEN MP_TAC(SET_RULE`~(y1=z1)/\ ~(y=z)/\ {y, z} INTER {y1, z1} = {y, z}==>  {y1, z1:real^3} = {y, z}`)\r
THEN RESA_TAC\r
THEN SET_TAC[];\r
\r
ASM_SIMP_TAC[];\r
\r
REMOVE_THEN "MA1"(fun th-> MRESA_TAC th[`e2:real^3->bool`;`v':real^3`])\r
THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`]\r
THEN ASM_REWRITE_TAC[];\r
\r
ASM_SIMP_TAC[];\r
\r
\r
\r
SUBGOAL_THEN`!i j.\r
     1 <= i /\\r
     i <= dimindex (:M) /\\r
     1 <= j /\\r
     j <= dimindex (:M) /\\r
     row i (vecmats l) = row j (vecmats (l:real^(M,3)finite_product))\r
     ==> i = j` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY3"(fun th-> MRESAL_TAC th[`i:num`;`j:num`][VECTOR_ARITH`A-A= vec 0`;NORM_0])\r
THEN DISJ_CASES_TAC(SET_RULE`~(i=j:num)\/ (i=j)`);\r
\r
MP_TAC(ARITH_RULE`i <= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
REMOVE_THEN"THYGIANG"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`])\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN MP_TAC(ARITH_RULE`1<= i==> ~(i = 0)`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`])\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN STRIP_TAC\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN ASM_SIMP_TAC[IN_NUMSEG]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`])\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MESON_TAC[];\r
\r
SET_TAC[];\r
\r
SUBGOAL_THEN`local_fan (V_SY (vecmats l),E_SY (vecmats l), F_SY(vecmats (l:real^(M,3)finite_product)))` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN REPEAT STRIP_TAC;\r
\r
EXISTS_TAC`(row 1 (vecmats (l:real^(M,3)finite_product)), row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`\r
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]\r
THEN STRIP_TAC;\r
\r
SIMP_TAC[darts_of_hyp;ord_pairs;E_SY;]\r
THEN MATCH_MP_TAC(SET_RULE`A IN B ==> A IN B UNION C`)\r
THEN REWRITE_TAC[IN_ELIM_THM]\r
THEN EXISTS_TAC`row 1 (vecmats (l:real^(M,3)finite_product))`\r
THEN EXISTS_TAC`row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`\r
THEN ASM_REWRITE_TAC[]\r
THEN EXISTS_TAC`1`\r
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1`; DIMINDEX_GE_1];\r
\r
MATCH_MP_TAC  FACE_HYP_FAN_SY\r
THEN ASM_REWRITE_TAC[]\r
THEN ASM_TAC\r
THEN MESON_TAC[];\r
\r
MRESA1_TAC (GEN_ALL DIH2K_FAN_HYP_SY)`l:real^(M,3)finite_product`\r
THEN POP_ASSUM MP_TAC\r
THEN FIND_ASSUM MP_TAC`2<k`\r
THEN ONCE_REWRITE_TAC[ARITH_RULE`2= SUC 1`]\r
THEN ASM_REWRITE_TAC[]\r
THEN REWRITE_TAC[ARITH_RULE`SUC 1=2`]\r
THEN RESA_TAC;\r
\r
POP_ASSUM (fun th-> MP_TAC th\r
THEN ASM_REWRITE_TAC[local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN DISCH_TAC THEN ASSUME_TAC th)\r
THEN ASM_REWRITE_TAC[]\r
THEN SUBGOAL_THEN`!i u v w. 1<= i /\ i<= dimindex (:M)\r
/\ row i (vecmats l)=u\r
/\  row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))=v\r
/\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w\r
==> &0<= (v cross w) dot u` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\\r
      SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
SUBGOAL_THEN`1 <= SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)) /\\r
      SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`SUC (i MOD dimindex (:M)):num`;`dimindex (:M):num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))`\r
THEN MRESA1_TAC th`(SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2"))\r
THEN\r
MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`v':real^3`;`w:real^3`;`u:real^3`]\r
THEN SUBGOAL_THEN`eventually\r
      (\x. &0 <=\r
           drop\r
           ((lift o\r
             (\n. (row (SUC (i MOD dimindex (:M))) (v n) cross\r
                   row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)))\r
                   (v n)) dot\r
                  row i ((v:num->real^3^M) n)))\r
           x))\r
      sequentially` ASSUME_TAC;\r
\r
REWRITE_TAC[EVENTUALLY_SEQUENTIALLY;o_DEF;LIFT_DROP]\r
THEN EXISTS_TAC`0`\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`)\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[convex_local_fan;]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY30")\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MP_TAC th\r
THEN REWRITE_TAC[local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN STRIP_TAC\r
THEN ASSUME_TAC th)\r
THEN SUBGOAL_THEN`row (SUC (i MOD dimindex (:M))) (v n),\r
      row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n) IN\r
      F_SY ((v:num->real^3^M) n)`ASSUME_TAC;\r
\r
REWRITE_TAC[F_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`(SUC (i MOD dimindex (:M)))`\r
THEN ASM_REWRITE_TAC[];\r
\r
STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESA1_TAC th`\r
row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n), \r
  row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)`)\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (((v:num->real^3^M) n))`;`F_SY (((v:num->real^3^M) n))`;`E_SY ( ((v:num->real^3^M) n))`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n), \r
  row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)`]\r
THEN FIND_ASSUM MP_TAC`1<k`\r
THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`]\r
THEN ASM_REWRITE_TAC[]\r
THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`]\r
THEN RESA_TAC\r
THEN SUBGOAL_THEN `(!i1 j.\r
           1 <= i1 /\\r
           i1 <= dimindex (:M) /\\r
           1 <= j /\\r
           j <= dimindex (:M) /\\r
           row i1 (v n) = row j ((v:num->real^3^M) n)\r
           ==> i1 = j)` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY30"(fun th-> MRESAL_TAC th[`i1:num`;`j:num`][VECTOR_ARITH`A-A= vec 0`;NORM_0])\r
THEN DISJ_CASES_TAC(SET_RULE`~(i1=j:num)\/ (i1=j)`);\r
\r
MP_TAC(ARITH_RULE`i1 <= dimindex (:M)==> i1 <= dimindex (:M)-1 \/ i1 = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
REMOVE_THEN"THYGIANG"MP_TAC\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j:num`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i1:num`;`j:num`][ARITH_RULE`0<= i:num`])\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`]\r
THEN MP_TAC(ARITH_RULE`1<= i1==> ~(i1 = 0)`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i1:num`;`0:num`][ARITH_RULE`0<= i1:num`])\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i1:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN STRIP_TAC\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`])\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MESON_TAC[];\r
\r
ASM_MESON_TAC[];\r
\r
MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i:num`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (i) ((v:num->real^3^M) n)`;`matvec((v:num-> real^3^M) n)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;VECMATS_MATVEC_ID]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`matvec ((v:num->real^3^M) n)`][VECMATS_MATVEC_ID]\r
THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`(SUC (i MOD dimindex (:M)))`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`;`matvec ((v:num->real^3^M) n)`][VECMATS_MATVEC_ID]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN RESA_TAC\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN RESA_TAC\r
THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_ge_fan[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`][azim;VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN RESA_TAC;\r
\r
MRESAL_TAC LIM_DROP_LBOUND[`sequentially`;`lift o\r
       (\n. (row (SUC (i MOD dimindex (:M))) (v n) cross\r
             row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)) dot\r
            row i ((v:num->real^3^M) n))`;`lift ((v' cross w:real^3) dot u)`;`&0`][TRIVIAL_LIMIT_SEQUENTIALLY;LIFT_DROP];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY30")\r
THEN GEN_TAC\r
THEN STRIP_TAC\r
THEN SUBGOAL_THEN`azim_in_fan x' (E_SY (vecmats (l:real^(M,3)finite_product))) <= pi` ASSUME_TAC;\r
\r
POP_ASSUM(fun th-> MP_TAC th\r
THEN REWRITE_TAC[F_SY;IN_ELIM_THM]\r
THEN STRIP_TAC\r
THEN ASSUME_TAC th)\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x':real^3#real^3`]\r
THEN ABBREV_TAC`u1=row i (vecmats (l:real^(M,3)finite_product))`\r
THEN ABBREV_TAC`v1=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`\r
THEN FIND_ASSUM MP_TAC`1<k`\r
THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`]\r
THEN ASM_REWRITE_TAC[]\r
THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`]\r
THEN RESA_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]\r
THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`u1:real^3`;`v1:real^3`;`(row \r
(dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN REMOVE_THEN"THY30"(fun th-> MRESAL_TAC th [`k:num`;`(row \r
(dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`u1:real^3`;`v1:real^3`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`])\r
THEN MP_TAC(REAL_ARITH`&0 <= (u1 cross v1) dot row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))\r
==> &0 < (u1 cross v1) dot row (dimindex (:M)) (vecmats l)\/  (u1 cross v1) dot row (dimindex (:M)) (vecmats l)= &0`)\r
THEN RESA_TAC;\r
\r
MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`1:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`]\r
THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`dimindex (:M):num`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]\r
THEN RESA_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.MIXED_PROD_POS_IMP_RANGE_AZIM)[`u1:real^3`;`v1:real^3`;`(row \r
(dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{C,A,B}={C,B,A}`]\r
THEN RESA_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[Local_lemmas.CROSS_DOT_COPLANAR]\r
THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`1:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`]\r
THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`dimindex (:M):num`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`]\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN STRIP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u1:real^3`;`v1:real^3`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`][PI_POS_LE;REAL_ARITH`a<=a`];\r
\r
MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)`)\r
THEN RESA_TAC \r
THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]\r
THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i-1:num`;`u1:real^3`;`v1:real^3`;`(row \r
(i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_THEN"THY30"(fun th-> MRESAL_TAC th [`i-1:num`;`(row \r
(i-1) (vecmats (l:real^(M,3)finite_product)))`;`u1:real^3`;`v1:real^3`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`])\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`)\r
THEN RESA_TAC \r
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])\r
THEN STRIP_TAC\r
THEN STRIP_TAC\r
THEN MP_TAC(REAL_ARITH`&0 <= (u1 cross v1) dot row (i-1) (vecmats (l:real^(M,3)finite_product))\r
==> &0 < (u1 cross v1) dot row (i-1) (vecmats l)\/  (u1 cross v1) dot row (i-1) (vecmats l)= &0`)\r
THEN RESA_TAC;\r
\r
MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`]\r
THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`i-1:num`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`)\r
THEN RESA_TAC \r
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])\r
THEN STRIP_TAC\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`]\r
THEN REMOVE_ASSUM_TAC\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.MIXED_PROD_POS_IMP_RANGE_AZIM)[`u1:real^3`;`v1:real^3`;`(row \r
(i-1) (vecmats (l:real^(M,3)finite_product)))`;]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{C,A,B}={C,B,A}`]\r
THEN RESA_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[Local_lemmas.CROSS_DOT_COPLANAR]\r
THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`]\r
THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`i-1:num`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`)\r
THEN RESA_TAC \r
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])\r
THEN STRIP_TAC\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`]\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN STRIP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN STRIP_TAC\r
THEN MRESAL_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u1:real^3`;`v1:real^3`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`][PI_POS_LE;REAL_ARITH`a<=a`];\r
\r
SUBGOAL_THEN`!i j u v w. 1<= i /\ i<= dimindex (:M)\r
/\ 1<= j /\ j<= dimindex (:M)\r
/\ row i (vecmats l)=u\r
/\  row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))=v\r
/\ row j (vecmats l)=w\r
==> &0<= (u cross v) dot w` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\\r
      SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;\r
\r
ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]\r
THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))`\r
THEN MRESA1_TAC th`j:num` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2"))\r
THEN\r
MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row i ((v:num->real^3^M) n))`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row j ((v:num->real^3^M) n))`;`u:real^3`;`v':real^3`;`w:real^3`]\r
THEN SUBGOAL_THEN`eventually\r
      (\x. &0 <=\r
           drop\r
           ((lift o\r
             (\n. (row i (v n) cross\r
                   row (SUC (i MOD dimindex (:M)))\r
                   (v n)) dot\r
                  row j ((v:num->real^3^M) n)))\r
           x))\r
      sequentially` ASSUME_TAC;\r
\r
REWRITE_TAC[EVENTUALLY_SEQUENTIALLY;o_DEF;LIFT_DROP]\r
THEN EXISTS_TAC`0`\r
THEN REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`)\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REWRITE_TAC[convex_local_fan;]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN STRIP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY31")\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MP_TAC th\r
THEN REWRITE_TAC[local_fan]\r
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) \r
THEN STRIP_TAC\r
THEN ASSUME_TAC th)\r
THEN SUBGOAL_THEN`row i (v n),\r
      row (SUC (i MOD dimindex (:M))) (v n) IN\r
      F_SY ((v:num->real^3^M) n)`ASSUME_TAC;\r
\r
REWRITE_TAC[F_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
SUBGOAL_THEN`row j ((v:num->real^3^M) n) IN V_SY((v:num->real^3^M) n)` ASSUME_TAC;\r
\r
REWRITE_TAC[V_SY;rows;IN_ELIM_THM]\r
THEN EXISTS_TAC`j:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`\r
row i ((v:num->real^3^M) n), \r
  row (SUC (i MOD dimindex (:M))) (v n)`[SUBSET;IN_ELIM_THM])\r
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`\r
row j ((v:num->real^3^M) n)`[SUBSET;IN_ELIM_THM])\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (((v:num->real^3^M) n))`;`F_SY (((v:num->real^3^M) n))`;`E_SY ( ((v:num->real^3^M) n))`;`row i ((v:num->real^3^M) n), \r
  row (SUC (i MOD dimindex (:M))) (v n)`]\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (((v:num->real^3^M) n))`;`F_SY (((v:num->real^3^M) n))`;`E_SY ( ((v:num->real^3^M) n))`;`row i ((v:num->real^3^M) n), \r
  row (SUC (i MOD dimindex (:M))) (v n)`]\r
THEN FIND_ASSUM MP_TAC`1<k`\r
THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`]\r
THEN ASM_REWRITE_TAC[]\r
THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`]\r
THEN RESA_TAC\r
THEN SUBGOAL_THEN `(!i1 j1.\r
           1 <= i1 /\\r
           i1 <= dimindex (:M) /\\r
           1 <= j1 /\\r
           j1 <= dimindex (:M) /\\r
           row i1 (v n) = row j1 ((v:num->real^3^M) n)\r
           ==> i1 = j1)` ASSUME_TAC;\r
\r
REPEAT STRIP_TAC\r
THEN REMOVE_THEN "THY31"(fun th-> MRESAL_TAC th[`i1:num`;`j1:num`][VECTOR_ARITH`A-A= vec 0`;NORM_0])\r
THEN DISJ_CASES_TAC(SET_RULE`~(i1=j1:num)\/ (i1=j1)`);\r
\r
MP_TAC(ARITH_RULE`i1 <= dimindex (:M)==> i1 <= dimindex (:M)-1 \/ i1 = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
MP_TAC(ARITH_RULE`j1 <= dimindex (:M)==> j1 <= dimindex (:M)-1 \/ j1 = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
REMOVE_THEN"THYGIANG"MP_TAC\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j1:num`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i1:num`;`j1:num`][ARITH_RULE`0<= i:num`])\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j1:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`]\r
THEN MP_TAC(ARITH_RULE`1<= i1==> ~(i1 = 0)`)\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i1:num`;`0:num`][ARITH_RULE`0<= i1:num`])\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i1:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
MP_TAC(ARITH_RULE`j1 <= dimindex (:M)==> j1 <= dimindex (:M)-1 \/ j1 = dimindex (:M)`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN STRIP_TAC\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]\r
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]\r
THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]\r
THEN REMOVE_THEN "THYGIANG2" MP_TAC\r
THEN REWRITE_TAC[constraint_system]\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j1:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A `])\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j1:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`])\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= j1==> ~(j1 = 0)`)\r
THEN RESA_TAC\r
THEN REMOVE_THEN"THYGIANG"MP_TAC\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j1:num`]\r
THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`]\r
THEN STRIP_TAC\r
THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j1:num`;`0:num`][ARITH_RULE`0<= i:num`])\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ARITH_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MESON_TAC[];\r
\r
ASM_MESON_TAC[];\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY32")\r
THEN REWRITE_TAC[REAL_ARITH`A<=B <=> A=B\/ A< B`]\r
THEN STRIP_TAC;\r
\r
MRESAL_TAC(GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE (row i (v n)) (E_SY (v n))) (vec 0) (row i (v n))\r
 (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)))`;`(row i ((v:num->real^3^M) n))`;`(row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`vec 0:real^3`][IN_ELIM_THM;REAL_ARITH`A=B\/ A< B<=> A<=B`;VECTOR_ARITH`A- vec 0=A`]\r
THEN REAL_ARITH_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN SUBGOAL_THEN`{row i (v n),\r
      row (SUC (i MOD dimindex (:M))) (v n)} IN\r
      E_SY ((v:num->real^3^M) n)`ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`]\r
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;]\r
THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`row i ((v:num->real^3^M) n)`]\r
THEN POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN STRIP_TAC\r
THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`]\r
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) (v n)))\r
==> azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) (v n))) = &0 \/\r
&0< azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)))`)\r
THEN REWRITE_TAC[azim]\r
THEN STRIP_TAC;\r
\r
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`]\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; SET_RULE`{A,A}={A}`])\r
THEN STRIP_TAC\r
THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{vec 0,row i ((v:num->real^3^M) n)}`;`{(row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))}`][GSYM aff]\r
THEN MP_TAC(SET_RULE`row j (v n) IN\r
      aff_ge {vec 0, row i (v n)} {row (SUC (i MOD dimindex (:M))) (v n)}\r
/\ aff_ge {vec 0, row i (v n)} {row (SUC (i MOD dimindex (:M))) (v n)} SUBSET\r
      aff\r
      ({vec 0, row i (v n)} UNION {row (SUC (i MOD dimindex (:M))) (v n)})\r
==> row j ((v:num->real^3^M) n) IN\r
            aff\r
      ({vec 0, row i (v n)} UNION {row (SUC (i MOD dimindex (:M))) (v n)})`)\r
THEN ASM_REWRITE_TAC[SET_RULE` {A,B}UNION{C}={A,B,C}`]\r
THEN MRESAL_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`]\r
[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]\r
THEN RESA_TAC;\r
\r
MP_TAC(REAL_ARITH`\r
&0<azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) (v n))) /\\r
      azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))) <\r
      pi\r
==> ~(azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) (v n))) =\r
      &0 \/\r
      azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))\r
      (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) (v n))) =\r
      pi)`)\r
THEN RESA_TAC\r
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]\r
THEN STRIP_TAC\r
THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`]\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;INTER;IN_ELIM_THM])\r
THEN STRIP_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`][VECTOR_ARITH`A- vec 0=A`]\r
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n))\r
      (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN ASM_REWRITE_TAC[IN_ELIM_THM]\r
THEN REAL_ARITH_TAC;\r
\r
MRESAL_TAC LIM_DROP_LBOUND[`sequentially`;`lift o\r
       (\n. (row i (v n) cross\r
             row (SUC (i MOD dimindex (:M))) (v n))dot\r
            row j ((v:num->real^3^M) n))`;`lift ((u cross v':real^3) dot w)`;`&0`][TRIVIAL_LIMIT_SEQUENTIALLY;LIFT_DROP];\r
\r
ASM_REWRITE_TAC[]\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN POP_ASSUM(fun th-> MP_TAC th\r
THEN REWRITE_TAC[F_SY;IN_ELIM_THM]\r
THEN STRIP_TAC\r
THEN ASSUME_TAC th)\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x':real^3#real^3`]\r
THEN MRESA_TAC(GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)\r
[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x':real^3#real^3`]\r
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]\r
THEN REWRITE_TAC[REAL_ARITH`A<=B <=> A=B\/ A< B`]\r
THEN STRIP_TAC;\r
\r
DISCH_THEN(LABEL_TAC"THY31")\r
THEN GEN_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MP_TAC th\r
THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows]\r
THEN STRIP_TAC\r
THEN ASSUME_TAC th)\r
THEN MRESAL_TAC(GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE (row i (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) (row i (vecmats l))\r
 (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))))`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`vec 0:real^3`][IN_ELIM_THM;REAL_ARITH`A=B\/ A< B<=> A<=B`;VECTOR_ARITH`A- vec 0=A`]\r
THEN REMOVE_THEN"THY31"(fun th-> MRESA_TAC th[`i:num`;`i':num`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`])\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
POP_ASSUM MP_TAC\r
THEN DISCH_THEN(LABEL_TAC"THY32")\r
THEN DISCH_THEN(LABEL_TAC"THY31")\r
THEN GEN_TAC\r
THEN STRIP_TAC\r
THEN POP_ASSUM(fun th-> MP_TAC th\r
THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows]\r
THEN STRIP_TAC\r
THEN ASSUME_TAC th)\r
THEN SUBGOAL_THEN`{row i (vecmats (l:real^(M,3)finite_product)),\r
      row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))} IN\r
      E_SY (vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;\r
\r
REWRITE_TAC[E_SY;IN_ELIM_THM]\r
THEN EXISTS_TAC`i:num`\r
THEN ASM_REWRITE_TAC[];\r
\r
MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`]\r
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]\r
THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]\r
THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]\r
THEN POP_ASSUM MP_TAC\r
THEN RESA_TAC\r
THEN REMOVE_THEN "THY32" MP_TAC\r
THEN RESA_TAC\r
THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]\r
THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))\r
==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/\r
&0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)\r
THEN REWRITE_TAC[azim]\r
THEN STRIP_TAC;\r
\r
MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]\r
THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]\r
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]\r
THEN POP_ASSUM MP_TAC\r
THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}\r
\/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);\r
\r
ASM_REWRITE_TAC[]\r
THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;                IN_INSERT; NOT_IN_EMPTY]\r
THEN ARITH_TAC;\r
\r
MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]\r
THEN REMOVE_ASSUM_TAC\r
THEN REMOVE_ASSUM_TAC\r
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);\r
\r
MP_TAC(REAL_ARITH`\r
&0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\\r
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <\r
      pi\r
==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =\r
      &0 \/\r
      azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))\r
      (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =\r
      pi)`)\r
THEN RESA_TAC\r
THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]\r
THEN STRIP_TAC\r
THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]\r
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;INTER;IN_ELIM_THM])\r
THEN STRIP_TAC;\r
\r
MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]\r
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN ASM_REWRITE_TAC[IN_ELIM_THM]\r
THEN REMOVE_THEN"THY31"(fun th-> MRESA_TAC th[`i:num`;`i':num`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`])\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]\r
THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))\r
      (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;][VECTOR_ARITH`A- vec 0=A`]\r
THEN POP_ASSUM MP_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]\r
THEN ASM_REWRITE_TAC[IN_ELIM_THM]\r
THEN FIND_ASSUM MP_TAC`1<k`\r
THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`]\r
THEN ASM_REWRITE_TAC[]\r
THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`]\r
THEN RESA_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)\r
THEN RESA_TAC;\r
\r
POP_ASSUM (fun th-> SUBST_ALL_TAC(th))\r
THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]\r
THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]\r
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th) THEN ASSUME_TAC th)\r
THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`row 1 (vecmats (l:real^(M,3)finite_product))`;`row (SUC 1) (vecmats (l:real^(M,3)finite_product))`;`(row \r
(dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN REMOVE_THEN"THY31"(fun th-> MRESAL_TAC th[`k:num`;`i':num`;`row (dimindex (:M)) (vecmats(l:real^(M,3)finite_product))`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`dimindex (:M) <= dimindex (:M) /\ SUC 0=1`])\r
THEN POP_ASSUM MP_TAC\r
THEN REAL_ARITH_TAC;\r
\r
MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)`)\r
THEN RESA_TAC \r
THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]\r
THEN \r
MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i-1:num`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row \r
(i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`)\r
THEN RESA_TAC \r
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])\r
THEN RESA_TAC\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]\r
THEN REMOVE_THEN"THY31"(fun th-> MRESA_TAC th[`i-1:num`;`i':num`;`row (i - 1)  (vecmats(l:real^(M,3)finite_product))`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`])\r
THEN POP_ASSUM MP_TAC\r
THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`)\r
THEN RESA_TAC \r
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])\r
THEN REAL_ARITH_TAC\r
]);;\r
\r
\r
\r
\r
let BOUNDED_SY=prove(`\r
stable_system k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)\r
/\ 1< k /\ 2<k\r
==> \r
bounded {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v /\ CONDITION2_SY v }`,\r
REPEAT STRIP_TAC\r
THEN MATCH_MP_TAC BOUNDED_SUBSET\r
THEN EXISTS_TAC`{matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) }`\r
THEN MP_TAC COMPACT_BALL_ANNULUS_MATVEC\r
THEN SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED]\r
THEN RESA_TAC\r
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]\r
THEN SET_TAC[]);;\r
\r
\r
let WJSCPRO= prove (`\r
stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)\r
/\ 2<k\r
==> \r
compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v /\ CONDITION2_SY v }`,\r
SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_SY; CLOSED_SY;]\r
THEN REPEAT STRIP_TAC\r
THEN MP_TAC(ARITH_RULE`2<k ==> 1<k`)\r
THEN RESA_TAC\r
THENL[ MRESA_TAC (GEN_ALL BOUNDED_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;];\r
MRESA_TAC (GEN_ALL CLOSED_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]]);;\r
\r
\r
\r
\r
\r
\r
\r
\r
\r
end;;\r
\r
\r