(* ========================================================================= *) (* Flyspeck "polar fan" formalization. *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* Some natural lemmas that I should perhaps put in Multivariate/flyspeck.ml *) (* ------------------------------------------------------------------------- *) module Polar_fan = struct let DIHV_ARCV = prove (`!e u v w:real^N. orthogonal (e - u) (v - u) /\ orthogonal (e - u) (w - u) /\ ~(e = u) ==> dihV u e v w = arcV u v w`, GEOM_ORIGIN_TAC `u:real^N` THEN REWRITE_TAC[dihV; orthogonal; VECTOR_SUB_RZERO] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN SIMP_TAC[DOT_SYM; VECTOR_MUL_LZERO; VECTOR_SUB_RZERO] THEN REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO] THEN REWRITE_TAC[VECTOR_ANGLE_LMUL; VECTOR_ANGLE_RMUL] THEN SIMP_TAC[DOT_POS_LE; DOT_EQ_0]);; let AZIM_DIHV_SAME_STRONG = prove (`!v w v1 v2:real^3. ~collinear {v,w,v1} /\ ~collinear {v,w,v2} /\ azim v w v1 v2 <= pi ==> azim v w v1 v2 = dihV v w v1 v2`, REWRITE_TAC[REAL_LE_LT] THEN MESON_TAC[AZIM_DIHV_SAME; AZIM_DIHV_EQ_PI]);; let AZIM_ARCV = prove (`!e u v w:real^3. orthogonal (e - u) (v - u) /\ orthogonal (e - u) (w - u) /\ ~collinear{u,e,v} /\ ~collinear{u,e,w} /\ azim u e v w <= pi ==> azim u e v w = arcV u v w`, REPEAT GEN_TAC THEN ASM_CASES_TAC `u:real^3 = e` THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN STRIP_TAC THEN ASM_SIMP_TAC[GSYM DIHV_ARCV] THEN MATCH_MP_TAC AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[]);; let PLANE_AFFINE_HULL_3 = prove (`!a b c:real^N. plane(affine hull {a,b,c}) <=> ~collinear{a,b,c}`, REWRITE_TAC[plane] THEN MESON_TAC[COLLINEAR_AFFINE_HULL_COLLINEAR]);; let AFFINE_HULL_3_GENERATED = prove (`!s u v w:real^N. s SUBSET affine hull {u,v,w} /\ ~collinear s ==> affine hull {u,v,w} = affine hull s`, REWRITE_TAC[COLLINEAR_AFF_DIM; INT_NOT_LE] THEN REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN GEN_REWRITE_TAC RAND_CONV [GSYM HULL_HULL] THEN MATCH_MP_TAC AFF_DIM_EQ_AFFINE_HULL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&2:int` THEN CONJ_TAC THENL [ALL_TAC; ASM_INT_ARITH_TAC] THEN REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN W(MP_TAC o PART_MATCH (lhand o rand) AFF_DIM_LE_CARD o lhand o goal_concl) THEN REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] INT_LE_TRANS) THEN REWRITE_TAC[INT_LE_SUB_RADD; INT_OF_NUM_ADD; INT_OF_NUM_LE] THEN SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN ARITH_TAC);; let COLLINEAR_AZIM_0_OR_PI = prove (`!u e v w. collinear {u,v,w} ==> azim u e v w = &0 \/ azim u e v w = pi`, REPEAT STRIP_TAC THEN ASM_CASES_TAC `collinear{u:real^3,e,v}` THEN ASM_SIMP_TAC[AZIM_DEGENERATE] THEN ASM_CASES_TAC `collinear{u:real^3,e,w}` THEN ASM_SIMP_TAC[AZIM_DEGENERATE] THEN ASM_SIMP_TAC[AZIM_EQ_0_PI_EQ_COPLANAR] THEN ONCE_REWRITE_TAC[SET_RULE `{u,e,v,w} = {u,v,w,e}`] THEN ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);; let ANGLES_ADD_AFF_GE = prove (`!u v w x:real^N. ~(v = u) /\ ~(w = u) /\ ~(x = u) /\ x IN aff_ge {u} {v,w} ==> angle(v,u,x) + angle(x,u,w) = angle(v,u,w)`, GEOM_ORIGIN_TAC `u:real^N` THEN REPEAT GEN_TAC THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_SIMP_TAC[AFF_GE_1_2_0] THEN REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN SUBGOAL_THEN `a = &0 /\ b = &0 \/ &0 < a + b` STRIP_ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]; ALL_TAC] THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^N`; `w:real^N`; `inv(a + b) % x:real^N`; `vec 0:real^N`] ANGLES_ADD_BETWEEN) THEN ASM_REWRITE_TAC[angle; VECTOR_SUB_RZERO] THEN ASM_SIMP_TAC[VECTOR_ANGLE_RMUL; VECTOR_ANGLE_LMUL; REAL_INV_EQ_0; REAL_LE_INV_EQ; REAL_LT_IMP_NZ; REAL_LT_IMP_LE] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[BETWEEN_IN_SEGMENT; CONVEX_HULL_2; SEGMENT_CONVEX_HULL] THEN REWRITE_TAC[IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC [`a / (a + b):real`; `b / (a + b):real`] THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE; VECTOR_ADD_LDISTRIB] THEN REWRITE_TAC[VECTOR_MUL_ASSOC; real_div; REAL_MUL_AC] THEN UNDISCH_TAC `&0 < a + b` THEN CONV_TAC REAL_FIELD);; let AFF_GE_SCALE_LEMMA = prove (`!a u v:real^N. &0 < a /\ ~(v = vec 0) ==> aff_ge {vec 0} {a % u,v} = aff_ge {vec 0} {u,v}`, REPEAT STRIP_TAC THEN ASM_CASES_TAC `u:real^N = vec 0` THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO] THEN ASM_SIMP_TAC[AFF_GE_1_2_0; VECTOR_MUL_EQ_0; REAL_LT_IMP_NZ; SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET; FORALL_IN_GSPEC] THEN CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THENL [EXISTS_TAC `a * b:real`; EXISTS_TAC `b / a:real`] THEN EXISTS_TAC `c:real` THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_LE_MUL; REAL_LT_IMP_LE] THEN REWRITE_TAC[VECTOR_MUL_ASSOC] THEN REPLICATE_TAC 2 (AP_THM_TAC THEN AP_TERM_TAC) THEN UNDISCH_TAC `&0 < a` THEN CONV_TAC REAL_FIELD);; let AZIM_SAME_WITHIN_AFF_GE = prove (`!a u v w z. v IN aff_ge {a} {u,w} /\ ~collinear{a,u,v} /\ ~collinear{a,u,w} ==> azim a u v z = azim a u w z`, GEOM_ORIGIN_TAC `a:real^3` THEN GEOM_BASIS_MULTIPLE_TAC 3 `u:real^3` THEN X_GEN_TAC `u:real` THEN ASM_CASES_TAC `u = &0` THEN ASM_SIMP_TAC[AZIM_DEGENERATE; VECTOR_MUL_LZERO; REAL_LE_LT] THEN ASM_SIMP_TAC[AZIM_SPECIAL_SCALE; COLLINEAR_SPECIAL_SCALE] THEN DISCH_TAC THEN REPEAT GEN_TAC THEN ASM_CASES_TAC `w:real^3 = vec 0` THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN ASM_SIMP_TAC[AFF_GE_SCALE_LEMMA] THEN REWRITE_TAC[COLLINEAR_BASIS_3; AZIM_ARG] THEN ASM_SIMP_TAC[AFF_GE_1_2_0; BASIS_NONZERO; ARITH; DIMINDEX_3; SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM; IN_ELIM_THM] THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `dropout 3:real^3->real^2`) THEN REWRITE_TAC[DROPOUT_ADD; DROPOUT_MUL; DROPOUT_BASIS_3] THEN REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN DISCH_THEN SUBST1_TAC THEN REPEAT DISCH_TAC THEN REWRITE_TAC[COMPLEX_CMUL] THEN REWRITE_TAC[complex_div; COMPLEX_INV_MUL; GSYM CX_INV] THEN ONCE_REWRITE_TAC[COMPLEX_RING `a * b * c:complex = b * a * c`] THEN MATCH_MP_TAC ARG_MUL_CX THEN REWRITE_TAC[REAL_LT_INV_EQ] THEN ASM_REWRITE_TAC[REAL_LT_LE] THEN ASM_MESON_TAC[VECTOR_MUL_LZERO]);; let AZIM_SAME_WITHIN_AFF_GE_ALT = prove (`!a u v w z. v IN aff_ge {a} {u,w} /\ ~collinear{a,u,v} /\ ~collinear{a,u,w} ==> azim a u z v = azim a u z w`, REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP AZIM_SAME_WITHIN_AFF_GE) THEN ASM_CASES_TAC `collinear {a:real^3,u,z}` THEN ASM_SIMP_TAC[AZIM_DEGENERATE] THEN W(MP_TAC o PART_MATCH (lhs o rand) AZIM_COMPL o lhand o goal_concl) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN W(MP_TAC o PART_MATCH (lhs o rand) AZIM_COMPL o rand o goal_concl) THEN ASM_SIMP_TAC[]);; let COLLINEAR_WITHIN_AFF_GE_COLLINEAR = prove (`!a u v w:real^N. v IN aff_ge {a} {u,w} /\ collinear{a,u,w} ==> collinear{a,v,w}`, GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT GEN_TAC THEN ASM_CASES_TAC `w:real^N = vec 0` THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN ASM_CASES_TAC `u:real^N = vec 0` THENL [ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF] THEN ASM_REWRITE_TAC[SET_RULE `{a} DIFF {a,b} = {}`] THEN REWRITE_TAC[GSYM CONVEX_HULL_AFF_GE] THEN ONCE_REWRITE_TAC[SET_RULE `{z,v,w} = {z,w,v}`] THEN ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN MESON_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET]; ONCE_REWRITE_TAC[SET_RULE `{z,v,w} = {z,w,v}`] THEN ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_TAC `a:real`)) THEN ASM_SIMP_TAC[AFF_GE_1_2_0; SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_MUL_ASSOC] THEN MESON_TAC[]]);; (* ------------------------------------------------------------------------- *) (* Borderline case. *) (* ------------------------------------------------------------------------- *) let GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE = prove (`!u v w. ~collinear{vec 0,v,u} /\ ~collinear{vec 0,v,w} /\ azim (vec 0) v w u = pi /\ aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {} ==> v IN aff_ge {vec 0} {u,w}`, REPEAT GEN_TAC THEN MAP_EVERY (fun t -> ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC]) [`v:real^3 = vec 0`; `u:real^3 = vec 0`; `w:real^3 = vec 0`; `u:real^3 = v`; `v:real^3 = w`] THEN REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_SIMP_TAC[AZIM_EQ_PI] THEN ASM_SIMP_TAC[AFF_LT_2_1; AFF_LT_1_1; AFF_GE_1_2; DISJOINT_INSERT; DISJOINT_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN REWRITE_TAC[TAUT `p /\ x = &1 /\ q <=> x = &1 /\ p /\ q`] THEN REWRITE_TAC[VECTOR_MUL_RZERO; REAL_ARITH `t1 + x = &1 <=> t1 = &1 - x`] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; VECTOR_ADD_LID] THEN ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN REWRITE_TAC[UNWIND_THM2] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2; IN_ELIM_THM] THEN REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`s:real`; `t:real`] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `&0 < s \/ s <= &0`) THENL [MAP_EVERY EXISTS_TAC [`--t / s:real`; `&1 / s`] THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; REAL_LT_IMP_LE; REAL_ARITH `t < &0 ==> &0 <= --t`] THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN VECTOR_ARITH_TAC; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `s INTER t = {} ==> !x. x IN s /\ x IN t ==> P`)) THEN EXISTS_TAC `t % u:real^3` THEN REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN MAP_EVERY EXISTS_TAC [`--s:real`; `&1`] THEN REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]);; let UNION_AFF_GE_1_2 = prove (`!a u v w:real^N. v IN aff_ge {a} {u,w} /\ ~(u = a) /\ ~(v = a) /\ ~(w = a) ==> aff_ge {a} {u,v} UNION aff_ge {a} {v,w} = aff_ge {a} {u,w}`, GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(v:real^N) IN aff_ge {vec 0} {u,w}` THEN ASM_SIMP_TAC[AFF_GE_1_2_0; SET_RULE `a UNION b = c <=> a SUBSET c /\ b SUBSET c /\ c SUBSET a UNION b`] THEN REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN REWRITE_TAC[IN_ELIM_THM; IN_UNION; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`m:real`; `n:real`] THEN STRIP_TAC THEN REPEAT CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THENL [MAP_EVERY EXISTS_TAC [`a + b * m:real`; `b * n:real`] THEN ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL] THEN VECTOR_ARITH_TAC; MAP_EVERY EXISTS_TAC [`a * m:real`; `a * n + b:real`] THEN ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL] THEN VECTOR_ARITH_TAC; ALL_TAC] THEN DISJ_CASES_TAC(REAL_ARITH `b * m <= a * n \/ a * n <= b * m`) THENL [DISJ1_TAC; DISJ2_TAC] THEN ASM_REWRITE_TAC[] THENL [MAP_EVERY EXISTS_TAC [`a - b / n * m:real`; `b / n:real`] THEN ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; VECTOR_ADD_ASSOC] THEN ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; REAL_SUB_ADD; VECTOR_MUL_RCANCEL; VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN ASM_SIMP_TAC[REAL_SUB_LE; REAL_LE_DIV] THEN ASM_CASES_TAC `n = &0` THENL [MAP_EVERY UNDISCH_TAC [`v:real^N = m % u + n % w`; `b * m <= a * n`] THEN ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LE_MUL; REAL_ENTIRE; REAL_ARITH `&0 <= x ==> (x <= &0 <=> x = &0)`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO]; ASM_SIMP_TAC[REAL_DIV_RMUL] THEN REWRITE_TAC[REAL_ARITH `b / n * m:real = (b * m) / n`] THEN ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_LE]]; MAP_EVERY EXISTS_TAC [`a / m:real`; `b - a / m * n:real`] THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN REWRITE_TAC[VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_RDISTRIB] THEN ASM_REWRITE_TAC[REAL_SUB_ADD2; VECTOR_MUL_RCANCEL; VECTOR_ARITH `x + a:real^N = y + a <=> x = y`] THEN ASM_SIMP_TAC[REAL_SUB_LE; REAL_LE_DIV] THEN ASM_CASES_TAC `m = &0` THENL [MAP_EVERY UNDISCH_TAC [`v:real^N = m % u + n % w`; `a * n <= b * m`] THEN ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LE_MUL; REAL_ENTIRE; REAL_ARITH `&0 <= x ==> (x <= &0 <=> x = &0)`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO]; ASM_SIMP_TAC[REAL_DIV_RMUL] THEN REWRITE_TAC[REAL_ARITH `b / n * m:real = (b * m) / n`] THEN ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_LE]]]);; (* ------------------------------------------------------------------------- *) (* More specialist lemmas. *) (* ------------------------------------------------------------------------- *) let AZIM_CYCLE_BASIC_PROPERTIES = prove (`!W v w p. FINITE W /\ p IN W ==> (azim_cycle W v w p) IN W /\ !q. q IN W /\ ~(q = p) ==> azim v w p (azim_cycle W v w p) <= azim v w p q`, REPEAT GEN_TAC THEN ASM_CASES_TAC `W SUBSET {p:real^3}` THENL [ASM_SIMP_TAC[Sphere.azim_cycle; AZIM_REFL; azim]; ALL_TAC] THEN UNDISCH_TAC `~(W SUBSET {p:real^3})` THEN ONCE_REWRITE_TAC[TAUT `p ==> q /\ r ==> s <=> p /\ q ==> r ==> s`] THEN DISCH_THEN(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) THEN SIMP_TAC[IN] THEN MESON_TAC[REAL_LE_LT]);; let AZIM_CYCLE_TWO_POINT_SET_ALT = prove (`!W x u v w. W = {v,w} ==> azim_cycle W x u v = w`, MESON_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]);; let IVS_AZIM_CYCLE_TWO_POINT_SET = prove (`!a b. ivs_azim_cycle {a, b} v w a = b`, REWRITE_TAC[Wrgcvdr_cizmrrh.ivs_azim_cycle; NOT_INSERT_EMPTY] THEN SIMP_TAC[SET_RULE `x IN {a,b} /\ P x <=> x = a /\ P a \/ x = b /\ P b`] THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN MESON_TAC[]);; let IVS_AZIM_CYCLE_TWO_POINT_SET_ALT = prove (`!W x u v w. W = {v,w} ==> ivs_azim_cycle W x u v = w`, MESON_TAC[IVS_AZIM_CYCLE_TWO_POINT_SET]);; let AZIM_CYCLE_SING = prove (`!x u v. azim_cycle {v} x u v = v`, REWRITE_TAC[Sphere.azim_cycle; SUBSET_REFL]);; let IVS_AZIM_CYCLE_SING = prove (`!x u v. ivs_azim_cycle {v} x u v = v`, ONCE_REWRITE_TAC[SET_RULE `{v} = {v,v}`] THEN REWRITE_TAC[IVS_AZIM_CYCLE_TWO_POINT_SET]);; let RHO_NODE1_INJECTIVE = prove (`!V E FF. local_fan(V,E,FF) ==> !v w. v IN V /\ w IN V ==> (rho_node1 FF v = rho_node1 FF w <=> v = w)`, MESON_TAC[Local_lemmas.IVS_RHO_IDD]);; let IVS_RHO_NODE1_IN_V = prove (`!V E FF. local_fan (V,E,FF) ==> !v. v IN V ==> ivs_rho_node1 FF v IN V`, ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V; Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);; let LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V = prove (`!V E FF. local_fan (V,E,FF) /\ v IN V ==> !i. ITER i (ivs_rho_node1 FF) v IN V`, REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[ITER] THEN ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]);; let LOCAL_FAN_ORBIT_MAP_EXPLICIT = prove (`!V E FF v w. local_fan(V,E,FF) /\ v IN V /\ w IN V ==> ?i. i < CARD V /\ w = ITER i (rho_node1 FF) v`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP Local_lemmas.LOCAL_FAN_ORBIT_MAP_V) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER; Hypermap.orbit_map] THEN ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN ASM_REWRITE_TAC[GE; LE_0] THEN DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN EXISTS_TAC `n MOD (CARD(V:real^3->bool))` THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN MP_TAC(ISPECL [`n:num`; `CARD(V:real^3->bool)`] DIVISION) THEN ABBREV_TAC `i = n MOD (CARD(V:real^3->bool))` THEN ABBREV_TAC `m = n DIV (CARD(V:real^3->bool))` THEN ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN(K ALL_TAC) THEN SPEC_TAC(`m:num`,`p:num`) THEN INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ONCE_REWRITE_TAC[ARITH_RULE `(a + b) + c:num = (a + c) + b`] THEN ONCE_REWRITE_TAC[GSYM ITER_ADD] THEN FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID) THEN ASM_SIMP_TAC[]);; let LOCAL_FAN_ORBIT_MAP_EXPLICIT_IVS = prove (`!V E FF v w. local_fan(V,E,FF) /\ v IN V /\ w IN V ==> ?i. i < CARD V /\ w = ITER i (ivs_rho_node1 FF) v`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPECL [`w:real^3`; `v:real^3`] o MATCH_MP (REWRITE_RULE[IMP_CONJ] LOCAL_FAN_ORBIT_MAP_EXPLICIT)) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN UNDISCH_TAC `(w:real^3) IN V` THEN SPEC_TAC(`w:real^3`,`w:real^3`) THEN SPEC_TAC(`i:num`,`n:num`) THEN INDUCT_TAC THENL [REWRITE_TAC[ITER]; ALL_TAC] THEN X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN ONCE_REWRITE_TAC[ITER_ALT] THEN REWRITE_TAC[ITER] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `ITER n (ivs_rho_node1 FF) (ITER n (rho_node1 FF) x)` THEN CONJ_TAC THENL [AP_TERM_TAC; ASM_SIMP_TAC[]] THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);; let ITER_IVS_RHO_IDD = prove (`!V E FF v n. local_fan (V,E,FF) /\ v IN V ==> ITER n (ivs_rho_node1 FF) (ITER n (rho_node1 FF) v) = v`, REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THENL [REWRITE_TAC[ITER]; ONCE_REWRITE_TAC[ITER_ALT] THEN REWRITE_TAC[ITER]] THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);; let ITER_RHO_IVS_IDD = prove (`!V E FF v n. local_fan (V,E,FF) /\ v IN V ==> ITER n (rho_node1 FF) (ITER n (ivs_rho_node1 FF) v) = v`, REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THENL [REWRITE_TAC[ITER]; ONCE_REWRITE_TAC[ITER_ALT] THEN REWRITE_TAC[ITER]] THEN ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD; LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V]);; let LOFA_IMP_ITER_IVS_RHO_NODE_ID = prove (`!V E FF'. local_fan (V,E,FF) ==> (!v. v IN V ==> ITER (CARD V) (ivs_rho_node1 FF) v = v)`, MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID; ITER_IVS_RHO_IDD]);; let GENERIC_LOCAL_FAN_AZIM_POS = prove (`!V E FF v w. convex_local_fan(V,E,FF) /\ generic V E /\ (!v. v IN V ==> interior_angle1 (vec 0) FF v < pi) /\ v IN V /\ w IN V /\ ~(w = v) /\ ~(w = rho_node1 FF v) ==> &0 < sin(azim (vec 0) v (rho_node1 FF v) w)`, REPEAT STRIP_TAC THEN FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [Wrgcvdr_cizmrrh.convex_local_fan]) THEN MATCH_MP_TAC SIN_POS_PI THEN REWRITE_TAC[REAL_LT_LE] THEN REWRITE_TAC[Local_lemmas.AZIM_RANGE] THEN ONCE_REWRITE_TAC[MESON[] `~(z = a) /\ p /\ q <=> p /\ ~(a = z) /\ q`] THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.IN_V_IMP_AZIM_LESS_PI]; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o SPECL [`v:real^3`; `w:real^3`] o MATCH_MP (REWRITE_RULE[IMP_CONJ] LOCAL_FAN_ORBIT_MAP_EXPLICIT)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` (STRIP_ASSUME_TAC o GSYM)) THEN ASM_CASES_TAC `m = 0` THENL [ASM_MESON_TAC[ITER]; ALL_TAC] THEN ASM_CASES_TAC `m = 1` THENL [ASM_MESON_TAC[Lvducxu.ITER12]; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP (REWRITE_RULE[IMP_CONJ] Local_lemmas.EGHNAVX)) THEN DISCH_THEN(MP_TAC o SPECL [`\i. azim (vec 0) v (rho_node1 FF v) (ITER i (rho_node1 FF) v)`; `m:num`; `v:real^3`; `\i. ITER i (rho_node1 FF) (v:real^3)`; `CARD(V:real^3->bool)`]) THEN ASM_REWRITE_TAC[IMP_IMP; Lvducxu.ITER12] THEN ANTS_TAC THENL [ASM_MESON_TAC[IN_INSERT; Nkezbfc_local.PROPERTIES_GENERIC1]; ALL_TAC] THEN REWRITE_TAC[TAUT `p ==> ~q /\ ~r <=> q \/ r ==> ~p`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL [DISCH_THEN(MP_TAC o SPEC `1` o el 3 o CONJUNCTS) THEN ASM_REWRITE_TAC[Lvducxu.ITER12; NOT_IMP] THEN CONJ_TAC THENL [ASM_ARITH_TAC; ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; REAL_LT_REFL]]; REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(MP_TAC o CONJUNCT2) THEN REWRITE_TAC[NOT_IMP] THEN FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `m < CARD V ==> m < CARD V - 1 \/ m = CARD V - 1`)) THEN DISCH_THEN DISJ_CASES_TAC THENL [REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [ASM_SIMP_TAC[LE_1] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `x = pi ==> x <= y /\ y <= pi ==> pi = y`)) THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "w" THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `CARD(V:real^3->bool) - 1` o CONJUNCT1) THEN REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V; REAL_LT_REFL]]; MATCH_MP_TAC(TAUT `F ==> p`) THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `x < pi /\ y = pi ==> ~(x = y)`) THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `ivs_rho_node1 FF v = w` (fun t -> ASM_REWRITE_TAC[t]) THEN SUBGOAL_THEN `v = rho_node1 FF w` MP_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]] THEN EXPAND_TAC "w" THEN REWRITE_TAC[GSYM(CONJUNCT2 ITER)] THEN SUBGOAL_THEN `SUC m = CARD(V:real^3->bool)` SUBST1_TAC THENL [ASM_ARITH_TAC; ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]]]]);; let nn_of_hyp3 = prove (`!x V E. nn_of_hyp (x,V,E) = \(v,w). if (v,w) IN darts_of_hyp E V then (v,azim_cycle (EE v E) x v w) else (v,w)`, REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; Wrgcvdr_cizmrrh.nn_of_hyp]);; let ff_of_hyp3 = prove (`!x V E. ff_of_hyp (x,V,E) = \(v,w). if (v,w) IN darts_of_hyp E V then (w,ivs_azim_cycle (EE w E) x w v) else (v,w)`, REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; Wrgcvdr_cizmrrh.ff_of_hyp]);; let ee_of_hyp3 = prove (`!x V E. ee_of_hyp (x,V,E) = \(v,w). if (v,w) IN darts_of_hyp E V then (w,v) else (v,w)`, REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; Wrgcvdr_cizmrrh.ee_of_hyp]);; let ORDER_AZIM_SUM2Pi_0 = prove (`!x y z n g. ~collinear {x, y, z} /\ (!i. i IN 0..n ==> ~collinear {x, y, g i}) /\ g(n+1) = g 0 /\ 0 < n /\ (!j k. j IN 0..n /\ k IN 0..n /\ j < k ==> azim x y z (g j) < azim x y z (g k)) ==> sum (0..n) (\i. azim x y (g i) (g (i + 1))) = &2 * pi`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`x:real^3`; `y:real^3`; `z:real^3`; `n + 1`; `\i. (g:num->real^3) (i - 1)`] Counting_spheres.ORDER_AZIM_SUM2Pi) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[ADD_SUB; SUB_REFL; ARITH_RULE `1 < n + 1 <=> 0 < n`] THEN REWRITE_TAC[IN_NUMSEG] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ASM_ARITH_TAC; GEN_REWRITE_TAC (funpow 4 LAND_CONV) [ARITH_RULE `1 = 0 + 1`] THEN REWRITE_TAC[SUM_OFFSET; ADD_SUB]]);; let LOCAL_FAN_NOT_EMPTY_FF = prove (`!V E FF. local_fan (V,E,FF) ==> ~(FF = {})`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP (REWRITE_RULE[IMP_CONJ] Wrgcvdr_cizmrrh.BIJ_BETWEEN_FF_AND_V)) THEN DISCH_THEN(MP_TAC o SPEC `FST:real^3#real^3->real^3`) THEN ASM_REWRITE_TAC[BIJ; INJ; SURJ; NOT_IN_EMPTY; ETA_AX] THEN FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN SET_TAC[]);; let LOCAL_FAN_NOT_CARD_FF_GE_2 = prove (`!V E FF. local_fan (V,E,FF) ==> 2 <= CARD FF`, REPEAT STRIP_TAC THEN REWRITE_TAC[ARITH_RULE `2 <= n <=> ~(n = 0) /\ ~(n = 1)`] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF) THEN ASM_SIMP_TAC[MESON[HAS_SIZE] `FINITE s ==> (CARD s = n <=> s HAS_SIZE n)`] THEN CONJ_TAC THEN CONV_TAC(RAND_CONV HAS_SIZE_CONV) THEN ASM_MESON_TAC[LOCAL_FAN_NOT_EMPTY_FF; Local_lemmas.LOCAL_FAN_NOT_SING_FF]);; let SIN_AZIM_MUTUAL_CROSS = prove (`(sin (azim (vec 0) u v w) < &0 <=> (u cross v) dot w < &0) /\ (&0 < sin (azim (vec 0) u v w) <=> &0 < (u cross v) dot w) /\ (sin (azim (vec 0) u v w) <= &0 <=> (u cross v) dot w <= &0) /\ (&0 <= sin (azim (vec 0) u v w) <=> &0 <= (u cross v) dot w) /\ (sin (azim (vec 0) u v w) = &0 <=> (u cross v) dot w = &0)`, REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS; GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT]);; let CROSS_POSITIVE_MULTIPLE_AZIM_AXIS = prove (`!x y z. ~(x = vec 0) /\ orthogonal x y /\ orthogonal x z /\ &0 < azim (vec 0) x y z /\ azim (vec 0) x y z < pi ==> ?a. &0 < a /\ y cross z = a % x`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `collinear{vec 0,x,y cross z}` MP_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM CROSS_EQ_0] THEN VEC3_TAC; ALL_TAC] THEN ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real` THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `&0 < sin(azim (vec 0) x y z)` MP_TAC THENL [ASM_SIMP_TAC[SIN_POS_PI]; REWRITE_TAC[SIN_AZIM_MUTUAL_CROSS]] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_SIMP_TAC[REAL_LT_MUL_EQ; DOT_LMUL; DOT_POS_LT]);; let CROSS_POSITIVE_MULTIPLE_AZIM_AXIS_ALT = prove (`!x y z. ~(x = vec 0) /\ orthogonal x y /\ orthogonal x z /\ &0 < azim (vec 0) x y z /\ azim (vec 0) x y z < pi ==> ?a. &0 < a /\ x = a % (y cross z)`, REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP CROSS_POSITIVE_MULTIPLE_AZIM_AXIS) THEN DISCH_THEN(X_CHOOSE_THEN `a:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `inv(a):real` THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ; VECTOR_MUL_LID]);; (* ------------------------------------------------------------------------- *) (* Equivalences for fan7 and so for FAN. *) (* ------------------------------------------------------------------------- *) let GMLWKPK = prove (`!x:real^N V E. graph E ==> (fan7(x,V,E) <=> !e1 e2. e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} ==> (e1 INTER e2 = {} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\ (!v. e1 INTER e2 = {v} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} {v}))`, REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN EQ_TAC THENL [SIMP_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]; ALL_TAC] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e1:real^N->bool` THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e2:real^N->bool` THEN MATCH_MP_TAC(TAUT `(p ==> q ==> r) ==> (q ==> p) ==> q ==> r`) THEN STRIP_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `e1 = e2 \/ e1 INTER e2 = {} \/ (?v:real^N. e1 INTER e2 = {v})` MP_TAC THENL [ALL_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN ASM_MESON_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]] THEN SUBGOAL_THEN `?a b:real^N c d:real^N. e1 = {a,b} /\ e2 = {c,d}` MP_TAC THENL [ALL_TAC; DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN SET_TAC[]] THEN FIRST_ASSUM(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[IN_UNION; IN_ELIM_THM] THEN SUBGOAL_THEN `!e:real^N->bool. e IN E ==> ?v w. ~(v = w) /\ e = {v,w}` (LABEL_TAC "*") THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.graph]) THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[IN] THEN CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[]; ASM_MESON_TAC[SET_RULE `{v,v} = {v}`]]);; let GMLWKPK_ALT = prove (`!x:real^N V E. graph E /\ (!e. e IN E ==> ~(x IN e)) ==> (fan7(x,V,E) <=> (!e1 e2. e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\ e1 INTER e2 = {} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\ (!e1 e2 v. e1 IN E /\ e2 IN E /\ e1 INTER e2 = {v} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} {v}))`, REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN EQ_TAC THEN SIMP_TAC[IN_UNION] THEN STRIP_TAC THEN MATCH_MP_TAC(MESON[] `(!x y. R x y ==> R y x) /\ (!x y. P x /\ P y ==> R x y) /\ (!x y. Q x /\ Q y ==> R x y) /\ (!x y. P x /\ Q y ==> R x y) ==> !x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y`) THEN CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ASM_SIMP_TAC[]] THEN CONJ_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THENL [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> a = c /\ b = c`] THEN SET_TAC[]; X_GEN_TAC `e1:real^N->bool` THEN DISCH_TAC THEN X_GEN_TAC `v:real^N`] THEN SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`u:real^N`; `w:real^N`] THEN STRIP_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[SET_RULE `{a,b} INTER {c} = {d} <=> d = c /\ (a = c \/ b = c)`] THEN REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]);; let FAN_ECONOMIZED = prove (`!x:real^N V E. FAN (x,V,E) <=> UNIONS E SUBSET V /\ graph E /\ fan1 (x,V,E) /\ fan2 (x,V,E) /\ fan6 (x,V,E) /\ (!e1 e2. e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} ==> (e1 INTER e2 = {} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\ (!v. e1 INTER e2 = {v} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} {v}))`, REPEAT GEN_TAC THEN REWRITE_TAC[Fan.FAN] THEN AP_TERM_TAC THEN MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN DISCH_TAC THEN REPEAT AP_TERM_TAC THEN ASM_SIMP_TAC[GMLWKPK]);; let FAN7_AFF_GT_CONDITION = prove (`!x:real^N V E. graph E /\ ~(x IN V) /\ (!e. e IN E ==> e SUBSET V /\ ~(x IN e)) /\ (!v w. v IN V /\ w IN V ==> aff_ge {x} {v} INTER aff_ge {x} {w} = aff_ge {x} ({v} INTER {w})) /\ (!v e. v IN V /\ e IN E ==> aff_gt {x} {v} INTER aff_gt {x} e = {}) /\ (!e1 e2. e1 IN E /\ e2 IN E /\ ~(e1 = e2) ==> aff_gt {x} e1 INTER aff_gt {x} e2 = {}) ==> fan7(x,V,E)`, let lemma1 = prove (`!x v:real^N. ~(v = x) ==> aff_ge {x} {v} = aff_gt {x} {v} UNION {x}`, REPEAT STRIP_TAC THEN W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_AFF_GT_DECOMP o lhand o goal_concl) THEN REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN REWRITE_TAC[SET_RULE `{f x | x IN {a}} = {f a}`; UNIONS_1] THEN REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; SET_RULE `{v} DELETE v = {}`] THEN REWRITE_TAC[AFFINE_HULL_SING]) and lemma2 = prove (`!x v w:real^N. ~(v = x) /\ ~(w = x) ==> aff_ge {x} {v,w} = aff_gt {x} {v,w} UNION aff_ge {x} {v} UNION aff_ge {x} {w}`, REPEAT STRIP_TAC THEN ASM_CASES_TAC `w:real^N = v` THENL [ASM_REWRITE_TAC[INSERT_AC; AFF_GT_SUBSET_AFF_GE; SET_RULE `s = t UNION s UNION s <=> t SUBSET s`]; W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_AFF_GT_DECOMP o lhand o goal_concl) THEN REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN REWRITE_TAC[SET_RULE `{f x | x IN {a,b}} = {f a,f b}`; UNIONS_2] THEN ASM_SIMP_TAC[SET_RULE `~(v = w) ==> {v,w} DELETE v = {w}`; SET_RULE `~(v = w) ==> {v,w} DELETE w = {v}`] THEN REWRITE_TAC[UNION_ACI]]) and slemma = prove (`!P:(A->bool)->(A->bool)->bool. (!v w. ~(v = w) ==> P {v,w} {v,w}) /\ (!v w y z. ~(v = w) /\ ~(y = z) /\ {v,w} INTER {y,z} = {} ==> P {v,w} {y,z}) /\ (!v w y. ~(v = w) /\ ~(w = y) /\ ~(v = y) ==> P {v,w} {w,y}) ==> !v w y z. ~(v = w) /\ ~(y = z) ==> P {v,w} {y,z}`, REPEAT STRIP_TAC THEN ASM_CASES_TAC `{v:A,w} = {y,z}` THEN ASM_SIMP_TAC[] THEN ASM_CASES_TAC `{v:A,w} INTER {y,z} = {}` THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `v:A = y \/ v = z \/ w = y \/ w = z` MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC) THEN ASM_MESON_TAC[SET_RULE `{a,b} = {b,a}`]) in REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN SUBGOAL_THEN `!v:real^N e. v IN V /\ e IN E ==> aff_gt {x} e INTER aff_gt {x} {v} = {}` ASSUME_TAC THENL [ASM_MESON_TAC[INTER_COMM]; ALL_TAC] THEN REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[] `(!e1 e2. R e1 e2 <=> R e2 e1) /\ (!e1. Q e1 ==> !e2. Q e2 ==> R e1 e2) /\ (!e1. P e1 ==> (!e2. P e2 ==> R e1 e2) /\ (!e2. Q e2 ==> R e1 e2)) ==> !e1 e2. (P e1 \/ Q e1) /\ (P e2 \/ Q e2) ==> R e1 e2`) THEN CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ALL_TAC] THEN ASM_SIMP_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `e1:real^N->bool` THEN DISCH_TAC THEN SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN DISCH_THEN(X_CHOOSE_THEN `v:real^N` (X_CHOOSE_THEN `w:real^N` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN SUBGOAL_THEN `{v:real^N,w} SUBSET V /\ ~(x IN {v,w})` STRIP_ASSUME_TAC THENL [ASM MESON_TAC[]; ALL_TAC] THEN CONJ_TAC THENL [X_GEN_TAC `e2:real^N->bool` THEN DISCH_TAC THEN SUBGOAL_THEN `(e2:real^N->bool) HAS_SIZE 2` MP_TAC THENL [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN DISCH_THEN(X_CHOOSE_THEN `y:real^N` (X_CHOOSE_THEN `z:real^N` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN SUBGOAL_THEN `{y:real^N,z} SUBSET V /\ ~(x IN {y,z})` STRIP_ASSUME_TAC THENL [ASM MESON_TAC[]; ALL_TAC] THEN MAP_EVERY UNDISCH_TAC [`{v:real^N, w} IN E`; `{y:real^N, z} IN E`; `{v:real^N, w} SUBSET V`; `{y:real^N, z} SUBSET V`; `~((x:real^N) IN {v,w})`; `~((x:real^N) IN {y,z})`; `~(y:real^N = z)`; `~(v:real^N = w)`] THEN GEN_REWRITE_TAC I [IMP_IMP] THEN MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`z:real^N`; `y:real^N`; `w:real^N`; `v:real^N`] THEN MATCH_MP_TAC slemma THEN CONJ_TAC THENL [REWRITE_TAC[INTER_IDEMPOT]; ALL_TAC] THEN REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN SIMP_TAC[SET_RULE `~(y = v) ==> {v,w} INTER {w,y} = {w}`] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN REWRITE_TAC[SET_RULE `{a,b} INTER {c,d} = {} <=> ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d)`] THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[lemma2; UNION_OVER_INTER] THEN REWRITE_TAC[ONCE_REWRITE_RULE[INTER_COMM] UNION_OVER_INTER] THEN ASM_SIMP_TAC[SET_RULE `~(a = b) ==> {a} INTER {b} = {}`] THEN ASM_SIMP_TAC[lemma1; UNION_OVER_INTER] THEN REWRITE_TAC[ONCE_REWRITE_RULE[INTER_COMM] UNION_OVER_INTER] THEN ASM_SIMP_TAC[SET_RULE `~(v = y) ==> ~({v,w} = {w,y})`; SET_RULE `~(v = y) /\ ~(v = z) ==> ~({v,w} = {y,z})`] THEN REWRITE_TAC[UNION_EMPTY; UNION_ASSOC; INTER_IDEMPOT] THEN ASM_SIMP_TAC[GSYM lemma1] THEN MATCH_MP_TAC SUBSET_ANTISYM THEN (CONJ_TAC THENL [REWRITE_TAC[UNION_SUBSET]; SET_TAC[]]) THEN REWRITE_TAC[SUBSET_REFL] THENL [REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN SET_TAC[]; ALL_TAC] THEN REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC AFF_GE_MONO_RIGHT) THEN ASM_REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN REWRITE_TAC[EMPTY_SUBSET] THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `{x:real^N}` THEN (CONJ_TAC THENL [SET_TAC[]; ALL_TAC]) THEN GEN_REWRITE_TAC LAND_CONV [GSYM AFFINE_HULL_SING] THEN REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]; RULE_ASSUM_TAC(REWRITE_RULE[INSERT_SUBSET; EMPTY_SUBSET]) THEN RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM]) THEN X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN SUBGOAL_THEN `~(y:real^N = x)` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ASM_SIMP_TAC[lemma2] THEN ASM_SIMP_TAC[SET_RULE `(s UNION t) INTER u = s INTER u UNION t INTER u`] THEN ASM_SIMP_TAC[lemma1; UNION_OVER_INTER; UNION_EMPTY] THEN ASM_CASES_TAC `y:real^N = v` THENL [ASM_REWRITE_TAC[INTER_IDEMPOT] THEN SUBGOAL_THEN `{w:real^N} INTER {v} = {} /\ {v,w} INTER {v} = {v}` (CONJUNCTS_THEN SUBST1_TAC) THENL [ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `{x} SUBSET t /\ u SUBSET t ==> (s INTER {x}) UNION t UNION u = t`) THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM AFFINE_HULL_SING] THEN REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]; ALL_TAC] THEN ASM_CASES_TAC `y:real^N = w` THENL [ASM_REWRITE_TAC[INTER_IDEMPOT] THEN SUBGOAL_THEN `{v:real^N} INTER {w} = {} /\ {v,w} INTER {w} = {w}` (CONJUNCTS_THEN SUBST1_TAC) THENL [ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `{x} SUBSET t /\ t SUBSET u ==> (s INTER {x}) UNION t UNION u = u`) THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM AFFINE_HULL_SING] THEN REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `{v:real^N} INTER {y} = {} /\ {w} INTER {y} = {} /\ {v, w} INTER {y} = {}` (REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THENL [ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `{x} SUBSET s ==> a INTER {x} UNION s UNION s = s`) THEN GEN_REWRITE_TAC LAND_CONV [GSYM AFFINE_HULL_SING] THEN REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]]);; let FAN_AFF_GT_CONDITION = prove (`!x:real^N V E. UNIONS E SUBSET V /\ graph E /\ fan1 (x,V,E) /\ fan2 (x,V,E) /\ fan6 (x,V,E) /\ (!v w. v IN V /\ w IN V ==> aff_ge {x} {v} INTER aff_ge {x} {w} = aff_ge {x} ({v} INTER {w})) /\ (!v e. v IN V /\ e IN E ==> aff_gt {x} {v} INTER aff_gt {x} e = {}) /\ (!e1 e2. e1 IN E /\ e2 IN E /\ ~(e1 = e2) ==> aff_gt {x} e1 INTER aff_gt {x} e2 = {}) ==> FAN (x,V,E)`, REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[Fan.FAN] THEN MATCH_MP_TAC FAN7_AFF_GT_CONDITION THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[Fan.fan2; UNIONS_SUBSET]) THEN ASM_SIMP_TAC[] THEN ASM SET_TAC[]);; let GMLWKPK_SIMPLE = prove (`!E V x:real^N. UNIONS E SUBSET V /\ graph E /\ fan6(x,V,E) /\ (!e. e IN E ==> ~(x IN e)) ==> (fan7 (x,V,E) <=> !e1 e2. e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\ e1 INTER e2 = {} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`, let lemma = prove (`!x u v w:real^N. ~collinear{x,u,v} /\ ~collinear{x,v,w} ==> (~(aff_ge {x} {u,v} INTER aff_ge {x} {v,w} = aff_ge {x} {v}) <=> u IN aff_ge {x} {v,w} \/ w IN aff_ge {x} {u,v})`, REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `x:real^N` THEN REPEAT GEN_TAC THEN MAP_EVERY (fun t -> ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC]) [`u:real^N = v`; `w:real^N = v`; `u:real^N = vec 0`; `v:real^N = vec 0`; `w:real^N = vec 0`] THEN STRIP_TAC THEN EQ_TAC THENL [DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE `~(s INTER s' = t) ==> t SUBSET s /\ t SUBSET s' ==> t PSUBSET s INTER s'`)) THEN ANTS_TAC THENL [CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]; REWRITE_TAC[PSUBSET_ALT]] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; LEFT_IMP_EXISTS_THM] THEN REWRITE_TAC[IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`c:real`; `d:real`] THEN STRIP_TAC THEN ASM_CASES_TAC `a = &0` THENL [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]; ALL_TAC] THEN ASM_CASES_TAC `d = &0` THENL [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]; ALL_TAC] THEN DISCH_THEN(K ALL_TAC) THEN DISJ_CASES_TAC (REAL_ARITH `b <= c \/ c <= b`) THENL [FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH `a % u + b % v:real^N = c % v + d % w ==> a % u = (c - b) % v + d % w`)) THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a):real^N->real^N`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN MAP_EVERY EXISTS_TAC [`inv a * (c - b):real`; `inv a * d:real`] THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE]; FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH `a % u + b % v:real^N = c % v + d % w ==> d % w = (b - c) % v + a % u`)) THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv d):real^N->real^N`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN DISCH_THEN(K ALL_TAC) THEN DISJ2_TAC THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN MAP_EVERY EXISTS_TAC [`inv d * a:real`; `inv d * (b - c):real`] THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE] THEN REWRITE_TAC[VECTOR_ADD_SYM]]; STRIP_TAC THEN MATCH_MP_TAC(SET_RULE `(?x. x IN s /\ x IN t /\ ~(x IN u)) ==> ~(s INTER t = u)`) THENL [EXISTS_TAC `u:real^N` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN CONJ_TAC THENL [MAP_EVERY EXISTS_TAC [`&1`; `&0`] THEN REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC; DISCH_THEN(X_CHOOSE_THEN `a:real` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN UNDISCH_TAC `~collinear{vec 0:real^N,a % v,v}` THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]]; EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN CONJ_TAC THENL [MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC; DISCH_THEN(X_CHOOSE_THEN `a:real` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN UNDISCH_TAC `~collinear{vec 0:real^N,v,a % v}` THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]]]]) in REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[] `(!x y. R x y ==> R y x) /\ (!x. Q x ==> !y. Q y ==> R x y) /\ (!x. P x ==> (!y. Q y ==> R x y) /\ (!y. P y ==> R x y)) ==> (!x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y)`) THEN CONJ_TAC THENL [SIMP_TAC[INTER_ACI]; ALL_TAC] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> c = a /\ b = a`] THEN REWRITE_TAC[INTER_IDEMPOT]; ALL_TAC] THEN X_GEN_TAC `ee1:real^N->bool` THEN DISCH_TAC THEN CONJ_TAC THENL [X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN REWRITE_TAC[SET_RULE `s INTER {a} = {b} <=> b = a /\ a IN s`] THEN SIMP_TAC[IMP_CONJ; FORALL_UNWIND_THM2] THEN DISCH_TAC THEN REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]; ALL_TAC] THEN X_GEN_TAC `ee2:real^N->bool` THEN DISCH_TAC THEN SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} INTER {c,d} = {v} <=> v = a /\ {a,b} INTER {c,d} = {v} \/ v = b /\ {a,b} INTER {c,d} = {v}`] THEN REWRITE_TAC[TAUT `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN REWRITE_TAC[FORALL_AND_THM; FORALL_UNWIND_THM2] THEN MAP_EVERY UNDISCH_TAC [`{v1:real^N,w1} IN E`; `~(v1:real^N = w1)`] THEN MAP_EVERY (fun s -> SPEC_TAC(s,s)) [`w1:real^N`; `v1:real^N`] THEN REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[] `(!v w. P v w ==> P w v) /\ (!v w. R v w ==> Q w v) /\ (!v w. P v w ==> R v w) ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} INTER {c,d} = {v} <=> v = c /\ {a,b} INTER {c,d} = {v} \/ v = d /\ {a,b} INTER {c,d} = {v}`] THEN REWRITE_TAC[TAUT `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN MAP_EVERY UNDISCH_TAC [`{v2:real^N,w2} IN E`; `~(v2:real^N = w2)`] THEN MAP_EVERY (fun s -> SPEC_TAC(s,s)) [`w2:real^N`; `v2:real^N`] THEN REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[] `(!v w. P v w ==> P w v) /\ (!v w. Q v w ==> R w v) /\ (!v w. P v w ==> Q v w) ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN MAP_EVERY X_GEN_TAC [`v':real^N`; `w:real^N`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN ASM_CASES_TAC `u:real^N = w` THENL [ASM SET_TAC[]; ALL_TAC] THEN DISCH_TAC THEN W(MP_TAC o PART_MATCH (rand o lhand o rand) lemma o goal_concl) THEN ANTS_TAC THENL [REWRITE_TAC[SET_RULE `{x,v,w} = {x} UNION {v,w}`] THEN ASM_MESON_TAC[Fan.fan6; INSERT_AC]; ALL_TAC] THEN MATCH_MP_TAC(TAUT `~q ==> (~p <=> q) ==> p`) THEN REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THEN MATCH_MP_TAC(SET_RULE `aff_ge {x} {v} INTER aff_ge {x} s = {x} /\ v IN aff_ge {x} {v} /\ ~(v = x) ==> ~(v IN aff_ge {x} s)`) THEN REPEAT CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_UNION] THEN CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `u:real^N` THEN REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{u:real^N,v}` THEN ASM SET_TAC[]; SUBGOAL_THEN `DISJOINT {x:real^N} {u:real^N}` ASSUME_TAC THENL [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN ASM_MESON_TAC[IN_INSERT]; ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC]; ASM_MESON_TAC[IN_INSERT]; FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_UNION] THEN CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `w:real^N` THEN REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{v:real^N,w}` THEN ASM SET_TAC[]; SUBGOAL_THEN `DISJOINT {x:real^N} {w:real^N}` ASSUME_TAC THENL [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN ASM_MESON_TAC[IN_INSERT]; ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC]; ASM_MESON_TAC[IN_INSERT]]);; let FAN_ECONOMIZED_SIMPLE = prove (`!x:real^N V E. FAN (x,V,E) <=> UNIONS E SUBSET V /\ graph E /\ fan1 (x,V,E) /\ fan2 (x,V,E) /\ fan6 (x,V,E) /\ (!e1 e2. e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\ e1 INTER e2 = {} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`, REPEAT GEN_TAC THEN REWRITE_TAC[Fan.FAN] THEN REWRITE_TAC[CONJ_ASSOC] THEN MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN REWRITE_TAC[GSYM CONJ_ASSOC] THEN STRIP_TAC THEN MATCH_MP_TAC GMLWKPK_SIMPLE THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `e:real^N->bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e:real^N->bool` o GEN_REWRITE_RULE I [Fan.fan6]) THEN ASM_REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_TAC THEN ASM_SIMP_TAC[SET_RULE `x IN u ==> {x} UNION u = u`] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.GRAPH]) THEN DISCH_THEN(MP_TAC o SPEC `e:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN STRIP_TAC THEN ASM_REWRITE_TAC[COLLINEAR_2]);; (* ------------------------------------------------------------------------- *) (* Definition of the polar fan. *) (* ------------------------------------------------------------------------- *) let JNVXCRC = new_definition `polar_fan(V,(E:(real^3->bool)->bool),FF) = let r = rho_node1 FF in let prime = \v. v cross (r v) in ({ prime v | v IN V}, { {prime v,prime(r v)} | v IN V}, { (prime v,prime(r v)) | v IN V})`;; (* ------------------------------------------------------------------------- *) (* Properties of the polar fan. *) (* ------------------------------------------------------------------------- *) let BGMIFTE = prove (`!V E FF V' E' FF'. convex_local_fan(V,E,FF) /\ generic V E /\ (!v. v IN V ==> interior_angle1 (vec 0) FF v < pi) /\ (V',E',FF') = polar_fan (V,E,FF) ==> convex_local_fan(V',E',FF') /\ generic V' E' /\ CARD V' = CARD V /\ let r = rho_node1 FF in let prime = \v. v cross (r v) in (!v. v IN V ==> arcV (vec 0) (prime v) (prime(r v)) = pi - interior_angle1 (vec 0) FF (r v) /\ &0 < arcV (vec 0) (prime v) (prime(r v)) /\ arcV (vec 0) (prime v) (prime(r v)) < pi) /\ (!v. v IN V ==> arcV (vec 0) v (r v) = pi - interior_angle1 (vec 0) FF' (prime v) /\ &0 < arcV (vec 0) v (r v) /\ arcV (vec 0) v (r v) < pi)`, let lemma1 = prove (`((v0 cross v1) cross (v1 cross v2)) dot (w0 cross w1) = ((v1 cross v2) dot v0) * ((w0 cross w1) dot v1)`, VEC3_TAC) and lemma2 = prove (`(v cross v') cross (w cross w') = ((w cross w') dot v) % v' - ((w cross w') dot v') % v`, VEC3_TAC) and lemma3 = prove (`a % v:real^N = b % w ==> a = &0 /\ b = &0 \/ collinear{vec 0,w,v}`, ASM_CASES_TAC `a = &0` THEN ASM_CASES_TAC `b = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0; VECTOR_ARITH `vec 0:real^N = a % b <=> a % b = vec 0`] THEN TRY(SIMP_TAC[INSERT_AC; COLLINEAR_2] THEN NO_TAC) THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a) :real^N->real^N`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN MESON_TAC[]) and lemma4 = prove (`(v1 cross v2) cross (v0 cross v1) = --(((v0 cross v1) dot v2) % v1)`, VEC3_TAC) and lemma5 = prove (`(v0 cross v1) cross (v1 cross v2) = ((v0 cross v1) dot v2) % v1`, VEC3_TAC) and lemma6 = prove (`(x cross y) dot z = (z cross x) dot y`, VEC3_TAC) and lemma7 = prove (`!a b c d:real^N. ~(aff_gt {a,b,c} {d} INTER affine hull {a,b,c} = {}) ==> d IN affine hull {a,b,c}`, REPEAT GEN_TAC THEN DISJ_CASES_TAC (SET_RULE `(d:real^N) IN {a,b,c} \/ DISJOINT {a,b,c} {d}`) THEN ASM_SIMP_TAC[HULL_INC] THEN ASM_SIMP_TAC[AFF_GT_3_1; AFFINE_HULL_3] THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[EXISTS_IN_GSPEC] THEN REWRITE_TAC[IN_ELIM_THM; RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`xa:real`; `xb:real`; `xc:real`; `ya:real`; `yb:real`; `yc:real`; `u:real`] THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[VECTOR_ARITH `xa % a + xb % b + xc % c :real^N = ya % a + yb % b + yc % c + d <=> d = (xa - ya) % a + (xb - yb) % b + (xc - yc) % c`] THEN DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`(xa - ya) / u:real`; `(xb - yb) / u:real`; `(xc - yc) / u:real`] THEN ASM_SIMP_TAC[REAL_FIELD `&0 < u ==> (a / u + b / u + c / u = &1 <=> a + b + c = u)`] THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `(%) (inv u) :real^N->real^N`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_LT_IMP_NZ; REAL_MUL_LINV] THEN REWRITE_TAC[VECTOR_MUL_LID] THEN DISCH_THEN SUBST1_TAC THEN VECTOR_ARITH_TAC) in REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT LET_TAC THEN FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [Wrgcvdr_cizmrrh.convex_local_fan]) THEN SUBGOAL_THEN `!v. v IN V ==> ~((prime:real^3->real^3) v = vec 0)` ASSUME_TAC THENL [GEN_TAC THEN STRIP_TAC THEN EXPAND_TAC "prime" THEN REWRITE_TAC[CROSS_EQ_0] THEN EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; ALL_TAC] THEN SUBGOAL_THEN `!v w. v IN V /\ w IN V /\ ~(v = w) ==> ~collinear{vec 0,(prime:real^3->real^3) v,prime w}` ASSUME_TAC THENL [REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[GSYM CROSS_EQ_0] THEN EXPAND_TAC "prime" THEN REWRITE_TAC[lemma2; VECTOR_SUB_EQ] THEN DISCH_THEN(MP_TAC o MATCH_MP lemma3) THEN REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]] THEN SUBGOAL_THEN `~(v:real^3 = r w /\ w = r v)` MP_TAC THENL [EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; REWRITE_TAC[DE_MORGAN_THM] THEN MATCH_MP_TAC MONO_OR THEN CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_NZ THEN REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "r" THEN ASM_MESON_TAC[RHO_NODE1_INJECTIVE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [JNVXCRC]) THEN ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN REWRITE_TAC[PAIR_EQ] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN SUBGOAL_THEN `!v w. v IN V /\ w IN V ==> ((prime:real^3->real^3) v = prime w <=> v = w)` ASSUME_TAC THENL [ASM_MESON_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN SUBGOAL_THEN `CARD(V':real^3->bool) = CARD(V:real^3->bool)` ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_MESON_TAC[]; ASM_REWRITE_TAC[]] THEN SUBGOAL_THEN `!v w:real^3. v IN V /\ w IN V /\ ~(w = v) /\ ~(w = r v) ==> &0 < sin(azim (vec 0) (prime v) (prime(r v)) (prime w))` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN EXPAND_TAC "prime" THEN REWRITE_TAC[lemma1] THEN MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN CONJ_TAC THENL [FIRST_ASSUM(MP_TAC o SPEC `(r:real^3->real^3) v` o MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN MATCH_MP_TAC(MESON[] `(c' = c /\ d = d') /\ &0 < sin i ==> i = azim a b c d ==> &0 < sin(azim a b c' d')`) THEN REWRITE_TAC[] THEN CONJ_TAC THENL [EXPAND_TAC "r" THEN MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD THEN ASM_MESON_TAC[]; MATCH_MP_TAC SIN_POS_PI THEN EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.INTERIOR_ANGLE1_POS; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]]; EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[RHO_NODE1_INJECTIVE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]]; ALL_TAC] THEN SUBGOAL_THEN `!v w:real^3. v IN V /\ w IN V /\ ~(w = v) /\ ~(w = r v) ==> &0 < azim (vec 0) (prime v) (prime(r v)) (prime w) /\ azim (vec 0) (prime v) (prime(r v)) (prime w) < pi` ASSUME_TAC THENL [REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC SIN_POS_PI_REV THEN ASM_SIMP_TAC[azim; REAL_LT_IMP_LE]; ALL_TAC] THEN ONCE_REWRITE_TAC[TAUT `p /\ q /\ r /\ s <=> r /\ s /\ p /\ q`] THEN CONJ_TAC THENL [X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN MP_TAC(ISPECL [`vec 0:real^3`; `(r:real^3->real^3) v`; `v:real^3`; `(r:real^3->real^3) (r v)`] Hvihvec.HVIHVEC) THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN ANTS_TAC THENL [EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOFA_IMP_V_DIFF; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN EXPAND_TAC "prime" THEN SUBST1_TAC(ISPECL [`v:real^3`; `(r:real^3->real^3) v`] CROSS_SKEW) THEN REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO; VECTOR_ANGLE_LNEG] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC(REAL_ARITH `x = y /\ &0 < x /\ x < pi ==> pi - x = pi - y /\ &0 < pi - x /\ pi - x < pi`) THEN FIRST_ASSUM(MP_TAC o SPEC `(r:real^3->real^3) v` o MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `&0 < i /\ i < pi /\ (&0 < a /\ a < pi ==> d = a) ==> i = a ==> d = i /\ &0 < d /\ d < pi`) THEN REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.INTERIOR_ANGLE1_POS; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC]) THEN SUBGOAL_THEN `ivs_rho_node1 FF (r v) = v` SUBST1_TAC THENL [ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]; ALL_TAC] THEN ONCE_REWRITE_TAC[DIHV_SYM] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_DIHV_SAME THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC (funpow 3 RAND_CONV) [SET_RULE `{a,c,b} = {a,b,c}`] THEN EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN SUBGOAL_THEN `!v w. v IN V /\ w IN V /\ ~(w = v) /\ ~(w = r v) /\ ~(w = ivs_rho_node1 FF v) ==> &0 < azim (vec 0) (prime v) (prime (r v)) (prime w) /\ azim (vec 0) (prime v) (prime (r v)) (prime w) < azim (vec 0) (prime v) (prime (r v)) (prime (ivs_rho_node1 FF v))` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `~(prime w = prime v) /\ ~(prime w = prime(r v)) /\ ~(prime w:real^3 = prime(ivs_rho_node1 FF v))` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN MP_TAC(ISPECL [`vec 0:real^3`; `(prime:real^3->real^3) v`; `prime(r(v:real^3):real^3):real^3`; `(prime:real^3->real^3) w`; `(prime:real^3->real^3) (ivs_rho_node1 FF v)`] Fan.sum3_azim_fan) THEN ANTS_TAC THENL [CONJ_TAC THENL [MATCH_MP_TAC(REAL_ARITH `(&0 < x /\ x < pi) /\ (&0 < y /\ y < pi) ==> x + y < &2 * pi`) THEN ASM_SIMP_TAC[]; REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]]; DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LT_ADDR] THEN MATCH_MP_TAC(REAL_ARITH `&0 < x /\ x < pi ==> &0 < x`)] THEN MATCH_MP_TAC SIN_POS_PI_REV THEN SIMP_TAC[azim; REAL_LT_IMP_LE] THEN REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN ONCE_REWRITE_TAC[lemma6] THEN REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN ABBREV_TAC `u = ivs_rho_node1 FF v` THEN (SUBGOAL_THEN `v = (r:real^3->real^3) u` ASSUME_TAC THENL [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD; IVS_RHO_NODE1_IN_V]; ALL_TAC]) THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN SUBGOAL_THEN `!v. v IN V ==> arcV (vec 0) v (r v) = pi - azim (vec 0) (prime v) (prime(r v)) (prime(ivs_rho_node1 FF v)) /\ &0 < arcV (vec 0) v (r v) /\ arcV (vec 0) v (r v) < pi` ASSUME_TAC THENL [X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH `!d. (&0 < a /\ a < pi) /\ (&0 < a /\ a < pi ==> d = a) /\ d = pi - v ==> v = pi - a /\ &0 < v /\ v < pi`) THEN EXISTS_TAC `dihV (vec 0:real^3) (prime v) (prime (r v)) (prime (ivs_rho_node1 FF v))` THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN CONJ_TAC THENL [STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_DIHV_SAME THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) Hvihvec.HVIHVEC o lhand o goal_concl) THEN ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN EXPAND_TAC "prime" THEN SUBGOAL_THEN `r (ivs_rho_node1 FF v) = v` SUBST1_TAC THENL [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN REWRITE_TAC[lemma4; lemma5; VECTOR_ANGLE_LNEG] THEN AP_TERM_TAC THEN SUBGOAL_THEN `&0 < (ivs_rho_node1 FF v cross v) dot r v /\ &0 < ((v cross r v) dot r (r v))` STRIP_ASSUME_TAC THENL [REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN CONJ_TAC THENL [ABBREV_TAC `w = ivs_rho_node1 FF v` THEN SUBGOAL_THEN `(w:real^3) IN V` ASSUME_TAC THENL [ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN SUBGOAL_THEN `v = (r:real^3->real^3) w` SUBST1_TAC THENL [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ALL_TAC]; ALL_TAC] THEN EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO] THEN REWRITE_TAC[VECTOR_ANGLE_LMUL; VECTOR_ANGLE_RMUL] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN ASM_REAL_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `FAN(vec 0:real^3,V',E')` ASSUME_TAC THENL [MATCH_MP_TAC FAN_AFF_GT_CONDITION THEN REPLICATE_TAC 4 (GEN_REWRITE_TAC I [CONJ_ASSOC]) THEN CONJ_TAC THENL [REWRITE_TAC[Fan.fan1; Fan.fan2; Fan.fan6; Polyhedron.GRAPH; UNIONS_SUBSET] THEN MAP_EVERY EXPAND_TAC ["V'"; "E'"] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN REWRITE_TAC[HAS_SIZE_2_EXISTS] THEN MAP_EVERY EXISTS_TAC [`(prime:real^3->real^3) (v:real^3)`; `(prime:real^3->real^3) ((r:real^3->real^3) v)`] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[]; UNDISCH_TAC `~(V:real^3->bool = {})` THEN SET_TAC[]; ASM SET_TAC[]; X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN REWRITE_TAC[SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]]; ALL_TAC] THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN MAP_EVERY EXPAND_TAC ["V'"; "E'"] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM] THEN CONJ_TAC THENL [MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN STRIP_TAC THEN ASM_CASES_TAC `w:real^3 = v` THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN ASM_SIMP_TAC[SET_RULE `~(x = y) ==> {x} INTER {y} = {}`] THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL [REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `(affine hull ({vec 0:real^3} UNION {prime v})) INTER (affine hull ({vec 0} UNION {prime(w:real^3)}))` THEN SIMP_TAC[AFF_GE_SUBSET_AFFINE_HULL; SET_RULE `s SUBSET s' /\ t SUBSET t' ==> s INTER t SUBSET s' INTER t'`] THEN W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INTER o lhand o goal_concl) THEN REWRITE_TAC[SET_RULE `({z} UNION {a}) UNION ({z} UNION {b}) = {z,a,b}`] THEN ANTS_TAC THENL [DISCH_THEN(MP_TAC o MATCH_MP AFFINE_DEPENDENT_IMP_COLLINEAR_3) THEN ASM_SIMP_TAC[]; DISCH_THEN SUBST1_TAC] THEN SUBGOAL_THEN `({vec 0} UNION {(prime:real^3->real^3) v}) INTER ({vec 0} UNION {prime w}) = {vec 0}` (fun th -> SIMP_TAC[th; AFFINE_HULL_SING; SUBSET_REFL]) THEN ASM SET_TAC[]; REWRITE_TAC[SUBSET_INTER] THEN CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `(!a b. P a /\ P b /\ f a = f b ==> a = b) /\ (!a b. R a b ==> R b a) /\ Q /\ (!a b. P a /\ P b /\ ~({f a,g a} = {f b,g b}) /\ ~(b = a) /\ ~(f b = f a) /\ ~(f b = g a) ==> R a b) ==> Q /\ !a b. (P a /\ P b) /\ ~({f a,g a} = {f b,g b}) ==> R a b`) THEN CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN CONJ_TAC THENL [SIMP_TAC[INTER_COMM]; ALL_TAC] THEN GEN_REWRITE_TAC LAND_CONV [SWAP_FORALL_THM] THEN GEN_REWRITE_TAC I [CONJ_SYM] THEN GEN_REWRITE_TAC I [AND_FORALL_THM] THEN X_GEN_TAC `v:real^3` THEN ASM_CASES_TAC `(v:real^3) IN V` THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [INTER_COMM] THEN SUBGOAL_THEN `aff_gt {vec 0} {(prime:real^3->real^3) v, prime (r v)} SUBSET affine hull {vec 0, prime v,prime(r v)}` ASSUME_TAC THENL [MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `aff_ge {vec 0} {(prime:real^3->real^3) v, prime (r v)}` THEN REWRITE_TAC[AFF_GT_SUBSET_AFF_GE] THEN REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL; aff_ge_def] THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `aff_gt {vec 0,prime v, prime (r v)} {prime(ivs_rho_node1 FF v)} INTER affine hull {vec 0, (prime:real^3->real^3) v,prime(r v)} = {}` ASSUME_TAC THENL [GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN DISCH_THEN(ASSUME_TAC o MATCH_MP lemma7) THEN SUBGOAL_THEN `coplanar {vec 0,(prime:real^3->real^3) v, prime (r v), prime(ivs_rho_node1 FF v)}` MP_TAC THENL [MATCH_MP_TAC(MESON[coplanar] `{a,b,c,d} SUBSET affine hull {a,b,c} ==> coplanar {a,b,c,d}`) THEN ASM_SIMP_TAC[INSERT_SUBSET; HULL_INC; IN_INSERT; EMPTY_SUBSET]; ALL_TAC] THEN W(MP_TAC o PART_MATCH (rhs o rand) AZIM_EQ_0_PI_EQ_COPLANAR o lhand o goal_concl) THEN ANTS_TAC THENL [CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC; DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC(REAL_ARITH `&0 < x /\ x < pi ==> x = &0 \/ x = pi ==> F`) THEN FIRST_X_ASSUM MATCH_MP_TAC] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; ALL_TAC] THEN SUBGOAL_THEN `!w z. {w,z} SUBSET aff_gt {vec 0,prime v, prime (r v)} {prime(ivs_rho_node1 FF v)} ==> aff_gt {vec 0} {(prime:real^3->real^3) v, prime (r v)} INTER aff_gt {vec 0} {w,z} = {}` ASSUME_TAC THENL [REPEAT GEN_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP(SET_RULE `t SUBSET a ==> ap INTER a = {} /\ (s SUBSET ap ==> aff_gt {vec 0} s SUBSET ap) ==> s SUBSET ap ==> t INTER aff_gt {vec 0} s = {}`)) THEN MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `!z. z IN a /\ (DISJOINT {z} p /\ p SUBSET g ==> q SUBSET g) ==> g INTER a = {} ==> p SUBSET g ==> q SUBSET g`) THEN EXISTS_TAC `vec 0:real^3` THEN SIMP_TAC[HULL_INC; IN_INSERT; AFF_GT_1_2] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_3_1 o rand o lhand o goal_concl) THEN ANTS_TAC THENL [REWRITE_TAC[SET_RULE `DISJOINT {a,b,c} {d} <=> ~(d = a) /\ ~(d = b) /\ ~(d = c)`] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN REWRITE_TAC[TAUT `p /\ t = &1 /\ q <=> t = &1 /\ p /\ q`] THEN REWRITE_TAC[REAL_ARITH `t + s = &1 <=> t = &1 - s`] THEN ONCE_REWRITE_TAC[MESON[] `(?a b c d. P a b c d) <=> (?d b c a. P a b c d)`] THEN REWRITE_TAC[UNWIND_THM2] THEN ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?b c a. P a b c)`] THEN REWRITE_TAC[UNWIND_THM2] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REWRITE_TAC[SUBSET; IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`x1:real`; `x2:real`; `x3:real`] THEN MAP_EVERY X_GEN_TAC [`y1:real`; `y2:real`; `y3:real`] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`p:real^3`; `z1:real`; `z2:real`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC `z1 * x1 + z2 * y1:real` THEN EXISTS_TAC `z1 * x2 + z2 * y2:real` THEN EXISTS_TAC `z1 * x3 + z2 * y3:real` THEN ASM_SIMP_TAC[REAL_LT_MUL; REAL_LT_ADD] THEN VECTOR_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `!w. w IN V /\ ~(w = v) /\ ~(w = r v) ==> prime w IN aff_gt {vec 0, prime v, prime(r v)} {(prime:real^3->real^3)(ivs_rho_node1 FF v)}` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN ASM_CASES_TAC `w = ivs_rho_node1 FF v` THENL [W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_3_1 o rand o goal_concl) THEN ANTS_TAC THENL [REWRITE_TAC[SET_RULE `DISJOINT {a,b,c} {d} <=> ~(d = a) /\ ~(d = b) /\ ~(d = c)`] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC [`&0`; `&0`; `&0`; `&1`] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN VECTOR_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `~(prime w = prime v) /\ ~(prime w = prime(r v)) /\ ~(prime w:real^3 = prime(ivs_rho_node1 FF v))` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN MP_TAC(ISPECL [`vec 0:real^3`; `(prime:real^3->real^3) v`; `(prime:real^3->real^3) (r(v:real^3))`; `(prime:real^3->real^3) (ivs_rho_node1 FF v)`] WEDGE_LUNE_GT) THEN REWRITE_TAC[wedge] THEN ANTS_TAC THENL [REPEAT(FIRST_ASSUM MATCH_MP_TAC ORELSE CONJ_TAC) THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; ALL_TAC] THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN DISCH_THEN(MP_TAC o SPEC `(prime:real^3->real^3) w`) THEN MATCH_MP_TAC(TAUT `(q ==> r) /\ p ==> (p <=> q) ==> r`) THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> x IN s ==> x IN t`) THEN REWRITE_TAC[aff_gt_def] THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[]; FIRST_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[]; ASM_MESON_TAC[]; ASM_MESON_TAC[]]; ALL_TAC] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN CONJ_TAC THEN X_GEN_TAC `w:real^3` THENL [DISCH_TAC THEN ASM_CASES_TAC `w:real^3 = v` THENL [ASM_REWRITE_TAC[] THEN W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_1 o rand o lhand o goal_concl) THEN ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_2 o lhand o lhand o goal_concl) THEN REWRITE_TAC[SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; DISCH_THEN SUBST1_TAC] THEN REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN REWRITE_TAC[TAUT `p /\ t = &1 /\ q <=> t = &1 /\ p /\ q`] THEN REWRITE_TAC[REAL_ARITH `t + s = &1 <=> t = &1 - s`] THEN ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN REWRITE_TAC[UNWIND_THM2] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN SIMP_TAC[SET_RULE `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN X_GEN_TAC `p:real^3` THEN REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`t1:real`; `t2:real`] THEN STRIP_TAC THEN DISCH_THEN(X_CHOOSE_THEN `t3:real` MP_TAC) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[VECTOR_ARITH `a % v + b % w:real^N = c % v <=> b % w = (c - a) % v`] THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv t2) :real^3->real^3`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN SUBGOAL_THEN `~collinear{vec 0,(prime:real^3->real^3) v,prime(r v)}` MP_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; REWRITE_TAC[COLLINEAR_LEMMA_ALT; VECTOR_MUL_LID] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN ASM_CASES_TAC `w:real^3 = (r:real^3->real^3) v` THENL [ASM_REWRITE_TAC[] THEN W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_1 o rand o lhand o goal_concl) THEN ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_2 o lhand o lhand o goal_concl) THEN REWRITE_TAC[SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; DISCH_THEN SUBST1_TAC] THEN REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN REWRITE_TAC[TAUT `p /\ t = &1 /\ q <=> t = &1 /\ p /\ q`] THEN REWRITE_TAC[REAL_ARITH `t + s = &1 <=> t = &1 - s`] THEN ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN REWRITE_TAC[UNWIND_THM2] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN SIMP_TAC[SET_RULE `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN X_GEN_TAC `p:real^3` THEN REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`t1:real`; `t2:real`] THEN STRIP_TAC THEN DISCH_THEN(X_CHOOSE_THEN `t3:real` MP_TAC) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[VECTOR_ARITH `a % v + b % w:real^N = c % w <=> a % v = (c - b) % w`] THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv t1) :real^3->real^3`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN SUBGOAL_THEN `~collinear{vec 0,prime(r v),(prime:real^3->real^3) v}` MP_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; REWRITE_TAC[COLLINEAR_LEMMA_ALT; VECTOR_MUL_LID] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN SUBST1_TAC(SET_RULE `{(prime:real^3->real^3) w} = {prime w,prime w}`) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[SET_RULE `{w,w} SUBSET s <=> w IN s`] THEN ASM_MESON_TAC[]; ALL_TAC] THEN STRIP_TAC THEN ASM_CASES_TAC `(r:real^3->real^3) w = v` THENL [ALL_TAC; FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.IVS_RHO_IDD]] THEN MATCH_MP_TAC(SET_RULE `!f. (!x. x IN s ==> f x = &0) /\ (!x. x IN t ==> ~(f x = &0)) ==> s INTER t = {}`) THEN EXISTS_TAC `\p. azim (vec 0) (prime(v:real^3)) (prime (r v)) p` THEN REWRITE_TAC[] THEN CONJ_TAC THENL [REPEAT STRIP_TAC THEN MATCH_MP_TAC AZIM_EQ_0_GE_IMP THEN MATCH_MP_TAC(SET_RULE `!s. x IN s /\ s SUBSET t ==> x IN t`) THEN EXISTS_TAC `aff_gt {vec 0} {(prime:real^3->real^3) v,prime(r v)}` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `aff_ge {vec 0} {(prime:real^3->real^3) v,prime(r v)}` THEN REWRITE_TAC[AFF_GT_SUBSET_AFF_GE] THEN REWRITE_TAC[aff_ge_def] THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[]; ALL_TAC] THEN X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN SUBGOAL_THEN `azim (vec 0) (prime(v:real^3)) (prime (r v)) x = azim (vec 0) (prime v) (prime (r v)) (prime w)` SUBST1_TAC THENL [MATCH_MP_TAC AZIM_EQ_IMP THEN REPEAT(CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; ALL_TAC]) THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `x IN s ==> s SUBSET t ==> x IN t`)) THEN ASM_REWRITE_TAC[aff_gt_def] THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `w = ivs_rho_node1 FF v` SUBST1_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.IVS_RHO_IDD]; ASM_MESON_TAC[REAL_ARITH `a = pi - z /\ &0 < a /\ a < pi ==> ~(z = &0)`]]; ALL_TAC] THEN SUBGOAL_THEN `local_fan(V':real^3->bool,E',FF')` ASSUME_TAC THENL [ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.local_fan] THEN LET_TAC THEN EXPAND_TAC "H" THEN REWRITE_TAC[Wrgcvdr_cizmrrh.dih2k] THEN REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN FIRST_ASSUM (fun th -> REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.HYP_LEMMA th] THEN REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP th]) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.HYP] THEN ABBREV_TAC `FF'' = { ((prime:real^3->real^3)(r v),prime v) | v IN V}` THEN SUBGOAL_THEN `darts_of_hyp E' (V':real^3->bool) = FF' UNION FF''` (fun th -> SUBST1_TAC th THEN ASSUME_TAC th) THENL [REWRITE_TAC[Wrgcvdr_cizmrrh.darts_of_hyp; Wrgcvdr_cizmrrh.ord_pairs; Wrgcvdr_cizmrrh.self_pairs; Wrgcvdr_cizmrrh.EE] THEN MATCH_MP_TAC(SET_RULE `t = {} /\ s = u ==> s UNION t = u`) THEN CONJ_TAC THENL [PURE_REWRITE_TAC[SET_RULE `s = {} <=> !x. x IN s ==> F`] THEN PURE_REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[TAUT `~(p /\ q) <=> p ==> ~q`] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN EXPAND_TAC "E'" THEN ASM SET_TAC[]; MAP_EVERY EXPAND_TAC ["E'"; "FF'"; "FF''"] THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[FORALL_PAIR_THM; IN_UNION; IN_ELIM_PAIR_THM] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN REWRITE_TAC[SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN MESON_TAC[]]; ALL_TAC] THEN SUBGOAL_THEN `!v:real^3. v IN V ==> EE (prime v) E' = {prime(r v):real^3,prime(ivs_rho_node1 FF v)}` ASSUME_TAC THENL [X_GEN_TAC `v:real^3 ` THEN DISCH_TAC THEN REWRITE_TAC[PAIR_EQ; Wrgcvdr_cizmrrh.EE] THEN EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM; SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN GEN_TAC THEN REWRITE_TAC[EXISTS_OR_THM; LEFT_OR_DISTRIB] THEN BINOP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.IVS_RHO_IDD; IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN SUBGOAL_THEN `!n v. v IN V ==> ITER n (r:real^3->real^3) v IN V` ASSUME_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]; ALL_TAC] THEN SUBGOAL_THEN `!n v. v IN V ==> ITER n (ivs_rho_node1 FF) v IN V` ASSUME_TAC THENL [ASM_MESON_TAC[LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V]; ALL_TAC] THEN SUBGOAL_THEN `!n v. v IN V ==> ITER n (ff_of_hyp (vec 0,V',E')) (prime v,prime (r v)) = ((prime:real^3->real^3)(ITER n r v),prime(r(ITER n r v)))` ASSUME_TAC THENL [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN COND_CASES_TAC THENL [SUBGOAL_THEN `r(ITER n (r:real^3->real^3) v) IN V` ASSUME_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ASM_SIMP_TAC[PAIR_EQ]] THEN MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN MATCH_MP_TAC(SET_RULE `a = a' /\ b = b' ==> {a,b} = {b',a'}`) THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT `~(a \/ b) ==> a ==> c`)) THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN SUBGOAL_THEN `!n v. v IN V ==> ITER n (ff_of_hyp (vec 0,V',E')) (prime(r v),prime v) = ((prime:real^3->real^3) (r(ITER n (ivs_rho_node1 FF) v)), prime(ITER n (ivs_rho_node1 FF) v))` ASSUME_TAC THENL [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN COND_CASES_TAC THENL [ASM_SIMP_TAC[PAIR_EQ] THEN CONJ_TAC THENL [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN ASM_SIMP_TAC[PAIR_EQ] THEN REWRITE_TAC[INSERT_AC]; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT `~(a \/ b) ==> b ==> c`)) THEN EXPAND_TAC "FF''" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN SUBGOAL_THEN `!x. x IN FF' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF'` ASSUME_TAC THENL [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `(!n. ITER n (r:real^3->real^3) v IN V) /\ (!w. w IN V ==> ?n. w = ITER n r v)` MP_TAC THENL [ASM_MESON_TAC[LOCAL_FAN_ORBIT_MAP_EXPLICIT]; REWRITE_TAC[GE; LE_0] THEN EXPAND_TAC "FF'" THEN SET_TAC[]]; ALL_TAC] THEN CONJ_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(SET_RULE `(?x. P x) /\ (!x. P x ==> R x) ==> ?x. (P x \/ Q x) /\ R x`) THEN ASM_SIMP_TAC[] THEN EXPAND_TAC "FF'" THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `CARD(FF':real^3#real^3->bool) = CARD(V:real^3->bool) /\ CARD(FF'':real^3#real^3->bool) = CARD V` STRIP_ASSUME_TAC THENL [MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN CONJ_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[]; ALL_TAC] THEN CONJ_TAC THENL [REWRITE_TAC[MULT_2] THEN MATCH_MP_TAC(MESON[CARD_UNION] `CARD t = CARD s /\ FINITE s /\ FINITE t /\ s INTER t = {} ==> CARD(s UNION t) = CARD s + CARD s`) THEN ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN REWRITE_TAC[SET_RULE `IMAGE f s INTER IMAGE g s = {} <=> !x y. x IN s /\ y IN s ==> ~(f x = g y)`] THEN REWRITE_TAC[PAIR_EQ] THEN MAP_EVERY(fun th -> FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP (REWRITE_RULE[IMP_CONJ] th))) [Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE] THEN ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!x. x IN FF'' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF''` ASSUME_TAC THENL [EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `(!n. ITER n (ivs_rho_node1 FF) v IN V) /\ (!w. w IN V ==> ?n. w = ITER n (ivs_rho_node1 FF) v)` MP_TAC THENL [ASM_MESON_TAC[LOCAL_FAN_ORBIT_MAP_EXPLICIT_IVS]; REWRITE_TAC[GE; LE_0] THEN EXPAND_TAC "FF''" THEN SET_TAC[]]; ALL_TAC] THEN REWRITE_TAC[Lvducxu.HAS_ORD2_INTERPRET] THEN SUBGOAL_THEN `(!x. x IN FF' ==> nn_of_hyp (vec 0,V',E') x IN FF'') /\ (!x. x IN FF'' ==> nn_of_hyp (vec 0,V',E') x IN FF')` STRIP_ASSUME_TAC THENL [ASM_SIMP_TAC[nn_of_hyp3; FORALL_PAIR_THM; IN_UNION] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THENL [EXISTS_TAC `ivs_rho_node1 FF v` THEN ASM_SIMP_TAC[] THEN REPEAT CONJ_TAC THENL [ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]; ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ASM_MESON_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]]; EXISTS_TAC `rho_node1 FF v` THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN ASM_SIMP_TAC[] THEN DISCH_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN ASM_MESON_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET; Local_lemmas.IVS_RHO_IDD]]; ALL_TAC] THEN SUBGOAL_THEN `nn_of_hyp (vec 0,V',E') o nn_of_hyp (vec 0,V',E') = I` ASSUME_TAC THENL [ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`w:real^3`; `z:real^3`] THEN ASM_CASES_TAC `(w:real^3,z:real^3) IN FF' UNION FF''` THENL [ALL_TAC; ASM_REWRITE_TAC[nn_of_hyp3]] THEN FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [IN_UNION]) THEN ONCE_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2] THEN ASM_SIMP_TAC[IN_UNION] THEN ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2; IN_UNION; PAIR_EQ] THENL [UNDISCH_TAC `(w:real^3,z:real^3) IN FF'` THEN EXPAND_TAC "FF'"; UNDISCH_TAC `(w:real^3,z:real^3) IN FF''` THEN EXPAND_TAC "FF''"] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC AZIM_CYCLE_TWO_POINT_SET_ALT THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THENL [SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `(r:real^3->real^3) v IN V` ASSUME_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `ivs_rho_node1 FF (r v) = v` SUBST1_TAC THENL [ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `a' = a ==> {a,b} = {a',b}`) THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [REWRITE_TAC[IN_UNION; MESON[] `(!x. P x \/ Q x ==> R x) <=> (!x. P x ==> R x) /\ (!x. Q x ==> R x)`] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `IMAGE (nn_of_hyp (vec 0,V',E')) FF' = FF'' /\ IMAGE (nn_of_hyp (vec 0,V',E')) FF'' = FF'` MP_TAC THENL [ALL_TAC; SET_TAC[]] THEN MATCH_MP_TAC(SET_RULE `(!x. f(f x) = x) /\ (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> f x IN s) ==> IMAGE f s = t /\ IMAGE f t = s`) THEN RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM]) THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders] THEN CONJ_TAC THENL [CONJ_TAC THENL [X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; I_THM; NOT_FORALL_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THEN EXISTS_TAC `((prime:real^3->real^3) v,prime(r v))` THEN ASM_SIMP_TAC[PAIR_EQ] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IMP_DIS_ELMS23; ITER]; REWRITE_TAC[FUN_EQ_THM; I_THM] THEN MATCH_MP_TAC(MESON[IN_UNION] `!FF' FF''. (!x. x IN FF' ==> P x) /\ (!x. x IN FF'' ==> P x) /\ (!x. ~(x IN FF' UNION FF'') ==> P x) ==> !x. P x`) THEN MAP_EVERY EXISTS_TAC [`FF':real^3#real^3->bool`; `FF'':real^3#real^3->bool`] THEN REPEAT CONJ_TAC THENL [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[PAIR_EQ] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]; EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[PAIR_EQ] THEN ASM_MESON_TAC[LOFA_IMP_ITER_IVS_RHO_NODE_ID]; ASM_REWRITE_TAC[FORALL_PAIR_THM; ff_of_hyp3] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN SPEC_TAC(`CARD(V:real^3->bool)`,`k:num`) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER]]]; ALL_TAC] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(v:real^3,w) IN darts_of_hyp E' V'` THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `(!v w:real^3. (v,w) IN FF' ==> (w,v) IN FF'') /\ (!v w:real^3. (v,w) IN FF'' ==> (w,v) IN FF')` MP_TAC THENL [ALL_TAC; REWRITE_TAC[IN_UNION] THEN MESON_TAC[]] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[]; REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; I_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN DISCH_THEN(MP_TAC o SPEC `(prime:real^3->real^3) v,prime(r v)`) THEN ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; PAIR_EQ; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; REWRITE_TAC[nn_of_hyp3; FUN_EQ_THM; I_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN DISCH_THEN(MP_TAC o SPEC `(prime:real^3->real^3) v,prime(r v)`) THEN ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN ASM_SIMP_TAC[PAIR_EQ; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN ASM_MESON_TAC[IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]]; ALL_TAC] THEN SUBGOAL_THEN `convex_local_fan(V':real^3->bool,E',FF')` ASSUME_TAC THENL [ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.convex_local_fan] THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN SIMP_TAC[Wrgcvdr_cizmrrh.azim_in_fan; Wrgcvdr_cizmrrh.wedge_in_fan_ge] THEN X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN ABBREV_TAC `d = azim_cycle (EE (prime(v:real^3)) E') (vec 0) (prime v) (prime (r v))` THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN SUBGOAL_THEN `CARD (EE (prime(v:real^3):real^3) E') = 2` SUBST1_TAC THENL [MATCH_MP_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1) THEN MAP_EVERY EXISTS_TAC [`FF':real^3#real^3->bool`; `V':real^3->bool`] THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "V'" THEN ASM SET_TAC[]; CONV_TAC NUM_REDUCE_CONV] THEN SUBGOAL_THEN `d:real^3 = prime(ivs_rho_node1 FF v)` SUBST1_TAC THENL [EXPAND_TAC "d" THEN SUBGOAL_THEN `EE (prime v:real^3) E' = {prime(r v),prime(ivs_rho_node1 FF v)}` (fun th -> REWRITE_TAC[th; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]) THEN FIRST_ASSUM(fun th -> REWRITE_TAC [MATCH_MP Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE th]) THEN REWRITE_TAC[Fan.set_of_edge] THEN MAP_EVERY EXPAND_TAC ["V'"; "E'"] THEN REWRITE_TAC[IN_ELIM_THM; SET_RULE `{w | P w /\ (?v. v IN V /\ w = prime v)} = IMAGE prime {v | v IN V /\ P(prime v)}`] THEN REWRITE_TAC[SET_RULE `{f a,f b} = IMAGE f {a,b}`] THEN AP_TERM_TAC THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM; IMAGE_CLAUSES] THEN SUBGOAL_THEN `!w z. w IN V /\ z IN V /\ {prime v:real^3,prime w} = {prime z,prime(r z)} <=> (w:real^3) IN V /\ z IN V /\ {v,w} = {z,r z}` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN REWRITE_TAC[SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN X_GEN_TAC `w:real^3` THEN ASM_CASES_TAC `(w:real^3) IN V` THENL [ASM_REWRITE_TAC[]; ASM_MESON_TAC[IVS_RHO_NODE1_IN_V; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]] THEN REWRITE_TAC[MESON[] `(?v. P v /\ (x = v /\ Q v \/ R v /\ y = v)) <=> P x /\ Q x \/ P y /\ R y`] THEN ASM_CASES_TAC `w = (r:real^3->real^3) v` THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN CONJ_TAC THENL [MATCH_MP_TAC(REAL_ARITH `&0 < x /\ x < pi ==> x <= pi`) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN X_GEN_TAC `w:real^3` THEN DISCH_TAC THEN REWRITE_TAC[Wrgcvdr_cizmrrh.wedge_ge; IN_ELIM_THM; azim] THEN ASM_CASES_TAC `(prime:real^3->real^3) w = prime v` THEN ASM_REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim] THEN ASM_CASES_TAC `w:real^3 = v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ASM_CASES_TAC `(prime:real^3->real^3) w = prime(ivs_rho_node1 FF v)` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN ASM_CASES_TAC `w = ivs_rho_node1 FF v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ASM_CASES_TAC `(prime:real^3->real^3) w = prime(r(v:real^3))` THEN ASM_REWRITE_TAC[AZIM_REFL; azim] THEN ASM_CASES_TAC `w = (r:real^3->real^3) v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN MP_TAC(ISPECL [`vec 0:real^3`; `(prime:real^3->real^3) v`; `prime(r(v:real^3):real^3):real^3`; `(prime:real^3->real^3) w`; `(prime:real^3->real^3) (ivs_rho_node1 FF v)`] Fan.sum3_azim_fan) THEN ANTS_TAC THENL [ALL_TAC; SIMP_TAC[REAL_LE_ADDR; azim]] THEN CONJ_TAC THENL [ALL_TAC; REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]] THEN MATCH_MP_TAC(REAL_ARITH `(&0 < x /\ x < pi) /\ (&0 < y /\ y < pi) ==> x + y < &2 * pi`) THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC SIN_POS_PI_REV THEN SIMP_TAC[azim; REAL_LT_IMP_LE] THEN REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN ONCE_REWRITE_TAC[lemma6] THEN REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN ABBREV_TAC `u = ivs_rho_node1 FF v` THEN SUBGOAL_THEN `v = (r:real^3->real^3) u` ASSUME_TAC THENL [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD; IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL [SUBGOAL_THEN `!v. v IN V ==> interior_angle1 (vec 0) FF' (prime v) = azim (vec 0) (prime v) (prime(rho_node1 FF v)) (prime(ivs_rho_node1 FF v))` (fun th -> ASM_SIMP_TAC[th]) THEN REWRITE_TAC[Local_lemmas.interior_angle1; Local_lemmas.rho_node1] THEN X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MATCH_MP_TAC(MESON[] `c = c' /\ d = d' ==> azim a b c d = azim a b c' d'`) THEN CONJ_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN ASM_REWRITE_TAC[GSYM Local_lemmas.rho_node1] THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD]; DISCH_TAC] THEN FIRST_ASSUM(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.CIZMRRH) THEN REWRITE_TAC[DE_MORGAN_THM] THEN DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN MP_TAC) THENL [SIMP_TAC[]; DISCH_THEN(MP_TAC o GEN_ALL o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT] Local_lemmas.KCHMAMG) o CONJUNCT1) THEN DISCH_THEN(MP_TAC o SPEC `FF':(real^3#real^3)->bool`) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `~p ==> p /\ q ==> r`) THEN EXPAND_TAC "V'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN RULE_ASSUM_TAC(REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]) THEN ASM_MESON_TAC[REAL_ARITH `a = pi - i /\ &0 < a /\ a < pi ==> ~(i = pi)`]; REWRITE_TAC[Wrgcvdr_cizmrrh.lunar; RIGHT_EXISTS_AND_THM] THEN MATCH_MP_TAC(TAUT `~q ==> (p /\ q) /\ r ==> s`) THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; RIGHT_EXISTS_AND_THM; GSYM CONJ_ASSOC] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[EXISTS_IN_GSPEC] THEN ASM_MESON_TAC[]]);; (* ------------------------------------------------------------------------- *) (* Perimeter and its bound of 2 pi *) (* ------------------------------------------------------------------------- *) let IQCPCGW = new_definition `fan_perimeter(V,(E:(real^3->bool)->bool),FF) = let v = @v. v IN V in sum(0..CARD(FF)-1) (\i. arcV (vec 0) (ITER i (rho_node1 FF) v) (ITER (i+1) (rho_node1 FF) v))`;; let FAN_PERIMETER_INVARIANT = prove (`!V E FF v. local_fan(V,E,FF) /\ v IN V ==> fan_perimeter(V,E,FF) = sum (0..CARD(FF)-1) (\i. arcV (vec 0) (ITER i (rho_node1 FF) v) (ITER (i+1) (rho_node1 FF) v))`, let lemma = prove (`!i j k. i < k /\ j < k ==> (i + j) MOD k = if i + j < k then i + j else (i + j) - k`, REPEAT STRIP_TAC THEN COND_CASES_TAC THEN MATCH_MP_TAC MOD_UNIQ THENL [EXISTS_TAC `0`; EXISTS_TAC `1`] THEN ASM_ARITH_TAC) in REPEAT STRIP_TAC THEN REWRITE_TAC[IQCPCGW] THEN FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN ABBREV_TAC `w:real^3 = @v. v IN V` THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN SUBGOAL_THEN `(w:real^3) IN V` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o SPECL [`v:real^3`; `w:real^3`] o MATCH_MP (REWRITE_RULE[IMP_CONJ] LOCAL_FAN_ORBIT_MAP_EXPLICIT)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC `\i. (i + m) MOD (CARD(V:real^3->bool))` THEN REWRITE_TAC[ITER_ADD] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `m < n ==> 0 < n`)) THEN ABBREV_TAC `k = CARD(V:real^3->bool)` THEN ASM_SIMP_TAC[IN_NUMSEG; LE_0; ARITH_RULE `0 < k ==> (n <= k - 1 <=> n < k)`] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL [REWRITE_TAC[EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL [EXISTS_TAC `((k - m) + i) MOD k` THEN ASM_SIMP_TAC[DIVISION; LE_1] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `((k - m + i) + m) MOD k` THEN CONJ_TAC THENL [FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[GSYM(MATCH_MP MOD_ADD_MOD (MATCH_MP (ARITH_RULE `0 < k ==> ~(k = 0)`) th))]) THEN ASM_MESON_TAC[MOD_MOD_REFL; LE_1]; MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC]; MAP_EVERY X_GEN_TAC [`p:num`; `q:num`] THEN DISCH_THEN(CONJUNCTS_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_SIMP_TAC[lemma] THEN ASM_ARITH_TAC]; ASM_SIMP_TAC[DIVISION; LE_1; lemma] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `(x + 1) + y = (x + y) + 1`] THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MATCH_MP(ARITH_RULE `~(i + m:num < k) ==> i + m = ((i + m) - k) + k`) th]) THEN REWRITE_TAC[ARITH_RULE `(x + k) + 1 = (x + 1) + k`] THEN REWRITE_TAC[GSYM ADD1] THEN REWRITE_TAC[GSYM ITER_ADD] THEN BINOP_TAC THEN AP_TERM_TAC THEN ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]]);; let FAN_PERIMETER_INVARIANT_CARD_V = prove (`!V E FF v. local_fan(V,E,FF) /\ v IN V ==> fan_perimeter(V,E,FF) = sum (0..CARD V - 1) (\i. arcV (vec 0) (ITER i (rho_node1 FF) v) (ITER (i+1) (rho_node1 FF) v))`, REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP FAN_PERIMETER_INVARIANT) THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ o CONJUNCT1) THEN REWRITE_TAC[]);; let FAN_PERIMETER = prove (`!V E FF. local_fan(V,E,FF) ==> fan_perimeter(V,E,FF) = sum V (\v. arcV (vec 0) v (rho_node1 FF v))`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `FINITE V /\ ~(V:real^3->bool = {})` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THENL [RULE_ASSUM_TAC(REWRITE_RULE [Localization.local_fan2; Fan.FAN; Fan.fan1; LET_DEF; LET_END_DEF]) THEN ASM SET_TAC[]; REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `v:real^3` THEN DISCH_TAC] THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP (REWRITE_RULE[IMP_CONJ] FAN_PERIMETER_INVARIANT_CARD_V)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC `\i. ITER i (rho_node1 FF) v` THEN REWRITE_TAC[GSYM ADD1; ITER] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]] THEN X_GEN_TAC `w:real^3` THEN ASM_CASES_TAC `V:real^3->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN DISCH_TAC THEN SUBGOAL_THEN `~(CARD(V:real^3->bool) = 0)` ASSUME_TAC THENL [ASM_SIMP_TAC[CARD_EQ_0]; ALL_TAC] THEN ASM_SIMP_TAC[IN_NUMSEG; EXISTS_UNIQUE_DEF; LE_0; ARITH_RULE `~(n = 0) ==> (i <= n - 1 <=> i < n)`] THEN ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA; Local_lemmas1.POINT_PRESENTED_IN_RHOND1]);; let WSEWPCH = prove (`!V E FF. convex_local_fan(V,E,FF) ==> fan_perimeter(V,E,FF) <= &2 * pi`, let lemma1 = prove (`!u v x. x IN affine hull {vec 0,u,v} ==> orthogonal (u cross v) x`, REWRITE_TAC[AFFINE_HULL_3; FORALL_IN_GSPEC; orthogonal] THEN REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_RZERO; DOT_CROSS_SELF] THEN REAL_ARITH_TAC) in let lemma2 = prove (`!u v x. x IN affine hull {vec 0,u,v} /\ ~collinear{vec 0,u,v} /\ ~(x = vec 0) ==> ~collinear{vec 0,u cross v,x}`, REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT `(s /\ p ==> q \/ r) ==> p /\ ~q /\ ~r ==> ~s`) THEN STRIP_TAC THEN REWRITE_TAC[GSYM CROSS_EQ_0] THEN REWRITE_TAC[GSYM NORM_AND_CROSS_EQ_0] THEN ASM_SIMP_TAC[CROSS_EQ_0; GSYM orthogonal; lemma1]) and lemma3 = prove (`(v cross v') cross (w cross w') = ((w cross w') dot v) % v' - ((w cross w') dot v') % v`, VEC3_TAC) and lemma4 = prove (`a % v:real^N = b % w ==> a = &0 /\ b = &0 \/ collinear{vec 0,w,v}`, ASM_CASES_TAC `a = &0` THEN ASM_CASES_TAC `b = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0; VECTOR_ARITH `vec 0:real^N = a % b <=> a % b = vec 0`] THEN TRY(SIMP_TAC[INSERT_AC; COLLINEAR_2] THEN NO_TAC) THEN REWRITE_TAC[COLLINEAR_LEMMA] THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a) :real^N->real^N`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN MESON_TAC[]) and lemma5 = prove (`(a INTER a = {} ==> f a INTER f a = z) /\ (!e1 e2. (e1 IN E \/ e1 IN V) /\ (e2 IN E \/ e2 IN V) /\ e1 INTER e2 = {} ==> f e1 INTER f e2 = z) /\ (!e. (e IN E /\ e IN E' \/ e IN V) /\ e INTER a = {} ==> f e INTER f a = z) ==> (!e. e IN E' ==> e = a \/ e IN E) ==> (!e1 e2. (e1 IN E' \/ e1 IN V) /\ (e2 IN E' \/ e2 IN V) /\ e1 INTER e2 = {} ==> f e1 INTER f e2 = z)`, STRIP_TAC THEN DISCH_THEN(fun th -> MP_TAC th THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN DISCH_THEN(fun th' -> MP_TAC th THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MP_TAC th')) THEN ONCE_REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[INTER_COMM]) in GEN_TAC THEN WF_INDUCT_TAC `CARD(V:real^3->bool)` THEN RULE_ASSUM_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]) THEN REPEAT STRIP_TAC THEN FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [Wrgcvdr_cizmrrh.convex_local_fan]) THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN) THEN FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP (REWRITE_RULE[IMP_CONJ] FAN_PERIMETER_INVARIANT)) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.CIZMRRH) THEN ASM_CASES_TAC `circular (V:real^3->bool) E` THEN ASM_REWRITE_TAC[] THENL [REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM] THEN STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] Local_lemmas.KCHMAMG)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(X_CHOOSE_THEN `A:real^3->bool` MP_TAC) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(X_CHOOSE_THEN `pl:real^3` STRIP_ASSUME_TAC) THEN MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum (0..CARD FF - 1) (\i. azim (vec 0) pl (ITER i (rho_node1 FF) v) (ITER (i + 1) (rho_node1 FF) v))` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_EQ_NUMSEG THEN REWRITE_TAC[GSYM ADD1; ITER] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]; ALL_TAC] THEN MATCH_MP_TAC ORDER_AZIM_SUM2Pi_0 THEN FIRST_ASSUM(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR) THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SET_RULE `{a,b,c} = {b,c,a}`] THEN DISCH_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP LOCAL_FAN_NOT_CARD_FF_GE_2) THEN EXISTS_TAC `v:real^3` THEN ASM_SIMP_TAC[] THEN ASM_SIMP_TAC[ARITH_RULE `2 <= f ==> 0 < f - 1 /\ (f - 1 + 1 = f)`] THEN REWRITE_TAC[IN_NUMSEG; LE_0] THEN REPEAT CONJ_TAC THENL [X_GEN_TAC `i:num` THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]; FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN REWRITE_TAC[ITER] THEN ASM_MESON_TAC[Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2]; SUBGOAL_THEN `?a. &0 < a /\ pl:real^3 = a % (v cross rho_node1 FF v)` STRIP_ASSUME_TAC THENL [MATCH_MP_TAC CROSS_POSITIVE_MULTIPLE_AZIM_AXIS_ALT THEN ASM_SIMP_TAC[orthogonal] THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.CYCLIC_SET]) THEN ASM_CASES_TAC `pl:real^3 = vec 0` THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[SUBSET; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC]) THEN REWRITE_TAC[REAL_LT_LE; Local_lemmas1.ARCV_BOUNDS] THEN DISCH_THEN(MP_TAC o AP_TERM `sin` o SYM) THEN REWRITE_TAC[SIN_0] THEN MATCH_MP_TAC Trigonometry2.NOT_COLLINEAR_IMP_NOT_SIN0 THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; ASM_SIMP_TAC[AZIM_SPECIAL_SCALE]] THEN ASM_SIMP_TAC[ARITH_RULE `2 <= f ==> (j <= f - 1 /\ k <= f - 1 /\ j < k <=> j < k /\ k < f /\ k <= f - 1)`] THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN MATCH_MP_TAC(GEN_ALL Local_lemmas.RHO_NODE1_MONO_WITH_AZIM) THEN MAP_EVERY EXISTS_TAC [`E:(real^3->bool)->bool`; `{ITER j (rho_node1 FF) v | j <= CARD(V:real^3->bool) - 1}`; `A:real^3->bool`] THEN ASM_SIMP_TAC[SUBSET; FORALL_IN_GSPEC] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V; SUBSET]]; ALL_TAC] THEN ASM_CASES_TAC `?v w:real^3. lunar (v,w) V E` THEN ASM_REWRITE_TAC[] THENL [DISCH_TAC THEN FIRST_X_ASSUM(X_CHOOSE_THEN `w:real^3` MP_TAC) THEN DISCH_THEN(X_CHOOSE_TAC `z:real^3`) THEN FIRST_ASSUM(MP_TAC o MATCH_MP (GEN_ALL (ONCE_REWRITE_RULE[IMP_CONJ_ALT] Local_lemmas.HKIRPEP))) THEN DISCH_THEN(MP_TAC o SPEC `FF:real^3#real^3->bool`) THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 4 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `n:num` MP_TAC) (X_CHOOSE_THEN `m:num` MP_TAC)) THEN REPEAT (REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC)) THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Localization.lunar]) THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `w:real^3` o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] FAN_PERIMETER_INVARIANT)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN SUBGOAL_THEN `CARD(V:real^3->bool) = m + n` SUBST1_TAC THENL [REWRITE_TAC[GSYM LE_ANTISYM] THEN CONJ_TAC THENL [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] (GEN_ALL Local_lemmas1.CARD_IS_LEAST_CYCLE))) THEN EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[GSYM ITER_ADD; ADD_EQ_0]; ALL_TAC] THEN ONCE_REWRITE_TAC[GSYM NOT_LT] THEN DISCH_TAC THEN SUBGOAL_THEN `CARD(V:real^3->bool) <= (m + n) - CARD V` MP_TAC THENL [ALL_TAC; ASM_ARITH_TAC] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] (GEN_ALL Local_lemmas1.CARD_IS_LEAST_CYCLE))) THEN EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[SUB_EQ_0; NOT_LE] THEN SUBGOAL_THEN `ITER (CARD(V:real^3->bool)) (rho_node1 FF) w = w` (fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SYM th]) THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]; ALL_TAC] THEN ASM_SIMP_TAC[ITER_ADD; ARITH_RULE `p:num < n ==> n - p + p = n`] THEN ASM_REWRITE_TAC[GSYM ITER_ADD]; ALL_TAC] THEN ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> (m + n) - 1 = (n - 1) + m`] THEN SIMP_TAC[SUM_ADD_SPLIT; LE_0] THEN ASM_SIMP_TAC[SUB_REFL; ARITH_EQ; ARITH_RULE `~(m = 0) /\ ~(n = 0) ==> m - 1 + n = m + (n - 1)`] THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] SUM_OFFSET] THEN REWRITE_TAC[GSYM ADD_ASSOC] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [ONCE_REWRITE_RULE[ADD_SYM] (GSYM ITER_ADD)] THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `~(w:real^3 = vec 0) /\ ~(z:real^3 = vec 0)` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[Fan.FAN; Fan.fan2]; ALL_TAC] THEN SUBGOAL_THEN `(!i. i <= n ==> ITER i (rho_node1 FF) w IN affine hull {vec 0,w,rho_node1 FF w}) /\ (!i. i <= m ==> ITER i (rho_node1 FF) z IN affine hull {vec 0,w,ivs_rho_node1 FF w})` STRIP_ASSUME_TAC THENL [SIMP_TAC[ARITH_RULE `i <= n <=> i = 0 \/ i = n \/ 0 < i /\ i < n`] THEN CONJ_TAC THEN UNDISCH_TAC `collinear {vec 0:real^3, w, z}` THEN ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN DISCH_TAC THEN (X_GEN_TAC `i:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[ITER; HULL_INC; IN_INSERT] THENL [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `z IN P hull s ==> P hull s SUBSET P hull t ==> z IN P hull t`)) THEN MATCH_MP_TAC HULL_MONO THEN SET_TAC[]; FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `{f i | P i} = s INTER t ==> P k /\ s SUBSET s' ==> f k IN s'`)) THEN ASM_REWRITE_TAC[] THEN MP_TAC(GEN_ALL(ISPECL [`sgn_gt`; `u:real^3->bool`] AFFSIGN_EQ_AFFINE_HULL)) THEN REWRITE_TAC[aff_gt_def] THEN DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]) THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[]]); ALL_TAC] THEN FIRST_ASSUM(MP_TAC o MATCH_MP (GEN_ALL (ONCE_REWRITE_RULE[IMP_CONJ] Local_lemmas.RHO_NODE1_MONO_WITH_AZIM))) THEN DISCH_THEN(fun th -> MP_TAC(SPECL [`{ITER i (rho_node1 FF) z | i <= m}`; `affine hull {vec 0, w, ivs_rho_node1 FF w}`; `m:num`; `z cross rho_node1 FF z`; `z:real^3`] th) THEN MP_TAC(SPECL [`{ITER i (rho_node1 FF) w | i <= n}`; `affine hull {vec 0, w, rho_node1 FF w}`; `n:num`; `w cross rho_node1 FF w`; `w:real^3`] th)) THEN ASM_REWRITE_TAC[PLANE_AFFINE_HULL_3; SUBSET; FORALL_IN_GSPEC] THEN SIMP_TAC[HULL_INC; IN_INSERT] THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; DISCH_THEN(LABEL_TAC "W")] THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]; DISCH_THEN(LABEL_TAC "Z")] THEN SUBGOAL_THEN `!i. i <= m ==> ITER i (rho_node1 FF) z IN affine hull {vec 0,z,rho_node1 FF z}` ASSUME_TAC THENL [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `(!x. P x ==> f x IN s) ==> P 0 /\ P(SUC 0) /\ (f 0 IN s /\ f(SUC 0) IN s ==> s = t) ==> (!x. P x ==> f x IN t)`)) THEN REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN REWRITE_TAC[ITER] THEN STRIP_TAC THEN MATCH_MP_TAC AFFINE_HULL_3_GENERATED THEN ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET; HULL_INC; IN_INSERT] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; ALL_TAC] THEN SUBGOAL_THEN `(!i. i <= n - 1 ==> azim (vec 0) (w cross rho_node1 FF w) (ITER i (rho_node1 FF) w) (ITER (i + 1) (rho_node1 FF) w) = azim (vec 0) (w cross rho_node1 FF w) w (ITER (i + 1) (rho_node1 FF) w) - azim (vec 0) (w cross rho_node1 FF w) w (ITER i (rho_node1 FF) w)) /\ (!i. i <= m - 1 ==> azim (vec 0) (z cross rho_node1 FF z) (ITER i (rho_node1 FF) z) (ITER (i + 1) (rho_node1 FF) z) = azim (vec 0) (z cross rho_node1 FF z) z (ITER (i + 1) (rho_node1 FF) z) - azim (vec 0) (z cross rho_node1 FF z) z (ITER i (rho_node1 FF) z))` STRIP_ASSUME_TAC THENL [CONJ_TAC THEN (REWRITE_TAC[REAL_ARITH `a:real = b - c <=> b = c + a`] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC Fan.sum4_azim_fan THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; REPEAT CONJ_TAC THEN MATCH_MP_TAC lemma2 THEN ASM_SIMP_TAC[HULL_INC; IN_INSERT] THEN TRY (CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; ALL_TAC] THEN MATCH_MP_TAC(MESON[] `!V. ~(z IN V) /\ w IN V ==> ~(w = z)`) THEN EXISTS_TAC `V:real^3->bool` THEN CONJ_TAC THENL [ASM_MESON_TAC[Fan.fan2; Fan.FAN]; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]]) THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]]); ALL_TAC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum (0..n - 1) (\i. azim (vec 0) (w cross rho_node1 FF w) (ITER i (rho_node1 FF) w) (ITER (i + 1) (rho_node1 FF) w)) + sum (0..m - 1) (\i. azim (vec 0) (z cross rho_node1 FF z) (ITER i (rho_node1 FF) z) (ITER (i + 1) (rho_node1 FF) z))` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_EQ_IMP_LE THEN BINOP_TAC THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_ARCV THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN (REPEAT CONJ_TAC THENL [MATCH_MP_TAC lemma1 THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; MATCH_MP_TAC lemma1 THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; MATCH_MP_TAC lemma2 THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; ALL_TAC] THEN MATCH_MP_TAC(MESON[] `!V. ~(z IN V) /\ w IN V ==> ~(w = z)`) THEN EXISTS_TAC `V:real^3->bool` THEN CONJ_TAC THENL [ASM_MESON_TAC[Fan.fan2; Fan.FAN]; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]]; MATCH_MP_TAC lemma2 THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; ALL_TAC] THEN MATCH_MP_TAC(MESON[] `!V. ~(z IN V) /\ w IN V ==> ~(w = z)`) THEN EXISTS_TAC `V:real^3->bool` THEN CONJ_TAC THENL [ASM_MESON_TAC[Fan.fan2; Fan.FAN]; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]]; ALL_TAC]) THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= y /\ x <= pi ==> x - y <= pi`) THEN REWRITE_TAC[azim] THEN MATCH_MP_TAC REAL_LE_TRANS THENL [EXISTS_TAC `azim (vec 0) (w cross rho_node1 FF w) w (ITER n (rho_node1 FF) w)`; EXISTS_TAC `azim (vec 0) (z cross rho_node1 FF z) z (ITER m (rho_node1 FF) z)`] THEN (CONJ_TAC THENL [FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `i <= n - 1 ==> ~(n = 0) ==> i + 1 = n \/ i + 1 < n`)) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN STRIP_TAC THENL [ASM_REWRITE_TAC[REAL_LE_REFL]; ALL_TAC] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ASM_REWRITE_TAC[]]) THEN MATCH_MP_TAC(REAL_ARITH `&0 < pi /\ (x = &0 \/ x = pi) ==> x <= pi`); ASM_SIMP_TAC[] THEN REWRITE_TAC[SUM_DIFFS_ALT; LE_0] THEN REWRITE_TAC[ITER; AZIM_REFL] THEN ASM_SIMP_TAC[SUB_ADD; LE_1; REAL_SUB_RZERO] THEN MATCH_MP_TAC(REAL_ARITH `&0 < pi /\ (x = &0 \/ x = pi) /\ (y = &0 \/ y = pi) ==> x + y <= &2 * pi`)] THEN REWRITE_TAC[PI_POS] THEN REPEAT CONJ_TAC THEN MATCH_MP_TAC COLLINEAR_AZIM_0_OR_PI THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN DISCH_TAC THEN ASM_CASES_TAC `!v. v IN V ==> interior_angle1 (vec 0) FF v < pi` THENL [SUBGOAL_THEN `?vef. vef = polar_fan(V,E,FF)` MP_TAC THENL [REWRITE_TAC[EXISTS_REFL]; REWRITE_TAC[EXISTS_PAIR_THM]] THEN FIRST_ASSUM(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] BGMIFTE)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `V':real^3->bool` THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `E':(real^3->bool)->bool` THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `FF':real^3#real^3->bool` THEN DISCH_THEN(fun th -> DISCH_THEN(ASSUME_TAC o SYM) THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN REPEAT LET_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL [`V':real^3->bool`; `E':(real^3->bool)->bool`; `FF':real^3#real^3->bool`] Localization.NKEZBFC) THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP Nkezbfc_local.SOL_LOFA_EQ_SUM_INANGLE) THEN MATCH_MP_TAC(REAL_ARITH `--s = t ==> &0 <= &2 * pi + s ==> t <= &2 * pi`) THEN REWRITE_TAC[GSYM SUM_NEG; REAL_NEG_SUB] THEN SUBGOAL_THEN `V' = IMAGE (prime:real^3->real^3) V` SUBST1_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE LAND_CONV [JNVXCRC]) THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ASM_REWRITE_TAC[PAIR_EQ] THEN ASM SET_TAC[]; ALL_TAC] THEN W(MP_TAC o PART_MATCH (lhand o rand) SUM_IMAGE o lhand o goal_concl) THEN ANTS_TAC THENL [SUBGOAL_THEN `!x y. x IN V /\ y IN V /\ ~(x = y) ==> ~collinear{vec 0,(prime:real^3->real^3) x,prime y}` MP_TAC THENL [ALL_TAC; ASM_MESON_TAC[INSERT_AC; COLLINEAR_2]] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[GSYM CROSS_EQ_0] THEN EXPAND_TAC "prime" THEN REWRITE_TAC[lemma3; VECTOR_SUB_EQ] THEN DISCH_THEN(MP_TAC o MATCH_MP lemma4) THEN REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]] THEN SUBGOAL_THEN `~(x:real^3 = r y /\ y = r x)` MP_TAC THENL [EXPAND_TAC "r" THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; REWRITE_TAC[DE_MORGAN_THM] THEN MATCH_MP_TAC MONO_OR THEN CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_NZ THEN REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "r" THEN ASM_MESON_TAC[RHO_NODE1_INJECTIVE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]]; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum V (\v:real^3. arcV (vec 0) v (r v))` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_EQ THEN ASM_MESON_TAC[]; ALL_TAC] THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC `\i. ITER i r (v:real^3)` THEN REWRITE_TAC[GSYM ADD1; ITER] THEN UNDISCH_THEN `rho_node1 FF = r` (SUBST_ALL_TAC o SYM) THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]] THEN X_GEN_TAC `w:real^3` THEN ASM_CASES_TAC `V:real^3->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN DISCH_TAC THEN SUBGOAL_THEN `~(CARD(V:real^3->bool) = 0)` ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.FAN]) THEN ASM_SIMP_TAC[Fan.fan1; CARD_EQ_0]; ALL_TAC] THEN ASM_SIMP_TAC[IN_NUMSEG; EXISTS_UNIQUE_DEF; LE_0; ARITH_RULE `~(n = 0) ==> (i <= n - 1 <=> i < n)`] THEN ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA; Local_lemmas1.POINT_PRESENTED_IN_RHOND1]; ALL_TAC] THEN UNDISCH_THEN `(v:real^3) IN V` (K ALL_TAC) THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN REWRITE_TAC[NOT_IMP] THEN DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH `~(a < pi) ==> a <= pi ==> a = pi`)) THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.CONVEX_LOFA_IMP_INANGLE_LE_PI]; DISCH_TAC] THEN SUBGOAL_THEN `FINITE(V:real^3->bool)` ASSUME_TAC THENL [ASM_MESON_TAC[Fan.FAN; Fan.fan1]; ALL_TAC] THEN DISJ_CASES_TAC(ARITH_RULE `CARD(V:real^3->bool) <= 2 \/ 3 <= CARD V`) THENL [FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] FAN_PERIMETER_INVARIANT)) THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum (0..CARD(V:real^3->bool) - 1) (\i. pi)` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_LE_NUMSEG THEN REWRITE_TAC[Local_lemmas1.ARCV_BOUNDS]; SIMP_TAC[SUM_CONST_NUMSEG; REAL_LE_RMUL_EQ; PI_POS] THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN ASM_ARITH_TAC]; ALL_TAC] THEN ABBREV_TAC `V' = V DIFF {v:real^3}` THEN ABBREV_TAC `r = \u. if rho_node1 FF u = v then rho_node1 FF v else rho_node1 FF u` THEN ABBREV_TAC `E' = {{v,r v} | (v:real^3) IN V'}` THEN ABBREV_TAC `FF' = {(v,(r:real^3->real^3) v) | v IN V'}` THEN SUBGOAL_THEN `!w:real^3. w IN V' ==> r w IN V'` ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN GEN_TAC THEN STRIP_TAC THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN SUBGOAL_THEN `!x y. x IN V' /\ y IN V' ==> ((r:real^3->real^3) x = r y <=> x = y)` ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN EXPAND_TAC "r" THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN ASM_MESON_TAC[RHO_NODE1_INJECTIVE]; ALL_TAC] THEN SUBGOAL_THEN `!w:real^3. w IN V' ==> ~(r w = w)` ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN GEN_TAC THEN STRIP_TAC THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; ALL_TAC] THEN SUBGOAL_THEN `!w. w IN V' ==> rho_node1 FF' w = r w` ASSUME_TAC THENL [EXPAND_TAC "FF'" THEN REWRITE_TAC[Localization.rho_node1] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `FINITE V' /\ CARD(V':real^3->bool) + 1 = CARD(V:real^3->bool)` STRIP_ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[SET_RULE `s DIFF {a} = s DELETE a`] THEN ASM_SIMP_TAC[FINITE_DELETE; CARD_DELETE] THEN ASM_SIMP_TAC[ARITH_RULE `v - 1 + 1 = v <=> ~(v = 0)`; CARD_EQ_0] THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `CARD(V':real^3->bool) < CARD(V:real^3->bool)` ASSUME_TAC THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN UNDISCH_TAC `interior_angle1 (vec 0) FF v = pi` THEN FIRST_ASSUM(fun th -> W(MP_TAC o PART_MATCH (lhand o rand) (MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS th) o lhand o lhand o goal_concl)) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `v IN aff_ge {vec 0} {ivs_rho_node1 FF v, rho_node1 FF v}` ASSUME_TAC THENL [MATCH_MP_TAC GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]; ALL_TAC] THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]; ASM_REWRITE_TAC[]] THEN FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [Localization.generic]) THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas1.LOCAL_RHO_NODE_PAIR_E; IN_DIFF]; ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]]; ALL_TAC] THEN SUBGOAL_THEN `fan_perimeter (V,E,FF) = sum V' (\v. arcV (vec 0) v (rho_node1 FF' v))` SUBST1_TAC THENL [MP_TAC(ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `FF:real^3#real^3->bool`] FAN_PERIMETER) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN SUBGOAL_THEN `V = (v:real^3) INSERT V'` SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN ASM_SIMP_TAC[SUM_CLAUSES] THEN COND_CASES_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN ABBREV_TAC `u = ivs_rho_node1 FF v` THEN SUBGOAL_THEN `(u:real^3) IN V'` ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN EXPAND_TAC "u" THEN ASM_MESON_TAC[Local_lemmas1.IVS_RHO_NODE_DIFF_ID; IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN SUBGOAL_THEN `V' = (u:real^3) INSERT (V' DELETE u)` SUBST1_TAC THENL [ASM SET_TAC[]; ASM_SIMP_TAC[SUM_CLAUSES; FINITE_DELETE]] THEN REWRITE_TAC[IN_DELETE] THEN MATCH_MP_TAC(REAL_ARITH `s' = s /\ a + b = c ==> b + a + s' = c + s`) THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC[IN_DELETE] THEN X_GEN_TAC `w:real^3` THEN STRIP_TAC THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN MAP_EVERY UNDISCH_TAC [`(u:real^3) IN V'`; `(w:real^3) IN V'`] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC[RHO_NODE1_INJECTIVE; Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]; ALL_TAC] THEN EXPAND_TAC "r" THEN REWRITE_TAC[] THEN COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARCV_ANGLE] THEN MATCH_MP_TAC ANGLES_ADD_AFF_GE THEN REPEAT(CONJ_TAC THENL [RULE_ASSUM_TAC(REWRITE_RULE[Fan.fan2; Fan.FAN]) THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IN_DIFF]; ALL_TAC]) THEN ASM_MESON_TAC[]; ALL_TAC] THEN DISJ_CASES_TAC(ARITH_RULE `CARD(V':real^3->bool) <= 2 \/ 3 <= CARD V'`) THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum (V':real^3->bool) (\i. pi)` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_LE THEN ASM_SIMP_TAC[Local_lemmas1.ARCV_BOUNDS]; ASM_SIMP_TAC[SUM_CONST; REAL_LE_RMUL_EQ; PI_POS] THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN ASM_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `convex_local_fan (V',E',FF')` ASSUME_TAC THENL [ALL_TAC; MP_TAC(ISPECL [`V':real^3->bool`; `E':(real^3->bool)->bool`; `FF':real^3#real^3->bool`] FAN_PERIMETER) THEN ASM_SIMP_TAC[Local_lemmas.CVX_LO_IMP_LO] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]] THEN FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `3 <= n ==> ~(n = 0)`)) THEN ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_TAC THEN SUBGOAL_THEN `~((vec 0:real^3) IN V')` ASSUME_TAC THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF] THEN ASM_MESON_TAC[Fan.FAN; Fan.fan2]; ALL_TAC] THEN SUBGOAL_THEN `FAN(vec 0:real^3,V',E')` ASSUME_TAC THENL [REWRITE_TAC[FAN_ECONOMIZED_SIMPLE] THEN REPEAT CONJ_TAC THENL [EXPAND_TAC "E'" THEN REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET]; EXPAND_TAC "E'" THEN REWRITE_TAC[Fan.GRAPH; FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[Local_lemmas1.SET2_HAS_SIZE2]; REWRITE_TAC[Fan.fan1] THEN ASM SET_TAC[]; ASM_REWRITE_TAC[Fan.fan2]; EXPAND_TAC "E'" THEN REWRITE_TAC[Fan.fan6; FORALL_IN_GSPEC] THEN X_GEN_TAC `u:real^3` THEN REWRITE_TAC[INSERT_UNION_EQ; UNION_EMPTY] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN STRIP_TAC THEN EXPAND_TAC "r" THEN COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] (GEN_ALL Local_lemmas.FAN_SUB_NOT_EQ_COLL_IN_CONV0))) THEN DISCH_THEN(MP_TAC o SPECL [`u:real^3`; `rho_node1 FF v`]) THEN ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; NOT_IMP] THEN CONJ_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN REWRITE_TAC[Collect_geom.CONV0_SET2; IN_ELIM_THM] THEN FIRST_X_ASSUM(MP_TAC o SPECL [`v:real^3`; `rho_node1 FF v`; `u:real^3`] o GEN_REWRITE_RULE I [Localization.generic]) THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas1.LOCAL_RHO_NODE_PAIR_E]; ALL_TAC] THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM; GSYM MEMBER_NOT_EMPTY] THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(ASSUME_TAC o SYM) THEN SUBGOAL_THEN `~(u:real^3 = vec 0) /\ ~(v = vec 0) /\ ~(rho_node1 FF v = vec 0)` STRIP_ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.FAN]) THEN REWRITE_TAC[Fan.fan2] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ASM_SIMP_TAC[AFF_GE_1_2_0; IN_INTER; EXISTS_IN_GSPEC] THEN MAP_EVERY EXISTS_TAC [`&0`; `b:real`] THEN ASM_SIMP_TAC[REAL_LE_REFL; REAL_LT_IMP_LE] THEN ASM_SIMP_TAC[AFF_LT_1_1; SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_RZERO; IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC [`&1 + a`; `--a`] THEN REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN ASM_REWRITE_TAC[VECTOR_ARITH `vec 0 + a:real^N = vec 0 + --x % b <=> x % b + a = vec 0`]]; SUBGOAL_THEN `E' SUBSET {ivs_rho_node1 FF v,rho_node1 FF v} INSERT E` MP_TAC THENL [EXPAND_TAC "E'" THEN REWRITE_TAC[FORALL_IN_GSPEC; SUBSET] THEN X_GEN_TAC `w:real^3` THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN STRIP_TAC THEN REWRITE_TAC[IN_INSERT] THEN EXPAND_TAC "r" THEN COND_CASES_TAC THENL [DISJ1_TAC THEN BINOP_TAC THEN REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]; DISJ2_TAC THEN ASM_MESON_TAC[Local_lemmas1.LOCAL_RHO_NODE_PAIR_E]]; REWRITE_TAC[SUBSET; IN_INSERT; IN_UNION]] THEN MATCH_MP_TAC lemma5 THEN CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN CONJ_TAC THENL [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FAN_ECONOMIZED_SIMPLE]) THEN DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN EXPAND_TAC "V'" THEN SET_TAC[]; ALL_TAC] THEN X_GEN_TAC `e:real^3->bool` THEN SIMP_TAC[SET_RULE `s INTER {a,b} = {} <=> ~(a IN s) /\ ~(b IN s)`] THEN SUBGOAL_THEN `aff_ge {vec 0} {ivs_rho_node1 FF v, rho_node1 FF v} = aff_ge {vec 0} {ivs_rho_node1 FF v, v} UNION aff_ge {vec 0} {v, rho_node1 FF v}` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN MATCH_MP_TAC UNION_AFF_GE_1_2 THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[Fan.fan2; Fan.FAN]) THEN ASM_MESON_TAC[IVS_RHO_NODE1_IN_V; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN MATCH_MP_TAC(SET_RULE `s INTER t = u /\ s INTER t' = u ==> s INTER (t UNION t') = u`) THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FAN_ECONOMIZED_SIMPLE]) THEN DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN DISCH_THEN(fun th -> CONJ_TAC THEN MATCH_MP_TAC th) THEN (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN ASM_REWRITE_TAC[SET_RULE `s INTER {a,b} = {} <=> ~(a IN s) /\ ~(b IN s)`] THEN (CONJ_TAC THENL [REWRITE_TAC[IN_UNION] THEN DISJ1_TAC THEN ASM_MESON_TAC[Tecoxbm.IVS_RHO_NODE_IN_EDGE; Local_lemmas1.LOCAL_RHO_NODE_PAIR_E; SET_RULE `{a,b} = {b,a}`]; ALL_TAC]) THEN FIRST_X_ASSUM(DISJ_CASES_THEN MP_TAC) THEN SIMP_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN EXPAND_TAC "V'" THEN SIMP_TAC[IN_SING; IN_DIFF] THEN EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN STRIP_TAC THEN ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]]; ALL_TAC] THEN MP_TAC(ISPECL [`V':real^3->bool`; `r:real^3->real^3`] SURJECTIVE_IFF_INJECTIVE) THEN ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN(MP_TAC o snd o EQ_IMP_RULE) THEN ANTS_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[RIGHT_IMP_EXISTS_THM]] THEN REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `r':real^3->real^3` THEN REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `!x y. x IN V' /\ y IN V' ==> ((r':real^3->real^3) x = r' y <=> x = y)` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!x. x IN V' ==> (r':real^3->real^3)(r x) = x` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `local_fan(V':real^3->bool,E',FF')` ASSUME_TAC THENL [ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.local_fan] THEN LET_TAC THEN EXPAND_TAC "H" THEN REWRITE_TAC[Wrgcvdr_cizmrrh.dih2k] THEN REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN FIRST_ASSUM (fun th -> REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.HYP_LEMMA th] THEN REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP th]) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.HYP] THEN ABBREV_TAC `FF'' = { ((r:real^3->real^3) v,v) | v IN V'}` THEN SUBGOAL_THEN `darts_of_hyp E' (V':real^3->bool) = FF' UNION FF''` (fun th -> SUBST1_TAC th THEN ASSUME_TAC th) THENL [REWRITE_TAC[Wrgcvdr_cizmrrh.darts_of_hyp; Wrgcvdr_cizmrrh.ord_pairs; Wrgcvdr_cizmrrh.self_pairs; Wrgcvdr_cizmrrh.EE] THEN MATCH_MP_TAC(SET_RULE `t = {} /\ s = u ==> s UNION t = u`) THEN CONJ_TAC THENL [PURE_REWRITE_TAC[SET_RULE `s = {} <=> !x. x IN s ==> F`] THEN PURE_REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `w:real^3` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `(r:real^3->real^3) w`)) THEN EXPAND_TAC "E'" THEN ASM SET_TAC[]; EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN SET_TAC[]]; ASM_REWRITE_TAC[]] THEN SUBGOAL_THEN `!w:real^3. w IN V' ==> EE w E' = {r w,(r':real^3->real^3) w}` ASSUME_TAC THENL [X_GEN_TAC `w:real^3 ` THEN DISCH_TAC THEN REWRITE_TAC[PAIR_EQ; Wrgcvdr_cizmrrh.EE] THEN EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM; SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!n w. w IN V' ==> ITER n (r:real^3->real^3) w IN V'` ASSUME_TAC THENL [INDUCT_TAC THEN REWRITE_TAC[ITER] THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!n w. w IN V' ==> ITER n (r':real^3->real^3) w IN V'` ASSUME_TAC THENL [INDUCT_TAC THEN REWRITE_TAC[ITER] THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!n w. w IN V' ==> ITER n (ff_of_hyp (vec 0,V',E')) (w,r w) = (ITER n r w,r(ITER n r w))` ASSUME_TAC THENL [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN COND_CASES_TAC THENL [SUBGOAL_THEN `r(ITER n (r:real^3->real^3) w) IN V'` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN AP_TERM_TAC THEN MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC(SET_RULE `a = a' /\ b = b' ==> {a,b} = {b',a'}`) THEN ASM_MESON_TAC[]; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT `~(a \/ b) ==> a ==> c`)) THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN SUBGOAL_THEN `!n w. w IN V' ==> ITER n (ff_of_hyp (vec 0,V',E')) (r w,w) = r(ITER n r' w),ITER n r' w` ASSUME_TAC THENL [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN COND_CASES_TAC THENL [SUBGOAL_THEN `(r:real^3->real^3) (ITER n (r':real^3->real^3) w) IN V'` ASSUME_TAC THENL [ASM_MESON_TAC[]; ASM_SIMP_TAC[]] THEN AP_TERM_TAC THEN MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC(SET_RULE `a = a' /\ b = b' ==> {a,b} = {b',a'}`) THEN ASM_MESON_TAC[]; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT `~(a \/ b) ==> b ==> c`)) THEN EXPAND_TAC "FF''" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN SUBGOAL_THEN `(!x:real^3 k. x IN V' /\ 0 < k /\ k < CARD V' ==> ~(ITER k r x = x)) /\ (!x y:real^3. x IN V' /\ y IN V' ==> ?i. i < CARD V' /\ y = ITER i r x) /\ (!x. x IN V' ==> ITER (CARD V') r x = x) /\ (!x. x IN V' ==> ITER (CARD V') r' x = x)` MP_TAC THENL [SUBGOAL_THEN `!k. k < CARD(V':real^3->bool) ==> ITER k r (rho_node1 FF v) = ITER (k + 1) (rho_node1 FF) v` ASSUME_TAC THENL [REWRITE_TAC[GSYM ITER_ADD; num_CONV `1`; ITER] THEN MATCH_MP_TAC num_INDUCTION THEN SIMP_TAC[ITER; ARITH_RULE `SUC k < n ==> k < n`] THEN X_GEN_TAC `i:num` THEN DISCH_THEN(K ALL_TAC) THEN DISCH_TAC THEN EXPAND_TAC "r" THEN REWRITE_TAC[GSYM(CONJUNCT2 ITER); GSYM(CONJUNCT2 ITER_ALT)] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `SUC i < V ==> ~(V + 1 <= SUC(SUC i))`)) THEN MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas1.CARD_IS_LEAST_CYCLE; NOT_SUC]; ALL_TAC] THEN SUBGOAL_THEN `ITER (CARD(V':real^3->bool)) r (rho_node1 FF v) = rho_node1 FF v` ASSUME_TAC THENL [FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE `3 <= n ==> n = SUC(n - 1)`)) THEN ASM_SIMP_TAC[ITER; ARITH_RULE `3 <= n ==> n - 1 < n /\ n - 1 + 1 = n`] THEN EXPAND_TAC "r" THEN REWRITE_TAC[GSYM(CONJUNCT2 ITER)] THEN ASM_REWRITE_TAC[ADD1] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]; ALL_TAC] THEN SUBGOAL_THEN `!x. x IN V' ==> ?k. k < CARD V' /\ ITER k r (rho_node1 FF v) = x` (LABEL_TAC "Reach") THENL [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN X_GEN_TAC `x:real^3` THEN STRIP_TAC THEN MP_TAC(ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `FF:real^3#real^3->bool`; `rho_node1 FF v`; `x:real^3`] LOCAL_FAN_ORBIT_MAP_EXPLICIT) THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; MATCH_MP_TAC MONO_EXISTS] THEN X_GEN_TAC `i:num` THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [SYM th]) THEN REWRITE_TAC[ARITH_RULE `i < v + 1 <=> i < v \/ i = v`] THEN DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN ASM_SIMP_TAC[GSYM ITER_ADD; num_CONV `1`; ITER] THEN ASM_REWRITE_TAC[GSYM(CONJUNCT2 ITER_ALT); ADD1] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]; ALL_TAC] THEN MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL [MAP_EVERY X_GEN_TAC [`x:real^3`; `i:num`] THEN STRIP_TAC THEN REMOVE_THEN "Reach" (MP_TAC o SPEC `x:real^3`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `j:num` (STRIP_ASSUME_TAC o GSYM)) THEN ASM_REWRITE_TAC[ITER_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ITER_ADD] THEN SUBGOAL_THEN `!j x y:real^3. x IN V' /\ y IN V' /\ ~(x = y) ==> ~(ITER j r x = ITER j r y)` MATCH_MP_TAC THENL [INDUCT_TAC THEN REWRITE_TAC[ITER] THEN ASM_MESON_TAC[]; ALL_TAC] THEN REPEAT CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC; ALL_TAC; ASM_SIMP_TAC[GSYM ITER_ADD; num_CONV `1`; ITER] THEN DISCH_TAC THEN UNDISCH_TAC `i < CARD(V':real^3->bool)` THEN MATCH_MP_TAC(ARITH_RULE `V + 1 <= i ==> i < V ==> F`) THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] (GEN_ALL Local_lemmas1.CARD_IS_LEAST_CYCLE))) THEN EXISTS_TAC `rho_node1 FF v` THEN ASM_SIMP_TAC[LE_1]] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]; DISCH_THEN(LABEL_TAC "Rdistinct")] THEN CONJ_TAC THENL [REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`IMAGE (\i. ITER i r (x:real^3)) {i | i < CARD(V':real^3->bool)}`; `V':real^3->bool`] SUBSET_CARD_EQ) THEN ASM_SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN MATCH_MP_TAC(TAUT `(q ==> r) /\ p ==> (p <=> q) ==> r`) THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_LT] THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN REWRITE_TAC[FINITE_NUMSEG_LT] THEN MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN REPEAT STRIP_TAC THEN REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`ITER i (r:real^3->real^3) x`; `j - i:num`]) THEN ASM_SIMP_TAC[ITER_ADD; LT_IMP_LE; SUB_ADD] THEN ASM_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL [X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN REMOVE_THEN "Reach" (MP_TAC o SPEC `x:real^3`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `j:num` (STRIP_ASSUME_TAC o GSYM)) THEN ASM_REWRITE_TAC[ITER_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ITER_ADD] THEN ASM_MESON_TAC[]; ALL_TAC] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:real^3` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM o AP_TERM `ITER (CARD(V':real^3->bool)) (r':real^3->real^3)`) THEN SPEC_TAC(`CARD(V':real^3->bool)`,`j:num`) THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[ITER_ALT] THEN ASM_SIMP_TAC[ITER]; DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "Rdistinct") MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "Rorbit") STRIP_ASSUME_TAC)] THEN SUBGOAL_THEN `!x. x IN FF' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF'` ASSUME_TAC THENL [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN ASM_SIMP_TAC[GE; LE_0] THEN EXPAND_TAC "FF'" THEN ASM SET_TAC[]; ALL_TAC] THEN CONJ_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `w:real^3`) THEN REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(SET_RULE `(?x. P x) /\ (!x. P x ==> R x) ==> ?x. (P x \/ Q x) /\ R x`) THEN ASM_SIMP_TAC[] THEN EXPAND_TAC "FF'" THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `CARD(FF':real^3#real^3->bool) = CARD(V':real^3->bool) /\ CARD(FF'':real^3#real^3->bool) = CARD V'` STRIP_ASSUME_TAC THENL [MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN CONJ_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[]; ALL_TAC] THEN CONJ_TAC THENL [REWRITE_TAC[MULT_2] THEN MATCH_MP_TAC(MESON[CARD_UNION] `CARD t = CARD s /\ FINITE s /\ FINITE t /\ s INTER t = {} ==> CARD(s UNION t) = CARD s + CARD s`) THEN ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN REWRITE_TAC[SET_RULE `IMAGE f s INTER IMAGE g s = {} <=> !x y. x IN s /\ y IN s ==> ~(f x = g y)`] THEN REWRITE_TAC[PAIR_EQ] THEN MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN STRIP_TAC THEN REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`x:real^3`; `SUC(SUC 0)`]) THEN ASM_SIMP_TAC[ITER; ARITH; ARITH_RULE `3 <= V ==> SUC(SUC 0) < V`] THEN MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!x. x IN FF'' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF''` ASSUME_TAC THENL [EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN ASM_SIMP_TAC[GE; LE_0] THEN EXPAND_TAC "FF''" THEN SUBGOAL_THEN `!y:real^3. y IN V' ==> ?i. ITER i r' x = y` MP_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN X_GEN_TAC `y:real^3` THEN DISCH_TAC THEN REMOVE_THEN "Rorbit" (MP_TAC o SPECL [`y:real^3`; `x:real^3`]) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SPEC_TAC(`i:num`,`j:num`) THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[ITER_ALT] THEN ASM_SIMP_TAC[ITER]; ALL_TAC] THEN REWRITE_TAC[Lvducxu.HAS_ORD2_INTERPRET] THEN SUBGOAL_THEN `(!x. x IN FF' ==> nn_of_hyp (vec 0,V',E') x IN FF'') /\ (!x. x IN FF'' ==> nn_of_hyp (vec 0,V',E') x IN FF')` STRIP_ASSUME_TAC THENL [ASM_SIMP_TAC[nn_of_hyp3; FORALL_PAIR_THM; IN_UNION] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN `w:real^3` STRIP_ASSUME_TAC) THENL [EXISTS_TAC `(r':real^3->real^3) w` THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]; EXISTS_TAC `(r:real^3->real^3) w` THEN ASM_SIMP_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]]; ALL_TAC] THEN SUBGOAL_THEN `nn_of_hyp (vec 0,V',E') o nn_of_hyp (vec 0,V',E') = I` ASSUME_TAC THENL [ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`w:real^3`; `z:real^3`] THEN ASM_CASES_TAC `(w:real^3,z:real^3) IN FF' UNION FF''` THENL [ALL_TAC; ASM_REWRITE_TAC[nn_of_hyp3]] THEN FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [IN_UNION]) THEN ONCE_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2] THEN ASM_SIMP_TAC[IN_UNION] THEN ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2; IN_UNION; PAIR_EQ] THENL [UNDISCH_TAC `(w:real^3,z:real^3) IN FF'` THEN EXPAND_TAC "FF'"; UNDISCH_TAC `(w:real^3,z:real^3) IN FF''` THEN EXPAND_TAC "FF''"] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN DISCH_THEN(X_CHOOSE_THEN `y:real^3` STRIP_ASSUME_TAC) THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC AZIM_CYCLE_TWO_POINT_SET_ALT THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THENL [SET_TAC[]; ALL_TAC] THEN BINOP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [REWRITE_TAC[IN_UNION; MESON[] `(!x. P x \/ Q x ==> R x) <=> (!x. P x ==> R x) /\ (!x. Q x ==> R x)`] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `IMAGE (nn_of_hyp (vec 0,V',E')) FF' = FF'' /\ IMAGE (nn_of_hyp (vec 0,V',E')) FF'' = FF'` MP_TAC THENL [ALL_TAC; SET_TAC[]] THEN MATCH_MP_TAC(SET_RULE `(!x. f(f x) = x) /\ (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> f x IN s) ==> IMAGE f s = t /\ IMAGE f t = s`) THEN RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM]) THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders] THEN CONJ_TAC THENL [CONJ_TAC THENL [X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; I_THM; NOT_FORALL_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_THEN `w:real^3` STRIP_ASSUME_TAC) THEN EXISTS_TAC `(w,(r:real^3->real^3) w)` THEN ASM_SIMP_TAC[PAIR_EQ]; REWRITE_TAC[FUN_EQ_THM; I_THM] THEN MATCH_MP_TAC(MESON[IN_UNION] `!FF' FF''. (!x. x IN FF' ==> P x) /\ (!x. x IN FF'' ==> P x) /\ (!x. ~(x IN FF' UNION FF'') ==> P x) ==> !x. P x`) THEN MAP_EVERY EXISTS_TAC [`FF':real^3#real^3->bool`; `FF'':real^3#real^3->bool`] THEN REPEAT CONJ_TAC THENL [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[PAIR_EQ]; EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[PAIR_EQ]; ASM_REWRITE_TAC[FORALL_PAIR_THM; ff_of_hyp3] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN SPEC_TAC(`CARD(V':real^3->bool)`,`k:num`) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER]]]; ALL_TAC] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(x:real^3,y) IN darts_of_hyp E' V'` THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `(!x y:real^3. (x,y) IN FF' ==> (y,x) IN FF'') /\ (!x y:real^3. (x,y) IN FF'' ==> (y,x) IN FF')` MP_TAC THENL [ALL_TAC; REWRITE_TAC[IN_UNION] THEN MESON_TAC[]] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[]; REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; I_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `x:real^3`) THEN DISCH_THEN(MP_TAC o SPEC `x,(r:real^3->real^3) x`) THEN ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[PAIR_EQ] THEN REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`x:real^3`; `SUC 0`]) THEN ASM_SIMP_TAC[ITER; ARITH; ARITH_RULE `3 <= V ==> 1 < V`] THEN ASM_MESON_TAC[PAIR_EQ]; REWRITE_TAC[nn_of_hyp3; FUN_EQ_THM; I_THM] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `x:real^3`) THEN DISCH_THEN(MP_TAC o SPEC `x,(r:real^3->real^3) x`) THEN ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN ASM_SIMP_TAC[PAIR_EQ; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`x:real^3`; `SUC(SUC 0)`]) THEN ASM_SIMP_TAC[ITER; ARITH; ARITH_RULE `3 <= V ==> 2 < V`] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.convex_local_fan] THEN EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN SIMP_TAC[Wrgcvdr_cizmrrh.azim_in_fan; Wrgcvdr_cizmrrh.wedge_in_fan_ge] THEN X_GEN_TAC `u:real^3` THEN DISCH_TAC THEN ABBREV_TAC `d = azim_cycle (EE u E') (vec 0) u (r u)` THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN SUBGOAL_THEN `CARD (EE (u:real^3) E') = 2` SUBST1_TAC THENL [MATCH_MP_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1) THEN MAP_EVERY EXISTS_TAC [`FF':real^3#real^3->bool`; `V':real^3->bool`] THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "V'" THEN ASM SET_TAC[]; CONV_TAC NUM_REDUCE_CONV] THEN SUBGOAL_THEN `d = (r':real^3->real^3) u` SUBST1_TAC THENL [EXPAND_TAC "d" THEN SUBGOAL_THEN `EE (u:real^3) E' = {r u,r' u}` (fun th -> REWRITE_TAC[th; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]) THEN FIRST_ASSUM(fun th -> REWRITE_TAC [MATCH_MP Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE th]) THEN REWRITE_TAC[Fan.set_of_edge] THEN EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!z. azim (vec 0) u (r u) z = azim (vec 0) u (rho_node1 FF u) z` ASSUME_TAC THENL [X_GEN_TAC `z:real^3` THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_SAME_WITHIN_AFF_GE THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL [SUBGOAL_THEN `u = ivs_rho_node1 FF v` (fun th -> ASM_REWRITE_TAC[th]) THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; IN_DIFF]; EXPAND_TAC "v" THEN ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; IN_DIFF]; DISCH_THEN(MP_TAC o SPEC `v:real^3` o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT] COLLINEAR_WITHIN_AFF_GE_COLLINEAR)) THEN REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [SUBGOAL_THEN `u = ivs_rho_node1 FF v` (fun th -> ASM_REWRITE_TAC[th]) THEN ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; IN_DIFF]; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]]]; ALL_TAC] THEN CONJ_TAC THENL [FIRST_ASSUM(MP_TAC o SPEC `u:real^3` o GEN_ALL o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] Local_lemmas.IN_V_IMP_AZIM_LESS_PI)) THEN ANTS_TAC THENL [ASM SET_TAC[]; ASM_REWRITE_TAC[]] THEN DISCH_THEN MATCH_MP_TAC THEN ASM SET_TAC[]; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I [Wrgcvdr_cizmrrh.convex_local_fan]) THEN DISCH_THEN(MP_TAC o SPEC `u,rho_node1 FF u`) THEN ANTS_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS; IN_DIFF]; DISCH_THEN(MP_TAC o CONJUNCT2)] THEN MP_TAC(GEN_ALL(MATCH_MP(ONCE_REWRITE_RULE[IMP_CONJ] Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND) (ASSUME `local_fan (V:real^3->bool,E,FF)`))) THEN DISCH_THEN(MP_TAC o SPEC `u:real^3`) THEN ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN ASM_CASES_TAC `rho_node1 FF v = u` THENL [ABBREV_TAC `w = ivs_rho_node1 FF v` THEN EXPAND_TAC "r" THEN COND_CASES_TAC THENL [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; ALL_TAC] THEN SUBGOAL_THEN `(r':real^3->real^3) u = w` SUBST1_TAC THENL [SUBGOAL_THEN `(r:real^3->real^3) (r'(u:real^3)) = r w` MP_TAC THENL [ASM_SIMP_TAC[] THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS; IN_DIFF]; MATCH_MP_TAC EQ_IMP THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN ASM_MESON_TAC[IN_DIFF; IN_SING; Local_lemmas1.LOCAL_FAN_IVS_IN_V; Local_lemmas1.IVS_RHO_NODE_DIFF_ID]]; ALL_TAC] THEN SUBGOAL_THEN `ivs_rho_node1 FF u = v` SUBST1_TAC THENL [ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; IN_DIFF]; REWRITE_TAC[Localization.wedge_ge; azim]] THEN MATCH_MP_TAC(SET_RULE `v' SUBSET v /\ s = t ==> v SUBSET s ==> v' SUBSET t`) THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `a = b ==> {x | f x <= a} = {x | f x <= b}`) THEN MATCH_MP_TAC AZIM_SAME_WITHIN_AFF_GE_ALT THEN REPEAT CONJ_TAC THENL [ASM_MESON_TAC[INSERT_AC]; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; INSERT_AC]; DISCH_THEN(MP_TAC o SPEC `v:real^3` o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT] COLLINEAR_WITHIN_AFF_GE_COLLINEAR)) THEN REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [ASM_MESON_TAC[INSERT_AC]; ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]]]; ASM_REWRITE_TAC[Localization.wedge_ge; azim] THEN SUBGOAL_THEN `(r':real^3->real^3) u = ivs_rho_node1 FF u` (fun th -> REWRITE_TAC[th] THEN ASM SET_TAC[]) THEN SUBGOAL_THEN `(r:real^3->real^3)((r':real^3->real^3) u) = r(ivs_rho_node1 FF u)` MP_TAC THENL [ASM_SIMP_TAC[] THEN EXPAND_TAC "r" THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[IN_DIFF; IN_SING; Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]; MATCH_MP_TAC EQ_IMP THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[] THEN EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN ASM_MESON_TAC[IN_DIFF; IN_SING; Local_lemmas1.LOCAL_FAN_IVS_IN_V; Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]]]);; end;;