1 flyspeck_needs "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";;
3 (* Module Tame_lemmas*)
4 module Tame_lemmas = struct
6 let reflection = new_definition `reflection n x = x - (&2 * (x dot n) / (n dot n)) % n`;;
8 let has_id = (fun t -> not(intersect ["KCBLRQC"] (Ineq.flypaper_ids t) = [])) in
15 "4240815464 a reduced";
16 "6944699408 a reduced";
17 "7043724150 a reduced v2";
19 let idl = (filter (fun t -> has_id t or mem t.idv extra_ids) !Ineq.ineqs) in
20 let tml = map (fun t -> t.ineq) idl in
21 end_itlist (curry mk_conj) tml;;
22 let kcblrqc_ineq_def = new_definition
23 (mk_eq (`kcblrqc_ineq_def:bool`, kcblrqc_ineq_tml));;
29 open Hypermap_and_fan;;
34 (* Section Reflection *)
35 Sections.begin_section "Reflection";;
36 let VECTOR_MUL_RZERO = GEN_ALL VECTOR_MUL_RZERO;;
37 let VECTOR_SUB_RZERO = GEN_ALL VECTOR_SUB_RZERO;;
38 let VECTOR_SUB_RDISTRIB = GEN_ALL VECTOR_SUB_RDISTRIB;;
39 let VECTOR_ADD_RDISTRIB = GEN_ALL VECTOR_ADD_RDISTRIB;;
40 let VECTOR_SUB_LDISTRIB = GEN_ALL VECTOR_SUB_LDISTRIB;;
41 (Sections.add_section_type (mk_var ("x", (`:real^N`))); Sections.add_section_type (mk_var ("y", (`:real^N`))); Sections.add_section_type (mk_var ("d", (`:real^N`))));;
43 (* Lemma reflection_at0 *)
44 let reflection_at0 = Sections.section_proof ["x"]
45 `reflection (vec 0) x = x`
47 (((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_RZERO", [VECTOR_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_SUB_RZERO", [VECTOR_SUB_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
50 (* Lemma reflection_eq *)
51 let reflection_eq = Sections.section_proof ["n";"x"]
52 `x dot n = &0 ==> reflection n x = x`
54 ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
55 (((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_LZERO", [VECTOR_MUL_LZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_SUB_RZERO", [VECTOR_SUB_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
58 (* Lemma reflection_eq2 *)
59 let reflection_eq2 = Sections.section_proof ["n";"x"]
60 `reflection n x = x <=> x dot n = &0`
62 ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("reflection_at0", [reflection_at0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_RZERO", [DOT_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
63 ((THENL_LAST) (split_tac) (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("reflection_eq", [reflection_eq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (done_tac)));
64 ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (VECTOR_ARITH `!x y. x - y = x <=> y = vec 0`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_EQ_0", [VECTOR_MUL_EQ_0]))(thm_tac (new_rewrite [] [])))));
65 (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbF", [orbF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_INV_EQ_0", [REAL_INV_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
68 (* Lemma reflection0 *)
69 let reflection0 = Sections.section_proof ["n"]
70 `reflection n (vec 0) = vec 0`
72 (((((use_arg_then2 ("reflection_eq", [reflection_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("DOT_LZERO", [DOT_LZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
75 (* Lemma reflection_sub *)
76 let reflection_sub = Sections.section_proof ["n";"x";"y"]
77 `reflection n (x - y) = reflection n x - reflection n y`
79 ((repeat_tactic 1 9 (((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_ASSOC", [REAL_MUL_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_SUB_LDISTRIB", [REAL_SUB_LDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_SUB_RDISTRIB", [REAL_SUB_RDISTRIB]))(thm_tac (new_rewrite [] [])))));
80 ((((use_arg_then2 ("VECTOR_SUB_RDISTRIB", [VECTOR_SUB_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
83 (* Lemma reflection_add *)
84 let reflection_add = Sections.section_proof ["n";"x";"y"]
85 `reflection n (x + y) = reflection n x + reflection n y`
87 ((repeat_tactic 1 9 (((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DOT_LADD", [DOT_LADD]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_ASSOC", [REAL_MUL_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ADD_LDISTRIB", [REAL_ADD_LDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_RDISTRIB", [REAL_ADD_RDISTRIB]))(thm_tac (new_rewrite [] [])))));
88 ((((use_arg_then2 ("VECTOR_ADD_RDISTRIB", [VECTOR_ADD_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
91 (* Lemma reflection_cmul *)
92 let reflection_cmul = Sections.section_proof ["n";"c";"x"]
93 `reflection n (c % x) = c % reflection n x`
95 ((repeat_tactic 1 9 (((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("VECTOR_SUB_LDISTRIB", [VECTOR_SUB_LDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_ASSOC", [VECTOR_MUL_ASSOC]))(thm_tac (new_rewrite [] [])))));
96 (((repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_ASSOC", [REAL_MUL_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("REAL_MUL_SYM", [REAL_MUL_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
99 (* Lemma norm_reflection *)
100 let norm_reflection = Sections.section_proof ["n";"x"]
101 `norm (reflection n x) = norm x`
103 ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("reflection_at0", [reflection_at0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
104 ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NORM_EQ", [NORM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RSUB", [DOT_RSUB]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RMUL", [DOT_RMUL]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("DOT_SYM", [DOT_SYM])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
105 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`~(n dot n = &0)`))) (term_tac (have_gen_tac []ALL_TAC)))) ((CONV_TAC REAL_FIELD) THEN (done_tac)));
106 ((((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
109 (* Lemma dist_reflection *)
110 let dist_reflection = Sections.section_proof ["n";"x";"y"]
111 `dist (reflection n x, reflection n y) = dist (x, y)`
113 (((repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("reflection_sub", [reflection_sub]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("norm_reflection", [norm_reflection]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
116 (* Lemma dist_reflection_special *)
117 let dist_reflection_special = Sections.section_proof ["n";"x";"y"]
118 `y dot n = &0 ==> dist (reflection n x, y) = dist (x, y)`
120 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("reflection_eq", [reflection_eq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [1] [])))))) THEN (((use_arg_then2 ("dist_reflection", [dist_reflection]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
123 (* Lemma reflection_dot *)
124 let reflection_dot = Sections.section_proof ["n";"x"]
125 `(reflection n x) dot n = --(x dot n)`
127 ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RZERO", [DOT_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_NEG_0", [REAL_NEG_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
128 ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] [])))));
129 ((((use_arg_then2 ("n0", [])) (disch_tac [])) THEN (clear_assumption "n0") THEN BETA_TAC) THEN (((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (CONV_TAC REAL_FIELD) THEN (done_tac));
132 (* Lemma dist_reflection_lemma *)
133 let dist_reflection_lemma = Sections.section_proof ["n";"x";"y"]
134 `dist (reflection n x, y) pow 2
135 = dist (x, y) pow 2 + &4 * ((y dot n) * (x dot n)) / (n dot n)`
137 (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
138 (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("reflection_at0", [reflection_at0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_RZERO", [DOT_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_RID", [REAL_ADD_RID]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
139 (((use_arg_then2 ("Collect_geom.DIST_POW2_DOT", [Collect_geom.DIST_POW2_DOT]))(thm_tac (new_rewrite [] []))));
140 ((fun arg_tac -> arg_tac (Arg_term (`y = reflection n y + (&2 * (y dot n) / (n dot n)) % n`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [1; 2] [])))))));
141 ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
142 ((fun arg_tac -> arg_tac (Arg_term (`&2 * _`))) (term_tac (set_tac "a")));
143 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`b - (c + d) = (b - c) - d:real^N`))) (term_tac (have_gen_tac ["b"; "c"; "d"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((VECTOR_ARITH_TAC) THEN (done_tac)));
144 ((fun arg_tac -> arg_tac (Arg_term (`(b - c) dot (b - c) = b dot b + c dot c - &2 * (b dot c:real^N)`))) (term_tac (have_gen_tac ["b"; "c"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
145 (((((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RSUB", [DOT_RSUB]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("DOT_SYM", [DOT_SYM])) (fun fst_arg -> (use_arg_then2 ("b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("c", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
146 ((((use_arg_then2 ("Collect_geom.DIST_POW2_DOT", [Collect_geom.DIST_POW2_DOT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dist_reflection", [dist_reflection]))(thm_tac (new_rewrite [] [])))));
147 ((((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RMUL", [DOT_RMUL]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("reflection_dot", [reflection_dot]))(thm_tac (new_rewrite [] []))))));
148 ((((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("n0", [])) (disch_tac [])) THEN (clear_assumption "n0") THEN BETA_TAC) THEN (((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))));
149 ((CONV_TAC REAL_FIELD) THEN (done_tac));
152 (* Finalization of the section Reflection *)
153 let reflection_at0 = Sections.finalize_theorem reflection_at0;;
154 let reflection_eq = Sections.finalize_theorem reflection_eq;;
155 let reflection_eq2 = Sections.finalize_theorem reflection_eq2;;
156 let reflection0 = Sections.finalize_theorem reflection0;;
157 let reflection_sub = Sections.finalize_theorem reflection_sub;;
158 let reflection_add = Sections.finalize_theorem reflection_add;;
159 let reflection_cmul = Sections.finalize_theorem reflection_cmul;;
160 let norm_reflection = Sections.finalize_theorem norm_reflection;;
161 let dist_reflection = Sections.finalize_theorem dist_reflection;;
162 let dist_reflection_special = Sections.finalize_theorem dist_reflection_special;;
163 let reflection_dot = Sections.finalize_theorem reflection_dot;;
164 let dist_reflection_lemma = Sections.finalize_theorem dist_reflection_lemma;;
165 Sections.end_section "Reflection";;
168 Sections.begin_section "Misc";;
169 (Sections.add_section_type (mk_var ("v", (`:real^3`))));;
171 (* Lemma delta_y_pos *)
172 let delta_y_pos = Sections.section_proof ["v";"w";"w'"]
176 let y4 = dist (w,w') in
177 let y5 = dist (v,w') in
178 let y6 = dist (v,w) in
179 &0 <= delta_y y1 y2 y3 y4 y5 y6`
181 (repeat_tactic 1 9 ((CONV_TAC let_CONV)));
182 ((((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))));
183 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom.DELTA_POS_4POINTS", [Collect_geom.DELTA_POS_4POINTS])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
184 ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
187 (* Lemma quadratic_root_plus_works *)
188 let quadratic_root_plus_works = Sections.section_proof ["a";"b";"c"]
189 `~(a = &0) /\ &0 <= b pow 2 - &4 * a * c ==>
190 let x = quadratic_root_plus (a,b,c) in
191 a * x pow 2 + b * x + c = &0`
193 ((BETA_TAC THEN (move ["ineqs"])) THEN (CONV_TAC let_CONV));
194 (((fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))));
195 ((((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
198 (* Lemma quadratic_root_plus_eq *)
199 let quadratic_root_plus_eq = Sections.section_proof ["a";"b";"c";"x"]
200 `&0 < a /\ &0 <= b pow 2 - &4 * a * c
201 /\ &0 <= b /\ (a * x pow 2 + b * x + c = &0) /\ &0 <= x
202 ==> quadratic_root_plus (a,b,c) = x`
204 (BETA_TAC THEN (case THEN (move ["a_gt0"])) THEN (case THEN (move ["disc_ge0"])) THEN (case THEN (move ["b_ge0"])) THEN (case THEN (move ["x_root"])) THEN (move ["x_ge0"]));
205 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(a = &0)`))) (term_tac (have_gen_tac [](move ["a_neq"])))) ((((use_arg_then2 ("a_gt0", [])) (disch_tac [])) THEN (clear_assumption "a_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
206 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("a_neq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("disc_ge0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
207 ((((use_arg_then2 ("x_root", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_neq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))));
208 ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ALL_TAC]) THEN ((TRY done_tac)) THEN (move ["x_eq"]));
209 ((fun arg_tac -> arg_tac (Arg_term (`x <= &0`))) (term_tac (have_gen_tac []ALL_TAC)));
210 (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] []))));
211 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 <= u ==> (--b - u) / (&2 * a) <= &0`))) (term_tac (have_gen_tac ["u"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((((use_arg_then2 ("SQRT_POS_LE", [SQRT_POS_LE]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
212 ((BETA_TAC THEN (move ["u_ge0"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `!x. x <= &0 <=> ~(&0 < x)`)))(thm_tac (new_rewrite [] [])))));
213 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_POS_LT", [REAL_MUL_POS_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))));
214 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&0 < inv (&2 * a)`))) (term_tac (have_gen_tac [](move ["h1"])))) (((((use_arg_then2 ("REAL_LT_INV", [REAL_LT_INV]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("a_gt0", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)));
215 ((((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("real_lt", [real_lt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_LE_LT", [REAL_LE_LT]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
216 ((((use_arg_then2 ("b_ge0", [])) (disch_tac [])) THEN (clear_assumption "b_ge0") THEN ((use_arg_then2 ("u_ge0", [])) (disch_tac [])) THEN (clear_assumption "u_ge0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
217 ((THENL_FIRST) ((((use_arg_then2 ("REAL_LE_LT", [REAL_LE_LT]))(thm_tac (new_rewrite [] [])))) THEN case) ((((use_arg_then2 ("x_ge0", [])) (disch_tac [])) THEN (clear_assumption "x_ge0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
218 (BETA_TAC THEN (move ["x_eq0"]));
219 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`c = &0`))) (term_tac (have_gen_tac [](move ["c_eq0"])))) ((((use_arg_then2 ("x_root", [])) (disch_tac [])) THEN (clear_assumption "x_root") THEN BETA_TAC) THEN ((((use_arg_then2 ("x_eq0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ADD_LID", [REAL_ADD_LID]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
220 ((((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("c_eq0", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_SUB_RZERO", [REAL_SUB_RZERO]))(thm_tac (new_rewrite [] [])))));
221 (((((use_arg_then2 ("POW_2_SQRT", [POW_2_SQRT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_ADD_LINV", [REAL_ADD_LINV]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
224 (* Lemma quadratic_root_plus_gt_eq *)
225 let quadratic_root_plus_gt_eq = Sections.section_proof ["a";"b";"c";"x";"y"]
226 `&0 < a /\ &0 <= b pow 2 - &4 * a * c
227 /\ a * x pow 2 + b * x + c = &0 /\ a * y pow 2 + b * y + c = &0 /\ y < x
228 ==> quadratic_root_plus (a,b,c) = x`
230 (BETA_TAC THEN (case THEN (move ["a_gt0"])) THEN (case THEN (move ["disc_ge0"])) THEN (case THEN (move ["x_root"])) THEN (case THEN (move ["y_root"])) THEN (move ["y_lt_x"]));
231 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(a = &0)`))) (term_tac (have_gen_tac [](move ["a_neq"])))) ((((use_arg_then2 ("a_gt0", [])) (disch_tac [])) THEN (clear_assumption "a_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
232 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("a_neq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("disc_ge0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["h"])));
233 ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("x_root", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_root", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_neq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))))));
234 (((repeat_tactic 1 9 (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(gsym_then (thm_tac (new_rewrite [1] [])))))) THEN ALL_TAC THEN ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ALL_TAC]) THEN ((TRY done_tac)) THEN (move ["x_eq"]));
235 ((THENL_LAST) ((case THEN (move ["y_eq"])) THEN (((use_arg_then2 ("y_lt_x", [])) (disch_tac [])) THEN (clear_assumption "y_lt_x") THEN BETA_TAC) THEN ((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
236 ((THENL_FIRST) ((repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LT_RMUL_EQ", [REAL_LT_RMUL_EQ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("REAL_LT_INV", [REAL_LT_INV]))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(fun tmp_arg1 -> (use_arg_then2 ("a_gt0", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
237 ((((fun arg_tac -> (use_arg_then2 ("SQRT_POS_LE", [SQRT_POS_LE])) (fun fst_arg -> (use_arg_then2 ("disc_ge0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
240 (* Lemma quadratic_root_plus_disc0_eq *)
241 let quadratic_root_plus_disc0_eq = Sections.section_proof ["a";"b";"c";"x"]
242 `~(a = &0) /\ b pow 2 - &4 * a * c = &0
243 /\ a * x pow 2 + b * x + c = &0
244 ==> quadratic_root_plus (a,b,c) = x`
246 (BETA_TAC THEN (case THEN (move ["a_neq0"])) THEN (case THEN (move ["disc0"])) THEN (move ["x_root"]));
247 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("a_neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("c", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC));
248 (((((use_arg_then2 ("disc0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_REFL", [REAL_LE_REFL]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
249 ((((use_arg_then2 ("x_root", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_neq0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))));
250 (((repeat_tactic 1 9 (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ALL_TAC]) THEN ((TRY done_tac)));
251 ((((((use_arg_then2 ("disc0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SQRT_0", [SQRT_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_SUB_RZERO", [REAL_SUB_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_RID", [REAL_ADD_RID]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
254 (* Finalization of the section Misc *)
255 let delta_y_pos = Sections.finalize_theorem delta_y_pos;;
256 let quadratic_root_plus_works = Sections.finalize_theorem quadratic_root_plus_works;;
257 let quadratic_root_plus_eq = Sections.finalize_theorem quadratic_root_plus_eq;;
258 let quadratic_root_plus_gt_eq = Sections.finalize_theorem quadratic_root_plus_gt_eq;;
259 let quadratic_root_plus_disc0_eq = Sections.finalize_theorem quadratic_root_plus_disc0_eq;;
260 Sections.end_section "Misc";;
262 (* Section FullySurrounded *)
263 Sections.begin_section "FullySurrounded";;
264 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
265 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
266 (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
267 (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;
270 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
271 `dart_of_fan (V,E) = dart1_of_fan (V,E)`
273 ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
277 Sections.add_section_lemma "confV" (Sections.section_proof []
278 `conforming_fan (vec 0,V,E)`
280 ((((use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
284 Sections.add_section_lemma "dartH" (Sections.section_proof []
285 `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
287 ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
290 (* Lemma dart_leads_into_eq1 *)
291 let dart_leads_into_eq1 = Sections.section_proof ["v";"w"]
292 `v,w IN dart_of_fan (V,E)
293 ==> dart_leads_into (vec 0) V E v w
294 = dartset_leads_into_fan (vec 0) V E
295 (IMAGE (ext_dart (V,E)) (face (hypermap_of_fan (V,E)) (v,w)))`
297 (BETA_TAC THEN (move ["vw_in"]));
298 ((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
299 ((fun arg_tac -> arg_tac (Arg_term (`ext_dart _`))) (term_tac (set_tac "h")));
300 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
301 ((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
302 ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f1")));
303 ((THENL_ROT (-1)) (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Planarity.DARTSET_LEADS_INTO_FAN", [Planarity.DARTSET_LEADS_INTO_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`h (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
304 (((((use_arg_then2 ("h_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr2", [Fan.pr2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr3", [Fan.pr3]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
305 ((((use_arg_then2 ("fully_surrounded_imp_fan80", [fully_surrounded_imp_fan80]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))));
306 (((((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (simp_tac) THEN (move ["u"]) THEN (move ["uV"]));
307 ((((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
310 (* Lemma dart_leads_into_same *)
311 let dart_leads_into_same = Sections.section_proof ["f";"v";"w";"x";"y"]
312 `f IN face_set (hypermap_of_fan (V,E))
313 /\ (v,w) IN f /\ (x,y) IN f
314 ==> dart_leads_into (vec 0) V E v w = dart_leads_into (vec 0) V E x y`
316 (BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (case THEN (case THEN ((move ["a"]) THEN (move ["b"])))) THEN (case THEN (move ["ab_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (case THEN ((move ["vw_in"]) THEN (move ["xy_in"]))));
317 ((fun arg_tac -> arg_tac (Arg_term (`x,y IN dart_of_fan (V,E) /\ v,w IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["all_in"]))));
318 (((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
319 ((repeat_tactic 1 9 (((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
320 (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
323 (* Lemma fully_surrounded_sol *)
324 let fully_surrounded_sol = Sections.section_proof ["v";"w"]
325 `v,w IN dart_of_fan (V,E)
326 ==> sol (vec 0) (dart_leads_into (vec 0) V E v w)
327 = &2 * pi + sum (face (hypermap_of_fan (V,E)) (v,w)) (\x. azim_dart (V,E) x - pi)`
329 (BETA_TAC THEN (move ["vw_in"]));
330 ((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
331 ((((use_arg_then2 ("confV", [])) (disch_tac [])) THEN (clear_assumption "confV") THEN BETA_TAC) THEN ((((use_arg_then2 ("Conforming.conforming_fan", [Conforming.conforming_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE Conforming.conforming_solid_angle_fan)))(thm_tac (new_rewrite [] []))))));
332 (BETA_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["f_sol"])) THEN (move ["_"]));
333 ((((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_sol", []))(thm_tac (new_rewrite [] [])))));
334 (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
335 ((congr_tac (`_1 + _2:real`)) THEN ((TRY done_tac)));
336 ((fun arg_tac -> arg_tac (Arg_term (`x IN face (hypermap_of_fan (V,E)) (v,w) ==> x IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac ["x"](move ["in_face"]))));
337 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
338 (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] []))));
339 (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_face", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["x_in"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_face", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["y_in"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))));
340 (((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
341 (((use_arg_then2 ("SUM_EQ", [SUM_EQ])) (thm_tac apply_tac)) THEN (BETA_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_face", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["d_in"])));
342 (((((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr2", [Fan.pr2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr3", [Fan.pr3]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("azim_dart_eq_azim_fan", [azim_dart_eq_azim_fan]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
345 (* Lemma fully_surrounded_sum_sol *)
346 let fully_surrounded_sum_sol = Sections.section_proof []
347 `sum (face_set (hypermap_of_fan (V,E)))
348 (\f. sol (vec 0) (dartset_leads_into_fan (vec 0) V E (IMAGE (ext_dart (V,E)) f)))
351 ((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
352 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Conforming.SUM_SOL_IN_FACE_SET_EQ_4PI", [Conforming.SUM_SOL_IN_FACE_SET_EQ_4PI])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("confV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
353 ((THENL_ROT (-1)) ((((fun arg_tac -> (use_arg_then2 ("iso_face_set", [iso_face_set])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] []))))));
354 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("SUM_EQ", [SUM_EQ])) (thm_tac apply_tac)) THEN (move ["f"]) THEN (move ["_"]) THEN (simp_tac)) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
355 (BETA_TAC THEN (move ["f1"]) THEN (move ["f2"]));
356 (BETA_TAC THEN (case THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (case THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
357 ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("image_inj_gen", [image_inj_gen])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart (hypermap_of_fan (V,E))`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
358 ((repeat_tactic 1 9 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
359 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
362 (* Lemma fully_surrounded_not_coplanar *)
363 let fully_surrounded_not_coplanar = Sections.section_proof ["v";"w"]
364 `v,w IN dart_of_fan (V,E)
365 ==> ~(coplanar {vec 0, v, w, sigma_fan (vec 0) V E v w})`
367 ((BETA_TAC THEN (move ["vw_in"])) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
368 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["vw'_in"])));
369 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
370 ((fun arg_tac -> arg_tac (Arg_term (`{vec 0, v, w, w'} = {vec 0, w', v, w}`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
371 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o CONJUNCT2 o CONJUNCT2) Collect_geom.PER_SET3))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
372 ((((fun arg_tac -> (use_arg_then2 ("Planarity.properties_fully_surrounded", [Planarity.properties_fully_surrounded])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
373 ((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
374 ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_switch", [dart1_switch]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw'_in", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("AZIM_DART_POS", [AZIM_DART_POS])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
375 ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
378 (* Lemma fully_surrounded_delta_pos *)
379 let fully_surrounded_delta_pos = Sections.section_proof ["v";"w"]
380 `v,w IN dart_of_fan (V,E) ==>
381 let w' = sigma_fan (vec 0) V E v w in
385 let y4 = dist (w,w') in
386 let y5 = dist (v,w') in
387 let y6 = dist (v,w) in
388 &0 < delta_y y1 y2 y3 y4 y5 y6`
390 (((((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
391 ((((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))));
392 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom2.POS_EQ_NOT_COPLANANR)))(thm_tac (new_rewrite [] []))));
393 ((THENL_FIRST) ((((use_arg_then2 ("Ckqowsa_3_points.coplanar_eq_coplanar_alt", [Ckqowsa_3_points.coplanar_eq_coplanar_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("DIMINDEX_3", [DIMINDEX_3]))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
394 (((use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (disch_tac [])) THEN (clear_assumption "fully_surrounded_not_coplanar") THEN (exact_tac));
397 (* Lemma fully_surrounded_azim_eq_dih_y *)
398 let fully_surrounded_azim_eq_dih_y = Sections.section_proof ["v";"w"]
399 `v,w IN dart_of_fan (V,E) ==>
400 let w' = sigma_fan (vec 0) V E v w in
404 let y4 = dist (w,w') in
405 let y5 = dist (v,w') in
406 let y6 = dist (v,w) in
407 azim_dart (V,E) (v,w) = dih_y y1 y2 y3 y4 y5 y6`
409 ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
410 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1])) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["vw'_in"])));
411 ((((use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("AZIM_DIVH", [AZIM_DIVH]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("DART1_NOT_COLLINEAR", [DART1_NOT_COLLINEAR])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
412 ((((use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
413 ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
414 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE DIHV_EQ_DIH_Y)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("DART1_NOT_COLLINEAR", [DART1_NOT_COLLINEAR])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
415 ((repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
418 (* Lemma fully_surrounded_sol_eq_sol_y *)
419 let fully_surrounded_sol_eq_sol_y = Sections.section_proof ["v";"w"]
420 `v,w IN dart_of_fan (V,E) /\
421 CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3 ==>
422 let w' = sigma_fan (vec 0) V E v w in
426 let y4 = dist (w,w') in
427 let y5 = dist (v,w') in
428 let y6 = dist (v,w) in
429 sol (vec 0) (dart_leads_into (vec 0) V E v w) = sol_y y1 y2 y3 y4 y5 y6`
431 ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
432 ((((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
433 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE TRIANGULAR_FACE))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["f_eq"]) THEN (move ["eqs"])))));
434 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
435 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
436 ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E) /\ w,w' IN dart_of_fan (V,E) /\ w',v IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["all_in"]))));
437 ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 ((split_tac))) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`face H (v,w)`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
438 ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"]))));
439 (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ", [PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
440 ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("SUM_SING", [SUM_SING]))(fun tmp_arg1 -> (use_arg_then2 ("SUM_CLAUSES", [SUM_CLAUSES]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("FINITE_INSERT", [FINITE_INSERT]))(fun tmp_arg1 -> (use_arg_then2 ("FINITE_EMPTY", [FINITE_EMPTY]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
441 ((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("neqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("neqs", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
442 ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_azim_eq_dih_y)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))));
443 (((((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
446 (* Lemma tauVEF_alt1 *)
447 let tauVEF_alt1 = Sections.section_proof ["v";"w"]
448 `v,w IN dart_of_fan (V,E)
449 ==> let f = face (hypermap_of_fan (V,E)) (v,w) in
450 tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w)
451 + (&2 - &(CARD f)) * sol0
452 - sol0 / pi * sum f (\x. azim_dart (V,E) x * (lmfun (h_dart x) - &1))`
454 ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
455 ((((use_arg_then2 ("Tame_defs.tauVEF", [Tame_defs.tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
456 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
457 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_FINITE", [FACE_FINITE])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fin_f"])));
458 (((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `!a b c. a * (&1 + b * (&1 - c)) = a - b * (a * (c - &1))`)))(thm_tac (new_rewrite [] []))));
459 (((repeat_tactic 1 9 (((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SUM_LMUL", [SUM_LMUL]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
462 (* Lemma tauVEF_alt2 *)
463 let tauVEF_alt2 = Sections.section_proof ["v";"w"]
464 `v,w IN dart_of_fan (V,E)
465 ==> let f = face (hypermap_of_fan (V,E)) (v,w) in
466 tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w) * (&1 + sol0 / pi)
467 - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`
469 ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
470 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE tauVEF_alt1)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
471 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
472 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_FINITE", [FACE_FINITE])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fin_f"])));
473 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a * (b - &1) = a * b - a`))) (term_tac (have_gen_tac ["a"; "b"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
474 ((repeat_tactic 1 9 (((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
475 ((((use_arg_then2 ("PI_POS", [PI_POS])) (disch_tac [])) THEN (clear_assumption "PI_POS") THEN BETA_TAC) THEN (CONV_TAC REAL_FIELD) THEN (done_tac));
478 (* Lemma tauVEF_alt2_alt *)
479 let tauVEF_alt2_alt = Sections.section_proof ["f"]
480 `f IN face_set (hypermap_of_fan (V,E))
482 = sol (vec 0) (dartset_leads_into_fan (vec 0) V E (IMAGE (ext_dart (V,E)) f))
484 - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`
486 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (case THEN ((move ["v"]) THEN (move ["w"]))))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["vw_in"])) THEN (move ["f_eq"])));
487 (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE tauVEF_alt2)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
490 (* Lemma tauVEF_alt3 *)
491 let tauVEF_alt3 = Sections.section_proof ["v";"w"]
492 `v,w IN dart_of_fan (V,E)
493 ==> let f = face (hypermap_of_fan (V,E)) (v,w) in
494 tauVEF (V,E,f) = sum f (\x. (&1 + sol0 / pi * (&1 - lmfun (h_dart x)))
495 * azim_dart (V,E) x - pi - sol0) + &2 * (pi + sol0)`
497 ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
498 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a * x - b - c = x * a - (b + c):real`))) (term_tac (have_gen_tac ["a"; "x"; "b"; "c"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
499 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
500 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_FINITE", [FACE_FINITE])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fin_f"])));
501 ((((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`pi + sol0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
502 ((((use_arg_then2 ("Tame_defs.tauVEF", [Tame_defs.tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
505 (* Lemma sum_tauVEF_upper_bound *)
506 let sum_tauVEF_upper_bound = Sections.section_proof []
507 `&12 <= scriptL V ==>
508 sum (face_set (hypermap_of_fan (V,E))) (\f. tauVEF (V,E,f))
509 <= &4 * pi - &20 * sol0`
511 ((((fun arg_tac -> (use_arg_then2 ("SUM_EQ", [SUM_EQ])) (fun fst_arg -> (use_arg_then2 ("tauVEF_alt2_alt", [tauVEF_alt2_alt])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (move ["ineq"]));
512 ((((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_LMUL", [SUM_LMUL])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`sol0 / pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_RMUL", [SUM_RMUL])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&1 + sol0 / pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
513 (((use_arg_then2 ("fully_surrounded_sum_sol", [fully_surrounded_sum_sol]))(thm_tac (new_rewrite [] []))));
514 ((((use_arg_then2 ("Tame_defs.face_set_of_fan", [Tame_defs.face_set_of_fan]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Hrxefdm_tame.HRXEFDM_lemma1", [Hrxefdm_tame.HRXEFDM_lemma1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
515 ((fun arg_tac -> arg_tac (Arg_term (`(&4 * pi) * (&1 + s / pi) - s / pi * &2 * pi * v = &4 * pi - (&2 * v - &4) * s`))) (term_tac (have_gen_tac ["v"; "s"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
516 ((((use_arg_then2 ("PI_NZ", [PI_NZ])) (disch_tac [])) THEN (clear_assumption "PI_NZ") THEN BETA_TAC) THEN (CONV_TAC REAL_FIELD) THEN (done_tac));
517 ((repeat_tactic 1 9 (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_LADD", [REAL_LE_LADD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))));
518 (((fun arg_tac -> (use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE])) (fun fst_arg -> (use_arg_then2 ("sol0_POS", [sol0_POS])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))));
519 ((((use_arg_then2 ("ineq", [])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
522 (* Lemma fully_surrounded_dot_cross *)
523 let fully_surrounded_dot_cross = Sections.section_proof ["v";"w"]
524 `v,w IN dart_of_fan (V,E)
525 ==> &0 < v dot (w cross sigma_fan (vec 0) V E v w)`
527 (BETA_TAC THEN (move ["vw_in"]));
528 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
529 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Trigonometry.JBDNJJB", [Trigonometry.JBDNJJB])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
530 ((((use_arg_then2 ("Trigonometry2.re_eqvl", [Trigonometry2.re_eqvl]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["t"])) THEN (case THEN (move ["t_gt0"])));
531 (((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["sin_eq"]));
532 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < sin (azim_dart (V,E) (v,w))`))) (term_tac (have_gen_tac []ALL_TAC))));
533 ((((use_arg_then2 ("sin_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Trigonometry1.cross_triple", [Trigonometry1.cross_triple]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_SYM", [DOT_SYM]))(thm_tac (new_rewrite [] [])))));
534 ((((use_arg_then2 ("REAL_MUL_POS_LT", [REAL_MUL_POS_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("t_gt0", [])) (disch_tac [])) THEN (clear_assumption "t_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
535 ((((use_arg_then2 ("SIN_POS_PI", [SIN_POS_PI]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("AZIM_DART_POS", [AZIM_DART_POS]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
536 ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
539 (* Section BallAnnulus *)
540 Sections.begin_section "BallAnnulus";;
541 (Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));;
544 Sections.add_section_lemma "v_norm" (Sections.section_proof ["v"]
545 `v IN V ==> norm v <= &2 * h0 /\ &2 <= norm v`
547 ((in_tac ["subV"] false (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("subV", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((((use_arg_then2 ("Ckqowsa_3_points.in_ball_annulus", [Ckqowsa_3_points.in_ball_annulus]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
550 (* Lemma fully_surrounded_lnazim *)
551 let fully_surrounded_lnazim = Sections.section_proof ["v";"w"]
552 `v,w IN dart_of_fan (V,E) ==>
553 let w' = sigma_fan (vec 0) V E v w in
557 let y4 = dist (w,w') in
558 let y5 = dist (v,w') in
559 let y6 = dist (v,w) in
560 azim_dart (V,E) (v,w) * lmfun (h_dart (v,w)) = lnazim y1 y2 y3 y4 y5 y6`
562 ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
563 ((((use_arg_then2 ("Sphere.lnazim", [Sphere.lnazim]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_azim_eq_dih_y))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))));
564 (((((use_arg_then2 ("REAL_MUL_SYM", [REAL_MUL_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ly_EQ_lmfun", [ly_EQ_lmfun]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("v_norm", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
567 (* Lemma fully_surrounded_tau_eq_taum *)
568 let fully_surrounded_tau_eq_taum = Sections.section_proof ["v";"w"]
569 `v,w IN dart_of_fan (V,E)
570 /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3
571 ==> let w' = sigma_fan (vec 0) V E v w in
575 let y4 = dist (w,w') in
576 let y5 = dist (v,w') in
577 let y6 = dist (v,w) in
578 tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = taum y1 y2 y3 y4 y5 y6`
580 ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
581 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE TRIANGULAR_FACE))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["f_eq"]) THEN (move ["eqs"])))));
582 ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH"]) THEN (move ["_"])))));
583 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
584 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
585 ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E) /\ w,w' IN dart_of_fan (V,E) /\ w',v IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["all_in"]))));
586 ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 ((split_tac))) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`face H (v,w)`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
587 ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"]))));
588 (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ", [PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
589 ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE tauVEF_alt2)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
590 ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("SUM_SING", [SUM_SING]))(fun tmp_arg1 -> (use_arg_then2 ("SUM_CLAUSES", [SUM_CLAUSES]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("FINITE_INSERT", [FINITE_INSERT]))(fun tmp_arg1 -> (use_arg_then2 ("FINITE_EMPTY", [FINITE_EMPTY]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
591 ((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("neqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("neqs", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
592 ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_lnazim)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))));
593 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_sol_eq_sol_y)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
594 (((((use_arg_then2 ("Sphere.taum", [Sphere.taum]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sol0_over_pi_EQ_const1", [sol0_over_pi_EQ_const1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
597 (* Finalization of the section BallAnnulus *)
598 let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;;
599 let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;;
600 Sections.end_section "BallAnnulus";;
602 (* Finalization of the section FullySurrounded *)
603 let dart_leads_into_eq1 = Sections.finalize_theorem dart_leads_into_eq1;;
604 let dart_leads_into_same = Sections.finalize_theorem dart_leads_into_same;;
605 let fully_surrounded_sol = Sections.finalize_theorem fully_surrounded_sol;;
606 let fully_surrounded_sum_sol = Sections.finalize_theorem fully_surrounded_sum_sol;;
607 let fully_surrounded_not_coplanar = Sections.finalize_theorem fully_surrounded_not_coplanar;;
608 let fully_surrounded_delta_pos = Sections.finalize_theorem fully_surrounded_delta_pos;;
609 let fully_surrounded_azim_eq_dih_y = Sections.finalize_theorem fully_surrounded_azim_eq_dih_y;;
610 let fully_surrounded_sol_eq_sol_y = Sections.finalize_theorem fully_surrounded_sol_eq_sol_y;;
611 let tauVEF_alt1 = Sections.finalize_theorem tauVEF_alt1;;
612 let tauVEF_alt2 = Sections.finalize_theorem tauVEF_alt2;;
613 let tauVEF_alt2_alt = Sections.finalize_theorem tauVEF_alt2_alt;;
614 let tauVEF_alt3 = Sections.finalize_theorem tauVEF_alt3;;
615 let sum_tauVEF_upper_bound = Sections.finalize_theorem sum_tauVEF_upper_bound;;
616 let fully_surrounded_dot_cross = Sections.finalize_theorem fully_surrounded_dot_cross;;
617 let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;;
618 let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;;
619 Sections.end_section "FullySurrounded";;
621 (* Section EnclosedTauq *)
622 Sections.begin_section "EnclosedTauq";;
625 let taum_sym = Sections.section_proof ["y1";"y2";"y3";"y4";"y5";"y6"]
626 `taum y1 y2 y3 y4 y5 y6 = taum y3 y2 y1 y6 y5 y4`
628 ((use_arg_then2 ("Nonlinear_lemma.dih_y_sym", [Nonlinear_lemma.dih_y_sym])) (fun arg -> thm_tac MP_TAC arg THEN (move ["sym"])));
629 ((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Sphere.taum", [Sphere.taum]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Sphere.lnazim", [Sphere.lnazim]))(thm_tac (new_rewrite [] []))))));
630 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sym", [])) (fun fst_arg -> (use_arg_then2 ("y3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sym", [])) (fun fst_arg -> (use_arg_then2 ("y2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sym", [])) (fun fst_arg -> (use_arg_then2 ("y1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
631 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a + b + c - d = c + b + a - d:real`))) (term_tac (have_gen_tac ["a"; "b"; "c"; "d"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
632 (((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(gsym_then (thm_tac (new_rewrite [] [])))));
633 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a + b + c = c + b + a:real`))) (term_tac (have_gen_tac ["a"; "b"; "c"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
634 (((repeat_tactic 1 9 (((use_arg_then2 ("Sphere.lnazim", [Sphere.lnazim]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("Sphere.taum", [Sphere.taum]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
636 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
637 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
638 (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
639 (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;
642 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
643 `dart_of_fan (V,E) = dart1_of_fan (V,E)`
645 ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
649 Sections.add_section_lemma "dartH" (Sections.section_proof []
650 `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
652 ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
655 (* Lemma fully_surrounded_enclosed *)
656 let fully_surrounded_enclosed = Sections.section_proof ["v";"w"]
657 `v,w IN dart_of_fan (V,E)
658 ==> let w' = sigma_fan (vec 0) V E v w in
659 let u = sigma_fan (vec 0) V E w' v in
663 let y4 = dist(w,w') in
664 let y5 = dist(v,w') in
665 let y6 = dist(v,w) in
667 let y8 = dist(w',u) in
668 let y9 = dist(w,u) in
669 dist (v,u) = enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9`
671 ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV))));
672 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
673 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "u")));
674 (((use_arg_then2 ("Enclosed.enclosed", [Enclosed.enclosed]))(thm_tac (new_rewrite [] []))));
675 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE Collect_geom2.CAYLEYR_5POINTS))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("u", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
676 ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Mur.muR", [Mur.muR]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
677 ((fun arg_tac -> arg_tac (Arg_term (`muR _1 _2 _3 _4 _5 _6 _7 _8 _9`))) (term_tac (set_tac "p")));
678 (BETA_TAC THEN (move ["p0"]));
679 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`quadratic_root_plus (abc_of_quadratic p) = dist (u,v) pow 2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
680 (((((use_arg_then2 ("POW_2_SQRT", [POW_2_SQRT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("DIST_POS_LE", [DIST_POS_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
681 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?a b c x. (p = \x. a * x pow 2 + b * x + c)
682 /\ &0 < a /\ &0 <= b pow 2 - &4 * a * c
683 /\ (p (dist (x, v) * dist (x, v)) = &0 /\ dist (x, v) < dist (u, v)
684 \/ b pow 2 - &4 * a * c = &0)`))) (term_tac (have_gen_tac []ALL_TAC))));
685 (BETA_TAC THEN (case THEN (move ["a"])) THEN (case THEN (move ["b"])) THEN (case THEN (move ["c"])) THEN (case THEN (move ["x"])) THEN (case THEN (move ["p_eq"])) THEN (case THEN (move ["a_gt0"])) THEN (case THEN (move ["disc_ge0"])) THEN (move ["h"]));
686 ((((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Nonlinear_lemma.abc_quadratic", [Nonlinear_lemma.abc_quadratic]))(thm_tac (new_rewrite [] [])))));
687 ((THENL_ROT (-1)) ((THENL) (((use_arg_then2 ("h", [])) (disch_tac [])) THEN (clear_assumption "h") THEN case) [((case THEN (move ["px0"])) THEN (move ["dist_lt"])); (move ["disc0"])]));
688 (((use_arg_then2 ("quadratic_root_plus_disc0_eq", [quadratic_root_plus_disc0_eq])) (disch_tac [])) THEN (clear_assumption "quadratic_root_plus_disc0_eq") THEN (DISCH_THEN apply_tac));
689 (((((use_arg_then2 ("disc0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POS_NZ", [REAL_POS_NZ]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("p0", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
690 ((((use_arg_then2 ("quadratic_root_plus_gt_eq", [quadratic_root_plus_gt_eq])) (disch_tac [])) THEN (clear_assumption "quadratic_root_plus_gt_eq") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`dist (x, v) * dist (x, v)`))) (term_tac exists_tac)));
691 ((((use_arg_then2 ("a_gt0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("disc_ge0", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] []))))));
692 ((((use_arg_then2 ("px0", [])) (disch_tac [])) THEN (clear_assumption "px0") THEN ((use_arg_then2 ("p0", [])) (disch_tac [])) THEN (clear_assumption "p0") THEN BETA_TAC) THEN (((((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
693 (((((use_arg_then2 ("REAL_LT_SQUARE_ABS", [REAL_LT_SQUARE_ABS]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ABS_NORM", [REAL_ABS_NORM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
694 ((((use_arg_then2 ("p_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Mur.muRa)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.LEMMA50)))(thm_tac (new_rewrite [] [])))));
695 ((fun arg_tac -> arg_tac (Arg_term (`ups_x _1 _2 _3`))) (term_tac (set_tac "a")));
696 ((fun arg_tac -> arg_tac (Arg_term (`cayleytr _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "b")));
697 ((fun arg_tac -> arg_tac (Arg_term (`cayleyR _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "c")));
698 ((fun arg_tac -> arg_tac (Arg_term (`reflection (w cross w') u`))) (term_tac (set_tac "y")));
699 (((((use_arg_then2 ("a", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("b", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("c", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("y", [])) (term_tac exists_tac))) THEN (simp_tac)) THEN (split_tac));
700 (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] [])))));
701 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o let_RULE) Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
702 (((repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN apply_tac));
703 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Planarity.notcoplanar_imp_notcollinear_fan", [Planarity.notcoplanar_imp_notcollinear_fan])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
704 ((((((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.PER_SET3)))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
706 ((((use_arg_then2 ("b_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("c_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.DISCRIMINANT_OF_CAY)))(thm_tac (new_rewrite [] [])))));
707 ((repeat_tactic 1 9 (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("u", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
708 ((THENL_LAST) (repeat_tactic 1 9 (((use_arg_then2 ("REAL_LE_MUL", [REAL_LE_MUL]))(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
709 ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE delta_y_pos)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
710 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_card_face_alt", [fully_surrounded_card_face_alt])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (move ["card_f"]));
711 ((DISJ2_TAC) THEN ((((use_arg_then2 ("b_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("c_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.DISCRIMINANT_OF_CAY)))(thm_tac (new_rewrite [] []))))));
712 ((repeat_tactic 1 9 (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("u", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
713 ((fun arg_tac -> arg_tac (Arg_term (`u = w`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
714 (((((use_arg_then2 ("u_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE TRIANGULAR_FACE))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
715 ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (DISJ2_TAC) THEN (DISJ2_TAC));
716 ((((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))));
717 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE Collect_geom.POLFLZY)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ckqowsa_3_points.coplanar_eq_coplanar_alt", [Ckqowsa_3_points.coplanar_eq_coplanar_alt]))(gsym_then (thm_tac (new_rewrite [] []))))));
718 ((((use_arg_then2 ("DIMINDEX_3", [DIMINDEX_3]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
719 (((fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o CONJUNCT2) Collect_geom2.PER_SET4)))(thm_tac (new_rewrite [] []))));
720 ((((use_arg_then2 ("COPLANAR_SMALL", [COPLANAR_SMALL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_CLAUSES", [CARD_CLAUSES]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("FINITE_INSERT", [FINITE_INSERT]))(fun tmp_arg1 -> (use_arg_then2 ("FINITE_EMPTY", [FINITE_EMPTY]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
721 (((repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("Geomdetail.CARD3", [Geomdetail.CARD3]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
722 ((DISJ1_TAC) THEN (split_tac));
723 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE Collect_geom2.CAYLEYR_5POINTS))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
724 ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
725 (((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("norm_reflection", [norm_reflection]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist_reflection_special", [dist_reflection_special]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("DOT_CROSS_SELF", [DOT_CROSS_SELF]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
726 ((repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ABS_NORM", [REAL_ABS_NORM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("REAL_ABS_NORM", [REAL_ABS_NORM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`u - v:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LT_SQUARE_ABS", [REAL_LT_SQUARE_ABS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(gsym_then (thm_tac (new_rewrite [] [])))))));
727 ((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dist_reflection_lemma", [dist_reflection_lemma]))(thm_tac (new_rewrite [] [])))));
728 ((fun arg_tac -> arg_tac (Arg_term (`w cross w'`))) (term_tac (set_tac "n")));
729 ((fun arg_tac -> arg_tac (Arg_term (`~(n = vec 0)`))) (term_tac (have_gen_tac [](move ["n0"]))));
730 ((((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CROSS_EQ_0", [CROSS_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))));
731 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Planarity.notcoplanar_imp_notcollinear_fan", [Planarity.notcoplanar_imp_notcollinear_fan])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
732 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < v dot n /\ u dot n < &0`))) (term_tac (have_gen_tac [](move ["ineqs"])))));
733 ((fun arg_tac -> arg_tac (Arg_term (`&4 * _`))) (term_tac (set_tac "t")));
734 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`t < &0`))) (term_tac (have_gen_tac []ALL_TAC)))) ((arith_tac) THEN (done_tac)));
735 ((((use_arg_then2 ("t_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LT_NEG", [REAL_LT_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_NEG_0", [REAL_NEG_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_RMUL", [REAL_NEG_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(thm_tac (new_rewrite [] [])))));
736 ((THENL_FIRST) (((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_RMUL", [REAL_NEG_RMUL]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
737 ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_LT_INV", [REAL_LT_INV]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("DOT_POS_LT", [DOT_POS_LT]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
738 ((((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
739 ((((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fully_surrounded_dot_cross", [fully_surrounded_dot_cross]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
740 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
741 ((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
742 (BETA_TAC THEN (case THEN (move ["fan2"])) THEN (case THEN (move ["dart2_eq"])) THEN (move ["f_surr2"]));
743 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < w' dot (w cross u)`))) (term_tac (have_gen_tac []ALL_TAC))));
744 (((((use_arg_then2 ("CROSS_SKEW", [CROSS_SKEW]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_RNEG", [DOT_RNEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_SYM", [DOT_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Trigonometry1.cross_triple", [Trigonometry1.cross_triple]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_SYM", [DOT_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_GT0", [REAL_NEG_GT0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
745 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`u = sigma_fan (vec 0) V ({w,w'} INSERT E) w' w`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
746 (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_dot_cross", [fully_surrounded_dot_cross])) (fun fst_arg -> (use_arg_then2 ("fan2", [fan2])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
747 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE n_split_fan_face))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["eq1"]) THEN (move ["_"])))));
748 ((((use_arg_then2 ("eq1", [])) (disch_tac [])) THEN (clear_assumption "eq1") THEN BETA_TAC) THEN (((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("u_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
750 (Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));;
752 (* Lemma fully_surrounded_tau_eq_tauq *)
753 let fully_surrounded_tau_eq_tauq = Sections.section_proof ["v";"w"]
754 `v,w IN dart_of_fan (V,E)
755 /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 4
756 ==> let w' = sigma_fan (vec 0) V E v w in
757 let u = sigma_fan (vec 0) V E w' v in
761 let y4 = dist(w,w') in
762 let y5 = dist(v,w') in
763 let y6 = dist(v,w) in
765 let y8 = dist(w',u) in
766 let y9 = dist(w,u) in
767 tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = tauq y1 y2 y3 y4 y5 y6 y7 y8 y9`
769 ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card4"])))) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV))));
770 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
771 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE face_split_fan_face_explicit))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
772 ((THENL_FIRST) (((((use_arg_then2 ("card4", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 - 1 = 3`)))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) ((arith_tac) THEN (done_tac)));
773 (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] []))));
774 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
775 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "w2")));
776 ((fun arg_tac -> arg_tac (Arg_term (`_ INSERT E`))) (term_tac (set_tac "E2")));
777 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E2)`))) (term_tac (set_tac "H2")));
778 (BETA_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["cards_eq"])) THEN (case THEN (move ["in_face"])) THEN (move ["neqs"]) THEN (case THEN (move ["fan2"])) THEN (case THEN (move ["dart2_eq"])) THEN (move ["f_surr2"]));
779 ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E2) /\ w',w IN dart_of_fan (V,E2)`))) (term_tac (have_gen_tac [](move ["all_in2"]))));
780 (((((use_arg_then2 ("dart2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
781 ((THENL_FIRST) (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE tau_split_fan_face_add))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("card4", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
782 ((((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E2_def", []))(thm_tac (new_rewrite [] [])))));
783 ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_tau_eq_taum)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
784 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
785 ((fun arg_tac -> arg_tac (Arg_term (`split_fan_face (V,E) (v,w) = (V,E2)`))) (term_tac (have_gen_tac [](move ["split_eq"]))));
786 (((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E2_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
787 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E2 v w = w'`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
788 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`n_fan_pair (V,E2) (v,w) = n_fan_pair (V,E) (v,w)`))) (term_tac (have_gen_tac []ALL_TAC))));
789 ((((repeat_tactic 1 9 (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
790 ((((use_arg_then2 ("split_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("n_split_fan_face_eq1", [n_split_fan_face_eq1])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("neqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
791 (((((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
792 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E2 w' w = w2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
793 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`n_fan_pair (V,E2) (w',w) = n_fan_pair (V,E) (w',v)`))) (term_tac (have_gen_tac []ALL_TAC))));
794 ((((repeat_tactic 1 9 (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w2_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
795 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE n_split_fan_face))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
796 ((((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card4", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `3 < 4`)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
797 (((((use_arg_then2 ("Sphere.tauq", [Sphere.tauq]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("taum_sym", [taum_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm w2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
800 (* Finalization of the section EnclosedTauq *)
801 let taum_sym = Sections.finalize_theorem taum_sym;;
802 let fully_surrounded_enclosed = Sections.finalize_theorem fully_surrounded_enclosed;;
803 let fully_surrounded_tau_eq_tauq = Sections.finalize_theorem fully_surrounded_tau_eq_tauq;;
804 Sections.end_section "EnclosedTauq";;
806 (* Section Contravening *)
807 Sections.begin_section "Contravening";;
808 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
809 (Sections.add_section_hyp "contrV" (`contravening V`));;
812 Sections.add_section_lemma "fanV" (Sections.section_proof []
813 `FAN (vec 0,V,ESTD V)`
815 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_FAN", [CONTRAVENING_FAN])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
819 Sections.add_section_lemma "f_surr" (Sections.section_proof []
820 `fully_surrounded (V,ESTD V)`
822 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_IMP_FULLY_SURROUNDED", [CONTRAVENING_IMP_FULLY_SURROUNDED])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
826 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
827 `dart_of_fan (V,ESTD V) = dart1_of_fan (V,ESTD V)`
829 (((fun arg_tac -> (use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
832 (* Lemma contravening_non_triangular_face_dist *)
833 let contravening_non_triangular_face_dist = Sections.section_proof ["v";"w"]
834 `v,w IN dart_of_fan (V,ESTD V)
835 /\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) (v,w))
836 ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
840 let y4 = dist (w,w') in
841 let y5 = dist (v,w') in
842 let y6 = dist (v,w) in
843 (&2 <= y1 /\ y1 <= &2 * h0) /\
844 (&2 <= y2 /\ y2 <= &2 * h0) /\
845 (&2 <= y3 /\ y3 <= &2 * h0) /\
846 (&2 * h0 <= y4 /\ y4 <= &4 * h0) /\
847 (&2 <= y5 /\ y5 <= &2 * h0) /\
848 (&2 <= y6 /\ y6 <= &2 * h0)`
850 ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
851 ((((use_arg_then2 ("h0", [h0]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `&2 * #1.26 = #2.52 /\ &2 = #2.0`)))(thm_tac (new_rewrite [] []))))));
852 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["vw_in1"])))) ((((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
853 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_fan_inV", [sigma_fan_inV])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["w'_in"])));
854 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["vw'_in"])));
855 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_fan_not_fixed", [sigma_fan_not_fixed])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["w'_neq_w"])));
856 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_diag_not_in_dart", [fully_surrounded_diag_not_in_dart])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["not_diag"])));
857 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["v_in"]) THEN (move ["w_in"])))));
858 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
859 ((repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_DIST", [CONTRAVENING_DIST])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
860 (((((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 4 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_DART_DIST", [CONTRAVENING_DART_DIST])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))))) THEN (split_tac));
861 ((((use_arg_then2 ("not_diag", [])) (disch_tac [])) THEN (clear_assumption "not_diag") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))))));
862 ((((fun arg_tac -> (fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC) THEN ((simp_tac) THEN (((use_arg_then2 ("IN_ESTD", [IN_ESTD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_neq_w", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (arith_tac) THEN (done_tac));
863 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("DIST_TRIANGLE_LE", [DIST_TRIANGLE_LE])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
864 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&4 * #1.26 = #2.52 + #2.52`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
865 (((((use_arg_then2 ("REAL_LE_ADD2", [REAL_LE_ADD2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DIST_SYM", [DIST_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_DART_DIST", [CONTRAVENING_DART_DIST])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
869 Sections.begin_section "Ineqs";;
870 (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));;
872 (* Lemma non_triangular_face_azim_dart_bound *)
873 let non_triangular_face_azim_dart_bound = Sections.section_proof ["d"]
874 `d IN dart_of_fan (V,ESTD V)
875 /\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) d)
876 ==> #1.15 < azim_dart (V,ESTD V) d`
878 (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt3"]))));
879 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE CONTRAVENING_AZIM_DART_EQ_DIH_Y)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("real_gt", [real_gt]))(gsym_then (thm_tac (new_rewrite [] []))))));
880 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
881 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Tame_inequalities.DIH_Y_INEQ))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm v`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm w'`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dist (w,w')`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dist (v,w')`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dist (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC));
882 ((((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN ((((use_arg_then2 ("kcblrqc_ineq_def", [kcblrqc_ineq_def]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
883 (((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (ANTS_TAC));
884 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`#2.0 = &2 /\ #2.52 = &2 * h0 /\ #5.04 = &4 * h0`))) (term_tac (have_gen_tac [](move ["eqs"])))) ((((use_arg_then2 ("h0", [h0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
885 (((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 12 0 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE contravening_non_triangular_face_dist))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
886 (((((use_arg_then2 ("REAL_NOT_LT", [REAL_NOT_LT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_delta_pos))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
889 (* Finalization of the section Ineqs *)
890 let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;;
891 Sections.end_section "Ineqs";;
893 (* Finalization of the section Contravening *)
894 let contravening_non_triangular_face_dist = Sections.finalize_theorem contravening_non_triangular_face_dist;;
895 let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;;
896 Sections.end_section "Contravening";;
898 (* Close the module *)