1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
5 (* Author: Alexey Solovyev *)
\r
6 (* Date: 2010-04-06 *)
\r
8 (* Equivalence of inverse_sigma_fan and inverse1_sigma_fan *)
\r
9 (* ========================================================================== *)
\r
11 (* TODO: results from this file should be added into introduction.hl *)
\r
13 (* flyspeck_needs "fan/fan_defs.hl";;*)
\r
15 module Fan_misc = struct
\r
18 let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse(extension_sigma_fan x V E v)`;;
\r
20 let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
\r
21 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
\r
22 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
\r
24 (* We are using this definition from tame_defs.hl *)
\r
25 let dart1_of_fan = new_definition
\r
26 `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) = { (v,w) | {v,w} IN E }`;;
\r
30 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
\r
33 let EXTENSION_SIGMA_FAN_EQ_RES = prove(`!x V E v. extension_sigma_fan x V E v = res (sigma_fan x V E v) (set_of_edge v V E)`,
\r
34 REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; Fan.extension_sigma_fan; Sphere.res] THEN
\r
38 (* ------------------------------------------------------------------------- *)
\r
39 (* inverse_sigma_fan_bis is the inverse of extension_sigma_fan *)
\r
40 (* ------------------------------------------------------------------------- *)
\r
42 let INVERSE_SIGMA_FAN = prove(`!x V E v. FAN (x,V,E)
\r
43 ==> (extension_sigma_fan x V E v) o (inverse_sigma_fan x V E v) = I
\r
44 /\ (inverse_sigma_fan x V E v) o (extension_sigma_fan x V E v) = I`,
\r
45 REPEAT GEN_TAC THEN REWRITE_TAC[inverse_sigma_fan] THEN
\r
47 MATCH_MP_TAC PERMUTES_INVERSES_o THEN
\r
48 DISJ_CASES_TAC (MESON[] `(?u:real^3. {v, u} IN E) \/ (!u. ~({v,u} IN E))`) THENL
\r
50 ASM_MESON_TAC[Fan.permutes_sigma_fan];
\r
54 EXISTS_TAC `{}:real^3->bool` THEN
\r
55 REWRITE_TAC[PERMUTES_EMPTY; FUN_EQ_THM] THEN
\r
56 X_GEN_TAC `w:real^3` THEN
\r
57 REWRITE_TAC[I_THM; Fan.extension_sigma_fan] THEN
\r
58 REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN
\r
63 let EXTENSION_SIGMA_FAN_INJECTIVE = prove(`!x V E v. FAN (x,V,E) ==> (!u w. extension_sigma_fan x V E v u = extension_sigma_fan x V E v w ==> u = w)`,
\r
65 DISCH_THEN (MP_TAC o (fun th -> CONJUNCT2 (SPEC `v:real^3` (MATCH_MP INVERSE_SIGMA_FAN th)))) THEN
\r
66 ABBREV_TAC `f = extension_sigma_fan (x:real^3) V E v` THEN
\r
67 ABBREV_TAC `g = inverse_sigma_fan (x:real^3) V E v` THEN
\r
68 REPEAT STRIP_TAC THEN
\r
69 POP_ASSUM (MP_TAC o (fun th -> AP_TERM `g:real^3->real^3` th)) THEN
\r
70 POP_ASSUM MP_TAC THEN
\r
71 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
\r
76 (* ------------------------------------------------------------------------- *)
\r
77 (* Connection between dart1_of_fan and set_of_edge *)
\r
78 (* ------------------------------------------------------------------------- *)
\r
80 let IN_SET_OF_EDGE = prove(`!V E (v:A) w. UNIONS E SUBSET V /\ (v, w) IN dart1_of_fan (V,E) ==> v IN V /\ w IN V /\ w IN set_of_edge v V E /\ v IN set_of_edge w V E`,
\r
81 REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
82 SUBGOAL_THEN `v:A IN V /\ w IN V` STRIP_ASSUME_TAC THENL
\r
84 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
\r
85 REWRITE_TAC[SUBSET; IN_UNIONS; dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
\r
86 STRIP_TAC THEN STRIP_TAC THEN
\r
87 FIRST_ASSUM (MP_TAC o SPEC `v:A`) THEN
\r
88 FIRST_X_ASSUM (MP_TAC o SPEC `w:A`) THEN
\r
89 ANTS_TAC THENL [EXISTS_TAC `{v':A,w'}` THEN ASM SET_TAC[]; ALL_TAC] THEN
\r
90 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
\r
91 ANTS_TAC THENL [EXISTS_TAC `{v':A,w'}` THEN ASM SET_TAC[]; ALL_TAC] THEN
\r
95 ASM_REWRITE_TAC[] THEN
\r
96 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
\r
97 REWRITE_TAC[dart1_of_fan; Fan.set_of_edge; IN_ELIM_THM; PAIR_EQ] THEN
\r
98 MESON_TAC[SET_RULE `{w, v} = {v, w}`]);;
\r
101 let FAN_IN_SET_OF_EDGE = prove(`!x V E v w. FAN (x,V,E) /\ {v,w} IN E ==> v IN V /\ w IN V /\ w IN set_of_edge v V E /\ v IN set_of_edge w V E`,
\r
102 REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
103 MATCH_MP_TAC IN_SET_OF_EDGE THEN
\r
104 REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
\r
107 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
\r
113 (* ------------------------------------------------------------------------- *)
\r
114 (* For fans, inverse1_sigma_fan and inverse_sigma_fan_bis are equivalent *)
\r
115 (* ------------------------------------------------------------------------- *)
\r
117 let INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN = prove(`!x V E v w. FAN (x,V,E) /\ {v, w} IN E ==>
\r
118 inverse1_sigma_fan x V E v w = inverse_sigma_fan x V E v w`,
\r
119 REPEAT GEN_TAC THEN
\r
121 FIRST_ASSUM (STRIP_ASSUME_TAC o fun th -> (MATCH_MP FAN_IN_SET_OF_EDGE th)) THEN
\r
122 MP_TAC (SPECL [`x:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] EXTENSION_SIGMA_FAN_INJECTIVE) THEN
\r
123 ASM_REWRITE_TAC[] THEN
\r
124 ABBREV_TAC `f = extension_sigma_fan (x:real^3) V E v` THEN
\r
125 ABBREV_TAC `g = inverse1_sigma_fan (x:real^3) V E v` THEN
\r
126 ABBREV_TAC `h = inverse_sigma_fan (x:real^3) V E v` THEN
\r
128 FIRST_X_ASSUM (MP_TAC o SPECL [`(g:real^3->real^3) w`; `(h:real^3->real^3) w`]) THEN
\r
129 ANTS_TAC THEN REWRITE_TAC[] THEN
\r
131 SUBGOAL_THEN `(f:real^3->real^3) ((g:real^3->real^3) w) = w` ASSUME_TAC THENL
\r
133 REMOVE_ASSUM THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
\r
134 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
\r
135 REWRITE_TAC[Fan.extension_sigma_fan] THEN
\r
136 MP_TAC (SPECL [`x:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] Fan.INVERSE1_SIGMA_FAN) THEN
\r
137 ASM_REWRITE_TAC[] THEN
\r
140 REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`)) THEN
\r
141 ASM_REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN
\r
143 ABBREV_TAC `u:real^3 = inverse1_sigma_fan x V E v w` THEN
\r
145 SUBGOAL_THEN `u:real^3 IN V` (fun th -> SIMP_TAC[th]) THEN
\r
146 ASM_MESON_TAC[FAN_IN_SET_OF_EDGE];
\r
150 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
\r
151 REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
\r
152 ASM_MESON_TAC[INVERSE_SIGMA_FAN; FUN_EQ_THM; I_THM; o_THM]);;
\r