flyspeck_needs "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";; (* Module Tame_lemmas*) module Tame_lemmas = struct let reflection = new_definition `reflection n x = x - (&2 * (x dot n) / (n dot n)) % n`;; let kcblrqc_ineq_tml = let has_id = (fun t -> not(intersect ["KCBLRQC"] (Ineq.flypaper_ids t) = [])) in let extra_ids = [ "3287695934"; "6988401556"; "3862621143 back"; "3862621143 front"; "3862621143 side"; "4240815464 a reduced"; "6944699408 a reduced"; "7043724150 a reduced v2"; ] in let idl = (filter (fun t -> has_id t or mem t.idv extra_ids) !Ineq.ineqs) in let tml = map (fun t -> t.ineq) idl in end_itlist (curry mk_conj) tml;; let kcblrqc_ineq_def = new_definition (mk_eq (`kcblrqc_ineq_def:bool`, kcblrqc_ineq_tml));; open Tame_general;; open Add_triangle;; open Fan_defs;; open Pack_defs;; open Hypermap;; open Hypermap_and_fan;; open Hypermap_iso;; open Ssrbool;; open Ssrnat;; (* Section Reflection *) Sections.begin_section "Reflection";; let VECTOR_MUL_RZERO = GEN_ALL VECTOR_MUL_RZERO;; let VECTOR_SUB_RZERO = GEN_ALL VECTOR_SUB_RZERO;; let VECTOR_SUB_RDISTRIB = GEN_ALL VECTOR_SUB_RDISTRIB;; let VECTOR_ADD_RDISTRIB = GEN_ALL VECTOR_ADD_RDISTRIB;; let VECTOR_SUB_LDISTRIB = GEN_ALL VECTOR_SUB_LDISTRIB;; (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`))));; (* Lemma reflection_at0 *) let reflection_at0 = Sections.section_proof ["x"] `reflection (vec 0) x = x` [ (((((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)); ];; (* Lemma reflection_eq *) let reflection_eq = Sections.section_proof ["n";"x"] `x dot n = &0 ==> reflection n x = x` [ ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (((((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)); ];; (* Lemma reflection_eq2 *) let reflection_eq2 = Sections.section_proof ["n";"x"] `reflection n x = x <=> x dot n = &0` [ ((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))); ((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))); ((((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 [] []))))); (((((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)); ];; (* Lemma reflection0 *) let reflection0 = Sections.section_proof ["n"] `reflection n (vec 0) = vec 0` [ (((((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)); ];; (* Lemma reflection_sub *) let reflection_sub = Sections.section_proof ["n";"x";"y"] `reflection n (x - y) = reflection n x - reflection n y` [ ((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 [] []))))); ((((use_arg_then2 ("VECTOR_SUB_RDISTRIB", [VECTOR_SUB_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac)); ];; (* Lemma reflection_add *) let reflection_add = Sections.section_proof ["n";"x";"y"] `reflection n (x + y) = reflection n x + reflection n y` [ ((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 [] []))))); ((((use_arg_then2 ("VECTOR_ADD_RDISTRIB", [VECTOR_ADD_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac)); ];; (* Lemma reflection_cmul *) let reflection_cmul = Sections.section_proof ["n";"c";"x"] `reflection n (c % x) = c % reflection n x` [ ((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 [] []))))); (((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)); ];; (* Lemma norm_reflection *) let norm_reflection = Sections.section_proof ["n";"x"] `norm (reflection n x) = norm x` [ ((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))); ((((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 [] []))))); ((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))); ((((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma dist_reflection *) let dist_reflection = Sections.section_proof ["n";"x";"y"] `dist (reflection n x, reflection n y) = dist (x, y)` [ (((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)); ];; (* Lemma dist_reflection_special *) let dist_reflection_special = Sections.section_proof ["n";"x";"y"] `y dot n = &0 ==> dist (reflection n x, y) = dist (x, y)` [ (((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)); ];; (* Lemma reflection_dot *) let reflection_dot = Sections.section_proof ["n";"x"] `(reflection n x) dot n = --(x dot n)` [ ((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))); ((((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 [] []))))); ((((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)); ];; (* Lemma dist_reflection_lemma *) let dist_reflection_lemma = Sections.section_proof ["n";"x";"y"] `dist (reflection n x, y) pow 2 = dist (x, y) pow 2 + &4 * ((y dot n) * (x dot n)) / (n dot n)` [ (((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 (((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)); (((use_arg_then2 ("Collect_geom.DIST_POW2_DOT", [Collect_geom.DIST_POW2_DOT]))(thm_tac (new_rewrite [] [])))); ((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] []))))))); ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`&2 * _`))) (term_tac (set_tac "a"))); ((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))); ((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 [] []))))))); (((((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)); ((((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 [] []))))); ((((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 [] [])))))); ((((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 [] [])))))); ((CONV_TAC REAL_FIELD) THEN (done_tac)); ];; (* Finalization of the section Reflection *) let reflection_at0 = Sections.finalize_theorem reflection_at0;; let reflection_eq = Sections.finalize_theorem reflection_eq;; let reflection_eq2 = Sections.finalize_theorem reflection_eq2;; let reflection0 = Sections.finalize_theorem reflection0;; let reflection_sub = Sections.finalize_theorem reflection_sub;; let reflection_add = Sections.finalize_theorem reflection_add;; let reflection_cmul = Sections.finalize_theorem reflection_cmul;; let norm_reflection = Sections.finalize_theorem norm_reflection;; let dist_reflection = Sections.finalize_theorem dist_reflection;; let dist_reflection_special = Sections.finalize_theorem dist_reflection_special;; let reflection_dot = Sections.finalize_theorem reflection_dot;; let dist_reflection_lemma = Sections.finalize_theorem dist_reflection_lemma;; Sections.end_section "Reflection";; (* Section Misc *) Sections.begin_section "Misc";; (Sections.add_section_type (mk_var ("v", (`:real^3`))));; (* Lemma delta_y_pos *) let delta_y_pos = Sections.section_proof ["v";"w";"w'"] `let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in &0 <= delta_y y1 y2 y3 y4 y5 y6` [ (repeat_tactic 1 9 ((CONV_TAC let_CONV))); ((((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 [] []))))))); ((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)); ((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)); ];; (* Lemma quadratic_root_plus_works *) let quadratic_root_plus_works = Sections.section_proof ["a";"b";"c"] `~(a = &0) /\ &0 <= b pow 2 - &4 * a * c ==> let x = quadratic_root_plus (a,b,c) in a * x pow 2 + b * x + c = &0` [ ((BETA_TAC THEN (move ["ineqs"])) THEN (CONV_TAC let_CONV)); (((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 [] [])))); ((((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma quadratic_root_plus_eq *) let quadratic_root_plus_eq = Sections.section_proof ["a";"b";"c";"x"] `&0 < a /\ &0 <= b pow 2 - &4 * a * c /\ &0 <= b /\ (a * x pow 2 + b * x + c = &0) /\ &0 <= x ==> quadratic_root_plus (a,b,c) = x` [ (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"])); ((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))); ((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)); ((((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 [] []))))); ((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"])); ((fun arg_tac -> arg_tac (Arg_term (`x <= &0`))) (term_tac (have_gen_tac []ALL_TAC))); (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))); ((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))); ((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 [] []))))); ((((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 [] []))))); ((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))); ((((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)); ((((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)); ((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))); (BETA_TAC THEN (move ["x_eq0"])); ((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))); ((((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 [] []))))); (((((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)); ];; (* Lemma quadratic_root_plus_gt_eq *) let quadratic_root_plus_gt_eq = Sections.section_proof ["a";"b";"c";"x";"y"] `&0 < a /\ &0 <= b pow 2 - &4 * a * c /\ a * x pow 2 + b * x + c = &0 /\ a * y pow 2 + b * y + c = &0 /\ y < x ==> quadratic_root_plus (a,b,c) = x` [ (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"])); ((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))); ((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"]))); ((((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 [] []))))))); (((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"])); ((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))); ((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))); ((((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)); ];; (* Lemma quadratic_root_plus_disc0_eq *) let quadratic_root_plus_disc0_eq = Sections.section_proof ["a";"b";"c";"x"] `~(a = &0) /\ b pow 2 - &4 * a * c = &0 /\ a * x pow 2 + b * x + c = &0 ==> quadratic_root_plus (a,b,c) = x` [ (BETA_TAC THEN (case THEN (move ["a_neq0"])) THEN (case THEN (move ["disc0"])) THEN (move ["x_root"])); (((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)); (((((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)); ((((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 [] []))))); (((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))); ((((((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)); ];; (* Finalization of the section Misc *) let delta_y_pos = Sections.finalize_theorem delta_y_pos;; let quadratic_root_plus_works = Sections.finalize_theorem quadratic_root_plus_works;; let quadratic_root_plus_eq = Sections.finalize_theorem quadratic_root_plus_eq;; let quadratic_root_plus_gt_eq = Sections.finalize_theorem quadratic_root_plus_gt_eq;; let quadratic_root_plus_disc0_eq = Sections.finalize_theorem quadratic_root_plus_disc0_eq;; Sections.end_section "Misc";; (* Section FullySurrounded *) Sections.begin_section "FullySurrounded";; (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));; (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));; (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));; (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));; (* Let dart1_eq *) Sections.add_section_lemma "dart1_eq" (Sections.section_proof [] `dart_of_fan (V,E) = dart1_of_fan (V,E)` [ ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ]);; (* Let confV *) Sections.add_section_lemma "confV" (Sections.section_proof [] `conforming_fan (vec 0,V,E)` [ ((((use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ]);; (* Let dartH *) Sections.add_section_lemma "dartH" (Sections.section_proof [] `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)` [ ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ]);; (* Lemma dart_leads_into_eq1 *) let dart_leads_into_eq1 = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> dart_leads_into (vec 0) V E v w = dartset_leads_into_fan (vec 0) V E (IMAGE (ext_dart (V,E)) (face (hypermap_of_fan (V,E)) (v,w)))` [ (BETA_TAC THEN (move ["vw_in"])); ((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"]))); ((fun arg_tac -> arg_tac (Arg_term (`ext_dart _`))) (term_tac (set_tac "h"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((((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))); ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f1"))); ((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 [] []))))); (((((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)); ((((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 [] [])))))); (((((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"])); ((((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma dart_leads_into_same *) let dart_leads_into_same = Sections.section_proof ["f";"v";"w";"x";"y"] `f IN face_set (hypermap_of_fan (V,E)) /\ (v,w) IN f /\ (x,y) IN f ==> dart_leads_into (vec 0) V E v w = dart_leads_into (vec 0) V E x y` [ (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"])))); ((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"])))); (((((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)); ((repeat_tactic 1 9 (((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((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)); ];; (* Lemma fully_surrounded_sol *) let fully_surrounded_sol = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> sol (vec 0) (dart_leads_into (vec 0) V E v w) = &2 * pi + sum (face (hypermap_of_fan (V,E)) (v,w)) (\x. azim_dart (V,E) x - pi)` [ (BETA_TAC THEN (move ["vw_in"])); ((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"]))); ((((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 [] [])))))); (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 ["_"])); ((((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 [] []))))); (((((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)); ((congr_tac (`_1 + _2:real`)) THEN ((TRY done_tac))); ((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"])))); (((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)); (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] [])))); (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))))); (((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((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"]))); (((((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)); ];; (* Lemma fully_surrounded_sum_sol *) let fully_surrounded_sum_sol = Sections.section_proof [] `sum (face_set (hypermap_of_fan (V,E))) (\f. sol (vec 0) (dartset_leads_into_fan (vec 0) V E (IMAGE (ext_dart (V,E)) f))) = &4 * pi` [ ((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"]))); ((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)); ((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 [] [])))))); ((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)); (BETA_TAC THEN (move ["f1"]) THEN (move ["f2"])); (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 [] []))))))); ((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))); ((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 [] [])))))); (((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)); ];; (* Lemma fully_surrounded_not_coplanar *) let fully_surrounded_not_coplanar = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> ~(coplanar {vec 0, v, w, sigma_fan (vec 0) V E v w})` [ ((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"]))); ((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"]))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'"))); ((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 [] []))))))); ((((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)); ((((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))); ((((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 [] []))))); ((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 [] []))))); ((((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)); ];; (* Lemma fully_surrounded_delta_pos *) let fully_surrounded_delta_pos = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let w' = sigma_fan (vec 0) V E v w in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in &0 < delta_y y1 y2 y3 y4 y5 y6` [ (((((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)))); ((((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 [] []))))))); (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom2.POS_EQ_NOT_COPLANANR)))(thm_tac (new_rewrite [] [])))); ((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))); (((use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (disch_tac [])) THEN (clear_assumption "fully_surrounded_not_coplanar") THEN (exact_tac)); ];; (* Lemma fully_surrounded_azim_eq_dih_y *) let fully_surrounded_azim_eq_dih_y = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let w' = sigma_fan (vec 0) V E v w in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in azim_dart (V,E) (v,w) = dih_y y1 y2 y3 y4 y5 y6` [ ((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"]))); ((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"]))); ((((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))); ((((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))); ((((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)))); ((((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))); ((repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma fully_surrounded_sol_eq_sol_y *) let fully_surrounded_sol_eq_sol_y = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3 ==> let w' = sigma_fan (vec 0) V E v w in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in sol (vec 0) (dart_leads_into (vec 0) V E v w) = sol_y y1 y2 y3 y4 y5 y6` [ ((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"]))); ((((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((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"]))))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((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"])))); ((((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)); ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"])))); (((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)); ((((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))); ((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)); ((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 [] [])))))); (((((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)); ];; (* Lemma tauVEF_alt1 *) let tauVEF_alt1 = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let f = face (hypermap_of_fan (V,E)) (v,w) in tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w) + (&2 - &(CARD f)) * sol0 - sol0 / pi * sum f (\x. azim_dart (V,E) x * (lmfun (h_dart x) - &1))` [ ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV)); ((((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))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((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"]))); (((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 [] [])))); (((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)); ];; (* Lemma tauVEF_alt2 *) let tauVEF_alt2 = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let f = face (hypermap_of_fan (V,E)) (v,w) in tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w) * (&1 + sol0 / pi) - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))` [ ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV)); ((((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))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((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"]))); ((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))); ((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))); ((((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)); ];; (* Lemma tauVEF_alt2_alt *) let tauVEF_alt2_alt = Sections.section_proof ["f"] `f IN face_set (hypermap_of_fan (V,E)) ==> tauVEF (V,E,f) = sol (vec 0) (dartset_leads_into_fan (vec 0) V E (IMAGE (ext_dart (V,E)) f)) * (&1 + sol0 / pi) - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))` [ (((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"]))); (((((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)); ];; (* Lemma tauVEF_alt3 *) let tauVEF_alt3 = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let f = face (hypermap_of_fan (V,E)) (v,w) in tauVEF (V,E,f) = sum f (\x. (&1 + sol0 / pi * (&1 - lmfun (h_dart x))) * azim_dart (V,E) x - pi - sol0) + &2 * (pi + sol0)` [ ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV)); ((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))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((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"]))); ((((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))); ((((use_arg_then2 ("Tame_defs.tauVEF", [Tame_defs.tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma sum_tauVEF_upper_bound *) let sum_tauVEF_upper_bound = Sections.section_proof [] `&12 <= scriptL V ==> sum (face_set (hypermap_of_fan (V,E))) (\f. tauVEF (V,E,f)) <= &4 * pi - &20 * sol0` [ ((((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"])); ((((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 [] []))))); (((use_arg_then2 ("fully_surrounded_sum_sol", [fully_surrounded_sum_sol]))(thm_tac (new_rewrite [] [])))); ((((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))); ((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 [] []))))))); ((((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)); ((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 [] []))))); (((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 [] [])))); ((((use_arg_then2 ("ineq", [])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma fully_surrounded_dot_cross *) let fully_surrounded_dot_cross = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> &0 < v dot (w cross sigma_fan (vec 0) V E v w)` [ (BETA_TAC THEN (move ["vw_in"])); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); ((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)); ((((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"]))); (((((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"])); (((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)))); ((((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 [] []))))); ((((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)); ((((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))); ((((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)); ];; (* Section BallAnnulus *) Sections.begin_section "BallAnnulus";; (Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));; (* Let v_norm *) Sections.add_section_lemma "v_norm" (Sections.section_proof ["v"] `v IN V ==> norm v <= &2 * h0 /\ &2 <= norm v` [ ((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)); ]);; (* Lemma fully_surrounded_lnazim *) let fully_surrounded_lnazim = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let w' = sigma_fan (vec 0) V E v w in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in azim_dart (V,E) (v,w) * lmfun (h_dart (v,w)) = lnazim y1 y2 y3 y4 y5 y6` [ ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV)))); ((((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 [] [])))))); (((((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)); ];; (* Lemma fully_surrounded_tau_eq_taum *) let fully_surrounded_tau_eq_taum = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3 ==> let w' = sigma_fan (vec 0) V E v w in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = taum y1 y2 y3 y4 y5 y6` [ ((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"]))); ((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"]))))); ((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 ["_"]))))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((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"])))); ((((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)); ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"])))); (((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)); ((((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 [] []))))); ((((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))); ((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)); ((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 [] [])))))); ((((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 [] []))))); (((((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)); ];; (* Finalization of the section BallAnnulus *) let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;; let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;; Sections.end_section "BallAnnulus";; (* Finalization of the section FullySurrounded *) let dart_leads_into_eq1 = Sections.finalize_theorem dart_leads_into_eq1;; let dart_leads_into_same = Sections.finalize_theorem dart_leads_into_same;; let fully_surrounded_sol = Sections.finalize_theorem fully_surrounded_sol;; let fully_surrounded_sum_sol = Sections.finalize_theorem fully_surrounded_sum_sol;; let fully_surrounded_not_coplanar = Sections.finalize_theorem fully_surrounded_not_coplanar;; let fully_surrounded_delta_pos = Sections.finalize_theorem fully_surrounded_delta_pos;; let fully_surrounded_azim_eq_dih_y = Sections.finalize_theorem fully_surrounded_azim_eq_dih_y;; let fully_surrounded_sol_eq_sol_y = Sections.finalize_theorem fully_surrounded_sol_eq_sol_y;; let tauVEF_alt1 = Sections.finalize_theorem tauVEF_alt1;; let tauVEF_alt2 = Sections.finalize_theorem tauVEF_alt2;; let tauVEF_alt2_alt = Sections.finalize_theorem tauVEF_alt2_alt;; let tauVEF_alt3 = Sections.finalize_theorem tauVEF_alt3;; let sum_tauVEF_upper_bound = Sections.finalize_theorem sum_tauVEF_upper_bound;; let fully_surrounded_dot_cross = Sections.finalize_theorem fully_surrounded_dot_cross;; let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;; let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;; Sections.end_section "FullySurrounded";; (* Section EnclosedTauq *) Sections.begin_section "EnclosedTauq";; (* Lemma taum_sym *) let taum_sym = Sections.section_proof ["y1";"y2";"y3";"y4";"y5";"y6"] `taum y1 y2 y3 y4 y5 y6 = taum y3 y2 y1 y6 y5 y4` [ ((use_arg_then2 ("Nonlinear_lemma.dih_y_sym", [Nonlinear_lemma.dih_y_sym])) (fun arg -> thm_tac MP_TAC arg THEN (move ["sym"]))); ((((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 [] [])))))); ((((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 [] []))))); ((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))); (((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(gsym_then (thm_tac (new_rewrite [] []))))); ((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))); (((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)); ];; (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));; (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));; (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));; (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));; (* Let dart1_eq *) Sections.add_section_lemma "dart1_eq" (Sections.section_proof [] `dart_of_fan (V,E) = dart1_of_fan (V,E)` [ ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ]);; (* Let dartH *) Sections.add_section_lemma "dartH" (Sections.section_proof [] `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)` [ ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ]);; (* Lemma fully_surrounded_enclosed *) let fully_surrounded_enclosed = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) ==> let w' = sigma_fan (vec 0) V E v w in let u = sigma_fan (vec 0) V E w' v in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist(w,w') in let y5 = dist(v,w') in let y6 = dist(v,w) in let y7 = norm u in let y8 = dist(w',u) in let y9 = dist(w,u) in dist (v,u) = enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9` [ ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV)))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "u"))); (((use_arg_then2 ("Enclosed.enclosed", [Enclosed.enclosed]))(thm_tac (new_rewrite [] [])))); ((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)); ((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 [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`muR _1 _2 _3 _4 _5 _6 _7 _8 _9`))) (term_tac (set_tac "p"))); (BETA_TAC THEN (move ["p0"])); (((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 [] [])))))))); (((((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)); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?a b c x. (p = \x. a * x pow 2 + b * x + c) /\ &0 < a /\ &0 <= b pow 2 - &4 * a * c /\ (p (dist (x, v) * dist (x, v)) = &0 /\ dist (x, v) < dist (u, v) \/ b pow 2 - &4 * a * c = &0)`))) (term_tac (have_gen_tac []ALL_TAC)))); (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"])); ((((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 [] []))))); ((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"])])); (((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)); (((((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)); ((((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))); ((((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 [] [])))))); ((((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))); (((((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)); ((((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 [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`ups_x _1 _2 _3`))) (term_tac (set_tac "a"))); ((fun arg_tac -> arg_tac (Arg_term (`cayleytr _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "b"))); ((fun arg_tac -> arg_tac (Arg_term (`cayleyR _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "c"))); ((fun arg_tac -> arg_tac (Arg_term (`reflection (w cross w') u`))) (term_tac (set_tac "y"))); (((((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)); (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))); ((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)); (((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)); (((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); ((((((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)); (split_tac); ((((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 [] []))))); ((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 [] [])))))); ((THENL_LAST) (repeat_tactic 1 9 (((use_arg_then2 ("REAL_LE_MUL", [REAL_LE_MUL]))(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac))); ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE delta_y_pos)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((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"])); ((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 [] [])))))); ((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 [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`u = w`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))); (((((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)); ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (DISJ2_TAC) THEN (DISJ2_TAC)); ((((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 [] []))))))); ((((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 [] [])))))); ((((use_arg_then2 ("DIMINDEX_3", [DIMINDEX_3]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); (((fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o CONJUNCT2) Collect_geom2.PER_SET4)))(thm_tac (new_rewrite [] [])))); ((((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 [] []))))); (((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)); ((DISJ1_TAC) THEN (split_tac)); ((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)); ((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 [] [])))))); (((((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)); ((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 [] []))))))); ((((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 [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`w cross w'`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`~(n = vec 0)`))) (term_tac (have_gen_tac [](move ["n0"])))); ((((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 [] [])))))); ((((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)); (((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"]))))); ((fun arg_tac -> arg_tac (Arg_term (`&4 * _`))) (term_tac (set_tac "t"))); ((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))); ((((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 [] []))))); ((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))); ((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))); ((((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((((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 [] []))))); ((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)); ((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] []))))); (BETA_TAC THEN (case THEN (move ["fan2"])) THEN (case THEN (move ["dart2_eq"])) THEN (move ["f_surr2"])); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < w' dot (w cross u)`))) (term_tac (have_gen_tac []ALL_TAC)))); (((((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)); (((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 [] [])))))))); (((((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)); ((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 ["_"]))))); ((((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)); ];; (Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));; (* Lemma fully_surrounded_tau_eq_tauq *) let fully_surrounded_tau_eq_tauq = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,E) /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 4 ==> let w' = sigma_fan (vec 0) V E v w in let u = sigma_fan (vec 0) V E w' v in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist(w,w') in let y5 = dist(v,w') in let y6 = dist(v,w) in let y7 = norm u in let y8 = dist(w',u) in let y9 = dist(w,u) in tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = tauq y1 y2 y3 y4 y5 y6 y7 y8 y9` [ ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card4"])))) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV)))); ((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)); ((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)); ((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))); (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "w2"))); ((fun arg_tac -> arg_tac (Arg_term (`_ INSERT E`))) (term_tac (set_tac "E2"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E2)`))) (term_tac (set_tac "H2"))); (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"])); ((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"])))); (((((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)); ((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))); ((((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E2_def", []))(thm_tac (new_rewrite [] []))))); ((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))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H"))); ((fun arg_tac -> arg_tac (Arg_term (`split_fan_face (V,E) (v,w) = (V,E2)`))) (term_tac (have_gen_tac [](move ["split_eq"])))); (((((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)); ((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 [] []))))))); (((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)))); ((((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)); ((((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)); (((((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)); ((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 [] []))))))); (((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)))); ((((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)); ((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)); ((((((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)); (((((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)); ];; (* Finalization of the section EnclosedTauq *) let taum_sym = Sections.finalize_theorem taum_sym;; let fully_surrounded_enclosed = Sections.finalize_theorem fully_surrounded_enclosed;; let fully_surrounded_tau_eq_tauq = Sections.finalize_theorem fully_surrounded_tau_eq_tauq;; Sections.end_section "EnclosedTauq";; (* Section Contravening *) Sections.begin_section "Contravening";; (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));; (Sections.add_section_hyp "contrV" (`contravening V`));; (* Let fanV *) Sections.add_section_lemma "fanV" (Sections.section_proof [] `FAN (vec 0,V,ESTD V)` [ (((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)); ]);; (* Let f_surr *) Sections.add_section_lemma "f_surr" (Sections.section_proof [] `fully_surrounded (V,ESTD V)` [ (((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)); ]);; (* Let dart1_eq *) Sections.add_section_lemma "dart1_eq" (Sections.section_proof [] `dart_of_fan (V,ESTD V) = dart1_of_fan (V,ESTD V)` [ (((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)); ]);; (* Lemma contravening_non_triangular_face_dist *) let contravening_non_triangular_face_dist = Sections.section_proof ["v";"w"] `v,w IN dart_of_fan (V,ESTD V) /\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in let y1 = norm v in let y2 = norm w in let y3 = norm w' in let y4 = dist (w,w') in let y5 = dist (v,w') in let y6 = dist (v,w) in (&2 <= y1 /\ y1 <= &2 * h0) /\ (&2 <= y2 /\ y2 <= &2 * h0) /\ (&2 <= y3 /\ y3 <= &2 * h0) /\ (&2 * h0 <= y4 /\ y4 <= &4 * h0) /\ (&2 <= y5 /\ y5 <= &2 * h0) /\ (&2 <= y6 /\ y6 <= &2 * h0)` [ ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV)))); ((((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 [] [])))))); ((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))); ((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"]))); ((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"]))); ((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"]))); ((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"]))); ((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"]))))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'"))); ((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 [] [])))))); (((((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)); ((((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 [] []))))))); ((((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)); (((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)); ((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))); (((((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)); ];; (* Section Ineqs *) Sections.begin_section "Ineqs";; (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));; (* Lemma non_triangular_face_azim_dart_bound *) let non_triangular_face_azim_dart_bound = Sections.section_proof ["d"] `d IN dart_of_fan (V,ESTD V) /\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) d) ==> #1.15 < azim_dart (V,ESTD V) d` [ (((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"])))); ((((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 [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'"))); (((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)); ((((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)); (((((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)); ((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))); (((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)); (((((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)); ];; (* Finalization of the section Ineqs *) let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;; Sections.end_section "Ineqs";; (* Finalization of the section Contravening *) let contravening_non_triangular_face_dist = Sections.finalize_theorem contravening_non_triangular_face_dist;; let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;; Sections.end_section "Contravening";; (* Close the module *) end;;