(* ============================================================= *)
(* ============================================================= *)
(* ============================================================= *)
(* =============================================================
#use "/home/user1/flyspeck/working/boot.hl";;
needs "/home/user1/flyspeck/working/local_lemmas1.hl";;
============================================================= *)
(*
let build_sequence =
["general/sphere.hl";
"leg/geomdetail.hl";
"leg/affprops.hl";
"leg/cayleyR_def.hl";
"leg/enclosed_def.hl";
"leg/collect_geom.hl";
(* flyspeck_needs "leg/collect_geom2.hl";*) (* slow and rarely needed *)
"jordan/refinement.hl";
"jordan/lib_ext.hl";
"jordan/hash_term.hl";
"jordan/parse_ext_override_interface.hl";
"jordan/goal_printer.hl";
"jordan/real_ext.hl";
"jordan/tactics_jordan.hl";
"jordan/num_ext_nabs.hl";
"jordan/taylor_atn.hl";
"jordan/float.hl";
"jordan/flyspeck_constants.hl";
"jordan/misc_defs_and_lemmas.hl";
"nonlinear/ineqdata3q1h.hl";
"nonlinear/ineq.hl";
"nonlinear/parse_ineq.hl";
"nonlinear/vukhacky_tactics.hl" ;
"trigonometry/trig1.hl";
"trigonometry/trig2.hl";
"nonlinear/compute_2158872499.hl"; (* need trig1.hl trig2.hl *)
"trigonometry/trigonometry.hl";
"trigonometry/delta_x.hl";
"trigonometry/euler_complement.hl";
"trigonometry/euler_multivariate.hl";
"trigonometry/euler_main_theorem.hl";
"volume/vol1.hl";
"hypermap/hypermap.hl"; (* svn 1898 not compatible with other files *)
"fan/fan_defs.hl";
"fan/introduction.hl";
"fan/topology.hl";
"fan/fan_misc.hl";
"fan/planarity.hl"; (* svn 1717 -- 1792 has errors. Build fails. *)
"fan/polyhedron.hl";
"fan/HypermapAndFan.hl";
"fan/Conforming.hl";
"packing/pack1.hl";
"packing/pack2.hl";
"packing/pack_defs.hl";
"packing/pack_concl.hl";
"packing/pack3.hl"; (* needs pack_defs.hl *)
"packing/Rogers.hl";
"packing/TARJJUW.hl"; (* weakly_saturated def. modified in svn 1912. *)
"packing/TIWWFYQ.hl";
"packing/RHWVGNP.hl";
"packing/DRUQUFE.hl";
"packing/BBDTRGC_def.hl";
"packing/NOPZSEH_def.hl";
"packing/JNRJQSM_def.hl";
"packing/KHEJKCI.hl";
"packing/IDBEZAL.hl";
"packing/JJGTQMN_def.hl";
"packing/PHZVPFY_def.hl";
(* ky's stuff *)
"packing/beta_pair_thm.hl";
"packing/lemma_negligible.hl";
(* "local/local_defs.hl"; *)
"local/WRGCVDR_CIZMRRH.hl";
"local/LVDUCXU.hl";
"local/LDURDPN.hl";
"local/LOCAL_LEMMAS.hl"];;
(* 1897 has an error Unbound value ivs_rho_node1*)
let build_all() =
(* (needs "Multivariate/flyspeck.ml"; *)
map flyspeck_needs build_sequence;;
build_all();;
*)
(* ============================================================== *)
(* ============================================================== *)
(* ============================================================== *)
module Local_lemmas1 = struct
open Ldurdpn;;
open Lvducxu;;
open Sphere;;
open Trigonometry1;;
open Trigonometry2;;
open Hypermap;;
open Fan;;
open Prove_by_refinement;;
open Wrgcvdr_cizmrrh;;
open Aff_sgn_tac;;
open Fan_misc;;
open Fan_defs;;
open Planarity;;
open Topology;;
open Local_lemmas;;
(* deprecated 2013-02-22:
let spherical_map = new_definition ` spherical_map (e1,e2,e3) (r,theta, phi) =
(r * cos theta * sin phi) % e1 +
(r * sin theta * sin phi ) % e2 + (r * cos phi) % e3 `;;
` spherical_coor v0 (e1,e2,e3) v = (dist (v0,v), azim v0 (v0 + e3) (v0 + e1) v, arcV v0 (v0 + e3) v)`;;
*)
(* deprecated 2013-02-22:
let v_slice = new_definition ` v_slice f (v,w) =
{ ITER i f v | ! j. j < i ==> ~( ITER j f v = w ) }`;;
let e_slice = new_definition ` e_slice f (v,w) =
{w,v} INSERT
{ {ITER i f v, ITER (i + 1) f v} | ! j. j < i + 1 ==> ~( ITER j f v = w)} `;;
let f_slice = new_definition ` f_slice f (v,w) =
(w,v) INSERT
{ (ITER i f v, ITER (i + 1) f v) | ! j. j < i + 1 ==> ~ (ITER j f v = w)} `;;
*)
let ARCV_EQ_0 = prove(` ~(u = v) /\ &0 < t ==>
arcV u v (u + t % (v - u)) = &0`,
NHANH
ACR_REFL THEN ONCE_REWRITE_TAC[Trigonometry2.ARCV_VEC0_FORM] THEN
SIMP_TAC[VECTOR_ARITH`(a + b) - a:real^N = b`; GSYM
Trigonometry2.WHEN_K_POS_ARCV_STABLE]);;
let ARCV_PI_OPPOSITE = prove(`~(u = v) /\ t < &0 ==>
arcV u v (u + t % (v - u)) =
pi`,
NHANH
ARC_OPPOSITE THEN ONCE_REWRITE_TAC[Trigonometry2.ARCV_VEC0_FORM] THEN
SIMP_TAC[VECTOR_ARITH`(a + b) - a:real^N = b`; VECTOR_ARITH` &2 % u - v - u = -- (v - u)`] THEN
ONCE_REWRITE_TAC[VECTOR_ARITH` a % x = (-- a) % ( -- x)`] THEN
SIMP_TAC[GSYM Trigonometry2.WHEN_K_POS_ARCV_STABLE; REAL_ARITH` t < &0 <=> &0 < -- t `]);;
let REAL_NEG_MUL_EQ = prove(` a < &0 ==> ( a * x < &0 <=> &0 < x ) /\
(&0 < a * x <=> x < &0) `,
REWRITE_TAC[REAL_ARITH` a < &0 <=> &0 < -- a `; REAL_ARITH` -- ( a * x) = -- a * x `] THEN
SIMP_TAC[
REAL_LT_MUL_EQ] THEN
ONCE_REWRITE_TAC[REAL_ARITH` a * b = -- a * -- b `] THEN
SIMP_TAC[
REAL_LT_MUL_EQ]);;
let COLL_AFF_GT_2_1 = prove(`!x v w:real^N.
~collinear {x, v, w}
==> aff_gt {x, v} {w} =
{y | ?t1 t2 t3.
&0 < t3 /\
t1 + t2 + t3 = &1 /\
y =
t1 % x + t2 % v + t3 % w}`,
let ARCV_EQ_IMP_NORMIZE = prove_by_refinement (
` (x:real^N)
IN aff_gt {
vec 0, u} {y} /\ ~
collinear {
vec 0, u, y} /\
arcV (
vec 0) u x =
arcV (
vec 0) u y ==> normize x = normize y `,
[NHANH
COLL_AFF_GT_2_1;
STRIP_TAC;
UNDISCH_TAC` x
IN aff_gt {
vec 0, u} {y:real^N} `;
ASM_REWRITE_TAC[
IN_ELIM_THM;
VECTOR_MUL_RZERO;
VECTOR_ADD_LID];
NHANH_PAT`\x. x ==> y` (MESON[]` x = y ==> (&1 /norm x) % x = (&1 /
norm x) % y `);
STRIP_TAC;
MP_TAC (ISPECL [`&1 `;` &1 /
norm (y:real^N)`;`u:real^N`;` y:real^N`]
COLLINEAR_SCALE_ALL);
SUBGOAL_THEN` &0 <
norm (y:real^N) /\ &0 <
norm (x:real^N)` ASSUME_TAC;
REWRITE_TAC[
NORM_POS_LT];
UNDISCH_TAC` ~
collinear {
vec 0, u, y:real^N}`;
NHANH Trigonometry2.NOT_COLLINEAR_IMP_2_UNEQUAL;
SIMP_TAC[];
REPEAT STRIP_TAC;
UNDISCH_TAC` x = t2 % u + t3 % (y:real^N)`;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (REAL_ARITH` &0 < t3 ==> ~( t3 = &0) `);
ASM_MESON_TAC[
COLL_EQ_DEPENDENT];
ANTS_TAC;
DOWN;
CONV_TAC REAL_FIELD;
SUBGOAL_THEN `&0 < &1 /
norm (x:real^N) * t3 ` MP_TAC;
REWRITE_TAC[REAL_ARITH` &1 / a * b = b / a `];
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[];
REWRITE_TAC[
VECTOR_MUL_LID];
STRIP_TAC;
DISCH_THEN (ASSUME_TAC o SYM);
DOWN THEN DOWN THEN DOWN;
ONCE_REWRITE_TAC[Collect_geom.POS_EQ_INV_POS];
NHANH (ISPECL [`u:real^N`;` &1 /
norm (v:real^N)`;`v:real^N`] (GEN_ALL
Trigonometry2.WHEN_K_POS_ARCV_STABLE));
REWRITE_TAC[GSYM Collect_geom.POS_EQ_INV_POS];
DOWN;
REWRITE_TAC[
NORM_POS_LT; Trigonometry2.NOT_VEC0_UNITABLE;
VECTOR_ADD_LDISTRIB;
VECTOR_MUL_ASSOC];
REPEAT STRIP_TAC;
REWRITE_TAC[normize];
MATCH_MP_TAC (GEN_ALL
ARCV_DETER_DIRECTION);
EXISTS_TAC` (&1 /
norm (x:real^N) * t2)`;
EXISTS_TAC` (&1 /
norm (x:real^N) * t3) * (
norm (y:real^N)) `;
EXISTS_TAC` u:real^N`;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ABBREV_TAC` nx = &1 /
norm x % (x:real^N)`;
ABBREV_TAC` ny = &1 /
norm y % (y:real^N)`;
SWITCH_TAC` x = t2 % u + t3 % (y:real^N)`;
SWITCH_TAC` nx = (&1 /
norm (x:real^N) * t2) % u + (&1 /
norm x * t3) % (y:real^N)`;
ASM_REWRITE_TAC[];
CONJ_TAC;
EXPAND_TAC "ny";
let AZIM_AND_ARCV_EQ_IMP_PARA = prove_by_refinement (
` ~
collinear {v0,u,v} /\
azim v0 u v x =
azim v0 u v y /\
arcV v0 u x =
arcV v0 u y ==> y = v0 \/ (? t. &0 <= t /\ x - v0 = t % (y - v0)) `,
[ASM_CASES_TAC`
collinear {v0,u,y:real^3}`;
ASM_SIMP_TAC[
AZIM_DEGENERATE];
ASM_CASES_TAC`
collinear {v0,u,x:real^3}`;
NHANH Fan.th3b;
NHANH (REWRITE_RULE[GSYM
RIGHT_IMP_FORALL_THM]
Trigonometry2.NOT_EQ_IMP_AFF_AND_COLL3);
STRIP_TAC;
SWITCH_TAC` !u'. u'
IN aff {v0, u} <=>
collinear {v0, u, u':real^3}`;
UNDISCH_TAC`
collinear {v0, u, y:real^3}`;
UNDISCH_TAC`
collinear {v0, u, x:real^3}`;
ASM_REWRITE_TAC[Trigonometry2.AFF2;
IN_ELIM_THM];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[VECTOR_ARITH` (t % v0 + (&1 - t) % u) - v0 = (&1 - t) % ( u - v0)`];
ASM_CASES_TAC` t' = &1 `;
DISJ1_TAC;
ASM_REWRITE_TAC[
REAL_SUB_REFL;
VECTOR_MUL_LZERO;
VECTOR_MUL_LID;
VECTOR_ADD_RID];
DISJ2_TAC;
EXISTS_TAC` ( &1 - t ) / ( &1 - t')`;
ASM_SIMP_TAC[
VECTOR_MUL_ASSOC; REAL_FIELD` ~(t' = &1) ==>
((&1 - t) / (&1 - t')) * (&1 - t') = &1 - t `];
UNDISCH_TAC`
arcV v0 u x =
arcV v0 (u:real^3) y `;
ONCE_REWRITE_TAC[Trigonometry2.ARCV_VEC0_FORM];
ASM_REWRITE_TAC[VECTOR_ARITH` (t % v0 + (&1 - t) % u) - v0 = (&1 - t) % (u - v0)`];
ASSUME_TAC2 (REAL_FIELD` ~( t' = &1 ) ==>
&1 - t = ((&1 - t)/ (&1 - t')) * ( &1 - t')`);
ABBREV_TAC` tt = (&1 - t) / (&1 - t') `;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (REAL_ARITH`~( t' = &1 ) ==> &0 < &1 - t' \/ &1 - t' < &0 `);
FIRST_X_ASSUM DISJ_CASES_TAC;
SUBGOAL_THEN`
arcV (
vec 0) (u:real^3 - v0) ((&1 - t') % (u - v0)) = &0` SUBST1_TAC;
MATCH_MP_TAC
ARCV_EQ_0_ORIGIN;
ASM_REWRITE_TAC[VECTOR_ARITH` a - b =
vec 0 <=> b = a `];
UNDISCH_TAC` ~(v0 = u:real^3)`;
ONCE_REWRITE_TAC[VECTOR_ARITH`a = b <=> b - a =
vec 0`];
SIMP_TAC[
ARCV_ORI_DIRECTIONS];
STRIP_TAC;
UNDISCH_TAC` &0 < &1 - t'`;
SIMP_TAC[
REAL_LT_MUL_EQ;
REAL_LT_IMP_LE];
ASSUME_TAC2 (ISPECL [`&1 - t'`;` u:real^3`;`v0:real^3`] (GEN_ALL
( ONCE_REWRITE_RULE[Trigonometry2.ARCV_VEC0_FORM]
ARCV_PI_OPPOSITE)));
DOWN;
SIMP_TAC[VECTOR_ARITH`(a + b:real^N) - a = b `];
STRIP_TAC;
UNDISCH_TAC` ~( v0 = u:real^3)`;
ONCE_REWRITE_TAC[VECTOR_ARITH` a = b <=> b - a =
vec 0`];
SIMP_TAC[
ARCV_ORI_DIRECTIONS];
STRIP_TAC;
UNDISCH_TAC` &1 - t' < &0 `;
SIMP_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM]
REAL_NEG_MUL_EQ;
REAL_LT_IMP_LE];
UNDISCH_TAC`
collinear {v0, u, y:real^3}`;
NHANH Fan.th3b;
ASM_CASES_TAC` y = v0:real^3`;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
SUBGOAL_THEN`
sin (
arcV v0 u (y:real^3)) = &0` MP_TAC;
MATCH_MP_TAC
COLLINEAR_SIN_ARCV_0;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ~(
sin (
arcV v0 u (x:real^3)) = &0 )` MP_TAC;
MATCH_MP_TAC Trigonometry2.NOT_COLLINEAR_IMP_NOT_SIN0;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[];
ASM_CASES_TAC` x = v0:real^3`;
STRIP_TAC;
DISJ2_TAC;
EXISTS_TAC` &0 `;
ASM_REWRITE_TAC[
REAL_LE_REFL;
VECTOR_SUB_REFL;
VECTOR_MUL_LZERO];
ASM_CASES_TAC`
collinear {v0, u, x:real^3}`;
STRIP_TAC;
SUBGOAL_THEN`
sin (
arcV v0 u (x:real^3)) = &0` MP_TAC;
MATCH_MP_TAC
COLLINEAR_SIN_ARCV_0;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Fan.th3b;
EXISTS_TAC` v:real^3`;
FIRST_ASSUM ACCEPT_TAC;
UNDISCH_TAC` ~collinear {v0, u, y:real^3}`;
ASM_SIMP_TAC[Trigonometry2.NOT_COLLINEAR_IMP_NOT_SIN0];
STRIP_TAC;
ASSUME_TAC2 (ISPECL [`v0:real^3`;` u:real^3`;`v:real^3`; ` x:real^3`;`
y:real^3`]
AZIM_EQ_ALT);
UNDISCH_TAC` ~collinear {v0, u, y:real^3}`;
NHANH
COLL_AFF_GT_2_1;
STRIP_TAC;
DISJ2_TAC;
UNDISCH_TAC`
azim v0 u v x =
azim v0 u v (y:real^3)`;
ASM_REWRITE_TAC[
IN_ELIM_THM; REAL_ARITH` a + b = &1 <=> a = &1 - b`];
STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[VECTOR_ARITH` x = (&1 - (t2 + t3)) % v0 + t2 % u + t3 % y <=>
x - v0 = t2 % ( u - v0) + t3 % (y - v0) `];
ABBREV_TAC` xx = x - v0:real^3`;
ABBREV_TAC` uu = u - v0:real^3 `;
ABBREV_TAC` yy = y - v0:real^3`;
STRIP_TAC;
EXISTS_TAC` t3:real`;
UNDISCH_TAC`
arcV v0 u x =
arcV v0 u (y:real^3)`;
NHANH (MESON[]`
arcV v0 u x =
arcV v0 u y ==>
cos (
arcV v0 u x) =
cos (
arcV v0 u y)`);
ASSUME_TAC2 (ISPECL [`v0:real^3`;`u:real^3`;` x:real^3`]
Collect_geom.NOT_COL3_IMP_DIFF);
ASSUME_TAC2 (ISPECL [`v0:real^3`;`u:real^3`;` y:real^3`]
Collect_geom.NOT_COL3_IMP_DIFF);
DOWN THEN DOWN;
REWRITE_TAC[DE_MORGAN_THM];
ASM_SIMP_TAC[Trigonometry2.NOT_EQ_IMPCOS_ARC];
STRIP_TAC THEN STRIP_TAC;
SUBGOAL_THEN` &0 <
norm (xx:real^3) /\ &0 <
norm (uu:real^3) /\
&0 <
norm (yy:real^3)` MP_TAC;
REWRITE_TAC[
NORM_POS_LT];
EXPAND_TAC "xx";
let NORM_CAUCHY_SCHWARZ_FRAC2 = prove(` -- &1 <= (u
dot v) / (
norm u *
norm v) /\
(u
dot v) / (
norm u *
norm (v:real^N)) <= &1 `,
ASM_CASES_TAC`~((u:real^N) =
vec 0) /\ ~((v: real^N) =
vec 0)` THEN
ASM_SIMP_TAC[Trigonometry1.NORM_CAUCHY_SCHWARZ_FRAC] THEN
DOWN THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THENL [
ASM_REWRITE_TAC[
DOT_LZERO] THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[
DOT_RZERO] THEN REAL_ARITH_TAC]);;
let AFF_CONV0_INTERSECTION_LEMMA = prove_by_refinement
(`! u x y (z:real^3).
coplanar {u,x,y,z} /\
~
collinear {u,x,y} /\
~
collinear {u,y,z} /\
~
collinear {u,z,x}
==> ~ ( aff {u,x}
INTER conv0 {y,z} = {} /\
aff {u,y}
INTER conv0 {x,z} = {} /\
aff {u,z}
INTER conv0 {x,y} = {} ) `,
[REWRITE_TAC[
coplanar];
REPEAT STRIP_TAC;
SUBGOAL_THEN`
affine hull {u', v, w} =
affine hull {u,x,y:real^3}` MP_TAC;
MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
ASM_REWRITE_TAC[];
MATCH_MP_TAC
SUBSET_TRANS;
EXISTS_TAC` {u,x,y,z:real^3}` ;
ASM_REWRITE_TAC[
INSERT_SUBSET;
IN_INSERT;
EMPTY_SUBSET];
STRIP_TAC;
SUBGOAL_THEN` {z:real^3}
SUBSET affine hull {u', v, w} ` MP_TAC;
MATCH_MP_TAC
SUBSET_TRANS;
EXISTS_TAC` {u,x,y,z:real^3}`;
ASM_REWRITE_TAC[
INSERT_SUBSET;
IN_INSERT;
EMPTY_SUBSET];
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
AFFINE_HULL_3;
IN_ELIM_THM];
STRIP_TAC;
ASM_CASES_TAC` &0 < v' /\ &0 < w' `;
ABBREV_TAC` tt = &0 % u + &1 % (z:real^3) `;
SUBGOAL_THEN` (?tt. tt
IN aff {u, z:real^3} /\ tt
IN conv0 {x, y})` MP_TAC;
MATCH_MP_TAC (GEN_ALL Local_lemmas.CONDS_FOR_INTER_AFF_CONV0);
EXISTS_TAC` u'':
real` ;
EXISTS_TAC` v':
real `;
EXISTS_TAC` w':
real`;
EXISTS_TAC` &1 `;
EXISTS_TAC` tt: real^3 `;
EXISTS_TAC`&0 `;
EXISTS_TAC` &1 `;
ASM_REWRITE_TAC[REAL_ADD_LID];
EXPAND_TAC "tt";
let TOW_REAL_EXISTS_COMBINED = prove_by_refinement
(` (? e1. &0 < e1 /\ (! t. -- e1 < t /\ t < e1 ==> P t )) /\
(? e1. &0 < e1 /\ (! t. -- e1 < t /\ t < e1 ==> Q t ))
==> (? e1. &0 < e1 /\ (! t. -- e1 < t /\ t < e1 ==> P t /\ Q t ))`,
[STRIP_TAC;
ASM_CASES_TAC` e1 < e1':real `;
EXISTS_TAC` e1:real `;
ASM_REWRITE_TAC[];
GEN_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` -- e1' < -- (e1:real) ` MP_TAC;
DOWN;
REAL_ARITH_TAC;
ASM_MESON_TAC[
REAL_LT_TRANS];
EXISTS_TAC` e1':real`;
ASM_REWRITE_TAC[];
GEN_TAC;
ASM_SIMP_TAC[];
SUBGOAL_THEN` ~(-- e1' < -- e1:real) ` MP_TAC;
DOWN;
REAL_ARITH_TAC;
ASM_MESON_TAC[REAL_ARITH` ~( a < b) /\ a < c ==> b < (c:real) `]]);;
let CONTINUOUS_FUNS_DISTINCT_POINTS = prove_by_refinement
(`f
continuous atreal r /\ g
continuous atreal rr /\ ~ ((f:real -> real^N) r = g rr)
==> ? d. &0 < d /\
(! x y. abs (x - r) < d /\ abs ( y - rr) < d ==> ~( f x = g y) )`,
[REWRITE_TAC[
continuous_atreal];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC`
dist ((f:real -> real^N) r, g (rr:real)) / &2`));
FIRST_X_ASSUM (MP_TAC o (SPEC`
dist ((f:real -> real^N) r, g (rr:real)) / &2`));
SUBGOAL_THEN` &0 <
dist ((f:real -> real^N) r,g (rr:real)) / &2 ` ASSUME_TAC;
ASM_REWRITE_TAC[REAL_ARITH` &0 < a / &2 <=> &0 < a `; GSYM
DIST_NZ];
ANTS_TAC;
FIRST_ASSUM ACCEPT_TAC;
STRIP_TAC;
ANTS_TAC;
FIRST_ASSUM ACCEPT_TAC;
STRIP_TAC;
EXISTS_TAC` min d d' `;
ASM_REWRITE_TAC[
REAL_LT_MIN];
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM NHANH;
REPEAT STRIP_TAC;
MP_TAC (SPECL [` (f:real -> real^N) r`; `(f:real -> real^N) x`;
`(g:real -> real^N) rr `]
DIST_TRIANGLE);
MP_TAC (SPECL [` (f:real -> real^N) x`; `(g:real -> real^N) y`;
`(g:real -> real^N) rr `]
DIST_TRIANGLE);
PHA;
NHANH (REAL_ARITH` a <= b + c /\ x <= y + a ==> x - y - c <= b `);
STRIP_TAC;
SUBGOAL_THEN` &0 <
dist ((f:real -> real^N) x,(g:real -> real^N) y)` MP_TAC;
DOWN;
MATCH_MP_TAC (REAL_ARITH` &0 < b ==> b <= a ==> &0 < a `);
MATCH_MP_TAC (REAL_ARITH` a < x / &2 /\ b < x / &2 ==> &0 < x - a - b `);
UNDISCH_TAC`
dist ((f:real -> real^N) x,f (r:real)) <
dist ((f:real ->
real^N) r,g (rr:real)) / &2`;
ASM_REWRITE_TAC[
DIST_SYM];
ASM_REWRITE_TAC[GSYM
DIST_NZ]]);;
let CONTINUOUS_FUN_DISTINCT_FINITE_SET = prove_by_refinement
(`! V. FINITE (V:real^N -> bool) ==>
(! v1. v1
IN V /\ ~( v0 = v1) ==> ~ (ff v0 r = ff v1 r)) /\
(! v. v
IN v0
INSERT V ==> ff v
continuous atreal r )
==> ? d. &0 < d /\
(! t. abs (t - r) < d ==>
(! v1. v1
IN V /\ ~(v0 = v1 ) ==>
~( ff v0 t = ((ff v1 t):real^M))))`,
[MATCH_MP_TAC
FINITE_INDUCT_STRONG;
REWRITE_TAC[
NOT_IN_EMPTY];
CONJ_TAC;
DISCH_TAC;
EXISTS_TAC` &1 `;
REAL_ARITH_TAC;
REPEAT STRIP_TAC;
UNDISCH_TAC` (!v1. (v1:real^N)
IN V /\ ~(v0 = v1) ==> ~((ff v0 r):real^M = ff v1 r)) /\
(!v. v
IN v0
INSERT V ==> ff v
continuous atreal r)
==> (?d. &0 < d /\
(!t. abs (t - r) < d
==> (!v1. v1
IN V /\ ~(v0 = v1) ==> ~(ff v0 t = ff v1 t)))) `;
ANTS_TAC;
DOWN THEN DOWN THEN PHA;
SIMP_TAC[
IN_INSERT];
MESON_TAC[];
STRIP_TAC;
ASM_CASES_TAC` v0 = x:real^N `;
EXISTS_TAC` d:real `;
ASM_REWRITE_TAC[
IN_INSERT];
DOWN THEN DOWN THEN PHA;
MESON_TAC[];
SUBGOAL_THEN` ff (v0:real^N)
continuous atreal r /\
ff x
continuous atreal r /\
~(ff v0 r = (ff x r):real^M) ` MP_TAC;
DOWN_TAC;
REWRITE_TAC[
IN_INSERT];
MESON_TAC[];
NHANH CONTINUOUS_TWO_POINTS_DISTINCT;
STRIP_TAC;
EXISTS_TAC` min d d'`;
ASM_REWRITE_TAC[
REAL_LT_MIN;
IN_INSERT];
ASM_MESON_TAC[]]);;
let CONTINUOUS_ATREAL_INJ_PRESERVED = prove_by_refinement
(`! V. FINITE (V:real^N -> bool) ==>
(! v1 v2. v1
IN V /\ v2
IN V /\ ~( v1 = v2) ==> ~ (ff v1 r = ff v2 r)) /\
(! v. v
IN V ==> ff v
continuous atreal r )
==> ? d. &0 < d /\
(! t. abs (t - r) < d ==>
(! v1 v2. v1
IN V /\ v2
IN V /\ ~(v1 = v2 ) ==>
~( ff v1 t = ((ff v2 t):real^M))))`,
[MATCH_MP_TAC
FINITE_INDUCT_STRONG;
REWRITE_TAC[
NOT_IN_EMPTY];
CONJ_TAC;
EXISTS_TAC` &1 `;
REAL_ARITH_TAC;
REPEAT STRIP_TAC;
SUBGOAL_THEN` (!v1 v2. (v1:real^N)
IN V /\ v2
IN V /\ ~(v1 = v2) ==> ~(ff v1 r = (ff v2 r):real^M)) /\
(!v. v
IN V ==> ff v
continuous atreal r) ` MP_TAC;
DOWN THEN DOWN THEN PHA;
SIMP_TAC[
IN_INSERT];
DISCH_TAC;
SUBGOAL_THEN` (?d. &0 < d /\
(!t. abs (t - r) < d
==> (!v1 v2.
v1
IN V /\ v2
IN V /\ ~(v1 = (v2:real^N))
==> ~(ff v1 t = (ff v2 t):real^M))))` MP_TAC;
DOWN;
FIRST_X_ASSUM ACCEPT_TAC;
STRIP_TAC;
MP_TAC (SPEC_ALL (
ISPECL [`r:real `;` x:real^N `] (GEN_ALL
CONTINUOUS_FUN_DISTINCT_FINITE_SET)));
PHA;
ANTS_TAC;
UNDISCH_TAC `!(v1:real^N) v2.
v1
IN x
INSERT V /\ v2
IN x
INSERT V /\ ~(v1 = v2)
==> ~(ff v1 (r:real) = (ff v2 r):real^M) `;
ASM_SIMP_TAC[
IN_INSERT];
STRIP_TAC;
EXISTS_TAC` min d d' `;
REWRITE_TAC[
REAL_LT_MIN];
ASM_REWRITE_TAC[];
FIRST_X_ASSUM NHANH;
DOWN;
FIRST_X_ASSUM NHANH;
SIMP_TAC[
IN_INSERT];
MESON_TAC[]]);;
let CONTINUOUS_ATREAL_DISTINCT_FINITE = prove_by_refinement
(`! V. FINITE (V:real^N -> bool)
==> (!v1. v1
IN V ==> ~(ff v1 r = (v0:real^M))) /\
(!v. v
IN V ==> ff v
continuous atreal r)
==> (?d. &0 < d /\
(!t. abs (t - r) < d
==> (!v1. v1
IN V ==> ~(ff v1 t = v0))))`,
[MATCH_MP_TAC FINITE_INDUCT;
REWRITE_TAC[
NOT_IN_EMPTY];
CONJ_TAC;
EXISTS_TAC ` &1 `;
REAL_ARITH_TAC;
REPEAT STRIP_TAC;
UNDISCH_TAC ` (!v1. (v1:real^N)
IN s ==> ~(ff v1 r = (v0:real^M))) /\
(!v. v
IN s ==> ff v
continuous atreal r)
==> (?d. &0 < d /\
(!t. abs (t - r) < d ==> (!v1. v1
IN s ==> ~(ff v1 t = v0)))) `;
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[
IN_INSERT];
STRIP_TAC;
MP_TAC (SPEC`x:real^N ` (GEN`v:real^N`
CONTINUOUS_ATREAL_DISTINCT));
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[
IN_INSERT];
STRIP_TAC;
EXISTS_TAC` min d d' `;
ASM_REWRITE_TAC[
REAL_LT_MIN];
FIRST_X_ASSUM NHANH;
DOWN;
FIRST_X_ASSUM NHANH;
SIMP_TAC[
IN_INSERT];
MESON_TAC[]]);;
let INV_VNI = prove(` inv x = &1 / x `,
PAT_ONCE_REWRITE_TAC `\x. inv x = y` [REAL_ARITH` x = x / &1 `]
THEN REWRITE_TAC[
REAL_INV_DIV]);;
let REAL_CONTINUOUS_IMP_MUL_FUN = prove_by_refinement
(` f
real_continuous at (x:real^N) /\
g
real_continuous at x ==>
(\x. (f x) * (g x))
real_continuous at x `,
[REWRITE_TAC[
real_continuous_at];
REPEAT STRIP_TAC;
ONCE_REWRITE_TAC[REAL_RING` a * b - x * y = (a - x ) * b + (b - y) * x`];
FIRST_X_ASSUM (MP_TAC o (SPEC` e / (&2 * max (abs (f (x:real^N))) (&1))`));
ANTS_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[
REAL_LT_MAX; REAL_ARITH` &0 < &2 * z <=> &0 < z `];
REAL_ARITH_TAC;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` e / (&2 * (abs (g (x:real^N)) + e / (&2 * max (abs (f (x:real^N))) (&1))) )`));
ANTS_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[
REAL_LT_MAX; REAL_ARITH` &0 < &2 * z <=> &0 < z `];
MATCH_MP_TAC (REAL_ARITH` &0 < x ==> &0 < abs a + x `);
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[
REAL_LT_MAX; REAL_ARITH` &0 < &2 * z <=> &0 < z `];
REAL_ARITH_TAC;
STRIP_TAC;
EXISTS_TAC `min d d'`;
ASM_REWRITE_TAC[
REAL_LT_MIN];
GEN_TAC;
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
SUBGOAL_THEN` abs (g (x':real^N)) < abs (g x) + e / (&2 * max (abs (f (x:real^N))) (&1))` MP_TAC;
ASM_REAL_ARITH_TAC;
ASM_CASES_TAC` f (x:real^N) = &0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
SIMP_TAC[
REAL_MUL_RZERO;
REAL_ADD_RID;
REAL_SUB_RZERO];
UNDISCH_TAC` &0 < e `;
REWRITE_TAC[
REAL_ABS_MUL];
REPEAT STRIP_TAC;
SUBGOAL_THEN` abs (f (x':real^N)) * abs (g (x':real^N)) < ( e / (&2 * (abs (g x) + e / (&2 * max (abs (&0)) (&1))))) * (abs (g x) + e / (&2 * max (abs (&0)) (&1)))` MP_TAC;
MATCH_MP_TAC
REAL_LT_MUL2;
ASM_REWRITE_TAC[
REAL_ABS_POS;
REAL_ABS_0;
real_max; REAL_ARITH` &0 <= &1 `;
REAL_MUL_RID];
ASSUME_TAC2 (REAL_ARITH` &0 < e ==> &0 < abs (g (x:real^N)) + e / &2`);
DOWN;
UNDISCH_TAC` &0 < e `;
SIMP_TAC[REAL_FIELD` &0 < a ==> e / (&2 * a) * a = e / &2 `;
REAL_ABS_0;
real_max; REAL_ARITH` &0 <= &1 `;
REAL_MUL_RID];
REAL_ARITH_TAC;
STRIP_TAC;
MATCH_MP_TAC (REAL_ARITH` abs a + abs b < e ==> abs ( a + b ) < e `);
REWRITE_TAC[
REAL_ABS_MUL];
MATCH_MP_TAC (REAL_ARITH` a < e / &2 /\ b < e / &2 ==> a + b < e `);
CONJ_TAC;
SUBGOAL_THEN` abs (f x' - f (x:real^N)) * abs (g x') < ( e / (&2 * (abs (g x) +
e / (&2 * max (abs (f x)) (&1))))) * (abs (g x) + e / (&2 * max (abs (f x)) (&1)))` MP_TAC;
MATCH_MP_TAC
REAL_LT_MUL2;
ASM_REWRITE_TAC[
REAL_ABS_POS];
SUBGOAL_THEN` &0 < abs (g (x:real^N)) + e / (&2 * max (abs (f x)) (&1))` MP_TAC;
MATCH_MP_TAC (REAL_ARITH` &0 < b ==> &0 < abs a + b `);
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
SIMP_TAC[REAL_FIELD` &0 < a ==> e / ( &2 * a ) * a = e / &2 `];
ASM_CASES_TAC` max (abs (f x)) (&1) = abs (f (x:real^N)) `;
UNDISCH_TAC` ~( f (x:real^N) = &0) `;
REWRITE_TAC[
REAL_ABS_NZ];
UNDISCH_TAC` abs (g x' - g (x:real^N)) < e / (&2 * max (abs (f (x:real^N))) (&1))`;
PHA;
NHANH
REAL_LT_RMUL;
ASM_REWRITE_TAC[];
IMP_TAC;
SIMP_TAC[REAL_FIELD` &0 < a ==> x / (&2 * a ) * a = x / &2 `];
SUBGOAL_THEN` e / &2 / max (abs (f x)) (&1) < e / &2 / abs (f (x:real^N))` MP_TAC;
MATCH_MP_TAC
INV_INEQUAL_GENERAL;
ASM_REWRITE_TAC[REAL_ARITH`&0 < a / &2 <=> &0 < a `; GSYM
REAL_ABS_NZ];
DOWN;
REAL_ARITH_TAC;
UNDISCH_TAC` abs (g x' - g (x:real^N)) < e / (&2 * max (abs (f (x:real^N))) (&1))`;
PHA;
REWRITE_TAC[REAL_FIELD` a / &2 / c = a / ( &2 * c ) `];
NHANH (REAL_ARITH` a < b /\ b < c ==> a < c `);
STRIP_TAC;
UNDISCH_TAC` ~( f (x:real^N) = &0)`;
REWRITE_TAC[
REAL_ABS_NZ];
DOWN THEN PHA;
NHANH
REAL_LT_RMUL;
IMP_TAC;
SIMP_TAC[REAL_FIELD` &0 < a ==> e / (&2 * a ) * a = e / &2 `]]);;
let PROVE_SLICING_FAN = prove_by_refinement
(`
local_fan (V,E,
FF) /\
v
IN V /\ w
IN V /\ ~( v = w) /\
(! z t. z
IN {v, w} /\ t
IN (V
DIFF {z}) ==> ~
collinear {
vec 0, z, t}) /\
(! x. x
IN FF ==> aff_gt {
vec 0} {v,w}
SUBSET wedge_in_fan_gt x E)
==>
FAN (
vec 0, V, E
UNION {{v,w}}) `,
[REWRITE_TAC[
FAN;
local_fan;
UNIONS_UNION;
UNIONS_1;
UNION_SUBSET];
LET_TAC;
SIMP_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
graph; SET_RULE` (A
UNION B) x <=>
A x \/ B x `; MESON[]`(!x. P x \/ Q x ==> L x) <=> (! x. P x ==> L x ) /\
(! x. Q x ==> L x )`];
SIMP_TAC[
SET2_HAS_SIZE2; Geomdetail.IN_ACT_SING];
ONCE_REWRITE_TAC[
EQ_SYM_EQ];
SIMP_TAC[
SET2_HAS_SIZE2; fan1; fan2; fan6; fan7;
IN_UNION; MESON[]`
(!x. P x \/ Q x ==> L x) <=> (! x. P x ==> L x) /\ (!x. Q x ==> L x) `; Geomdetail.IN_ACT_SING];
STRIP_TAC;
CONJ_TAC;
GEN_TAC;
SIMP_TAC[Local_lemmas.INSERT_UNION2;
UNION_EMPTY];
STRIP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[
IN_INSERT;
IN_DIFF;
NOT_IN_EMPTY];
ONCE_REWRITE_TAC[TAUT` (a \/ b) \/ c <=> b \/ a \/ c `];
ONCE_REWRITE_TAC[TAUT` (a \/ b) /\ (x \/ y) ==> l <=> ( a /\ x ==> l) /\
( a /\ y ==> l ) /\ ( b /\ x ==> l) /\ (b /\ y ==> l) `];
ASM_SIMP_TAC[
INTER_IDEMPOT];
MATCH_MP_TAC (
MESON[]` (! e1 e2. L e1 e2 ==> L e2 e1) /\ (! e1 e2. e1 = x /\ Q e2 ==> L x e2)
==> (! e1 e2. (e1 = x /\ Q e2 ==> L x e2) /\ (Q e1 /\ e2 = x ==> L e1 x))`);
SIMP_TAC[
INTER_COMM];
REPEAT STRIP_TAC;
SUBGOAL_THEN` (e2: real^3 -> bool)
HAS_SIZE 2` ASSUME_TAC;
DOWN;
ASM_REWRITE_TAC[
IN];
DOWN;
REWRITE_TAC[
HAS_SIZE_2_EXISTS2];
STRIP_TAC;
SUBGOAL_THEN` (x':real^3, y:real^3)
IN FF \/ (y,x')
IN FF ` MP_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_IN_E_IMP_IN_FF;
ASM_REWRITE_TAC[
local_fan];
LET_TAC;
ASM_REWRITE_TAC[
FAN;
graph; fan1; fan6; fan7; fan2;
IN_UNION];
CONJ_TAC;
EXISTS_TAC` x:real^3 # real^3 `;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (SUBST1_TAC o SYM);
FIRST_ASSUM ACCEPT_TAC;
ASM_REWRITE_TAC[];
DOWN THEN DOWN THEN PHA;
SPEC_TAC (`x':real^3 `,` x': real^3 `);
SPEC_TAC (`y:real^3 `,` y: real^3 `);
REWRITE_TAC[TAUT` a /\ b /\ c <=> (a/\b) /\ c `];
MATCH_MP_TAC (MESON[]`(! x y. Q x y ==> Q y x) /\
(! x y. Q x y /\ P x y ==> L x y ) /\ (! x y. L x y ==> L y x)
==> (! (x:real^3) (y:real^3). Q x y /\ (P x y \/ P y x) ==> L x y )`);
SIMP_TAC[
INSERT_COMM];
REPEAT STRIP_TAC;
SUBGOAL_THEN `~collinear {
vec 0, v, w:real^3}` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[
IN_INSERT;
IN_DIFF; DE_MORGAN_THM;
NOT_IN_EMPTY];
DOWN;
NHANH Planarity.aff_ge_eq_aff_gt_union_aff_ge;
SIMP_TAC[
UNION_OVER_INTER];
STRIP_TAC;
UNDISCH_TAC `y':real^3, y:real^3
IN FF `;
FIRST_ASSUM NHANH;
REWRITE_TAC[
wedge_in_fan_gt];
SUBGOAL_THEN`
local_fan (V,E,
FF)` MP_TAC;
ASM_REWRITE_TAC[
IN_UNION;
local_fan;
FAN; fan1; fan2; fan6; fan7;
graph];
LET_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC` x:real^3 # real^3 `;
ASM_REWRITE_TAC[];
STRIP_TAC;
STRIP_TAC;
ASSUME_TAC2 (SPEC`y': real^3 ` (GEN `x:real^3 `
Local_lemmas.LOCAL_FAN_IMP_IN_V));
SUBGOAL_THEN`
CARD (
EE (y':real^3) E) = 2 ` ASSUME_TAC;
MATCH_MP_TAC Local_lemmas.LOFA_CARD_EE_V_1;
ASM_SIMP_TAC[];
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN THEN DOWN THEN PHA;
REWRITE_TAC[ARITH_RULE` 2 > 1 `];
STRIP_TAC;
MP_TAC (REWRITE_RULE[
EMPTY_SUBSET;
INSERT_SUBSET;
IN_INSERT]
(ISPECL [` {y':real^3} `;` {
vec 0, y':real^3}`; `{y:real^3 }`]
(GEN_ALL Local_lemmas.AFF_GE_MONO_TRANS)));
SUBGOAL_THEN` ~ (y':real^3 =
vec 0 )` MP_TAC;
UNDISCH_TAC` y':real^3
IN V `;
UNDISCH_TAC` ~(
vec 0
IN (V:real^3 -> bool)) `;
MESON_TAC[];
SIMP_TAC[SET_RULE` ~( y' =
vec 0) ==> {
vec 0, y'}
DIFF {y'} = {
vec 0} `];
REWRITE_TAC[Local_lemmas.INSERT_UNION2;
UNION_EMPTY];
REPEAT STRIP_TAC;
MP_TAC (SPECL [`
vec 0:real^3 `;` y':real^3`;` y:real^3 `;
` (
azim_cycle (
EE y' E) (
vec 0) y' y) `] (GEN_ALL
AFF_GE_WEDGE_DISJOINTION));
STRIP_TAC;
SUBGOAL_THEN` aff_ge {
vec 0} {y:real^3, y'}
INTER aff_gt {
vec 0} {v, w} = {} ` MP_TAC;
REPLICATE_TAC 3 DOWN THEN PHA;
SET_TAC[];
SIMP_TAC[
UNION_EMPTY];
STRIP_TAC;
UNDISCH_TAC` !e1 e2.
(e1
IN E \/ e1
IN {{v:real^3} | v
IN V}) /\
(e2
IN E \/ e2
IN {{v} | v
IN V})
==> aff_ge {
vec 0} e1
INTER aff_ge {
vec 0} e2 =
aff_ge {
vec 0} (e1
INTER e2) `;
STRIP_TAC;
SUBGOAL_THEN` ({y, y'}
IN E \/ {y, y'}
IN {{v:real^3} | v
IN V}) /\
({v}
IN E \/ {v}
IN {{v} | v
IN V})` MP_TAC;
UNDISCH_TAC` (e2:real^3 -> bool)
IN E `;
ASM_SIMP_TAC[
IN_ELIM_THM];
STRIP_TAC;
DISJ2_TAC;
EXISTS_TAC` v:real^3 `;
ASM_REWRITE_TAC[];
FIRST_ASSUM NHANH;
SIMP_TAC[];
REMOVE_TAC;
SUBGOAL_THEN` ({y, y'}
IN E \/ {y, y'}
IN {{v:real^3} | v
IN V}) /\
({w}
IN E \/ {w}
IN {{v} | v
IN V})` MP_TAC;
UNDISCH_TAC` (e2:real^3 -> bool)
IN E `;
ASM_SIMP_TAC[
IN_ELIM_THM];
STRIP_TAC;
DISJ2_TAC;
EXISTS_TAC` w:real^3 `;
ASM_REWRITE_TAC[];
FIRST_ASSUM NHANH;
SIMP_TAC[];
REMOVE_TAC;
ASM_CASES_TAC` {y, y'}
INTER {v, w:real^3} = {} `;
DOWN;
NHANH (SET_RULE` S
INTER {a,b} = {} ==> S
INTER {a} = {} /\ S
INTER {b} = {}`);
SIMP_TAC[
UNION_IDEMPOT];
ASM_CASES_TAC` {y, y': real^3}
INTER {v} = {} \/
{y, y': real^3}
INTER {w} = {}`;
DOWN THEN DOWN;
SPEC_TAC (`w:real^3 `,` w:real^ 3 `);
SPEC_TAC (`v:real^3 `,` v:real^ 3 `);
MATCH_MP_TAC (MESON[]` (! x y. A x y ==> A y x) /\
(! x y. B x y ==> B y x ) /\
(! x y. A x y ==> M x ==> B x y)
==> (! x y. A x y ==> M x \/ M y ==> B x y ) `);
SIMP_TAC[
INSERT_COMM;
UNION_COMM];
PHA;
NHANH (SET_RULE` ~({y, y'}
INTER {v, w} = {}) /\ {y, y'}
INTER {v} = {}
==> {y, y'}
INTER {v, w} = {w} /\ {y, y'}
INTER {w} = {w}`);
SIMP_TAC[];
REPEAT STRIP_TAC;
REWRITE_TAC[
AFF_GE_EQ_AFFINE_HULL;
AFFINE_HULL_SING];
MATCH_MP_TAC (SET_RULE` x
IN S ==> {x}
UNION S = S `);
REWRITE_TAC[
IN_ELIM_THM;
HALFLINE];
EXISTS_TAC ` &0 `;
REWRITE_TAC[
REAL_LE_REFL];
VECTOR_ARITH_TAC;
DOWN THEN DOWN THEN PHA;
UNDISCH_TAC` ~ ( w = v:real^3)`;
PHA;
NHANH (SET_RULE `~(w = v) /\
~({y, y'}
INTER {v, w} = {}) /\
~({y, y'}
INTER {v} = {} \/ {y, y'}
INTER {w} = {})
==> {y,y'} = {v, w} `);
STRIP_TAC;
UNDISCH_TAC` aff_ge {
vec 0} {y, y'}
INTER aff_gt {
vec 0} {v:real^3, w} = {}`;
ASM_REWRITE_TAC[];
NHANH (SET_RULE` (A
UNION B)
INTER A = {} ==> A = {} `);
SUBGOAL_THEN`
DISJOINT {
vec 0} {v, w:real^3 }` MP_TAC;
UNDISCH_TAC` ~(
vec 0
IN (V:real^3 -> bool)) `;
UNDISCH_TAC` (v:real^3)
IN V `;
UNDISCH_TAC` (w:real^3)
IN V `;
REWRITE_TAC[
DISJOINT; Trigonometry2.INSERT_INTER_EMPTY;
IN_INSERT;
NOT_IN_EMPTY];
MESON_TAC[];
NHANH Planarity.AFF_GT_1_2;
SIMP_TAC[];
REPEAT STRIP_TAC;
DOWN;
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
NOT_IN_EMPTY];
DISCH_THEN (MP_TAC o (SPEC` (&1 / &2) % v + (&1 / &2 ) % (w:real^3)`));
REWRITE_TAC[
NOT_EXISTS_THM];
DISCH_THEN (MP_TAC o (SPECL [` &0 `;` &1 / &2`;` &1 / &2 `]));
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_LID; REAL_ARITH` &0 < &1 / &2 /\
&0 + &1 / &2 + &1 / &2 = &1`];
DOWN;
REWRITE_TAC[
IN_ELIM_THM];
STRIP_TAC;
SUBGOAL_THEN`
local_fan (V,E,
FF) ` MP_TAC;
ASM_REWRITE_TAC[
local_fan;
FAN; fan1; fan2; fan6; fan7;
graph];
LET_TAC;
ASM_REWRITE_TAC[
IN_UNION];
EXISTS_TAC` x: real^3 # real^3 `;
ASM_REWRITE_TAC[];
NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`v': real^3`));
UNDISCH_TAC` !x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E`;
DISCH_THEN (ASSUME_TAC2 o (SPEC `v',
rho_node1 FF v' `));
SUBGOAL_THEN` ~((v:real^3 ) =
vec 0)/\ ~( (w:real^3) =
vec 0) ` MP_TAC;
UNDISCH_TAC` v:real^3
IN V `;
UNDISCH_TAC` w:real^3
IN V `;
UNDISCH_TAC` ~(
vec 0
IN (V:real^3 -> bool)) `;
MESON_TAC[];
NHANH Wrgcvdr_cizmrrh.AFF_GE_TO_AFF_GT2_GE1;
DOWN;
REWRITE_TAC[
wedge_in_fan_gt];
ASSUME_TAC2 (
SPEC` v':real^3 ` (GEN `v:real^3 ` Local_lemmas.LOFA_CARD_EE_V_1));
ASM_REWRITE_TAC[ARITH_RULE` 2 > 1 `];
MP_TAC (SPECL [`
vec 0: real^3 `;` v': real^3 `; `
rho_node1 FF v' `;
`(
azim_cycle (
EE v' E) (
vec 0) v' (
rho_node1 FF v')) `]
(GEN_ALL
EDGE_NOT_INTER_WITH_WEDGE));
MP_TAC (ISPECL [`
vec 0:real^3 `;` v':real^3`] (GEN_ALL
AFF_GE11_SUB_AFF2));
PHA;
NHANH (SET_RULE` a
SUBSET B /\ B
INTER S = {} /\ l ==> a
INTER S = {} `);
STRIP_TAC;
ASM_REWRITE_TAC[
UNION_OVER_INTER];
SUBGOAL_THEN` aff_ge {
vec 0} {v'}
INTER aff_gt {
vec 0} {v, w:real^3} = {}` ASSUME_TAC;
DOWN;
MATCH_MP_TAC (SET_RULE` a
SUBSET b ==> x
INTER b = {} ==> x
INTER a = {} `);
FIRST_X_ASSUM ACCEPT_TAC;
ASM_REWRITE_TAC[
UNION_EMPTY];
UNDISCH_TAC` !e1 e2.
(e1
IN E \/ e1
IN {{v:real^3} | v
IN V}) /\
(e2
IN E \/ e2
IN {{v} | v
IN V})
==> aff_ge {
vec 0} e1
INTER aff_ge {
vec 0} e2 =
aff_ge {
vec 0} (e1
INTER e2)`;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [` {v':real^3} `;` {v:real^3}`]));
ANTS_TAC;
ASM_REWRITE_TAC[
IN_ELIM_THM];
UNDISCH_TAC` v:real^3
IN V `;
UNDISCH_TAC` v':real^3
IN V `;
MESON_TAC[];
FIRST_ASSUM (MP_TAC o (SPECL [` {v':real^3} `;` {w:real^3}`]));
ANTS_TAC;
ASM_REWRITE_TAC[
IN_ELIM_THM];
UNDISCH_TAC` w:real^3
IN V `;
UNDISCH_TAC` v':real^3
IN V `;
MESON_TAC[];
SIMP_TAC[];
REPEAT STRIP_TAC;
ASM_CASES_TAC` {v'}
INTER {v, w} = {v':real^3} `;
DOWN;
SIMP_TAC[];
UNDISCH_TAC` ~( w = (v:real^3) )`;
PHA;
NHANH (SET_RULE`{v'}
INTER {v, w} = {v'}
==> v = v' \/ w = v' `);
NHANH (SET_RULE` ~( a = b ) ==> {a}
INTER {b} = {} `);
STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN THEN DOWN THEN PHA;
SIMP_TAC[
INTER_IDEMPOT;
INTER_COMM;
AFF_GE_EQ_AFFINE_HULL;
AFFINE_HULL_SING];
STRIP_TAC;
MP_TAC (ISPECL [` {
vec 0:real^3 }`;` {v': real^3 }`]
AFFINE_HULL_SUBSET_AFF_GE);
ANTS_TAC;
UNDISCH_TAC` ~((v':real^3) =
vec 0) `;
REWRITE_TAC[
DISJOINT];
SET_TAC[];
REWRITE_TAC[
AFFINE_HULL_SING];
SET_TAC[];
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_REWRITE_TAC[];
DOWN THEN DOWN THEN PHA;
SIMP_TAC[
INTER_IDEMPOT;
INTER_COMM;
AFF_GE_EQ_AFFINE_HULL;
AFFINE_HULL_SING];
MP_TAC (ISPECL [` {
vec 0:real^3 }`;` {v': real^3 }`]
AFFINE_HULL_SUBSET_AFF_GE);
ANTS_TAC;
UNDISCH_TAC` ~((v':real^3) =
vec 0) `;
REWRITE_TAC[
DISJOINT];
SET_TAC[];
REWRITE_TAC[
AFFINE_HULL_SING];
SET_TAC[];
DOWN;
NHANH (SET_RULE` ~({v'}
INTER {v, w} = {v'})
==> {v'}
INTER {v} = {} /\ {v'}
INTER {w} = {} /\ {v, w}
INTER {v'} = {}`);
SIMP_TAC[
UNION_IDEMPOT;
INTER_COMM]]);;
let FACE_MAP_ADD_SET2_EQ = prove_by_refinement
(` (x,y)
IN darts_of_hyp ( E
UNION {{a,b}}) V /\
~( y = a) /\ ~ ( y = b ) /\
FAN (
vec 0, V, E) /\
FAN (
vec 0, V, E
UNION {{a,b}} )
==> (
face_map (hypermap (
HYP (
vec 0, V, (E
UNION {{a,b}}))))) (x,y) =
(
face_map (hypermap (
HYP (
vec 0, V, E)))) (x,y) `,
[NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` (x,y)
IN darts_of_hyp ( E
UNION {{a,b:real^3}}) V ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[
darts_of_hyp;
IN_UNION];
DISCH_TAC;
SUBGOAL_THEN` (x,y)
IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;
REWRITE_TAC[
darts_of_hyp;
IN_UNION];
DOWN THEN STRIP_TAC;
DISJ1_TAC;
DOWN;
REWRITE_TAC[
ord_pairs;
IN_ELIM_THM;
IN_UNION];
STRIP_TAC;
EXISTS_TAC` a': real^3 `;
EXISTS_TAC` b': real^3 `;
ASM_REWRITE_TAC[];
DOWN THEN DOWN;
REWRITE_TAC[
IN_SING;
PAIR_EQ; Collect_geom.PAIR_EQ_EXPAND];
REPEAT STRIP_TAC;
UNDISCH_TAC` ~( y = b:real^3 ) `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~( y = a:real^3) `;
ASM_REWRITE_TAC[];
DOWN;
REWRITE_TAC[
self_pairs;
IN_ELIM_THM];
STRIP_TAC;
DISJ2_TAC;
EXISTS_TAC` v:real^3 `;
ASM_REWRITE_TAC[];
DOWN THEN DOWN;
SIMP_TAC[
EE;
IN_UNION];
SET_TAC[];
ASM_SIMP_TAC[
ff_of_hyp];
SUBGOAL_THEN` (
EE y (E
UNION {{a, b}})) = (
EE (y:real^3) E)` SUBST1_TAC;
REWRITE_TAC[
EE;
EXTENSION;
IN_ELIM_THM;
IN_UNION];
GEN_TAC;
MATCH_MP_TAC (TAUT` (a ==> b) ==> ( b \/ a <=> b )`);
REWRITE_TAC[
IN_SING; Collect_geom.PAIR_EQ_EXPAND];
ASM_REWRITE_TAC[];
PHA]);;
let LOCAL_FACE_MAP_RHO_NODE1 = prove_by_refinement
(`
local_fan (V,E,
FF) /\
(x,y)
IN FF
==>
face_map ( hypermap (
HYP (
vec 0,V,E))) (x,y) =
(
rho_node1 FF x,
rho_node1 FF y ) `,
[NHANH Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
SIMP_TAC[];
NHANH Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
STRIP_TAC;
SUBGOAL_THEN` x,y
IN darts_of_hyp E (V:real^3 -> bool) ` MP_TAC;
ASM_REWRITE_TAC[
IN_UNION];
SIMP_TAC[
ff_of_hyp];
ASSUME_TAC2 (SPECL [` x:real^3 `;` y:real^3 `] (
GENL [`v: real^3 `;` w:real^3 `] Local_lemmas.DETER_RHO_NODE));
ASM_REWRITE_TAC[
PAIR_EQ];
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_IN_V;
DOWN THEN STRIP_TAC;
ASSUME_TAC2 (SPECL [`x:real^3 `;` y:real^3 `] (
GENL [`vv: real^ 3 `;` v: real^3 `] Local_lemmas.LOFA_IMP_EE_TWO_ELMS));
ASM_REWRITE_TAC[
ivs_azim_cycle; SET_RULE` ~( x
INSERT S = {} )`];
ABBREV_TAC` tt = (@x'. x'
IN {
rho_node1 FF y, x} /\
azim_cycle {
rho_node1 FF y, x} (
vec 0) y x' = x)` ;
SUBGOAL_THEN`tt
IN {
rho_node1 FF y, x} /\
azim_cycle {
rho_node1 FF y, x} (
vec 0) y tt = x` MP_TAC;
EXPAND_TAC "tt";
let LOFA_HYP_UNION_CARD_GT2 = prove_by_refinement
(`(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==> 2 <
CARD fv `,
[NHANH
PROVE_SLICING_FAN;
NHANH Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
STRIP_TAC;
SUBGOAL_THEN` ~(
rho_node1 FF v = w) ` ASSUME_TAC;
USE_FIRST ` !x. x
IN V ==> x,
rho_node1 FF x
IN FF ` (ASSUME_TAC2 o (SPEC`v: real^3 `));
DOWN;
USE_FIRST` !x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E ` NHANH;
REWRITE_TAC[
wedge_in_fan_gt];
ASSUME_TAC2 Local_lemmas.LOFA_CARD_EE_V_1;
ASM_REWRITE_TAC[ARITH_RULE` 2 > 1 `];
MP_TAC (ISPECL [` {v:real^3} `; ` {
vec 0, v:real^3} `;` {
rho_node1 FF v} `]
(GEN_ALL Local_lemmas.AFF_GE_MONO_TRANS));
ANTS_TAC;
SIMP_TAC[
SUBSET;
IN_SING;
IN_INSERT];
SUBGOAL_THEN`
FAN (
vec 0,V,E
UNION {{v:real^3, w}}) ` MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
REWRITE_TAC[
FAN; fan1; fan2];
STRIP_TAC;
SUBGOAL_THEN ` ~( v:real^3 =
vec 0) ` MP_TAC;
ASM_MESON_TAC[];
SIMP_TAC[SET_RULE` ~( a = b) ==> {b,a}
DIFF {a} = {b} `; SET_RULE` {a}
UNION {b} = {b,a}`];
REPEAT STRIP_TAC;
MP_TAC (SPECL [`
vec 0: real^3 `;` v: real^3 `;`
rho_node1 FF v `;
` (
azim_cycle (
EE v E) (
vec 0) v (
rho_node1 FF v)) ` ]
(GEN_ALL
AFF_GE_WEDGE_DISJOINTION));
ABBREV_TAC` tv =
azim_cycle (
EE v E) (
vec 0) v (
rho_node1 FF v) `;
STRIP_TAC;
UNDISCH_TAC` aff_gt {
vec 0} {v, w}
SUBSET wedge (
vec 0) v (
rho_node1 FF v) tv `;
UNDISCH_TAC` aff_ge {
vec 0, v} {
rho_node1 FF v}
INTER
wedge (
vec 0) v (
rho_node1 FF v) tv =
{} `;
MP_TAC (ISPECL [` {
vec 0: real^ 3} `; ` {v, w:real^3} `]
AFF_GT_SUBSET_AFF_GE);
ASM_REWRITE_TAC[];
MATCH_MP_TAC (
SET_RULE` ge12
SUBSET ge21 /\ ~( gt = {} ) ==>
gt
SUBSET ge12 ==> ge21
INTER we = {} ==> ~( gt
SUBSET we ) `);
UNDISCH_TAC` aff_ge {
vec 0} {v,
rho_node1 FF v}
SUBSET
aff_ge {
vec 0, v} {
rho_node1 FF v}`;
ASM_SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN`
DISJOINT {
vec 0} {v, w:real^3}` MP_TAC;
REWRITE_TAC[SET_RULE`
DISJOINT {a} {x,y} <=> ~( x = a) /\ ~( y = a) `];
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~(
vec 0:real^3
IN V ) `;
UNDISCH_TAC` w:real^3
IN V `;
MESON_TAC[];
SIMP_TAC[Planarity.AFF_GT_1_2;
EXTENSION;
IN_ELIM_THM;
NOT_IN_EMPTY];
REPEAT STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC` &1 / &2 % v + &1 / &2 % (w:real^3) `));
REWRITE_TAC[];
EXISTS_TAC` &0 `;
EXISTS_TAC` &1 / &2 `;
EXISTS_TAC` &1 / &2 `;
REWRITE_TAC[REAL_ARITH` &0 < &1 / &2 /\
&0 < &1 / &2 /\
&0 + &1 / &2 + &1 / &2 = &1 `];
REWRITE_TAC[VECTOR_ARITH` &0 % v + x = x `];
ASM_CASES_TAC`
rho_node1 FF (
rho_node1 FF v) = v `;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_V;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC `v:real^3 `));
REPLICATE_TAC 3 DOWN;
NHANH (GEN_ALL Local_lemmas.ORD2_ORBIT_MAP);
SIMP_TAC[];
REPEAT STRIP_TAC;
UNDISCH_TAC` w
IN (V:real^3 -> bool) `;
EXPAND_TAC "V";
let AZIM_POS_IMP_CYCLIC_SET = prove_by_refinement
(` &0 <
azim v0 v1 w1 w2 ==>
cyclic_set {w1, w2} v0 v1 `,
[REWRITE_TAC[
cyclic_set];
STRIP_TAC;
CONJ_TAC;
STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
REWRITE_TAC[AZ_REFL11];
REAL_ARITH_TAC;
REWRITE_TAC[Geomdetail.FINITE6];
ASM_CASES_TAC` v0 = v1:real^3 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
REWRITE_TAC[AZ_REFL11; REAL_ARITH` ~( a < a ) `];
ASM_CASES_TAC` w1
IN affine hull {v0, v1:real^3}`;
DOWN;
NHANH (REWRITE_RULE[CONTRAPOS_THM; aff] Fan.th3c);
STRIP_TAC;
UNDISCH_TAC` &0 <
azim v0 v1 w1 w2 `;
ASM_SIMP_TAC[
AZIM_DEGENERATE; REAL_ARITH` ~( a < a ) `];
ASM_CASES_TAC` w2
IN affine hull {v0, v1:real^3}`;
DOWN;
NHANH (REWRITE_RULE[CONTRAPOS_THM; aff] Fan.th3c);
STRIP_TAC;
UNDISCH_TAC` &0 <
azim v0 v1 w1 w2 `;
ASM_SIMP_TAC[
AZIM_DEGENERATE; REAL_ARITH` ~( a < a ) `];
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
NOT_IN_EMPTY;
IN_INSERT;
IN_INTER];
CONJ_TAC;
REWRITE_TAC[SET_RULE` ( {w1, w2} p /\ {w1, w2} q /\ L ==> p = q ) <=>
( p = w1 /\ q = w2 /\ L ==> p = q ) /\
(p = w2 /\ q = w1 /\ L ==> p = q )`];
MATCH_MP_TAC (
MESON[]` ( ! h. w1 = w2 + h % (v0 - v1) ==> w1 = w2 ) /\
(! h. w2 = w1 + h % (v0 - v1) ==> w1 = w2 + ( -- h) % ( v0 - v1 ))
==>
!p q h.
(p = w1 /\ q = w2 /\ p = q + h % (v0 - v1) ==> p = q) /\
(p = w2 /\ q = w1 /\ p = q + h % (v0 - v1) ==> p = q)`);
CONJ_TAC;
REPEAT STRIP_TAC;
SUBGOAL_THEN` w1
IN aff_ge {v0, v1} {w2:real^3} ` MP_TAC;
DOWN;
ASSUME_TAC2 (ISPECL [` v0:real^3 `;` v1:real^3 `; `w2:real^3 `]
COLLINEAR_3_AFFINE_HULL);
UNDISCH_TAC` ~(w2
IN affine hull {v0, v1: real^3})`;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
NHANH Fan.th3a;
NHANH Collect_geom.simp_def_ge;
SIMP_TAC[
IN_ELIM_THM];
REPEAT STRIP_TAC;
EXISTS_TAC` h:real` ;
EXISTS_TAC` -- h:real` ;
EXISTS_TAC` &1 `;
REWRITE_TAC[REAL_ARITH` a + -- a + b = b /\ &0 <= &1 `];
VECTOR_ARITH_TAC;
ASSUME_TAC2 (ISPECL [` v1:real^3 `;` v0: real^3 `; ` w2:real ^3 `] (GSYM
COLLINEAR_3_AFFINE_HULL));
UNDISCH_TAC ` ~(w2
IN affine hull {v0, v1:real^3})`;
DOWN;
ASM_SIMP_TAC[
INSERT_COMM];
SIMP_TAC[ GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2];
FIRST_X_ASSUM (SUBST_ALL_TAC o SYM);
REPEAT STRIP_TAC;
UNDISCH_TAC` &0 <
azim v0 v1 w1 w2 `;
DOWN;
ASM_SIMP_TAC[Local_lemmas.AZIM_EQ_0_SYM2; REAL_ARITH` ~( a < a ) `];
GEN_TAC;
VECTOR_ARITH_TAC;
GEN_TAC;
REWRITE_TAC[DE_MORGAN_THM];
ASM_MESON_TAC[]]);;
let FACE_MAP_AT_TURNING_DART = prove_by_refinement
(` (
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
(x,v)
IN FF
==>
face_map (hypermap (
HYP (
vec 0,V,E
UNION {{v, w}}))) (x,v)
= (v, w)`,
[NHANH
PROVE_SLICING_FAN;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
SIMP_TAC[];
STRIP_TAC;
ASSUME_TAC2 (SPECL [`x:real^3 `;` v:real^3 `] (
GENL [`x:real^3 `;` y:real^3 `] Local_lemmas.LOCAL_FAN_IN_FF_IN_ORD_PAIRS2));
DOWN THEN NHANH (ISPEC `{{v, w:real^3}} ` (GEN` S: (A -> bool) -> bool `
IN_DARTS_EXTENSION));
SIMP_TAC[
ff_of_hyp;
PAIR_EQ];
STRIP_TAC;
ASSUME_TAC2 (SET_RULE` {x,v:real^3}
IN E ==> {x,v}
IN E
UNION {{v,w}} `);
DOWN;
PAT_ONCE_REWRITE_TAC`\x. x
IN Y ==> L ` [
INSERT_COMM];
UNDISCH_TAC`
FAN (
vec 0,V,E
UNION {{v, w:real^3}})`;
PHA;
NHANH Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN;
SIMP_TAC[];
NHANH (GSYM Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE);
STRIP_TAC;
MATCH_MP_TAC (REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `] Wrgcvdr_cizmrrh.SIG_AND_INVERSE1_SIG);
ASM_REWRITE_TAC[
IN_UNION;
IN_SING];
MATCH_MP_TAC Fan.UNIQUE_SIGMA_FAN;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (SPECL [` x:real^3 `;` v:real^3 `]
(GENL [` v:real^3 `;` w:real^3 `] Local_lemmas.DETER_RHO_NODE));
SUBGOAL_THEN` x:real^3
IN V /\ v
IN V ` MP_TAC;
MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2 (SPEC` x:real^3 ` (GEN `vv:real^3 ` Local_lemmas.LOFA_IMP_EE_TWO_ELMS));
ASM_REWRITE_TAC[
EE_UNION;
EE_SING_SING;
IN_UNION;
IN_SING;
IN_INSERT];
SUBGOAL_THEN` ~( x = w:real^3 ) ` MP_TAC;
STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
UNDISCH_TAC` w:real^3
IN V `;
PHA;
FIRST_ASSUM NHANH;
STRIP_TAC;
DOWN THEN PHA;
MATCH_MP_TAC
CROSS_PAIR_NOT_IN_FF;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[
INSERT_COMM];
FIRST_ASSUM ACCEPT_TAC;
SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
DOWN THEN SET_TAC[];
REPEAT STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
UNDISCH_TAC` v:real^3
IN V `;
FIRST_ASSUM NHANH;
USE_FIRST` !x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E`
NHANH;
STRIP_TAC;
DOWN;
ASSUME_TAC2 Local_lemmas.LOFA_CARD_EE_V_1;
DOWN THEN SIMP_TAC[
wedge_in_fan_gt];
REWRITE_TAC[ARITH_RULE` 2 > 1 `];
ASSUME_TAC2 (SPECL [` x:real^3 `]
(GENL [` vv:real^3 `] Local_lemmas.LOFA_IMP_EE_TWO_ELMS));
ASM_REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];
SUBGOAL_THEN` &1 / &2 % v + &1 / &2 % w
IN aff_gt {
vec 0} {v, w:real^3}` ASSUME_TAC;
SUBGOAL_THEN`
DISJOINT {
vec 0} {v, w:real^3} ` MP_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3`));
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3`));
DOWN THEN DOWN THEN PHA;
REWRITE_TAC[
DISJOINT;
EXTENSION;
NOT_IN_EMPTY;
IN_INTER;
IN_INSERT];
MESON_TAC[];
SIMP_TAC[Planarity.AFF_GT_1_2;
IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` &0 `;
EXISTS_TAC` &1 / &2 `;
EXISTS_TAC` &1 / &2 `;
REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_ADD_LID];
REAL_ARITH_TAC;
ABBREV_TAC` vw: real^3 = &1 / &2 % v + &1 / &2 % w `;
REWRITE_TAC[
SUBSET];
REPEAT STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` vw: real^3 `));
DOWN;
REWRITE_TAC[
wedge;
IN_ELIM_THM];
SUBGOAL_THEN` vw
IN aff_gt {
vec 0, v} {w:real^3} ` MP_TAC;
SUBGOAL_THEN`
DISJOINT {
vec 0, v} {w:real^3} ` MP_TAC;
ASM_REWRITE_TAC[
DISJOINT;
EXTENSION;
IN_INSERT;
IN_INTER;
NOT_IN_EMPTY];
UNDISCH_TAC` ~( v = w:real^3 ) `;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
DOWN;
MESON_TAC[];
SIMP_TAC[
AFF_GT_2_1;
IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` &0 `;
EXISTS_TAC` &1 / &2 `;
EXISTS_TAC` &1 / &2 `;
EXPAND_TAC "vw";
let FACE_MAP_SLICING_HYP_TRANS_POINT = prove_by_refinement
( `(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E))
==>
face_map (hypermap (
HYP (
vec 0,V,E
UNION {{v, w}}))) (v,w) = w,
rho_node1 FF w `,
[NHANH
PROVE_SLICING_FAN;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
SIMP_TAC[];
STRIP_TAC;
REPLICATE_TAC 4 (DOWN THEN REMOVE_TAC);
REWRITE_TAC[
ff_of_hyp];
SUBGOAL_THEN` v,w
IN darts_of_hyp (E
UNION {{v, w:real^3}}) V ` MP_TAC;
MATCH_MP_TAC (ONCE_REWRITE_RULE[
UNION_COMM]
IN_DARTS_EXTENSION);
REWRITE_TAC[
IN_SING];
SIMP_TAC[
PAIR_EQ];
STRIP_TAC;
SUBGOAL_THEN` {v,w:real^3}
IN E
UNION {{v, w}} ` MP_TAC;
REWRITE_TAC[
IN_UNION;
IN_SING];
UNDISCH_TAC`
FAN (
vec 0,V,E
UNION {{v, w:real^3}})`;
PHA;
NHANH (ONCE_REWRITE_RULE[
INSERT_COMM] Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN);
SIMP_TAC[];
STRIP_TAC;
MATCH_MP_TAC (REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `] Wrgcvdr_cizmrrh.SIG_AND_INVERSE1_SIG);
ASSUME_TAC2 (SPEC `w:real^3 `
LOCAL_RHO_NODE_PAIR_E);
ASM_REWRITE_TAC[
IN_UNION];
ASSUME_TAC2 Local_lemmas.LOFA_IMAGE_RHO_NODE_IDE;
DOWN;
REWRITE_TAC[
IMAGE];
STRIP_TAC;
UNDISCH_TAC` w:real^3
IN V `;
EXPAND_TAC "V";
let FACE_MAP_AT_TURNING_DART1 = prove(
` (
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
x,w
IN FF
==>
face_map (hypermap (
HYP (
vec 0,V,E
UNION {{v, w}}))) (x,w) = w, v`,
let DETERMINE_FV = prove_by_refinement
(`(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==> fv = (w,v)
INSERT
{ (
ITER n (
rho_node1 FF) v,
ITER (n + 1) (
rho_node1 FF) v) | n |
! m. m < n + 1 ==> ~(
ITER m (
rho_node1 FF) v = w)} `,
let TWO_EQ_SYSTEM_THM = prove_by_refinement (
`
FAN (
vec 0,V,E) /\
graph E /\
UNIONS E
SUBSET V ==>
dart_of_fan (V,E),
res (
e_fan_pair (V,E)) (
dart1_of_fan (V,E)),
res (
n_fan_pair (V,E)) (
dart1_of_fan (V,E)),
res (
f_fan_pair (V,E)) (
dart1_of_fan (V,E)) =
darts_of_hyp E V,
ee_of_hyp (
vec 0,V,E),
nn_of_hyp (
vec 0,V,E),
ff_of_hyp (
vec 0,V,E)`,
[REWRITE_TAC[
PAIR_EQ];
STRIP_TAC;
SUBGOAL_THEN`
dart_of_fan (V,E) =
darts_of_hyp E V ` MP_TAC;
REWRITE_TAC[
dart_of_fan;
darts_of_hyp;
ord_pairs;
self_pairs];
DOWN;
NHANH (REWRITE_RULE[
RIGHT_FORALL_IMP_THM] (GEN `v: A` Wrgcvdr_cizmrrh.UNI_E_IMP_EE_EQ_SET_OF_EDGE));
SIMP_TAC[
EXTENSION;
IN_UNION];
MESON_TAC[];
SIMP_TAC[];
STRIP_TAC;
REWRITE_TAC[res;
FUN_EQ_THM;
ee_of_hyp2];
CONJ_TAC;
GEN_TAC;
REWRITE_TAC[
dart1_of_fan;
darts_of_hyp;
IN_UNION;
ord_pairs];
ASM_CASES_TAC` x
IN {a,b | {a, b:real^3}
IN E}`;
ASM_REWRITE_TAC[];
PAT_ONCE_REWRITE_TAC`\p. P p = PP `[GSYM
PAIR];
PURE_ONCE_REWRITE_TAC[
e_fan_pair];
REWRITE_TAC[];
ASM_REWRITE_TAC[
self_pairs;
IN_ELIM_THM];
MESON_TAC[
PAIR_EQ;
FST;
SND];
CONJ_TAC;
REWRITE_TAC[
nn_of_hyp3;
dart1_of_fan];
GEN_TAC;
ASM_CASES_TAC` x
IN {v,w | {v:real^3, w}
IN E}`;
ASM_REWRITE_TAC[
darts_of_hyp;
ord_pairs;
self_pairs;
IN_UNION;
EE];
DOWN;
REWRITE_TAC[
IN_ELIM_THM];
STRIP_TAC;
ASM_REWRITE_TAC[
n_fan_pair];
DOWN_TAC;
REWRITE_TAC[
graph];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` {v, w:real^3}`));
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[
IN];
REWRITE_TAC[
SET2_HAS_SIZE2];
STRIP_TAC;
SUBGOAL_THEN` ~( {w | {v, w:real^3}
IN E} = {} ) ` MP_TAC;
UNDISCH_TAC` {v:real^3,w}
IN E `;
SET_TAC[];
SIMP_TAC[];
NHANH (MESON[
PAIR_EQ]` (?v'. v'
IN V /\ {w | {v', w}
IN E} = {} /\ v,w = v',v')
==> {w | {v, w}
IN E} = {} `);
SIMP_TAC[
PAIR_EQ];
STRIP_TAC;
UNDISCH_TAC` {v, w:real^3}
IN E `;
UNDISCH_TAC`
FAN (
vec 0, V:real^3 -> bool, E) `;
PHA;
NHANH Wrgcvdr_cizmrrh.ITER_AZIM_CYCLE_EQ_ITER_SIGMA;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` w:real^3 `));
ANTS_TAC;
REWRITE_TAC[
EE;
IN_ELIM_THM];
FIRST_ASSUM ACCEPT_TAC;
DISCH_THEN (MP_TAC o (SPEC` 1 `));
SIMP_TAC[
ITER12;
EE];
ASM_REWRITE_TAC[
darts_of_hyp;
IN_UNION; TAUT`~( a \/ b) \/ b <=> ~ a \/ b`];
ASM_REWRITE_TAC[
ord_pairs];
(* ------------------ *)
GEN_TAC;
REWRITE_TAC[
dart1_of_fan;
f_fan_pair; Wrgcvdr_cizmrrh.ff_of_hyp3;
f_fan_pair];
ASM_CASES_TAC` (x:real^3#real^3)
IN {v,w | {v, w}
IN E}`;
ASM_REWRITE_TAC[
darts_of_hyp;
IN_UNION; TAUT` ~(a \/ b) \/ b <=> ~ a \/ b `;
ord_pairs];
DOWN_TAC;
REWRITE_TAC[
graph;
IN_ELIM_THM];
STRIP_TAC;
SUBGOAL_THEN` ~ ( x
IN self_pairs E (V:real^3 -> bool))` MP_TAC;
REWRITE_TAC[
self_pairs;
IN_ELIM_THM];
DOWN THEN DOWN THEN PHA;
REWRITE_TAC[
IN];
FIRST_X_ASSUM NHANH;
SIMP_TAC[
SET2_HAS_SIZE2;
PAIR_EQ];
MESON_TAC[];
ASM_SIMP_TAC[
f_fan_pair;
PAIR_EQ];
STRIP_TAC;
UNDISCH_TAC` {v, w:real^3}
IN E `;
UNDISCH_TAC`
FAN (
vec 0, V:real^3 -> bool, E) `;
ONCE_REWRITE_TAC[
INSERT_COMM];
PHA;
NHANH Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN;
NHANH Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN;
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[
darts_of_hyp;
IN_UNION; TAUT` ~( a \/ b) \/ b <=> ~ a \/ b `];
ASM_REWRITE_TAC[
ord_pairs]]);;
let HAFL_CIRCLE_FORM_LOCAL_FAN = prove_by_refinement
(`(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==>
local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv, fv) `,
[NHANH
PROVE_SLICING_FAN;
STRIP_TAC;
SUBGOAL_THEN` (v,
rho_node1 FF v)
IN darts_of_hyp (E
UNION {{v,w}}) V` ASSUME_TAC;
REWRITE_TAC[
darts_of_hyp];
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
DOWN;
UNDISCH_TAC`
local_fan (V,E,
FF) `;
PHA;
NHANH Local_lemmas.LOCAL_FAN_IN_FF_IN_ORD_PAIRS2;
REWRITE_TAC[
IN_ELIM_THM;
IN_UNION;
ord_pairs];
STRIP_TAC;
DISJ1_TAC;
EXISTS_TAC` v:real^3 `;
EXISTS_TAC`
rho_node1 FF v `;
ASM_REWRITE_TAC[];
MP_TAC
LOFA_HYP_UNION_CARD_GT2;
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN`
simple_hypermap (hypermap (
HYP (
vec 0,
v_prime V fv,
e_prime (E
UNION {{v, w}} ) fv)))` MP_TAC;
REWRITE_TAC[
simple_hypermap];
SUBGOAL_THEN`
FAN (
vec 0:real^3,
v_prime (V:real^3 -> bool) fv,
e_prime (E
UNION {{v,w}} ) fv) ` MP_TAC;
MATCH_MP_TAC Wrgcvdr_cizmrrh.IMP_FAN_V_PRIME_E_PRIME;
ASM_REWRITE_TAC[];
EXISTS_TAC` (v,
rho_node1 FF v) `;
ASM_REWRITE_TAC[];
UNDISCH_TAC `
FAN (
vec 0, V:real^3 -> bool, E
UNION {{v, w}})`;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
ASM_SIMP_TAC[];
SWITCH_TAC` HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w: real^3}})) `;
SWITCH_TAC` fv = face HS (v,
rho_node1 FF v) `;
STRIP_TAC;
SUBGOAL_THEN` 1 <
CARD (fv:real^3 # real^3 -> bool) ` MP_TAC;
ASM_ARITH_TAC;
SUBGOAL_THEN` fv = face (hypermap (
HYP (
vec 0,V,(E
UNION {{v,w:real^3}})))) (v,
rho_node1 FF v)` MP_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN`
FAN (
vec 0, V, E
UNION {{v,w:real^3}}) ` MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
PHA;
NHANH Lvducxu.DARTS_E_PRIME_GT1_SWITCH;
STRIP_TAC;
UNDISCH_TAC`
FAN (
vec 0,
v_prime V fv,
e_prime (E
UNION {{v:real^3, w}}) fv) `;
NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
SIMP_TAC[];
STRIP_TAC;
SWITCH_TAC` fv =
face (hypermap (
HYP (
vec 0,V,E
UNION {{v, w}}))) (v,
rho_node1 FF v)`;
ASM_REWRITE_TAC[];
REWRITE_TAC[
IN_UNION];
GEN_TAC THEN STRIP_TAC;
DOWN;
ASSUME_TAC2
LOCAL_FAN_SIMPLE_HYP;
MP_TAC
DETERMINE_FV;
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[
IN_ELIM_THM;
IN_INSERT];
FIRST_X_ASSUM (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
MP_TAC (SPECL [`E
UNION {{v,w:real^3 }} `; ` fv: real^3 # real^3 -> bool `;` v,
rho_node1 FF v`;`
vec 0: real^3 `] (
GENL [`E:(real^3 -> bool) -> bool `;` FF: real^3 # real^3 -> bool`; `x:real^3 # real^3`;`v:real^3`] Lvducxu.LOCALIZE_PRESERVE_FACE));
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` v,
rho_node1 FF v
IN darts_of_hyp (E
UNION {{v, w}}) V`;
UNDISCH_TAC`
FAN (
vec 0,V,E
UNION {{v, w:real^3}})`;
NHANH Lvducxu.FAN_DART_DARTS;
ASM_SIMP_TAC[];
STRIP_TAC;
DISCH_TAC;
SUBGOAL_THEN` x
IN face
(hypermap (
HYP (
vec 0,
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv)))
(v,
rho_node1 FF v) ` MP_TAC;
UNDISCH_TAC` fv =
face
(hypermap (
HYP (
vec 0,
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv)))
(v,
rho_node1 FF v) `;
DISCH_THEN (SUBST1_TAC o SYM);
EXPAND_TAC "fv";
let HAFL_CIRCLE_FORM_LOCAL_FAN2 = prove_by_refinement
(` (
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==>
local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) /\
local_fan (
v_prime V fw,
e_prime (E
UNION {{w, v}}) fw,fw) `,
let LOCAL_FAN_RHO_NODE_IVS = prove_by_refinement (
`
local_fan (V,E,
FF) /\ v
IN V
==>
rho_node1 FF (
ivs_rho_node1 FF v ) = v `,
[NHANH Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
STRIP_TAC;
DOWN;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
REWRITE_TAC[GSYM
ITER];
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_FINITE_V;
DOWN THEN DOWN THEN PHA;
REWRITE_TAC[SET_RULE` a
IN X <=> {a}
SUBSET X `];
NHANH
CARD_SUBSET;
STRIP_TAC;
DOWN;
SUBST1_TAC (ISPEC`v:real^3` Trigonometry2.CARD_SING);
NHANH (ARITH_RULE` 1 <= a ==> SUC (a - 1) = a`);
SIMP_TAC[];
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID;
FIRST_X_ASSUM MATCH_MP_TAC;
DOWN_TAC;
SIMP_TAC[
INSERT_SUBSET]]);;
let POINT_PRESENTED_IN_RHOND1 = prove(
`
local_fan (V,E,
FF) /\ v
IN V /\ w
IN V ==> ? n. n <
CARD V /\
ITER n (
rho_node1 FF) v = w /\ (! m. m < n ==> ~(
ITER m (
rho_node1 FF) v = w )) `,
STRIP_TAC THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_LT_CARD_SET_V THEN
UNDISCH_TAC ` w:real^3
IN V ` THEN EXPAND_TAC "V" THEN
REWRITE_TAC[
IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23 THEN GEN_TAC THEN
STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o (SPECL [`m:num `;` n:num`])) THEN PHA
THEN PHA THEN ANTS_TAC THENL [ASM_REWRITE_TAC[]; SIMP_TAC[]]);;
let POINTS_IN_HAFL_CIRCLE = prove_by_refinement
(` (
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==>
v_prime V fv = {
ITER n (
rho_node1 FF) v| n | ! m . m < n ==> ~(
ITER m (
rho_node1 FF ) v = w)} `,
let COVEX_OF_LOFA_HALF_CIRCLE = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\
(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==>
convex_local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) `,
let COVEX_OF_LOFA_HALF_CIRCLE2 = prove(
`
convex_local_fan (V,E,
FF) /\
(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==>
convex_local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) /\
convex_local_fan (
v_prime V fw,
e_prime (E
UNION {{w, v}}) fw,fw)`,
let LT_CARD_MONO_LOFA = prove(`
local_fan (V,E,
FF) /\ v
IN V
==> (! i j. i <
CARD V /\ j <
CARD V /\
ITER i (
rho_node1 FF) v =
ITER j (
rho_node1 FF) v
==> i = j )`,
NHANH Local_lemmas.LOFA_IMP_DIS_ELMS23 THEN REPEAT STRIP_TAC THEN
ASM_CASES_TAC` i = (j:num) ` THENL [FIRST_X_ASSUM ACCEPT_TAC; DOWN] THEN
REWRITE_TAC[ARITH_RULE` ~( a = (b:num)) <=> a < b \/ b < a `] THEN
DOWN_TAC THEN PHA THEN MESON_TAC[]);;
let CONDS_IN_V_PRIME_NUM = prove_by_refinement
(` (
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==> n <
CARD V /\
ITER n (
rho_node1 FF) v = w
==> ! i. i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fv <=> i < n + 1 `,
[NHANH
POINTS_IN_HAFL_CIRCLE;
STRIP_TAC THEN STRIP_TAC;
GEN_TAC;
EQ_TAC;
ASM_REWRITE_TAC[
IN_ELIM_THM];
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
ASSUME_TAC2 (SPECL [` n': num `] (GENL [` m:num `]
DIFFERENCE_IMP_LT_CARDV));
ASSUME_TAC2
LT_CARD_MONO_LOFA;
FIRST_X_ASSUM (MP_TAC o (SPECL [`i:num `;` n': num `]));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
DISCH_THEN (SUBST_ALL_TAC o SYM);
ASM_CASES_TAC` i < n + 1 `;
FIRST_X_ASSUM ACCEPT_TAC;
ASSUME_TAC2 (ARITH_RULE` ~(i < n + 1) ==> n < i `);
DOWN;
FIRST_X_ASSUM NHANH;
ASM_REWRITE_TAC[];
STRIP_TAC;
CONJ_TAC;
REPLICATE_TAC 3 DOWN THEN PHA;
ARITH_TAC;
ASM_REWRITE_TAC[
IN_ELIM_THM];
EXISTS_TAC`i: num `;
REWRITE_TAC[];
REPEAT STRIP_TAC;
ASSUME_TAC2 (ARITH_RULE` i < n + 1 /\ m < i ==> m < n `);
MP_TAC Local_lemmas.LOFA_IMP_DIS_ELMS23;
ANTS_TAC;
ASM_REWRITE_TAC[];
ASM_MESON_TAC[]]);;
let CONDS_IN_V_PRIME_NUM2 = prove_by_refinement
(`(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fw = face HS (w,
rho_node1 FF w)
==> n <
CARD V /\
ITER n (
rho_node1 FF) v = w
==> (!i. i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fw <=>
i = 0 \/ n <= i /\ i <
CARD V )`,
[STRIP_TAC;
ASSUME_TAC2 (SPECL [` w:real^3 `;` v:real^3 `] (GENL [`v:real^3 `;` w:real^3 `]
POINT_PRESENTED_IN_RHOND1));
DOWN THEN STRIP_TAC;
MP_TAC (SPECL [` w:real^3 `;` v:real^3 `; ` fw: real^3#real^3 -> bool`;` n': num `] (GENL [` v: real^3`;` w:real^3 `;` fv: real^3#real^3 -> bool`; `n:num `]
CONDS_IN_V_PRIME_NUM));
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[
INSERT_COMM];
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
STRIP_TAC;
GEN_TAC;
UNDISCH_TAC` !i. i <
CARD (V:real^3 -> bool) /\
ITER i (
rho_node1 FF) w
IN v_prime V (fw:real^3 # real^3 -> bool) <=>
i < n' + 1 `;
EXPAND_TAC "w";
let DETERMINE_FV2 = prove_by_refinement
(`(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==> n <
CARD V /\
ITER n (
rho_node1 FF) v = w
==> fv =
(w,v)
INSERT
{
ITER m (
rho_node1 FF) v,
ITER (m + 1) (
rho_node1 FF) v | m |
m < n} `,
[NHANH
DETERMINE_FV;
SIMP_TAC[];
REPEAT STRIP_TAC;
MATCH_MP_TAC (SET_RULE` X = Y ==> a
INSERT X = a
INSERT Y `);
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM];
GEN_TAC;
EQ_TAC;
STRIP_TAC;
EXISTS_TAC` n':num`;
ASM_REWRITE_TAC[];
ASM_CASES_TAC` n' < (n:num) `;
FIRST_ASSUM ACCEPT_TAC;
ASSUME_TAC2 (ARITH_RULE` ~(n' < (n:num)) ==> n < n' + 1 `);
DOWN;
FIRST_X_ASSUM NHANH;
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC` m:num`;
ASM_REWRITE_TAC[];
GEN_TAC;
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23;
FIRST_X_ASSUM (MP_TAC o (SPECL [`m': num `;` n:num`]));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
DOWN;
UNDISCH_TAC` m < n:num`;
ARITH_TAC;
ASM_SIMP_TAC[]]);;
let INTERIOR_ANGLE_LEM_SLICING_FAN = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\
(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==>
interior_angle1 (
vec 0) fv v +
interior_angle1 (
vec 0) fw v =
interior_angle1 (
vec 0)
FF v `,
[REWRITE_TAC[
convex_local_fan] THEN
STRIP_TAC THEN ASSUME_TAC2
POINT_PRESENTED_IN_RHOND1 THEN
DOWN THEN STRIP_TAC THEN MP_TAC
DETERMINE_FV2 THEN PHA THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC o SYM)] THEN
ASSUME_TAC2 (SPECL [` w:real^3 `;` v:real^3 `] (GENL [` v:real^3 `;` w:real^3 `]
POINT_PRESENTED_IN_RHOND1)) THEN DOWN THEN STRIP_TAC THEN
MP_TAC (SPECL [` w:real^3`;` v:real^3 `;`n': num`;` fw: real^3 #real^3 -> bool`]
(GENL [` v:real^3`;` w:real^3 `;`n: num`;` fv: real^3 #real^3 -> bool`]
DETERMINE_FV2)) THEN
PHA THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[
INSERT_COMM] THEN
UNDISCH_TAC` !z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z:real^3, t} ` THEN
DISCH_THEN NHANH THEN
SIMP_TAC[
INSERT_COMM];
DISCH_THEN (ASSUME_TAC o SYM)] THEN
REWRITE_TAC[
interior_angle1; GSYM
ivs_rho_node1] THEN
MP_TAC2
HAFL_CIRCLE_FORM_LOCAL_FAN2 THEN
STRIP_TAC;
SUBGOAL_THEN ` v,
rho_node1 FF v
IN fv /\ (w,v)
IN fv ` MP_TAC;
EXPAND_TAC "fv" THEN
REWRITE_TAC[
IN_INSERT;
IN_ELIM_THM] THEN
DISJ2_TAC THEN
EXISTS_TAC` 0` THEN
REWRITE_TAC[
ITER; GSYM
ADD1] THEN
ASM_CASES_TAC` 0 < n ` THENL [FIRST_X_ASSUM ACCEPT_TAC; DOWN] THEN
REWRITE_TAC[ARITH_RULE` ~( 0 < n) <=> n = 0 `] THEN
DISCH_THEN SUBST_ALL_TAC THEN
UNDISCH_TAC`
ITER 0 (
rho_node1 FF) v = w ` THEN
ASM_REWRITE_TAC[
ITER];
STRIP_TAC;
DOWN;
UNDISCH_TAC`
local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) `;
PHA;
NHANH Local_lemmas.IVS_RHO_NODE1_DETE;
STRIP_TAC;
UNDISCH_TAC` v,
rho_node1 FF v
IN fv `;
UNDISCH_TAC`
local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) `;
PHA;
NHANH Local_lemmas.DETER_RHO_NODE;
STRIP_TAC;
UNDISCH_TAC` fw = face HS (w,
rho_node1 FF w) `;
DISCH_THEN (ASSUME_TAC o SYM);
UNDISCH_TAC` fv = face HS (v,
rho_node1 FF v) `;
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[];
SUBGOAL_THEN` (v,w)
IN fw /\
ivs_rho_node1 FF v, v
IN fw ` MP_TAC;
UNDISCH_TAC`(v,w)
INSERT
{
ITER m (
rho_node1 FF) w,
ITER (m + 1) (
rho_node1 FF) w | m < n'} =
fw `;
STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "fw";
let INTERIOR_ANGLE_LEM_SLICING_FAN2 = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\
(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==>
interior_angle1 (
vec 0) fv v +
interior_angle1 (
vec 0) fw v =
interior_angle1 (
vec 0)
FF v /\
interior_angle1 (
vec 0) fw w +
interior_angle1 (
vec 0) fv w =
interior_angle1 (
vec 0)
FF w`,
let INTERIOR_AGL_EQ = prove_by_refinement
(`(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v)
==> n <
CARD V /\
ITER n (
rho_node1 FF) v = w
==> ! i. 0 < i /\ i < n
==>
interior_angle1 (
vec 0) fv (
ITER i (
rho_node1 FF) v)
=
interior_angle1 (
vec 0)
FF (
ITER i (
rho_node1 FF) v) `,
let SUM_INTERIOR_AGL_LEMMA = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\
(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==> ! ff.
sum {i | i <
CARD V } (\i. (ff i) * (
interior_angle1 (
vec 0)
FF (
ITER i (
rho_node1 FF) v))) =
sum { i | i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fv} (\i. ff i *
interior_angle1 (
vec 0) fv (
ITER i (
rho_node1 FF) v)) +
sum { i | i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fw} (\i. ff i *
interior_angle1 (
vec 0) fw (
ITER i (
rho_node1 FF) v)) `,
[STRIP_TAC;
GEN_TAC;
ASSUME_TAC2
POINT_PRESENTED_IN_RHOND1;
DOWN THEN STRIP_TAC;
MP_TAC
POINTS_IN_HAFL_CIRCLE;
ANTS_TAC;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (SPECL [`w:real^3 `;` v:real^3` ] (GENL [` v:real^3 `;` w:real^3 `]
POINT_PRESENTED_IN_RHOND1));
DOWN THEN STRIP_TAC;
STRIP_TAC;
MP_TAC (SPECL [` w:real^3 `;` v:real^3`;` fw:real^3#real^3 -> bool` ] (GENL
[` v:real^3 `;` w:real^3 `; `fv:real^3#real^3 -> bool`]
POINTS_IN_HAFL_CIRCLE));
ANTS_TAC;
ASM_REWRITE_TAC[
INSERT_COMM];
UNDISCH_TAC` !z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t:real^3}`;
DISCH_THEN NHANH;
SIMP_TAC[
INSERT_COMM];
STRIP_TAC;
MP_TAC
CONDS_IN_V_PRIME_NUM;
ANTS_TAC;
ASM_REWRITE_TAC[];
ANTS_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;
MP_TAC
CONDS_IN_V_PRIME_NUM2;
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` {i | i < n + 1} = {i | 0 < i /\ i < n}
UNION {0, n} ` MP_TAC;
REWRITE_TAC[
EXTENSION];
REWRITE_TAC[
IN_UNION;
IN_INSERT;
NOT_IN_EMPTY;
IN_ELIM_THM];
GEN_TAC;
ARITH_TAC;
SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` {i | i = 0 \/ n <= i /\ i <
CARD V} = {i | n < i /\ i <
CARD (V:real^3 -> bool) }
UNION {0, n} ` MP_TAC;
REWRITE_TAC[
EXTENSION;
IN_UNION;
IN_INSERT;
NOT_IN_EMPTY;
IN_ELIM_THM];
GEN_TAC;
SIMP_TAC[ARITH_RULE` (n:num) <= x <=> n < x \/ x = n `];
UNDISCH_TAC` n <
CARD (V:real^3 -> bool) `;
MESON_TAC[];
SIMP_TAC[];
STRIP_TAC;
MP_TAC (SPEC` n + 1 `
FINITE_NUMSEG_LT);
ASM_REWRITE_TAC[];
UNDISCH_TAC` fv = face HS (v,
rho_node1 FF v) `;
UNDISCH_TAC` fw = face HS (w,
rho_node1 FF w) `;
DISCH_THEN (ASSUME_TAC o SYM);
DISCH_THEN (ASSUME_TAC o SYM);
ASM_REWRITE_TAC[
FINITE_UNION];
SUBGOAL_THEN` {i | n < i /\ i <
CARD (V:real^3 -> bool)} =
{i | n < i }
INTER {i | i <
CARD V} ` MP_TAC;
SET_TAC[];
STRIP_TAC;
SUBGOAL_THEN` FINITE {i | n < i /\ i <
CARD (V:real^3 -> bool)}` MP_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC
FINITE_INTER;
DISJ2_TAC;
REWRITE_TAC[
FINITE_NUMSEG_LT];
DISCH_TAC;
STRIP_TAC;
SUBGOAL_THEN`
DISJOINT {m | 0 < m /\ m < n } {0, n} ` ASSUME_TAC;
REWRITE_TAC[
DISJOINT;
EXTENSION;
IN_INTER;
NOT_IN_EMPTY;
IN_INSERT;
IN_ELIM_THM];
GEN_TAC;
ARITH_TAC;
SUBGOAL_THEN`
DISJOINT {i | n < i /\ i <
CARD (V:real^3 -> bool)} {0, n}` ASSUME_TAC;
REWRITE_TAC[
DISJOINT;
EXTENSION;
IN_INTER;
NOT_IN_EMPTY;
IN_INSERT;
IN_ELIM_THM];
GEN_TAC;
ARITH_TAC;
MP_TAC (ISPECL [` (\i. ff i *
interior_angle1 (
vec 0) fv (
ITER i (
rho_node1 FF)
v)) `; `{i | 0 < i /\ i < n} `; ` {0, n} `]
SUM_UNION);
ANTS_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];
MP_TAC (ISPECL [` (\i. ff i *
interior_angle1 (
vec 0) fw (
ITER i (
rho_node1 FF)
v)) `; `{i | n < i /\ i <
CARD (V:real^3 -> bool)}`; ` {0, n} `]
SUM_UNION);
ANTS_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC THEN STRIP_TAC;
SUBGOAL_THEN`
sum {i | n < i /\ i <
CARD (V:real^3 -> bool)}
(\i. ff i *
interior_angle1 (
vec 0) fw (
ITER i (
rho_node1 FF) v)) =
sum {i | n < i /\ i <
CARD V}
(\i. ff i *
interior_angle1 (
vec 0)
FF (
ITER i (
rho_node1 FF) v)) ` MP_TAC;
MATCH_MP_TAC
SUM_EQ;
GEN_TAC;
REWRITE_TAC[
IN_ELIM_THM];
STRIP_TAC;
REWRITE_TAC[
REAL_EQ_MUL_LCANCEL];
DISJ2_TAC;
REWRITE_TAC[Local_lemmas.interior_angle1; GSYM
ivs_rho_node1];
MP_TAC
HAFL_CIRCLE_FORM_LOCAL_FAN2;
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
MP_TAC (SPECL [` w:real^3 `;` v:real^3 `;` n':num`; `fw:real^3#real^3 -> bool`]
(GENL [` v:real^3`;` w:real^3 `;` n:num`;` fv:real^3#real^3 -> bool`]
DETERMINE_FV2));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
DOWN_TAC;
SIMP_TAC[
INSERT_COMM];
DISCH_THEN (ASSUME_TAC o SYM);
SUBGOAL_THEN`
ITER x (
rho_node1 FF) v,
rho_node1 FF (
ITER x (
rho_node1 FF) v)
IN fw ` MP_TAC;
EXPAND_TAC "fw";
let THE_SLICING_INTO_2_LEMMA = prove(`
convex_local_fan (V,E,
FF) /\
(
local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t}) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==>
convex_local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) /\
convex_local_fan (
v_prime V fw,
e_prime (E
UNION {{w, v}}) fw,fw) /\
(!ff.
sum {i | i <
CARD V}
(\i. ff i *
interior_angle1 (
vec 0)
FF (
ITER i (
rho_node1 FF) v)) =
sum
{i | i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fv}
(\i. ff i *
interior_angle1 (
vec 0) fv (
ITER i (
rho_node1 FF) v)) +
sum
{i | i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fw}
(\i. ff i *
interior_angle1 (
vec 0) fw (
ITER i (
rho_node1 FF) v)))`,
let PROVE_THE_SLICE_ASSUMPTION = prove_by_refinement
(`! v w.
convex_local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E)
==> (!z t. z
IN {v, w} /\ t
IN V
DIFF {z} ==> ~collinear {
vec 0, z, t})`,
[REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY];
MATCH_MP_TAC (MESON[]`(!v w. P v w ==> P w v) /\
(!v w. P v w ==> (!z t. z = v /\ Q z t ==> R z t))
==> (!v w. P v w ==> (!z t. (z = v \/ z = w) /\ Q z t ==> R z t))`);
SIMP_TAC[
INSERT_COMM;
IN_DIFF;
IN_SING];
REPEAT STRIP_TAC;
MP_TAC (SPEC` t:real^3 ` (GEN`w:real^3 `
CVLF_COLLINEAR_CIRCULAR_LUNAR));
ANTS_TAC;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
INSERT_COMM];
UNDISCH_TAC` ~(t = z:real^3)`;
ASM_SIMP_TAC[];
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.KCHMAMG;
DOWN THEN STRIP_TAC;
SUBGOAL_THEN`
interior_angle1 (
vec 0)
FF v =
pi` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
SUBGOAL_THEN`
convex_local_fan (V,E,
FF) ` MP_TAC;
ASM_REWRITE_TAC[];
REWRITE_TAC[
convex_local_fan];
STRIP_TAC;
ASSUME_TAC2
WEDGE_IN_FAN_LOFA_DETER2;
SUBGOAL_THEN` aff {
vec 0, v, w:real^3}
SUBSET A` MP_TAC;
MATCH_MP_TAC
AFF_SUB_PLANE;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET];
UNDISCH_TAC` (V:real^3 -> bool)
SUBSET A `;
REWRITE_TAC[
SUBSET];
STRIP_TAC;
CONJ_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
MP_TAC (ISPECL[`{
vec 0: real^3}`;` {v,w:real^3}`] (GEN_ALL Local_lemmas.AFF_GT_SUB_AFF_UNION));
REWRITE_TAC[SET_RULE` {a}
UNION S = a
INSERT S `];
PHA;
NHANH (
SUBSET_TRANS);
STRIP_TAC;
DOWN;
REWRITE_TAC[
SUBSET];
SUBGOAL_THEN`
DISJOINT {
vec 0} {v,w:real^3} ` MP_TAC;
ASM_REWRITE_TAC[SET_RULE`
DISJOINT {a} S <=> ~( a
IN S) `;
IN_INSERT;
NOT_IN_EMPTY; DE_MORGAN_THM];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
UNDISCH_TAC` v:real^3
IN V `;
UNDISCH_TAC` w:real^3
IN V `;
FIRST_X_ASSUM NHANH;
SIMP_TAC[];
NHANH Planarity.exists_in_aff_gt_disjoint;
STRIP_TAC;
DISCH_THEN (ASSUME_TAC2 o (SPEC` y:real^3 `));
SUBGOAL_THEN`
coplanar {
vec 0, v,
rho_node1 FF v, y} ` MP_TAC;
UNDISCH_TAC`
plane (A:real^3 -> bool) `;
REWRITE_TAC[
coplanar;
plane];
STRIP_TAC;
EXISTS_TAC` u:real^3 `;
EXISTS_TAC` v':real^3 `;
EXISTS_TAC` w':real^3 `;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET];
ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
DOWN;
UNDISCH_TAC` v:real^3
IN V `;
UNDISCH_TAC` (V:real^3 -> bool)
SUBSET A `;
REWRITE_TAC[
SUBSET];
DISCH_THEN NHANH;
SIMP_TAC[];
REWRITE_TAC[ GSYM
AZIM_COND_FOR_COPLANAR];
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
DOWN;
UNDISCH_TAC` !x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E `;
DISCH_THEN NHANH;
ASM_REWRITE_TAC[
SUBSET];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC`y: real^3 `));
DOWN;
REWRITE_TAC[
wedge;
IN_ELIM_THM;
interior_angle1; GSYM
ivs_rho_node1];
REAL_ARITH_TAC;
MP_TAC (SPEC`t:real^3 ` (GEN` w:real^3 ` Local_lemmas.HKIRPEP));
ANTS_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
ASSUME_TAC2
WEDGE_IN_FAN_LOFA_DETER2;
SUBGOAL_THEN` i + j =
CARD (V:real^3 -> bool) ` MP_TAC;
MATCH_MP_TAC (GEN`w:real^3 `
CARD_V_TWO_HAFL_CIRCLE);
EXISTS_TAC` t: real^3 `;
SWITCH_TAC` t =
ITER i (
rho_node1 FF) v `;
SWITCH_TAC` v =
ITER j (
rho_node1 FF) t `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~(t = (z:real^3))`;
ASM_REWRITE_TAC[
EQ_SYM_EQ];
ASSUME_TAC2
POINT_PRESENTED_IN_RHOND1;
DOWN THEN STRIP_TAC;
ASM_CASES_TAC` n = 0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN THEN DOWN;
SWITCH_TAC` t =
ITER i (
rho_node1 FF) v `;
SWITCH_TAC` v =
ITER j (
rho_node1 FF) t `;
ASM_REWRITE_TAC[
ITER];
ASM_CASES_TAC` n < (i:num) `;
SUBGOAL_THEN` w
IN {
ITER l (
rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
REWRITE_TAC[
IN_ELIM_THM];
EXISTS_TAC`n:num `;
ASM_REWRITE_TAC[];
DOWN THEN DOWN;
ARITH_TAC;
SWITCH_TAC` t =
ITER i (
rho_node1 FF) v `;
SWITCH_TAC` v =
ITER j (
rho_node1 FF) t `;
ASM_REWRITE_TAC[
IN_INTER];
STRIP_TAC;
SUBGOAL_THEN` aff_gt {
vec 0, v} {
rho_node1 FF v} = aff_gt {
vec 0, v} {w}` MP_TAC;
MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
ASM_REWRITE_TAC[];
MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASM_REWRITE_TAC[];
MP_TAC (REWRITE_RULE[
SING_SUBSET;
IN_INSERT] (
ISPECL [`{v:real^3}`;` {
vec 0, v:real^3}`; `{w:real^3}`] (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS)));
REWRITE_TAC[Packing3.SING_UNION_EQ_INSERT];
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
SUBGOAL_THEN` {
vec 0, v}
DIFF {v:real^3} = {
vec 0}` MP_TAC;
REWRITE_TAC[
DIFF;
EXTENSION;
IN_ELIM_THM;
IN_INSERT;
NOT_IN_EMPTY];
GEN_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3`));
DOWN;
MESON_TAC[];
SIMP_TAC[];
PHA THEN STRIP_TAC;
SUBGOAL_THEN`
DISJOINT {
vec 0} {w, v:real^3}` MP_TAC;
REWRITE_TAC[SET_RULE`
DISJOINT {a} S <=> ~( a
IN S)`;
IN_INSERT;
NOT_IN_EMPTY; DE_MORGAN_THM];
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
DOWN THEN DOWN;
SIMP_TAC[];
NHANH Planarity.exists_in_aff_gt_disjoint;
STRIP_TAC;
SUBGOAL_THEN` y
IN aff_gt {
vec 0, v} {
rho_node1 FF v}` MP_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` aff_gt {
vec 0} {w, v}
SUBSET aff_gt {
vec 0, v} {w:real^3} `;
REWRITE_TAC[
SUBSET];
DISCH_THEN MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
STRIP_TAC;
SUBGOAL_THEN` ~collinear {
vec 0, v, y:real^3}` MP_TAC;
MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
EXISTS_TAC`
rho_node1 FF v `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~collinear {
vec 0, v,
rho_node1 FF v}`;
PHA;
NHANH
AZIM_EQ_0_ALT;
STRIP_TAC;
FIRST_X_ASSUM (SUBST_ALL_TAC o SYM);
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
DOWN;
UNDISCH_TAC` !x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E `;
DISCH_THEN NHANH;
REWRITE_TAC[
SUBSET];
ONCE_REWRITE_TAC[
INSERT_COMM];
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC`y: real^3 `));
DOWN;
ASM_REWRITE_TAC[
wedge;
IN_ELIM_THM];
REAL_ARITH_TAC;
SWITCH_TAC` v =
ITER j (
rho_node1 FF) t `;
SWITCH_TAC` t =
ITER i (
rho_node1 FF) v `;
ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
DOWN;
UNDISCH_TAC` !x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E `;
STRIP_TAC;
PHA;
FIRST_ASSUM NHANH;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
SUBGOAL_THEN`
DISJOINT {
vec 0} {v, w:real^3} ` MP_TAC;
REWRITE_TAC[
DISJOINT;
INTER;
EXTENSION;
IN_ELIM_THM;
IN_INSERT;
NOT_IN_EMPTY];
DOWN;
UNDISCH_TAC` (v:real^3)
IN V `;
UNDISCH_TAC` (w:real^3)
IN V `;
MESON_TAC[];
PHA;
NHANH Planarity.exists_in_aff_gt_disjoint;
STRIP_TAC;
ASM_CASES_TAC` n = (i:num) `;
UNDISCH_TAC`
collinear {t, v:real^3,
vec 0} `;
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[GSYM
COLLINEAR_AFFINE_HULL_COLLINEAR];
REWRITE_TAC[GSYM aff];
SUBGOAL_THEN` {
vec 0, v, (y:real^3)}
SUBSET aff {t,v,
vec 0} ` MP_TAC;
MP_TAC (ISPECL [` {t, v:real^3,
vec 0} `] (ISPECL [`
affine` ]
HULL_SUBSET));
SIMP_TAC[GSYM aff;
INSERT_SUBSET;
EMPTY_SUBSET];
SUBGOAL_THEN` t = (w:real^3) ` SUBST_ALL_TAC;
EXPAND_TAC "t";
let EJRCFJD = prove(`
convex_local_fan (V,E,
FF) /\
v
IN V /\
w
IN V /\
~(v = w) /\
(!x. x
IN FF ==> aff_gt {
vec 0} {v, w}
SUBSET wedge_in_fan_gt x E) /\
HS = hypermap (
HYP (
vec 0,V,E
UNION {{v, w}})) /\
fv = face HS (v,
rho_node1 FF v) /\
fw = face HS (w,
rho_node1 FF w)
==>
convex_local_fan (
v_prime V fv,
e_prime (E
UNION {{v, w}}) fv,fv) /\
convex_local_fan (
v_prime V fw,
e_prime (E
UNION {{w, v}}) fw,fw) /\
(!ff.
sum {i | i <
CARD V}
(\i. ff i *
interior_angle1 (
vec 0)
FF (
ITER i (
rho_node1 FF) v)) =
sum
{i | i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fv}
(\i. ff i *
interior_angle1 (
vec 0) fv (
ITER i (
rho_node1 FF) v)) +
sum
{i | i <
CARD V /\
ITER i (
rho_node1 FF) v
IN v_prime V fw}
(\i. ff i *
interior_angle1 (
vec 0) fw (
ITER i (
rho_node1 FF) v)))`,
STRIP_TAC THEN
ASSUME_TAC2
PROVE_THE_SLICE_ASSUMPTION THEN
MATCH_MP_TAC
THE_SLICING_INTO_2_LEMMA THEN
ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO THEN
ASM_REWRITE_TAC[] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN
DOWN THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
FIRST_X_ASSUM ACCEPT_TAC);;
let CON_ATREAL_REAL_CON2_REDO = prove_by_refinement
(` (f:real -> real^N)
continuous atreal r /\ g
continuous atreal r
==> (\t.
dist (f t,g t))
real_continuous atreal r`,
[REWRITE_TAC[
real_continuous_atreal;
continuous_atreal];
REPEAT STRIP_TAC;
SUBGOAL_THEN` &0 < e / &2 ` ASSUME_TAC;
DOWN;
REAL_ARITH_TAC;
ASM_REWRITE_TAC[];
FIRST_X_ASSUM (MP_TAC o (SPEC` e / &2 `));
ANTS_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` e / &2 `));
ANTS_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
STRIP_TAC;
STRIP_TAC;
EXISTS_TAC` min d d'`;
ASM_REWRITE_TAC[
REAL_LT_MIN];
GEN_TAC;
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
SUBST1_TAC (REAL_ARITH`
dist ((f:real -> real^N) x',g x') -
dist (f r,g r) =
(
dist (f x',g x') -
dist (f x', g r)) + (
dist (f x', g r) -
dist (f r,g r))`);
MP_TAC (SPECL [`
dist ((f:real -> real^N) x',g x') -
dist (f x',g r)`; `
dist ((f:real -> real^N) x',g r) -
dist (f r,g r) `]
REAL_ABS_TRIANGLE);
SUBGOAL_THEN` abs (
dist ((f:real -> real^N) x',g x') -
dist (f x',g r)) +
abs (
dist (f x',g r) -
dist (f r,g r)) < e ` MP_TAC;
MATCH_MP_TAC
REAL_LET_TRANS;
EXISTS_TAC`
dist (g x',(g:real -> real^N) r) +
dist (f x',(f:real -> real^N) r)`;
CONJ_TAC;
MATCH_MP_TAC (REAL_ARITH` a <= b /\ d <= c ==> a + d <= b + c `);
REWRITE_TAC[
DIST_TRIANGLE_AS_ABS];
REWRITE_TAC[
DIST_SYM];
ONCE_REWRITE_TAC[
DIST_SYM];
REWRITE_TAC[
DIST_TRIANGLE_AS_ABS];
ASM_REAL_ARITH_TAC;
REAL_ARITH_TAC]);;
let REAL_CONTINUOUS_ATREAL_IMP_MUL_FUN = prove_by_refinement
(` f
real_continuous atreal r /\ g
real_continuous atreal r
==> (\t. (f t) * (g t))
real_continuous atreal r `,
[REWRITE_TAC[
real_continuous_atreal];
STRIP_TAC;
GEN_TAC;
STRIP_TAC;
SUBGOAL_THEN` &0 < e / (&2 * ( abs (f (r:real)) + &1)) ` MP_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` e / (&2 * (abs (f (r:real)) + &1))`));
ANTS_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
STRIP_TAC;
ABBREV_TAC` dd = e / (&2 * (abs (f (r:real)) + &1)) `;
SUBGOAL_THEN` &0 < e / (&2 * (abs (g (r:real)) + dd)) ` ASSUME_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[];
UNDISCH_TAC` &0 < dd `;
REAL_ARITH_TAC;
UNDISCH_TAC` !e. &0 < e
==> (?d. &0 < d /\ (!x'. abs (x' - r) < d ==> abs (f x' - f (r:real)) < e))`;
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` e / (&2 * (abs (g (r:real)) + dd))`));
DOWN THEN STRIP_TAC;
EXISTS_TAC` min d d' `;
ASM_REWRITE_TAC[
REAL_LT_MIN];
GEN_TAC;
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
SUBST1_TAC (REAL_ARITH` f (x':real) * g x' - f r * g r = (f x' - f r) * g x' + ( g x' - g r) * f r `);
MATCH_MP_TAC
REAL_LET_TRANS;
EXISTS_TAC` abs ((f x' - f r) * g x') + abs ((g x' - g r) * f (r:real)) `;
REWRITE_TAC[
REAL_ABS_TRIANGLE;
REAL_ABS_MUL];
MP_TAC (SPECL[`abs (g x' - g (r:real)) `;` dd:real `; ` abs (f (r:real))`]
REAL_LE_RMUL);
ANTS_TAC;
REWRITE_TAC[
REAL_ABS_POS];
MATCH_MP_TAC
REAL_LT_IMP_LE;
FIRST_X_ASSUM ACCEPT_TAC;
MP_TAC (SPECL [`(g:real ->
real) x' `; `(g:real ->
real) r`]
REAL_SUB_ABS);
REWRITE_TAC[REAL_ARITH` a - b <= c <=> a <= b + c `];
STRIP_TAC;
ASSUME_TAC2 (REAL_ARITH` abs (g x' - g (r:real)) < dd /\
abs (g x') <= abs (g r) + abs (g x' - g r) ==> abs (g x') < abs (g r) + dd`);
STRIP_TAC;
MP_TAC (ISPECL [`abs (f x' - f (r:real)) `;` abs ( g (x':real)) `;
` e / (&2 * (abs (g (r:real)) + dd)) `;` abs (g (r:real)) + dd`] (GEN_ALL
REAL_POS_LT_MUL));
ANTS_TAC;
ASM_REWRITE_TAC[
REAL_ABS_POS];
DOWN THEN PHA;
NHANH (REAL_ARITH` a <= b /\ c < d ==> c + a < b + d `);
STRIP_TAC;
DOWN;
SUBGOAL_THEN` e / (&2 * (abs (g r) + dd)) * (abs (g (r:real)) + dd) = e / &2 ` SUBST1_TAC;
UNDISCH_TAC` &0 < dd `;
CONV_TAC REAL_FIELD;
EXPAND_TAC "dd";
let REAL_CONS_STILL_DIFF = prove(` f
real_continuous atreal r /\ ~( f r = a)
==> ?d. &0 < d /\ (! rr. abs (rr - r) < d ==> ~( f rr = a)) `,
ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
REWRITE_TAC[
real_continuous_atreal;
REAL_ABS_NZ] THEN
STRIP_TAC THEN
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` abs ((f:real ->
real) r - a)`)) THEN
DOWN THEN STRIP_TAC THEN
EXISTS_TAC` d:real ` THEN
ASM_REWRITE_TAC[] THEN
GEN_TAC THEN FIRST_X_ASSUM NHANH THEN
REAL_ARITH_TAC);;
let EACH_ELM_PRESERVED_IMP_ALL = prove_by_refinement
(` (!x. x
IN (E: A -> bool)
==> (?e. &0 < e /\
(!t. abs t < e
==> P x t))) /\
FINITE E
==> (?e. &0 < e /\
(!t. abs t < e
==> ! x. x
IN E ==> P x t))`,
[ABBREV_TAC` n =
CARD (E: A -> bool) `;
DOWN;
SPEC_TAC (` E: A -> bool `,` E:A -> bool `);
SPEC_TAC (`n:num `,` n:num `);
INDUCT_TAC;
NHANH
CARD_EQ_0;
STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_REWRITE_TAC[
IMAGE_CLAUSES;
NOT_IN_EMPTY];
EXISTS_TAC` &1 `;
REAL_ARITH_TAC;
GEN_TAC;
ASM_CASES_TAC` (E: A -> bool) = {} `;
ASM_REWRITE_TAC[
CARD_CLAUSES;
ADD1];
REWRITE_TAC[ARITH_RULE` ~( 0 = n + 1) `];
DOWN;
REWRITE_TAC[Local_lemmas.EMPTY_NOT_EXISTS_IN];
REPEAT STRIP_TAC;
UNDISCH_TAC` (x:A)
IN E `;
FIRST_ASSUM NHANH;
STRIP_TAC;
UNDISCH_TAC` !E.
CARD (E: A -> bool) = n
==> (!x. x
IN E ==> (?e. &0 < e /\ (!t. abs t < e ==> P x t))) /\
FINITE E
==> (?e. &0 < e /\ (!t. abs t < e ==> (!x. x
IN E ==> P x t))) `;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` E
DELETE (x:A)`));
PHA;
ANTS_TAC;
ASSUME_TAC2 (ISPECL [` x:A `;` E: A -> bool `]
CARD_DELETE);
ASM_REWRITE_TAC[ARITH_RULE` SUC n - 1 = n `;
IN_DELETE;
FINITE_DELETE];
REPEAT STRIP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
STRIP_TAC;
EXISTS_TAC` min e e' `;
REWRITE_TAC[
REAL_LT_MIN];
ASM_REWRITE_TAC[];
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM NHANH;
GEN_TAC;
SET_TAC[]]);;
let EACH_ELM_PRESERVED_IMP_ALLL =
prove_by_refinement (
` (! x. (x:real^3 -> bool)
IN E ==> (? e. &0 < e /\ (! t. abs t < e ==> ~collinear ({
vec 0}
UNION (
IMAGE (\v. (phii:
real ^3 ->
real -> real^3) v t) x))))) /\
FINITE E
==> ?e. &0 < e /\
(!t. abs t < e
==> (!e. e
IN IMAGE (
IMAGE (\v. phii v t)) E
==> ~collinear ({
vec 0}
UNION e))) `,
[ABBREV_TAC` n =
CARD (E:(real^3 -> bool) -> bool) `;
DOWN;
SPEC_TAC (` E:(real^3 -> bool) -> bool `,` E:(real^3 -> bool) -> bool `);
SPEC_TAC (`n:num `,` n:num `);
INDUCT_TAC;
NHANH
CARD_EQ_0;
STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_REWRITE_TAC[
IMAGE_CLAUSES;
NOT_IN_EMPTY];
EXISTS_TAC` &1 `;
REAL_ARITH_TAC;
GEN_TAC;
ASM_CASES_TAC` (E:(real^3 -> bool) -> bool) = {} `;
ASM_REWRITE_TAC[
CARD_CLAUSES;
ADD1];
REWRITE_TAC[ARITH_RULE` ~( 0 = n + 1) `];
DOWN;
REWRITE_TAC[Local_lemmas.EMPTY_NOT_EXISTS_IN];
REPEAT STRIP_TAC;
UNDISCH_TAC` (x:real^3 -> bool)
IN E `;
FIRST_ASSUM NHANH;
STRIP_TAC;
UNDISCH_TAC` !E.
CARD (E: (real^3 -> bool) -> bool) = n
==> (!x. x
IN E
==> (?e. &0 < e /\
(!t. abs t < e
==> ~collinear
({
vec 0}
UNION IMAGE (\v. (phii:real^3 ->
real -> real^3) v t ) x)))) /\
FINITE E
==> (?e. &0 < e /\
(!t. abs t < e
==> (!e. e
IN IMAGE (
IMAGE (\v. phii v t)) E
==> ~collinear ({
vec 0}
UNION e)))) `;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` E
DELETE (x:real^3 -> bool)`));
PHA;
ANTS_TAC;
ASSUME_TAC2 (ISPECL [` x:real ^3 -> bool `;` E: (real^3 -> bool) -> bool `]
CARD_DELETE);
ASM_REWRITE_TAC[ARITH_RULE` SUC n - 1 = n `;
IN_DELETE;
FINITE_DELETE];
REPEAT STRIP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
STRIP_TAC;
EXISTS_TAC` min e e' `;
REWRITE_TAC[
REAL_LT_MIN];
ASM_REWRITE_TAC[];
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM NHANH;
GEN_TAC;
SET_TAC[]]);;
let ALL_TO_THE_NONPARALLEL_PART = prove_by_refinement
(` deformation phii (V:real^3 -> bool) (a,b) /\
FAN (
vec 0, V,E)
==> (?e. &0 < e /\
(!t. --e < t /\ t < e
==>
UNIONS (
IMAGE (
IMAGE (\v. phii v t)) E)
SUBSET
IMAGE (\v. phii v t) V /\
graph (
IMAGE (
IMAGE (\v. phii v t)) E) /\
fan1
(
vec 0,
IMAGE (\v. phii v t) V,
IMAGE (
IMAGE (\v. phii v t)) E) /\
fan2
(
vec 0,
IMAGE (\v. phii v t) V,
IMAGE (
IMAGE (\v. phii v t)) E) /\
fan6
(
vec 0,
IMAGE (\v. phii v t) V,
IMAGE (
IMAGE (\v. phii v t)) E) ))`,
[REWRITE_TAC[
FAN];
STRIP_TAC;
MATCH_MP_TAC (GEN_ALL
TOW_REAL_EXISTS_COMBINED);
CONJ_TAC;
EXISTS_TAC` &1 `;
REWRITE_TAC[REAL_ARITH` &0 < &1 `];
GEN_TAC;
STRIP_TAC;
REWRITE_TAC[GSYM
IMAGE_UNIONS];
MATCH_MP_TAC
IMAGE_SUBSET;
ASM_REWRITE_TAC[];
MATCH_MP_TAC (GEN_ALL
TOW_REAL_EXISTS_COMBINED);
CONJ_TAC;
DOWN_TAC;
REWRITE_TAC[deformation;
graph; fan1; fan2];
STRIP_TAC;
MP_TAC (ISPECL [` &0 `;`phii:real^3 ->
real -> real^3 `;`V:real^3 -> bool`]
(GEN_ALL
CONTINUOUS_ATREAL_INJ_PRESERVED));
PHA;
ANTS_TAC;
ASM_SIMP_TAC[];
ASM_SIMP_TAC[
REAL_SUB_RZERO];
STRIP_TAC;
EXISTS_TAC `d:real `;
ASM_REWRITE_TAC[
REAL_BOUNDS_LT;
IMAGE;
IN_ELIM_THM];
FIRST_X_ASSUM NHANH;
DOWN_TAC;
REWRITE_TAC[
HAS_SIZE_2_EXISTS;
IN];
REPEAT STRIP_TAC;
SUBGOAL_THEN` (?xx y. ~(xx = y) /\ (!z. x (z:real^3) <=> z = xx \/ z = y))`
MP_TAC;
UNDISCH_TAC` (E:(real^3 -> bool) -> bool) x `;
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC` (phii: real^3 -> (
real -> real^3)) xx t `;
EXISTS_TAC` (phii: real^3 -> (
real -> real^3)) y t `;
CONJ_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (SET_RULE`
UNIONS E
SUBSET (V:real^3 -> bool) /\
E x ==> (! z. x z ==> V z) `);
DOWN THEN DOWN;
MESON_TAC[];
ASM_REWRITE_TAC[
IN_ELIM_THM];
MESON_TAC[];
MATCH_MP_TAC (GEN_ALL
TOW_REAL_EXISTS_COMBINED);
CONJ_TAC;
REWRITE_TAC[fan1];
EXISTS_TAC` &1 `;
REWRITE_TAC[REAL_ARITH` &0 < &1 `];
REPEAT STRIP_TAC;
MATCH_MP_TAC
FINITE_IMAGE;
DOWN_TAC;
SIMP_TAC[fan1];
DOWN_TAC;
SIMP_TAC[SET_RULE` s
SUBSET {} <=> s = {} `; fan1;
IMAGE_EQ_EMPTY];
CONV_TAC TAUT;
MATCH_MP_TAC (GEN_ALL
TOW_REAL_EXISTS_COMBINED);
CONJ_TAC;
DOWN_TAC;
REWRITE_TAC[fan2; deformation];
STRIP_TAC;
MP_TAC (ISPECL [`&0`;` phii:real^3 ->
real -> real^ 3 `;`
vec 0:real^3 `;
` V:real^3 -> bool `] (GEN_ALL
CONTINUOUS_ATREAL_DISTINCT_FINITE));
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[fan2; fan1];
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[fan2; fan1];
STRIP_TAC;
UNDISCH_TAC` ~(
vec 0
IN (V:real^3 -> bool)) `;
MESON_TAC[];
REWRITE_TAC[
REAL_SUB_RZERO;
REAL_BOUNDS_LT;
IN_IMAGE];
MESON_TAC[];
REWRITE_TAC[fan6];
UNDISCH_TAC`
graph (E:(real^3 -> bool) -> bool) `;
REWRITE_TAC[Fan.GRAPH];
DOWN_TAC;
REWRITE_TAC[fan1; fan2];
STRIP_TAC;
ASSUME_TAC2 (ISPECL [`
UNIONS (E:(real^3 -> bool) -> bool) `;` V:real^3 -> bool`]
FINITE_SUBSET);
DOWN;
REWRITE_TAC[
FINITE_UNIONS;
REAL_BOUNDS_LT];
STRIP_TAC;
MATCH_MP_TAC
EACH_ELM_PRESERVED_IMP_ALLL;
ASM_REWRITE_TAC[];
GEN_TAC;
STRIP_TAC;
SUBGOAL_THEN` (x:real^3 -> bool)
HAS_SIZE 2 ` MP_TAC;
DOWN;
ASM_REWRITE_TAC[];
DOWN_TAC;
REWRITE_TAC[fan6; deformation;
HAS_SIZE_2_EXISTS2];
STRIP_TAC;
SUBGOAL_THEN` ~collinear ({
vec 0: real^3}
UNION x)` MP_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
ASM_REWRITE_TAC[
IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2;
UNION_EMPTY];
ONCE_REWRITE_TAC[REAL_ARITH` abs t = abs (&0 - t) `];
STRIP_TAC;
MATCH_MP_TAC
CONTINUOUS_PRESERVE_COLLINEAR;
ASSUME_TAC2 (SET_RULE`
UNIONS E
SUBSET V /\ (x:real^3 -> bool)
IN E ==> x
SUBSET V `);
DOWN;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET];
UNDISCH_TAC` !v. (v:real^3)
IN V ==> phii v (&0) = v`;
DISCH_THEN NHANH;
ASM_SIMP_TAC[ETA_AX]]);;