(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Fan *)
(* Author: Hoang Le Truong *)
(* Date: 2010-02-09 *)
(* ========================================================================== *)
module Dartset_leads_into = struct
open Sphere;;
open Fan_defs;;
open Hypermap_of_fan;;
open Tactic_fan;;
open Lemma_fan;;
open Fan;;
open Hypermap_of_fan;;
open Node_fan;;
open Azim_node;;
open Sum_azim_node;;
open Disjoint_fan;;
open Lead_fan;;
open Fan_misc;;
open Leads_into_fan;;
open Fully_surrounded;;
open Sin_azim_cross_dot;;
open Leads_intos;;
open Hypermap;;
(* ========================================================================== *)
(* FAN AND CONVEX *)
(* ========================================================================== *)
let angle_is_small_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
azim x v u w <=
azim x v u (
sigma_fan x V E v u) `,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `v:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN DISJ_CASES_TAC(SET_RULE`
set_of_edge v V E = {u} \/ ~(
set_of_edge v V E = {u:real^3})`)
THENL(*1*)[
MRESA_TAC
CARD_SING[`u:real^3`; `(
set_of_edge v V E):real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(
th)])
THEN ASM_TAC THEN ARITH_TAC;(*1*)
MRESA_TAC
SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`
sigma_fan x V E v (u:real^3)`;` (v:real^3)`]
THEN POP_ASSUM MP_TAC THEN RESA_TAC
THEN MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w:real^3`]
THEN ABBREV_TAC`w1=(
sigma_fan x V E v u) :real^3`
THEN MRESA_TAC
properties_of_fully_surrounded1_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
THEN DISJ_CASES_TAC(REAL_ARITH`
azim x v u w1 <
azim x v u w\/
azim x v u w <=
azim x v u w1 `)
THENL(*2*)[
MP_TAC(REAL_ARITH`
azim x v u w1 <
azim x v u w ==>
azim x v u w1 <=
azim x v u w`)
THEN RESA_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
THEN MP_TAC(REAL_ARITH` &0<
azim x v u w1 /\
azim x v u w1 <
azim x v u w /\
azim x v u w =
azim x v u w1 +
azim x v w1 w
==> &0<
azim x v w1 w /\
azim x v w1 w <=
azim x v u w`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`
azim x v w1 w <=
azim x v u w /\
azim x v u w <
pi
==>
azim x v w1 w <
pi`)
THEN RESA_TAC
THEN MRESA_TAC
exists_cut_in_edge_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?x. x
IN A`;
INTER]
THEN REWRITE_TAC[
IN_ELIM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`va=(&1-a)%u + a%w:real^3`
THEN MRESA_TAC
not_collinear_is_properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`va:real^3`]
decomposition_planar_by_angle_fan)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL(*3*)[
MRESA_TAC
point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w1:real^3)`]
THEN MRESA_TAC
not_cut_in_edges_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
THEN MP_TAC(SET_RULE`w1
IN aff_gt {x} {v, va}
/\ w1
IN aff_ge {x} {v, w1}==> ~(aff_gt {x} {v, va}
INTER aff_ge {x:real^3} {v, w1}={})`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC`{v,w1:real^3}
IN E`
THEN SET_TAC[];(*3*)
MRESA_TAC
pos_in_aff_ge_fan [`x:real^3`;`u:real^3`;`w:real^3`;`a:real`]
THEN MP_TAC(SET_RULE`va
IN aff_ge {x} {v, w1:real^3} /\ va
IN aff_ge {x} {u, w}
==>va
IN aff_ge {x} {u, w}
INTER aff_ge {x} {v, w1:real^3} `)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC `
FAN(x:real^3,V,E)`
THEN REWRITE_TAC[
FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MP_TAC(ISPECL[`{(u:real^3),(w:real^3)}`;`{(v:real^3),(w1:real^3)}`]
th))
THEN ASM_REWRITE_TAC[
UNION;
IN_ELIM_THM;]
THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`~(v=u) /\
DISJOINT{x,v} {w} ==> ~(v
IN {u,w:real^3}) `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(v
IN {u,w:real^3})/\ ~(u=w)==> ~({u, w}
INTER {v, w1} = {u, w:real^3})`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~({u, w}
INTER {v, w1} = {u, w:real^3}) ==> {u, w}
INTER {v, w1}
PSUBSET {u, w} `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{u, w}
INTER {v, w1}
PSUBSET {u, w:real^3} ==> {u, w}
INTER {v, w1}
SUBSET {u}\/ {u, w}
INTER {v, w1}
SUBSET {w} `)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL(*4*)[
MRESAL_TAC
AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w}
INTER {v, w1:real^3}`; `{u:real^3}`][
DISJOINT;SET_RULE`{x}
INTER {u} = {}<=> ~(x=u:real^3)`]
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{u:real^3}`][SET_RULE`{x}
UNION {u}={x,u}`;GSYM aff]
THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w}
INTER {v, w1})
SUBSET aff_ge {x} {u}/\ aff_ge {x} {u}
SUBSET aff {x, u}/\ va
IN aff_ge {x} ({u, w}
INTER {v, w1})==> va
IN aff {x,u}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % u
<=> a % w = u' % x + (v''+a- &1) % u`]
THEN MP_TAC(REAL_ARITH`&0< a==> ~(a = &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`a:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`a % w = u' % x + (v' + a - &1) % u:real^3 ==> (inv (a))%(a % w ) = (inv (a))%( u' % x + (v' + a - &1) % u)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN `w
IN aff {x,u:real^3}` ASSUME_TAC
THENL(*5*)[
REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`(inv a * u'):real`
THEN EXISTS_TAC`(inv a * (v' + a - &1)):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv a * u' + inv a * (v' + a - &1) =inv a * ( a+ (u' + v') - &1)`;REAL_ARITH`A+ &1- &1=A`];(*5*)
POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC `~(w
IN aff {x, u:real^3})`
THEN SET_TAC[]](*5*);(*4*)
FIND_ASSUM MP_TAC`{u,w:real^3}
IN E`
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN MRESA_TAC
remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`w:real^3`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC
AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w}
INTER {v, w1:real^3}`; `{w:real^3}`][
DISJOINT;SET_RULE`{x}
INTER {w} = {}<=> ~(x=w:real^3)`]
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{w:real^3}`][SET_RULE`{x}
UNION {w}={x,w}`;GSYM aff]
THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w}
INTER {v, w1})
SUBSET aff_ge {x} {w}/\ aff_ge {x} {w}
SUBSET aff {x, w}/\ va
IN aff_ge {x} ({u, w}
INTER {v, w1})==> va
IN aff {x,w}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % w
<=> (&1-a) % u = u' % x + (v''-a) % w`]
THEN MP_TAC(REAL_ARITH`a < &1==> ~(&1- a= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`&1-a:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(&1-a) % u = u' % x + (v' - a) % w:real^3 ==> (inv (&1-a))%((&1-a) % u ) = (inv (&1-a))%( u' % x + (v' - a) % w)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN `u
IN aff {x,w:real^3}` ASSUME_TAC
THENL(*5*)[
REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`(inv (&1-a) * u'):real`
THEN EXISTS_TAC`(inv (&1-a) * (v' - a)):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (&1-a') * u' + inv (&1-a') * (v' - a') =inv (&1-a') * ( (u' + v') - a')`;];(*5*)
POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC `~(u
IN aff {x, w:real^3})`
THEN SET_TAC[]](*5*)](*4*)](*3*);(*2*)
ASM_REWRITE_TAC[]]]);;
let angle_is_smallpi_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
&0<
azim x v u w /\
azim x v u w <
pi`,
REPEAT STRIP_TAC
THENL[
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN SUBGOAL_THEN`~(
azim x v u (w:real^3)= &0)`ASSUME_TAC
THENL[STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`];
MATCH_MP_TAC(REAL_ARITH`~(
azim x v u (w:real^3)= &0)/\ &0<=
azim x v u w ==> &0 <
azim x v u w`)
THEN ASM_REWRITE_TAC[
azim]];
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
angle_is_small_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`;`w:real^3`]
THEN ASM_TAC THEN REAL_ARITH_TAC]);;
let exists_rw_dart_inter_aff_gt_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 .
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
(?h:real. &0< h /\
(!t:real. &0< t /\ t< h==>
(!s:real. &0<s /\ s< pi/ &2
==>
~(
rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),(
sigma_fan x V E v (u:real^3))) (
cos(s))
INTER aff_gt {x} {v, (&1-t)%u+t%w}={})
)))`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `v:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN DISJ_CASES_TAC(SET_RULE`
set_of_edge v V E = {u} \/ ~(
set_of_edge v V E = {u:real^3})`)
THENL(*1*)[
MRESA_TAC
CARD_SING[`u:real^3`; `(
set_of_edge v V E):real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(
th)])
THEN ASM_TAC THEN ARITH_TAC;(*1*)
MRESA_TAC
SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`
sigma_fan x V E v (u:real^3)`;` (v:real^3)`]
THEN POP_ASSUM MP_TAC THEN RESA_TAC
THEN MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`x:real^3`;`v:real^3`;`w:real^3`]
THEN ABBREV_TAC`w1=(
sigma_fan x V E v u) :real^3`
THEN MRESA_TAC
properties_of_fully_surrounded1_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
THEN DISJ_CASES_TAC(REAL_ARITH`
azim x v u w1 <
azim x v u w\/
azim x v u w <=
azim x v u w1 `)
THENL(*2*)[
MP_TAC(REAL_ARITH`
azim x v u w1 <
azim x v u w ==>
azim x v u w1 <=
azim x v u w`)
THEN RESA_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
THEN MP_TAC(REAL_ARITH` &0<
azim x v u w1 /\
azim x v u w1 <
azim x v u w /\
azim x v u w =
azim x v u w1 +
azim x v w1 w
==> &0<
azim x v w1 w /\
azim x v w1 w <=
azim x v u w`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`
azim x v w1 w <=
azim x v u w /\
azim x v u w <
pi
==>
azim x v w1 w <
pi`)
THEN RESA_TAC
THEN MRESA_TAC
exists_cut_in_edge_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?x. x
IN A`;
INTER]
THEN REWRITE_TAC[
IN_ELIM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`va=(&1-a)%u + a%w:real^3`
THEN MRESA_TAC
not_collinear_is_properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`va:real^3`]
decomposition_planar_by_angle_fan)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL(*3*)[
MRESA_TAC
point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w1:real^3)`]
THEN MRESA_TAC
not_cut_in_edges_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
THEN MP_TAC(SET_RULE`w1
IN aff_gt {x} {v, va}
/\ w1
IN aff_ge {x} {v, w1}==> ~(aff_gt {x} {v, va}
INTER aff_ge {x:real^3} {v, w1}={})`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC`{v,w1:real^3}
IN E`
THEN SET_TAC[];(*3*)
MRESA_TAC
pos_in_aff_ge_fan [`x:real^3`;`u:real^3`;`w:real^3`;`a:real`]
THEN MP_TAC(SET_RULE`va
IN aff_ge {x} {v, w1:real^3} /\ va
IN aff_ge {x} {u, w}
==>va
IN aff_ge {x} {u, w}
INTER aff_ge {x} {v, w1:real^3} `)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC `
FAN(x:real^3,V,E)`
THEN REWRITE_TAC[
FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MP_TAC(ISPECL[`{(u:real^3),(w:real^3)}`;`{(v:real^3),(w1:real^3)}`]
th))
THEN ASM_REWRITE_TAC[
UNION;
IN_ELIM_THM;]
THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`~(v=u) /\
DISJOINT{x,v} {w} ==> ~(v
IN {u,w:real^3}) `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(v
IN {u,w:real^3})/\ ~(u=w)==> ~({u, w}
INTER {v, w1} = {u, w:real^3})`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~({u, w}
INTER {v, w1} = {u, w:real^3}) ==> {u, w}
INTER {v, w1}
PSUBSET {u, w} `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{u, w}
INTER {v, w1}
PSUBSET {u, w:real^3} ==> {u, w}
INTER {v, w1}
SUBSET {u}\/ {u, w}
INTER {v, w1}
SUBSET {w} `)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL(*4*)[
MRESAL_TAC
AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w}
INTER {v, w1:real^3}`; `{u:real^3}`][
DISJOINT;SET_RULE`{x}
INTER {u} = {}<=> ~(x=u:real^3)`]
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{u:real^3}`][SET_RULE`{x}
UNION {u}={x,u}`;GSYM aff]
THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w}
INTER {v, w1})
SUBSET aff_ge {x} {u}/\ aff_ge {x} {u}
SUBSET aff {x, u}/\ va
IN aff_ge {x} ({u, w}
INTER {v, w1})==> va
IN aff {x,u}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % u
<=> a % w = u' % x + (v''+a- &1) % u`]
THEN MP_TAC(REAL_ARITH`&0< a==> ~(a = &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`a:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`a % w = u' % x + (v' + a - &1) % u:real^3 ==> (inv (a))%(a % w ) = (inv (a))%( u' % x + (v' + a - &1) % u)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN `w
IN aff {x,u:real^3}` ASSUME_TAC
THENL(*5*)[
REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`(inv a * u'):real`
THEN EXISTS_TAC`(inv a * (v' + a - &1)):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv a * u' + inv a * (v' + a - &1) =inv a * ( a+ (u' + v') - &1)`;REAL_ARITH`A+ &1- &1=A`];(*5*)
POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC `~(w
IN aff {x, u:real^3})`
THEN SET_TAC[]](*5*);(*4*)
FIND_ASSUM MP_TAC`{u,w:real^3}
IN E`
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN MRESA_TAC
remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`w:real^3`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN MRESAL_TAC
AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w}
INTER {v, w1:real^3}`; `{w:real^3}`][
DISJOINT;SET_RULE`{x}
INTER {w} = {}<=> ~(x=w:real^3)`]
THEN STRIP_TAC
THEN MRESAL_TAC
AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{w:real^3}`][SET_RULE`{x}
UNION {w}={x,w}`;GSYM aff]
THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w}
INTER {v, w1})
SUBSET aff_ge {x} {w}/\ aff_ge {x} {w}
SUBSET aff {x, w}/\ va
IN aff_ge {x} ({u, w}
INTER {v, w1})==> va
IN aff {x,w}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % w
<=> (&1-a) % u = u' % x + (v''-a) % w`]
THEN MP_TAC(REAL_ARITH`a < &1==> ~(&1- a= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`&1-a:real`
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`(&1-a) % u = u' % x + (v' - a) % w:real^3 ==> (inv (&1-a))%((&1-a) % u ) = (inv (&1-a))%( u' % x + (v' - a) % w)`)
THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[
th])
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN `u
IN aff {x,w:real^3}` ASSUME_TAC
THENL(*5*)[REWRITE_TAC[aff;
AFFINE_HULL_2;
IN_ELIM_THM]
THEN EXISTS_TAC`(inv (&1-a) * u'):real`
THEN EXISTS_TAC`(inv (&1-a) * (v' - a)):real`
THEN ASM_REWRITE_TAC[REAL_ARITH`inv (&1-a') * u' + inv (&1-a') * (v' - a') =inv (&1-a') * ( (u' + v') - a')`;];(*5*)
POP_ASSUM MP_TAC
THEN FIND_ASSUM MP_TAC `~(u
IN aff {x, w:real^3})`
THEN SET_TAC[]](*5*)](*4*)](*3*);(*2*)
EXISTS_TAC`&1`
THEN REWRITE_TAC[REAL_ARITH`&0< &1`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`va=(&1-t)%u + t%w:real^3`
THEN MRESA_TAC
not_collinear_is_properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`t:real`]
THEN MRESA_TAC
inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`t:real`]
THEN ASM_REWRITE_TAC[
rw_dart_fan;
w_dart_fan]
THEN SUBGOAL_THEN`aff_gt {x} {v,va:real^3}
SUBSET wedge x v u w1` ASSUME_TAC
THENL(*3*)[
REWRITE_TAC[
SUBSET;
IN_ELIM_THM;
wedge]
THEN GEN_TAC
THEN MRESAL_TAC
aff_gt_inter_aff_gt [`(x:real^3)`;`(v:real^3)`;`(va:real^3)`][
INTER;
IN_ELIM_THM]
THEN STRIP_TAC
THEN MRESAL_TAC
properties_of_collinear4_points_fan[`x:real^3`;`v:real^3`;`va:real^3`;`x':real^3`][
IN_ELIM_THM]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`v:real^3`;`u:real^3`; `x':real^3`;`va:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;(*3*)
MP_TAC(SET_RULE`aff_gt {x} {v, va:real^3}
SUBSET wedge x v u w1 ==> (
wedge x v u w1
INTER rcone_fan x v (
cos s))
INTER aff_gt {x} {v, va}=(
rcone_fan x v (
cos s))
INTER aff_gt {x} {v, va}`)
THEN RESA_TAC
THEN REWRITE_TAC[
rcone_fan;
INTER;
IN_ELIM_THM]
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`;
IN_ELIM_THM]
THEN DISJ_CASES_TAC(REAL_ARITH`(v - x)
dot (va - x:real^3) <= &0 \/ &0< (v - x)
dot (va - x)`)
THENL(*4*)[
ABBREV_TAC`s1= s/ &2:real`
THEN MP_TAC(REAL_ARITH`&0< s /\ s< pi/ &2/\ s1= s/ &2 /\ &0<
pi ==> &0<= s1 /\ s1< s /\ s <= pi/\ &0<s1 /\ s1<pi/ &2`)
THEN REWRITE_TAC[
PI_WORKS]
THEN RESA_TAC
THEN EXISTS_TAC`
sin (s1) % (
e1_fan x v va) + (
cos s1) %(
e3_fan x v va)+x :real^3 `
THEN REWRITE_TAC[
dist;
vector_norm;VECTOR_ARITH`(B+C+A)-A=(B+C:real^3)`;
DOT_LADD;
DOT_RADD;
DOT_RMUL;
DOT_LMUL;]
THEN MRESAL_TAC
properties_coordinate[`x:real^3`;`v:real^3`;`va:real^3`][
orthonormal]
THEN ONCE_REWRITE_TAC[
DOT_SYM]
THEN ASSUME_TAC(ISPEC`s1:real`
SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`
sin s *
sin s +
cos s *
cos s =(
sin s) pow 2 + (
cos s) pow 2`;
e3_fan;
DOT_RMUL; ]
THEN ONCE_REWRITE_TAC[GSYM
vector_norm;]
THEN REWRITE_TAC[
DOT_SQUARE_NORM;]
THEN MRESAL1_TAC
SQRT_POW_2`&1`[REAL_ARITH`a pow 2 = a * a`;REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
SQRT_MUL[`&1`;`&1`][REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th); REAL_ARITH`&1* &1= &1`])
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN SUBGOAL_THEN`~(
norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
THENL(*5*)[ ASM_REWRITE_TAC[
NORM_EQ_0;VECTOR_ARITH`v-x=
vec 0<=> x=v`];(*5*)
MP_TAC(ISPEC`
norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN REWRITE_TAC[REAL_ARITH`A*B*D *D=(B*D) *D *A`;REAL_ARITH`A>B<=> B<A`]
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN ASSUME_TAC(ISPEC`v-x:real^3`
NORM_POS_LE)
THEN STRIP_TAC
THENL(*6*)[
MATCH_MP_TAC
REAL_LT_LMUL
THEN MP_TAC(REAL_ARITH`~(
norm (v - x:real^3) = &0)/\ &0 <=
norm (v - x)==> &0<
norm (v - x) `)
THEN RESA_TAC
THEN MATCH_MP_TAC
COS_MONO_LT
THEN ASM_REWRITE_TAC[];(*6*)
MRESA_TAC
condition1_to_in_aff_gt_by_angle[`x:real^3`;`v:real^3`;`va:real^3`;`s1:real`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
e3_fan]](*6*)](*5*);(*4*)
SUBGOAL_THEN`&0<(
atn ((
norm ((v - x)
cross (va - x))) * inv((v - x)
dot (va - x))))` ASSUME_TAC
THENL(*5*)[
MP_TAC(ISPEC`(v - x)
dot (va - x:real^3)`
REAL_LT_INV)
THEN RESA_TAC
THEN ASSUME_TAC(
PI_WORKS)
THEN MP_TAC(REAL_ARITH`&0<
pi ==> --(
pi / &2) < &0`)
THEN RESA_TAC
THEN MRESAL_TAC
ATN_MONO_LT[`&0:real`;` (
norm ((v - x)
cross (va - x)) * inv ((v - x)
dot (va - x))):real`][
ATN_0]
THEN POP_ASSUM MATCH_MP_TAC
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~(
norm((v - x)
cross (va - x:real^3))= &0)` ASSUME_TAC
THENL(*6*)[ASM_REWRITE_TAC[
NORM_EQ_0]
THEN MP_TAC(ISPECL[`v-x:real^3`;`va-x:real^3`]
CROSS_EQ_0)
THEN ONCE_REWRITE_TAC[GSYM
COLLINEAR_3;]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN MP_TAC(ISPEC`(v - x)
cross (va - x:real^3)`
NORM_POS_LE)
THEN REAL_ARITH_TAC];(*5*)
ABBREV_TAC`s1= min (s:real) (
atn ((
norm ((v - x)
cross (va - x))) * inv((v - x)
dot (va - x)))) / &2`
THEN ASSUME_TAC(ISPEC`(
norm ((v - x)
cross (u - x)) * inv ((v - x)
dot (u - x))):real`
ATN_BOUNDS)
THEN MP_TAC(REAL_ARITH`&0< s /\ s< pi/ &2/\ s1= min (s:real) (
atn ((
norm ((v - x)
cross (va - x))) * inv((v - x)
dot (va - x)))) / &2
/\ &0<
pi /\ &0< (
atn ((
norm ((v - x)
cross (va - x))) * inv((v - x)
dot (va - x))))
/\ (
atn ((
norm ((v - x)
cross (va - x))) * inv((v - x)
dot (va - x)))) < pi/ &2
==> &0<= s1 /\ s1< s /\ s <= pi/\ &0<s1 /\ s1<pi/ &2
/\ s1< (
atn ((
norm ((v - x)
cross (va - x))) * inv((v - x)
dot (va - x))))
`)
THEN REWRITE_TAC[
PI_WORKS]
THEN RESA_TAC
THEN EXISTS_TAC`
sin (s1) % (
e1_fan x v va) + (
cos s1) %(
e3_fan x v va)+x :real^3 `
THEN REWRITE_TAC[
dist;
vector_norm;VECTOR_ARITH`(B+C+A)-A=(B+C:real^3)`;
DOT_LADD;
DOT_RADD;
DOT_RMUL;
DOT_LMUL;]
THEN MRESAL_TAC
properties_coordinate[`x:real^3`;`v:real^3`;`va:real^3`][
orthonormal]
THEN ONCE_REWRITE_TAC[
DOT_SYM]
THEN ASSUME_TAC(ISPEC`s1:real`
SIN_CIRCLE)
THEN ASM_REWRITE_TAC[]
THEN REDUCE_ARITH_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`
sin s *
sin s +
cos s *
cos s =(
sin s) pow 2 + (
cos s) pow 2`;
e3_fan;
DOT_RMUL; ]
THEN ONCE_REWRITE_TAC[GSYM
vector_norm;]
THEN REWRITE_TAC[
DOT_SQUARE_NORM;]
THEN MRESAL1_TAC
SQRT_POW_2`&1`[REAL_ARITH`a pow 2 = a * a`;REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC
SQRT_MUL[`&1`;`&1`][REAL_ARITH`&0<= &1`;]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th); REAL_ARITH`&1* &1= &1`])
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN SUBGOAL_THEN`~(
norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
THENL(*6*)[ASM_REWRITE_TAC[
NORM_EQ_0;VECTOR_ARITH`v-x=
vec 0<=> x=v`];(*6*)
MP_TAC(ISPEC`
norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
THEN REWRITE_TAC[REAL_ARITH`A*B*D *D=(B*D) *D *A`;REAL_ARITH`A>B<=> B<A`]
THEN RESA_TAC
THEN REDUCE_ARITH_TAC
THEN ASSUME_TAC(ISPEC`v-x:real^3`
NORM_POS_LE)
THEN STRIP_TAC
THENL(*7*)[
MATCH_MP_TAC
REAL_LT_LMUL
THEN MP_TAC(REAL_ARITH`~(
norm (v - x:real^3) = &0)/\ &0 <=
norm (v - x)==> &0<
norm (v - x) `)
THEN RESA_TAC
THEN MATCH_MP_TAC
COS_MONO_LT
THEN ASM_REWRITE_TAC[];
MRESA_TAC
condition_to_in_aff_gt_by_angle[`x:real^3`;`v:real^3`;`va:real^3`;`s1:real`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
e3_fan]]]]]]]]);;
let exists_point_inside_domain_cone_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 s:real.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ &0<s /\ s<pi/ &2
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
(?y:real^3. y
IN rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(w2:real^3)) (
cos(s)) /\
azim x v u y<
azim x v u w)`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `u:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN DISJ_CASES_TAC(SET_RULE`
set_of_edge u V E = {w} \/ ~(
set_of_edge u V E = {w:real^3})`)
THENL(*1*)[
MRESA_TAC
CARD_SING[`w:real^3`; `(
set_of_edge u V E):real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(
th)])
THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;(*1*)
MRESA_TAC
not_empty_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`; `w:real^3`]
THEN POP_ASSUM(fun th-> MRESA1_TAC
th `s:real`)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`;
rw_dart_fan;
INTER;
w_dart_fan;
wedge;
IN_ELIM_THM;]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v==>
azim x u w y<=
azim x u w (v:real^3)`)
THEN RESA_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"YEU EM")
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v/\ &0<
azim x u w y/\
azim x u w v <
pi /\
azim x u w v =
azim x u w y +
azim x u y v==> ~(
azim x u y (v:real^3)= &0)/\ &0<
azim x u y v/\
azim x u y v < pi/\ ~(
azim x u y (v:real^3)=
pi)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN REPEAT DISCH_TAC
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`y:real^3`;`u:real^3`]
THEN SUBGOAL_THEN`~(
azim x v u (y:real^3)= &0)`ASSUME_TAC
THENL(*2*)[
STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[];(*2*)
SUBGOAL_THEN`~(
azim x v u (y:real^3)=
pi)`ASSUME_TAC
THENL(*3*)[
STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[];(*3*)
MP_TAC(REAL_ARITH`~(
azim x v u y=
pi)==>pi<
azim x v u y \/
azim x v u (y:real^3) <
pi`)
THEN RESA_TAC
THENL(*4*)[
MRESA_TAC
AZIM_COMPL[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN MRESA_TAC
azim[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN MP_TAC(REAL_ARITH`pi<
azim x v u y /\
azim x v u y < &2 *
pi /\
azim x v y u = &2 *
pi -
azim x v u y
==>
azim x v y u< pi/\ &0<
azim x v y u `)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN REPEAT STRIP_TAC
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;
CROSS_TRIPLE;]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;(*4*)
DISJ_CASES_TAC(REAL_ARITH`
azim x v u w <=
azim x v u (y:real^3) \/
azim x v u y <
azim x v u w`)
THENL(*5*)[
ABBREV_TAC`a1=(v-x):real^3`
THEN ABBREV_TAC`a2=(y-x):real^3`
THEN ABBREV_TAC`a3=(u-x) :real^3`
THEN ABBREV_TAC`a4=w-x:real^3`
THEN ABBREV_TAC`va=a1
cross a4:real^3`
THEN ABBREV_TAC`vb=a2
cross a3:real^3`
THEN ABBREV_TAC`v3= (vb:real^3)
cross (va:real^3)+(x:real^3)`
THEN ABBREV_TAC`v4= &1/ &2 % v3+ &1/ &2 % u:real^3`
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;
CROSS_TRIPLE;]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW; ]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN STRIP_TAC
THEN SUBGOAL_THEN `v3
IN aff_gt {x,u} {y:real^3}` ASSUME_TAC
THENL(*6*)[
MRESA_TAC
th3[`(x:real^3)` ;` (u:real^3)`;`(y:real^3) `;]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`u:real^3`;`y:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&1-(va:real^3)
dot (a2:real^3)+va
dot (a3:real^3)`
THEN EXISTS_TAC`((va:real^3)
dot (a2:real^3))`
THEN EXISTS_TAC`(--((va:real^3)
dot (a3:real^3)))`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - va
dot a3 + va
dot a2) + (va
dot a3) + --(va
dot a2) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
THEN EXPAND_TAC"v3"
THEN EXPAND_TAC"vb"
THEN ONCE_REWRITE_TAC[
CROSS_SKEW; ]
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`];(*6*)
SUBGOAL_THEN `(v4:real^3)
IN aff_gt {x,u} {y:real^3}` ASSUME_TAC
THENL(*7*)[
POP_ASSUM MP_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (u:real^3)`;`(y:real^3) `;]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`u:real^3`;`y:real^3`][
IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`&1/ &2 * t1:real`
THEN EXISTS_TAC`&1/ &2 * t2+ &1/ &2:real`
THEN EXISTS_TAC`&1/ &2*t3:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 / &2 *
t1 + (&1 / &2 * t2 + &1 / &2) + &1 / &2 * t3 = &1/ &2*(t1+t2+t3)+ &1/ &2`; REAL_ARITH`&1/ &2 * &1 + &1/ &2= &1`;VECTOR_ARITH`(&1 / &2 *
t1) % x + (&1 / &2 * t2 + &1 / &2) % u + (&1 / &2 * t3) % y= &1/ &2 %(
t1 % x + t2 % u + t3 % y)+ &1/ &2 % u`]
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC
REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;(*7*)
MRESA_TAC
aff_gt_imp_not_collinear[`x:real^3`;`y:real^3`;`u:real^3`; `v4:real^3`]
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`w:real^3`; `v4:real^3`;`y:real^3`]
THEN EXISTS_TAC`v4:real^3`
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN `v3
IN aff_gt {x,v} {w:real^3}` ASSUME_TAC
THENL(*8*)[
MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(w:real^3) `;]
THEN MRESAL_TAC
AFF_GT_2_1[`x:real^3`;`v:real^3`;`w:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&1-(vb:real^3)
dot (a4:real^3)+vb
dot (a1:real^3)`
THEN EXISTS_TAC`((vb:real^3)
dot (a4:real^3))`
THEN EXISTS_TAC`(--((vb:real^3)
dot (a1:real^3)))`
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - vb
dot a4 + vb
dot a1) + (vb
dot a4) + --(vb
dot a1) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
THEN EXPAND_TAC"v3"
THEN EXPAND_TAC"va"
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`]
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`v:real^3`;`y:real^3`;`u:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;
CROSS_TRIPLE;]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW; ]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN MRESA_TAC
azim[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN FIND_ASSUM(MP_TAC)`~(
azim x v u (y:real^3)= &0)`
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;(*8*)
REMOVE_THEN "YEU EM"(fun th-> ASM_REWRITE_TAC[SYM(
th)])
THEN MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
aff_gt_imp_not_collinear[`x:real^3`;`w:real^3`;`v:real^3`; `v3:real^3`]
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`v:real^3`;`u:real^3`; `v3:real^3`;`w:real^3`]
THEN SUBGOAL_THEN`~(
coplanar{x,v,u,v3:real^3})`ASSUME_TAC
THENL(*9*)[
STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`v3:real^3`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`];(*9*)
SUBGOAL_THEN`~(
azim x u v3 (v:real^3)= &0)`ASSUME_TAC
THENL(*10*)[
POP_ASSUM MP_TAC
THEN MATCH_MP_TAC MONO_NOT
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_IMP_COPLANAR[`x:real^3`;`u:real^3`;`v3:real^3`;`v:real^3`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN ASM_REWRITE_TAC[];(*10*)
MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`v3:real^3`]
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`v:real^3`; `v3:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"YEU EM")
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
THEN RESA_TAC
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`v3:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&2 *
pi -
azim x u y v = &2 *
pi -
azim x u v3 v==>
azim x u v3 v=
azim x u y v `)
THEN RESA_TAC
THEN MRESAL_TAC
inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`v3:real^3`;`&1/ &2`][REAL_ARITH`&1- &1/ &2= &1/ &2/\ &0< &1/ &2 /\ &1/ &2< &1`;VECTOR_ARITH`A+B=B+A:real^3`]
THEN MATCH_MP_TAC
conditions_in_rcone_fan
THEN EXISTS_TAC `y:real^3`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC
th3[`(x:real^3)` ;` (u:real^3)`;`(y:real^3) `;]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`u:real^3`;`y:real^3`][
IN_ELIM_THM]
THEN EXISTS_TAC`&1/ &2 *(&1-(va:real^3)
dot (a2:real^3)+va
dot (a3:real^3))`
THEN EXISTS_TAC`&1/ &2 *((va:real^3)
dot (a2:real^3))+ &1/ &2`
THEN EXISTS_TAC`&1/ &2 *(--((va:real^3)
dot (a3:real^3)))`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 / &2 *
t1 + (&1 / &2 * t2 + &1 / &2) + &1 / &2 * t3 = &1/ &2*(t1+t2+t3)+ &1/ &2`; REAL_ARITH`&1/ &2 * &1 + &1/ &2= &1`;VECTOR_ARITH`(&1 / &2 *
t1) % x + (&1 / &2 * t2 + &1 / &2) % u + (&1 / &2 * t3) % y= &1/ &2 %(
t1 % x + t2 % u + t3 % y)+ &1/ &2 % u`;REAL_ARITH`(&1 - va
dot a3 + va
dot a2) + (va
dot a3) + --(va
dot a2) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
THEN EXPAND_TAC"v4"
THEN EXPAND_TAC"v3"
THEN EXPAND_TAC"vb"
THEN ONCE_REWRITE_TAC[
CROSS_SKEW; ]
THEN REWRITE_TAC[
CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`]
THEN MP_TAC(REAL_ARITH`&0< --(va
dot (a3:real^3))==> &0 < &1 / &2 * --(va
dot a3)`)
THEN RESA_TAC
THEN MATCH_MP_TAC(REAL_ARITH`&0<= (va
dot (a2:real^3))==> &0 < &1 / &2 * (va
dot a2)+ &1/ &2`)
THEN MRESA_TAC
cross_dot_fully_surrounded_ge_fan[`x:real^3`;`v:real^3`;`y:real^3`;`w:real^3`]
THEN POP_ASSUM MATCH_MP_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`y:real^3`]
THEN REWRITE_TAC[
azim]
THEN MATCH_MP_TAC(REAL_ARITH`
azim x v u y =
azim x v u w +
azim x v w y/\ &0<=
azim x v u w /\
azim x v u y <
pi ==>
azim x v w y <=
pi`)
THEN ASM_REWRITE_TAC[
azim]](*10*)](*9*)](*8*)](*7*)](*6*);(*5*)
EXISTS_TAC`y:real^3`
THEN REMOVE_THEN "YEU EM" (fun th-> REWRITE_TAC[SYM(
th)])
THEN ASM_REWRITE_TAC[]]]]]]);;
let exists_cut_rcone_fan_with_edge_run_fan=prove(
`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 s:real.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ &0<s /\ s<pi/ &2
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
(?t:real. &0< t /\ t< &1 /\
~(
rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(
sigma_fan x V E u w:real^3)) (
cos(s))
INTER aff_gt {x} {v, (&1-t)%u+t%w}={}))`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `u:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN DISJ_CASES_TAC(SET_RULE`
set_of_edge u V E = {w} \/ ~(
set_of_edge u V E = {w:real^3})`)
THENL[
MRESA_TAC
CARD_SING[`w:real^3`; `(
set_of_edge u V E):real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(
th)])
THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`;
rw_dart_fan;
INTER;
w_dart_fan;
wedge;
IN_ELIM_THM;]
THEN MRESA_TAC
inequality3_aim_in_convex_fan
[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;` w:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"NHO EM")
THEN MRESA_TAC
exists_point_inside_domain_cone_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `w:real^3`;`s:real`]
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
rw_dart_fan;
INTER;
w_dart_fan;
wedge;
IN_ELIM_THM;]
THEN REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v==>
azim x u w y<=
azim x u w (v:real^3)`)
THEN RESA_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"YEU EM")
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v/\ &0<
azim x u w y/\
azim x u w v <
pi /\
azim x u w v =
azim x u w y +
azim x u y v==> ~(
azim x u y (v:real^3)= &0)/\ &0<
azim x u y v/\
azim x u y v < pi/\ ~(
azim x u y (v:real^3)=
pi)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN REPEAT DISCH_TAC
THEN MRESA_TAC
NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`y:real^3`;`u:real^3`]
THEN SUBGOAL_THEN`~(
azim x v u (y:real^3)= &0)`ASSUME_TAC
THENL[STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[];
MP_TAC(REAL_ARITH`&0<=
azim x v u (y:real^3) /\ ~(
azim x v u y= &0)==> &0<
azim x v u y`)
THEN ASM_REWRITE_TAC[
azim] THEN STRIP_TAC
THEN MRESA_TAC
angle_is_smallpi_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN ABBREV_TAC`a1=(v-x):real^3`
THEN ABBREV_TAC`a2=(y-x):real^3`
THEN ABBREV_TAC`a3=(u-x) :real^3`
THEN ABBREV_TAC`a4=w-x:real^3`
THEN ABBREV_TAC`va=a2
cross a1:real^3`
THEN ABBREV_TAC`vb=a4
cross a3:real^3`
THEN ABBREV_TAC`v3=(va:real^3)
cross (vb:real^3)+(x:real^3)`
THEN MRESA_TAC
cut_in_angle_fan[`x:real^3`;`w:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN DISCH_TAC
THEN MRESA_TAC
scale_in_edges_fan[`(x:real^3)`;`(u:real^3)`;`(w:real^3)`;`(v3:real^3)`]
THEN EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`y:real^3`
THEN REMOVE_THEN "YEU EM" (fun th-> REWRITE_TAC[SYM(
th)])
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(REAL_ARITH`&0<t:real==> ~(t= &0)`) THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0<a:real==> ~(a= &0)`) THEN RESA_TAC
THEN MRESA_TAC
continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `t:real`)
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`(&1 - t) % u + t % w:real^3`]
THEN MRESAL_TAC
aff_gt_1_2_scale_fan[`x:real^3`;`v:real^3`;`v3:real^3`;`(&1 - t) % u + t % w:real^3`;`a:real`][VECTOR_ARITH`(&1 - t) % u + t % w - x = ((&1 - t) % u + t % w) - x`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN MRESAL_TAC
COLLINEAR_SPECIAL_SCALE[`a:real`;`(v3 - x):real^3`;`v-x:real^3`][VECTOR_ARITH`(&1 - t) % u + t % w - x = ((&1 - t) % u + t % w) - x`]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a1"
THEN ONCE_REWRITE_TAC[GSYM
COLLINEAR_3]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v3:real^3)`;`(v:real^3) `;]
THEN MRESAL_TAC
AFF_GT_1_2[`x:real^3`;`v3:real^3`;`v:real^3`][
IN_ELIM_THM;]
THEN EXPAND_TAC"v3"
THEN EXPAND_TAC"va"
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN REWRITE_TAC[
CROSS_LAGRANGE;]
THEN MP_TAC(REAL_ARITH`
azim x u w y <
azim x u w v /\
azim x u w v<
pi==>
azim x u w y<
pi`)
THEN RESA_TAC
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN STRIP_TAC
THEN MRESA_TAC
cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[
DOT_LNEG]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< --(vb
dot (a1:real^3))==> ~(--(vb
dot (a1:real^3))= &0)`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV `(--(vb
dot (a1:real^3)):real)`
THEN MRESA1_TAC
REAL_LT_INV `(--(vb
dot (a1:real^3)):real)`
THEN MRESA_TAC
REAL_LT_MUL [`inv(--(vb
dot (a1:real^3)):real)`;`--(vb
dot (a2:real^3)):real`]
THEN EXISTS_TAC`&1- inv (--(vb
dot (a1:real^3)))- inv (--(vb
dot a1)) * --(vb
dot a2)`
THEN EXISTS_TAC`inv (--(vb
dot (a1:real^3)))`
THEN EXISTS_TAC`inv (--(vb
dot a1)) * --(vb
dot (a2:real^3))`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1- T1 -T2 +T1 +T2 = &1`;VECTOR_ARITH`A%(--(B%X-C%Y)+Z)=(A*(--B))%X-(A*(--C))%Y+A%Z:real^3`]
THEN EXPAND_TAC"a1"
THEN EXPAND_TAC"a2"
THEN VECTOR_ARITH_TAC]]);;
let aff_gt_in_rw_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 y:real^3 s:real.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ &0<s /\ s<pi/ &2
/\ y
IN rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(v:real^3)) (
cos(s))
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==> aff_gt {x} {u,y}
SUBSET rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(
sigma_fan x V E u w:real^3)) (
cos(s)) `,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "CON")
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `u:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN DISJ_CASES_TAC(SET_RULE`
set_of_edge u V E = {w} \/ ~(
set_of_edge u V E = {w:real^3})`)
THENL[MRESA_TAC
CARD_SING[`w:real^3`; `(
set_of_edge u V E):real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(
th)])
THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
REMOVE_THEN "CON" MP_TAC
THEN ASM_REWRITE_TAC[
rw_dart_fan;
INTER;
SUBSET;
w_dart_fan;
wedge;
IN_ELIM_THM;]
THEN STRIP_TAC THEN GEN_TAC THEN STRIP_TAC
THEN MRESA_TAC
aff_gt_inter_aff_gt [`(x:real^3)`;`(u:real^3)`;`(y:real^3)`]
THEN MP_TAC(SET_RULE`aff_gt {x} {u, y} = aff_gt {x, u} {y}
INTER aff_gt {x, y} {u}
/\ x'
IN aff_gt {x} {u, y:real^3} ==> x'
IN aff_gt {x,u} {y}`) THEN RESA_TAC
THEN MRESA_TAC
aff_gt_imp_not_collinear[`x:real^3`;`y:real^3`;`u:real^3`; `x':real^3`]
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`w:real^3`;`x':real^3`;`y:real^3`;]
THEN MATCH_MP_TAC
conditions_in_rcone_fan
THEN EXISTS_TAC`y:real^3`
THEN ASM_REWRITE_TAC[]]);;
let exists_rw_dart_inter_aff_gt1_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 s:real.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ &0<s /\ s<pi/ &2
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
(?h:real. &0< h /\
(!t:real. &0< t /\ t< h==>
~(
rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(
sigma_fan x V E u w:real^3)) (
cos(s))
INTER aff_gt {x} {v, (&1-t)%u+t%w}={})
))`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `u:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN DISJ_CASES_TAC(SET_RULE`
set_of_edge u V E = {w} \/ ~(
set_of_edge u V E = {w:real^3})`)
THENL[ MRESA_TAC
CARD_SING[`w:real^3`; `(
set_of_edge u V E):real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(
th)])
THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
MRESA_TAC
exists_cut_rcone_fan_with_edge_run_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;`u:real^3`;`w:real^3`;`s:real`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`;
INTER;
IN_ELIM_THM;]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"OK") THEN DISCH_TAC
THEN USE_THEN "OK" MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[
rw_dart_fan;]
THEN ASM_REWRITE_TAC[
INTER;
w_dart_fan;
wedge;
IN_ELIM_THM;]
THEN STRIP_TAC
THEN EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`vt= (&1 - t':real) % u + t' % w :real^3`
THEN ABBREV_TAC`a1=(v-x):real^3`
THEN ABBREV_TAC`a2=vt-x:real^3`
THEN ABBREV_TAC`a3=(y-x):real^3`
THEN ABBREV_TAC`a4=(u-x) :real^3`
THEN ABBREV_TAC`va=a1
cross a2:real^3`
THEN ABBREV_TAC`vb=a3
cross a4:real^3`
THEN ABBREV_TAC`v3=(vb:real^3)
cross (va:real^3)+(x:real^3)`
THEN MP_TAC(REAL_ARITH`&0< t'/\ t'< t /\ t< &1==> ~(t'= &0) /\ t'< &1`) THEN RESA_TAC
THEN MRESA_TAC
in_aff_gt_1_2[`x:real^3`;`u:real^3`;`w:real^3 `;`t':real`]
THEN MRESA_TAC
aff_gt_inter_aff_gt [`(x:real^3)`;`(u:real^3)`;`(w:real^3)`]
THEN MP_TAC(SET_RULE`aff_gt {x} {u, w} = aff_gt {x, u} {w}
INTER aff_gt {x, w} {u}
/\ vt
IN aff_gt {x} {u, w:real^3} ==> vt
IN aff_gt {x,u} {w}`) THEN RESA_TAC
THEN MRESA_TAC
aff_gt_imp_not_collinear[`x:real^3`;`w:real^3`;`u:real^3`; `vt:real^3`]
THEN MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`v:real^3`;`vt:real^3`;`w:real^3`;]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
THEN RESA_TAC
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`vt:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN STRIP_TAC
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`y:real^3`;`vt:real^3`;`w:real^3`;]
THEN MP_TAC(REAL_ARITH`&0<
azim x u w y /\
azim x u w y<
azim x u w v /\
azim x u w v<
pi==>
azim x u w y<=
azim x u w v/\ ~(
azim x u w y = &0 \/
azim x u w y=
pi)`) THEN RESA_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,B,D,C}`]
THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`y:real^3`;`vt:real^3`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN STRIP_TAC
THEN MRESA_TAC
continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `t':real`)
THEN MRESA_TAC
cut_in_angle_fan[`x:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN RESA_TAC
THEN MRESA_TAC
aff_gt_in_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`s:real`]
THEN EXISTS_TAC`v3:real^3`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`aff_gt {x} {u, y}
SUBSET rw_dart_fan x V E (x,u,w,v) (
cos s)
/\ v3
IN aff_gt {x} {u, y} ==> v3
IN rw_dart_fan x V E (x,u,w,v) (
cos s)`)
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC
cut_in_angle_fan[`x:real^3`;`y:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`]
THEN POP_ASSUM MP_TAC
THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[
CROSS_SKEW]
THEN ASM_REWRITE_TAC[
CROSS_LNEG;
CROSS_RNEG]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_RNEG]
THEN ONCE_REWRITE_TAC[GSYM
CROSS_SKEW]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN POP_ASSUM MATCH_MP_TAC
THEN MRESA_TAC
sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"NHO EM")
THEN MP_TAC(REAL_ARITH`
azim x u w y<
azim x u w v/\ &0<
azim x u w y/\
azim x u w v <
pi /\
azim x u w v =
azim x u w y +
azim x u y v==> ~(
azim x u y (v:real^3)= &0 \/
azim x u y (v:real^3)=
pi)`)
THEN RESA_TAC
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`u:real^3`;`v:real^3`;`y:real^3`]
THEN MRESA_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0<=
azim x v u y /\ ~(
azim x v u y= &0)==> &0<
azim x v u y`)
THEN ASM_REWRITE_TAC[
azim] THEN RESA_TAC
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`]
THEN MRESAL_TAC
AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`][DE_MORGAN_THM]
THEN MP_TAC(REAL_ARITH`&0<=
azim x v u vt /\ ~(
azim x v u vt= &0)==> &0<
azim x v u vt`)
THEN ASM_REWRITE_TAC[
azim] THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0<t==> ~(t= &0)`) THEN RESA_TAC
THEN MRESA_TAC
continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `t:real`)
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`(&1-t) %u+ t%w:real^3`]
THEN MRESA_TAC
aff_gt_inter_aff_gt [`(x:real^3)`;`(v:real^3)`;`((&1-t) %u+ t%w:real^3)`]
THEN MP_TAC(SET_RULE`aff_gt {x} {v, (&1-t) %u+ t%w} = aff_gt {x, v} {(&1-t) %u+ t%w}
INTER aff_gt {x, (&1-t) %u+ t%w} {v}
/\ y
IN aff_gt {x} {v, (&1-t) %u+ t%w:real^3} ==> y
IN aff_gt {x,v} {(&1-t) %u+ t%w}`) THEN RESA_TAC
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`;`(&1-t) %u+ t%w:real^3`;]
THEN MRESA_TAC
inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`t:real`]
THEN MRESA_TAC
angle_is_smallpi_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MP_TAC(REAL_ARITH`
azim x v u w<
pi /\
azim x v u ((&1 - t) % u + t % w) <
azim x v u w
==>
azim x v u ((&1 - t) % u + t % w) <
pi`) THEN RESA_TAC
THEN ABBREV_TAC`vs= (&1 - t:real) % u + t % w :real^3`
THEN MRESA_TAC
in_aff_gt_1_2[`x:real^3`;`u:real^3`;`w:real^3 `;`t:real`]
THEN MP_TAC(SET_RULE`aff_gt {x} {u, w} = aff_gt {x, u} {w}
INTER aff_gt {x, w} {u}
/\ vs
IN aff_gt {x} {u, w:real^3} ==> vs
IN aff_gt {x,u} {w}`) THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t:real`
THEN MRESA1_TAC
REAL_LT_INV`t:real`
THEN MRESA_TAC
REAL_LT_MUL[`inv t:real`;`t':real`]
THEN MRESA_TAC
REAL_LT_LMUL[`inv t:real`;`t':real`;`t:real`]
THEN MRESA_TAC
AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`v:real^3`;`vs:real^3`;`w:real^3`;]
THEN REMOVE_THEN"NHO EM" MP_TAC
THEN DISCH_TAC THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`vs:real^3`]
THEN MRESA_TAC
AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
THEN MRESA_TAC
inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`vs:real^3`;`inv (t) * t':real`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM(
th)])
THEN STRIP_TAC
THEN MATCH_MP_TAC(SET_RULE`
azim x v u ((&1 - inv t * t') % u + (inv t * t') % vs) <
azim x v u vs /\
(&1 - inv t * t') % u + (inv t * t') % vs = vt ==>
azim x v u vt <
azim x v u vs`)
THEN ASM_REWRITE_TAC[]
THEN EXPAND_TAC"vs"
THEN ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - inv t * t') % u + (inv t * t') % ((&1 - t) % u + t % w)
= (&1 - (inv t * t) * t') % u + ((inv t * t) *t') % w`;REAL_ARITH`&1* A=A`]]);;
let there_exists_component_contain_aff_gt_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ fan80(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
==>
(?h:real. &0< h /\ (?y:real^3.
aff_gt {x} {v, (&1-h)%u+h%w}
SUBSET connected_component (yfan(x,V,E)) y ))`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"EM")
THEN USE_THEN "BE" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
` (v:real^3)`]
THEN MRESA_TAC
remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
` (u:real^3)`]
THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC
th `u:real^3` THEN MP_TAC (
th) THEN DISCH_THEN(LABEL_TAC"EM"))
THEN MRESA_TAC
fan_run_in_small_is_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM(fun th-> MRESA1_TAC
th `h/ &2`)
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0< h==> ~(h/ &2 = &0)/\ &0< h/ &2 /\ h/ &2 < h`) THEN RESA_TAC
THEN DISCH_TAC
THEN EXISTS_TAC`h/ &2 :real`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`&1/ &2 % v + &1/ &2 %((&1 - h / &2) % u + h / &2 % w:real^3)`
THEN MATCH_MP_TAC
CONNECTED_COMPONENT_MAXIMAL
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC
CONVEX_AFF_GT[`{x:real^3}`;`{v, (&1 - h / &2) % u + h / &2 % w:real^3}`]
THEN MRESA_TAC
properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN MRESA_TAC
continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `h/ &2:real`)
THEN MRESA_TAC
notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`(&1-h/ &2) %u+ h / &2 %w:real^3`]
THEN MRESA_TAC
th3[`(x:real^3)` ;` (v:real^3)`;`(&1 - h/ &2) % (u:real^3) + h / &2 % (w:real^3)`;]
THEN MRESAL_TAC
in_aff_gt_1_2[`x:real^3`;`v:real^3`;`(&1 - h / &2) % u + h / &2 % w:real^3 `;`&1/ &2:real`]
[REAL_ARITH`&1/ &2 < &1 /\ &0< &1/ &2 `; REAL_ARITH`&1 - &1/ &2 = &1/ &2` ]
THEN MATCH_MP_TAC
CONVEX_CONNECTED
THEN ASM_REWRITE_TAC[]);;
let connected_component_of_faces_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
FAN(x,V,E)/\ {v,u}
IN E /\ {u,w}
IN E
/\
sigma_fan x V E u w = v
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
/\ fan80(x,V,E)
==>
dart_leads_into x V E v u =
dart_leads_into x V E u w`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC "BE")
THEN DISCH_THEN(LABEL_TAC"con")
THEN USE_THEN "con" MP_TAC
THEN REWRITE_TAC[fan80]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`u:real^3`;`w:real^3`]
THEN MRESA_TAC
th [`v:real^3`;`u:real^3`])
THEN MRESA_TAC
exists_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"ANH")
THEN MRESA_TAC
exists_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`;` w:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"YEU")
THEN ABBREV_TAC`h00= min h' (pi/ &2) / &2 :real`
THEN MP_TAC(REAL_ARITH`&0< h' /\ &0<
pi /\ h00= min h' (pi/ &2) / &2 :real==> &0< h00 /\ h00 <
pi / &2`)
THEN REWRITE_TAC[
PI_WORKS]
THEN RESA_TAC
THEN MRESA_TAC
exists_rw_dart_inter_aff_gt1_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;` w:real^3`;`h00:real`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`]
THEN DISCH_THEN (LABEL_TAC"EM")
THEN MRESA_TAC
exists_rw_dart_inter_aff_gt_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;` w:real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`]
THEN DISCH_THEN (LABEL_TAC"NHIEU")
THEN MRESA_TAC
fan_run_in_small_is_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"HA")
THEN ABBREV_TAC`h1' = min h'' h''' / &2 :real`
THEN ABBREV_TAC`h1= min h1' h'''' / &2 :real`
THEN MP_TAC(REAL_ARITH`&0< h'' /\ &0 < h''' /\ h1'= min h'' h''' / &2 ==> &0< h1' /\ h1'< h'' /\ h1' < h'''`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&0< h1'/\ h1'< h'' /\ h1' < h''' /\ &0 < h'''' /\ h1= min h1' h'''' / &2 ==> &0< h1 /\ h1< h'' /\ h1 < h''' /\ h1< h''''`)
THEN RESA_TAC
THEN ABBREV_TAC`h2= min h (pi/ &2) / &2 :real`
THEN MP_TAC(REAL_ARITH`&0< h /\ &0<
pi /\ h2= min h (pi/ &2) / &2 :real==> &0< h2 /\ h2 <
pi / &2`)
THEN REWRITE_TAC[
PI_WORKS]
THEN RESA_TAC
THEN REMOVE_THEN "NHIEU" (fun th-> MRESAL1_TAC
th `h1:real`[
INTER;
IN_ELIM_THM])
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `h2:real`)
THEN MP_TAC(REAL_ARITH`&0< h2 /\ h2= min h (pi/ &2) / &2 :real==> h2 < h`)
THEN RESA_TAC
THEN USE_THEN "ANH" (fun
th -> MP_TAC(ISPECL[`h2:real`;`y:real^3`]
th))
THEN POP_ASSUM (fun th-> REWRITE_TAC[
th])
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN (LABEL_TAC"LAM")
THEN REMOVE_THEN "EM" (fun th-> MRESAL1_TAC
th `h1:real`[
INTER;
IN_ELIM_THM])
THEN MP_TAC(REAL_ARITH`&0< h00 /\ h00= min h' (pi/ &2) / &2 :real==> h00 < h'`)
THEN RESA_TAC
THEN USE_THEN "YEU" (fun
th -> MP_TAC(ISPECL[`h00:real`;`y':real^3`]
th))
THEN POP_ASSUM (fun th-> REWRITE_TAC[
th])
THEN RESA_TAC
THEN SUBGOAL_THEN `U=U':real^3->bool` ASSUME_TAC
THENL[
REMOVE_THEN "LAM" (fun th-> REWRITE_TAC[SYM(
th)])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(
th)])
THEN REWRITE_TAC[
CONNECTED_COMPONENT_EQ_EQ]
THEN MRESA_TAC
CONVEX_AFF_GT[`{x:real^3}`;`{v, (&1 - h1) % u + h1 % w:real^3}`]
THEN MRESA_TAC
CONVEX_CONNECTED[`aff_gt {x} {v, (&1 - h1) % u + h1 % w}:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
CONNECTED_IFF_CONNECTED_COMPONENT]
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC
th [`y:real^3`;`y':real^3`])
THEN REMOVE_THEN "HA" (fun th-> MRESA1_TAC
th `h1:real`)
THEN MRESA_TAC
CONNECTED_COMPONENT_OF_SUBSET[`aff_gt {x} {v, (&1 - h1) % u + h1 % w:real^3}:real^3-> bool`;`yfan (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):real^3->bool`;`y:real^3`;`y':real^3`]
THEN ASM_TAC THEN SET_TAC[];
SUBGOAL_THEN`
dart_leads_into x V E v u= U:real^3->bool` ASSUME_TAC
THENL[
REMOVE_ASSUM_TAC
THEN MATCH_MP_TAC
unique_dart_leads_into
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`h:real`
THEN ASM_REWRITE_TAC[];
SUBGOAL_THEN`
dart_leads_into x V E u w= U':real^3->bool` ASSUME_TAC
THENL[ MATCH_MP_TAC
unique_dart_leads_into
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`h':real`
THEN ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[]]]]);;
let exists_dartset_leads_into_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
FAN(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
/\ fan80(x,V,E)
/\ ds
IN face_set(
hypermap1_of_fanx (x,V,E))
==>
?s:real^3->bool. !y. y
IN ds==> s=
dart_leads_into x V E (pr2 y) (pr3 y)`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
hypermap_of_fan_rep[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x V E) (
d1_fan (x,V,E)))`]
THEN ASM_REWRITE_TAC[
face_set;
set_of_orbits;
IN_ELIM_THM]
THEN STRIP_TAC
THEN EXISTS_TAC`
dart_leads_into x V E (pr2 x') (pr3 x'):real^3->bool`
THEN ASM_REWRITE_TAC[
orbit_map;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`~(x'
IN d1_fan (x,V,E) )\/ (x'
IN d1_fan (x:real^3,V,E))`)
THENL[MRESA_TAC
id_power_enf_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool) `;`x':real^3#real^3#real^3#real^3` ;`n:num`;`(\t. res (t x V E) (
d1_fan (x,V,E)))`]
THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
SPEC_TAC (`y:real^3#real^3#real^3#real^3`,`y:real^3#real^3#real^3#real^3`)
THEN SPEC_TAC (`n:num`,`n:num`)
THEN INDUCT_TAC
THENL[
REWRITE_TAC[
POWER_0;
I_THM]
THEN SET_TAC[];
POP_ASSUM MP_TAC
THEN MRESA_TAC
into_domain_power_efn_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool) `;`n:num`;`(\t. res (t x V E) (
d1_fan (x,V,E)))`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th`x':real^3#real^3#real^3#real^3` )
THEN MRESA_TAC
into_domain_power_efn_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool) `;`SUC n:num`;`(\t. res (t x V E) (
d1_fan (x,V,E)))`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th`x':real^3#real^3#real^3#real^3` )
THEN ABBREV_TAC`y1=(
f1_fan x V E
POWER n) (x':real^3#real^3#real^3#real^3)`
THEN DISCH_THEN(LABEL_TAC "EM")
THEN ASM_REWRITE_TAC[
COM_POWER;
o_DEF]
THEN POP_ASSUM (fun th-> MRESAL1_TAC
th`y1:real^3#real^3#real^3#real^3`[ARITH_RULE`(n:num)>= 0`])
THEN REPEAT STRIP_TAC
THEN MRESA_TAC
into_domain1_power_efn_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`n:num`]
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`x':real^3#real^3#real^3#real^3`)
THEN MRESA_TAC
properties_of_f1_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`y:real^3#real^3#real^3#real^3`; `y1:real^3#real^3#real^3#real^3`]
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`u=pr2 (
f1_fan x V E y1):real^3`
THEN ABBREV_TAC`w=pr3 (
f1_fan x V E y1):real^3`
THEN ABBREV_TAC`v=
sigma_fan x V E u w:real^3`
THEN REMOVE_THEN "EM" MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN MRESA_TAC
connected_component_of_faces_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `w:real^3`]]]);;
let UNIQUE_DARTSET_LEADS_INTO_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
FAN(x,V,E)
/\ (!v. v
IN V==>
CARD (
set_of_edge v V E) >1)
/\ fan80(x,V,E)
/\ ds
IN face_set(
hypermap1_of_fanx (x,V,E))
/\ (!y. y
IN ds==> s=
dart_leads_into x V E (pr2 y) (pr3 y))
==>
dartset_leads_into_fan x V E ds= s`,
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
FACE_FAN_NOT_EMPTY[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
`ds:real^3#real^3#real^3#real^3->bool`]
THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y
IN A`]
THEN STRIP_TAC
THEN MRESA_TAC
DARTSET_LEADS_INTO_FAN[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
`ds:real^3#real^3#real^3#real^3->bool`]
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `y:real^3#real^3#real^3#real^3`)
THEN DISCH_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC
th `y:real^3#real^3#real^3#real^3`));;