1 needs "../formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl";;
2 needs "../formal_lp/hypermap/ssreflect/list_hypermap_iso-compiled.hl";;
4 (* Module More_list_hypermap*)
5 module More_list_hypermap = struct
13 open Hypermap_and_fan;;
16 let list_pairs2 = (GEN_ALL o define)
17 `list_pairs2 [] (hd:A) = [] /\
18 list_pairs2 [h] hd = [h,hd] /\
19 list_pairs2 (h1 :: (h2 :: t)) hd = (h1,h2) :: (list_pairs2 (h2 :: t) hd)`;;
21 (* Lemma size_list_pairs2 *)
22 let size_list_pairs2 = Sections.section_proof ["x";"s"]
23 `sizel (list_pairs2 s x) = sizel s`
25 (((THENL) (((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN elim) [ALL_TAC; ((move ["h"]) THEN ((THENL) case [ALL_TAC; ((move ["h2"]) THEN (move ["t"]))]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("list_pairs2", [list_pairs2]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("size_nil", [size_nil]))(fun tmp_arg1 -> (use_arg_then2 ("size_cons", [size_cons]))(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 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
28 (* Lemma nth_list_pairs2 *)
29 let nth_list_pairs2 = Sections.section_proof ["x0";"x";"s";"i"]
31 ==> nth (x0,x0) (list_pairs2 s x) i =
32 nth x0 s i, if i = sizel s - 1 then x else nth x0 s (i + 1)`
34 (((THENL) (((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN ((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN elim) [ALL_TAC; ((move ["h"]) THEN ((THENL) case [ALL_TAC; ((move ["h2"]) THEN (move ["t"]))]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("list_pairs2", [list_pairs2]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("size_nil", [size_nil]))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("size_cons", [size_cons]))(fun tmp_arg1 -> (use_arg_then2 ("ltn0", [ltn0]))(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 [] []))))) THEN ((TRY done_tac))));
35 (BETA_TAC THEN (move ["i"]) THEN (move ["i_lt"]));
36 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`i = 0`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
37 (((((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subnn", [subnn]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
38 ((THENL_FIRST) ((THENL) case [ALL_TAC; (move ["i"])]) (((((use_arg_then2 ("succnK", [succnK]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_SUC", [NOT_SUC]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
39 (((((use_arg_then2 ("ltSS", [ltSS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("succnK", [succnK]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqSS", [eqSS]))(thm_tac (new_rewrite [] []))))) THEN (move ["i_lt"]));
40 (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("succnK", [succnK]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
43 (* Lemma list_pairs_eq_list_pairs2 *)
44 let list_pairs_eq_list_pairs2 = Sections.section_proof ["s"]
45 `list_pairs s = list_pairs2 s (HD s)`
47 ((fun arg_tac -> (use_arg_then2 ("eq_from_nth", [eq_from_nth])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`HD s,HD s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac));
48 (((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs2", [size_list_pairs2]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["i"]) THEN (move ["i_lt"]));
49 ((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("nth_list_pairs2", [nth_list_pairs2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
50 (((fun arg_tac -> arg_tac (Arg_term (`i = _`))) (disch_tac [])) THEN case THEN (simp_tac));
51 (((((use_arg_then2 ("nth0", [nth0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq2.head_HD", [Seq2.head_HD]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
54 (* Lemma node_hypermap_of_list_explicit *)
55 let node_hypermap_of_list_explicit = Sections.section_proof ["L";"n";"d"]
57 MEM n (list_of_nodes L) /\ MEM d n
58 ==> node (hypermap_of_list L) d = set_of_list n`
60 ((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["eq"])) THEN (case THEN (move ["mem_n"])) THEN (move ["mem_d"]));
61 ((fun arg_tac -> arg_tac (Arg_term (`set_of_list n IN node_set (hypermap_of_list L)`))) (term_tac (have_gen_tac []ALL_TAC)));
62 (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN (done_tac));
63 ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["_"])) THEN (move ["eq2"]));
64 (((((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("lemma_node_identity", [lemma_node_identity])) (thm_tac apply_tac)));
65 (((((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
68 (* Lemma nodes_hypermap_of_list_all *)
69 let nodes_hypermap_of_list_all = Sections.section_proof ["L"]
71 ==> ALL (\n. ALL (\d. node (hypermap_of_list L) d = set_of_list n) n) (list_of_nodes L)`
73 ((repeat_tactic 1 9 (((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("node_hypermap_of_list_explicit", [node_hypermap_of_list_explicit])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["eq"]) THEN (move ["n"]) THEN (move ["mem_n"]) THEN (simp_tac) THEN (move ["d"]) THEN (move ["mem_d"]));
74 ((((fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (use_arg_then2 ("mem_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
77 (* Lemma face_hypermap_of_list_explicit *)
78 let face_hypermap_of_list_explicit = Sections.section_proof ["L";"f";"d"]
80 MEM f (list_of_faces L) /\ MEM d f
81 ==> face (hypermap_of_list L) d = set_of_list f`
83 ((BETA_TAC THEN (case THEN (move ["goodL"])) THEN (case THEN (move ["mem_f"])) THEN (move ["mem_d"])) THEN (((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"])));
84 ((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_d2"]))));
85 (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq2.mem_flatten", [Seq2.mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
86 (((((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((congr_tac (`_1 _2`)) THEN (simp_tac)));
87 ((((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
90 (* Lemma faces_hypermap_of_list_all *)
91 let faces_hypermap_of_list_all = Sections.section_proof ["L"]
93 ==> ALL (\f. ALL (\d. face (hypermap_of_list L) d = set_of_list f
94 /\ find_face L d = f) f) (list_of_faces L)`
96 ((repeat_tactic 1 9 (((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["goodL"]) THEN (move ["f"]) THEN (move ["mem_f"]) THEN (simp_tac) THEN (move ["d"]) THEN (move ["mem_d"]));
97 ((((fun arg_tac -> (use_arg_then2 ("face_hypermap_of_list_explicit", [face_hypermap_of_list_explicit])) (fun fst_arg -> (use_arg_then2 ("mem_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 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
98 ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN (clear_assumption "goodL") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])) THEN ((((use_arg_then2 ("goodL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
99 (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq2.mem_flatten", [Seq2.mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
101 let f_list_ext_table = (GEN_ALL o define)
102 `(f_list_ext_table L [] (first:A#A) <=> T)
103 /\ (f_list_ext_table L (CONS h1 (CONS h2 t)) first
104 <=> f_list_ext L h1 = h2
105 /\ inverse (f_list_ext L) h2 = h1
106 /\ f_list_ext_table L (CONS h2 t) first)
107 /\ (f_list_ext_table L [h1] first
108 <=> f_list_ext L h1 = first
109 /\ inverse (f_list_ext L) first = h1)`;;
111 (* Lemma f_list_ext_table_list_of_faces *)
112 let f_list_ext_table_list_of_faces = Sections.section_proof ["L"]
114 ==> ALL (\f. f_list_ext_table L f (HD f)) (list_of_faces L)`
116 ((BETA_TAC THEN (move ["goodL"])) THEN (((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"])));
117 (((((use_arg_then2 ("Seq2.ALL_all", [Seq2.ALL_all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["f"]) THEN (simp_tac) THEN (move ["mem_f"]));
118 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN ((move ["mem_d"]) THEN (move ["f_eq"])))))));
119 ((fun arg_tac -> arg_tac (Arg_term (`0 < sizel f`))) (term_tac (have_gen_tac [](move ["f_size"]))));
120 ((THENL_LAST) ((THENL) (((use_arg_then2 ("f_eq", [])) (disch_tac [])) THEN (clear_assumption "f_eq") THEN ((use_arg_then2 ("f", [])) (disch_tac [])) THEN (clear_assumption "f") THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) (((((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("gtS0", [gtS0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
121 (((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_empty", [find_face_empty]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
122 ((fun arg_tac -> arg_tac (Arg_term (`f = s1 ++ [x] ++ s2 /\ f_list_ext_table L s2 (HD f)
123 ==> f_list_ext_table L (x :: s2) (HD f)`))) (term_tac (have_gen_tac ["s2"; "s1"; "x"](move ["h"]))));
124 (BETA_TAC THEN (case THEN (move ["f_eq_cat"])));
125 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM x f`))) (term_tac (have_gen_tac [](move ["mem_xf"])))) (((((use_arg_then2 ("f_eq_cat", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_seq1", [mem_seq1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
126 ((fun arg_tac -> arg_tac (Arg_term (`find_face L x = f`))) (term_tac (have_gen_tac [](move ["fx_eq"]))));
127 ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (fun fst_arg -> (use_arg_then2 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
128 ((fun arg_tac -> arg_tac (Arg_term (`MEM x (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_x"]))));
129 (((use_arg_then2 ("dart_in_darts", [dart_in_darts])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac exists_tac)));
130 (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
131 ((((THENL) (((use_arg_then2 ("f_eq_cat", [])) (disch_tac [])) THEN (clear_assumption "f_eq_cat") THEN ((use_arg_then2 ("s2", [])) (disch_tac [])) THEN (clear_assumption "s2") THEN case) [ALL_TAC; ((move ["h2"]) THEN (move ["t"]))]) THEN (move ["f_eq_cat"]) THEN (move ["Ih"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("f_list_ext_table", [f_list_ext_table]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
132 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f_list_ext L x = (HD f)`))) (term_tac (have_gen_tac [](move ["eq"])))));
133 (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`inverse _`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_list_ext_inverse_works", [f_list_ext_inverse_works]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
134 ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fx_eq", []))(thm_tac (new_rewrite [] [])))));
135 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`x = last (HD f) f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
136 (((((use_arg_then2 ("Seq2.next_el_last", [Seq2.next_el_last]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
137 (((((use_arg_then2 ("f_eq_cat", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last_rcons", [last_rcons]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
138 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f_list_ext L x = h2`))) (term_tac (have_gen_tac [](move ["eq"])))));
139 (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`inverse _`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_list_ext_inverse_works", [f_list_ext_inverse_works]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
140 ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
141 ((((fun arg_tac -> (use_arg_then2 ("Seq2.next_el_rot_eq", [Seq2.next_el_rot_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`sizel s1`))) (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 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
142 (((((use_arg_then2 ("rot", [rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fx_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq_cat", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Seq2.next_el_hd_cons2", [Seq2.next_el_hd_cons2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
143 ((fun arg_tac -> arg_tac (Arg_term (`\k. ?s1 x s2. f = s1 ++ [x] ++ s2 /\ sizel s1 = k /\ f_list_ext_table L s2 (HD f)`))) (term_tac (set_tac "P")));
144 ((fun arg_tac -> arg_tac (Arg_term (`?n. P n`))) (term_tac (have_gen_tac []ALL_TAC)));
145 (((fun arg_tac -> arg_tac (Arg_term (`sizel f - 1`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("P_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
146 (((fun arg_tac -> arg_tac (Arg_term (`butlast f`))) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`last (HD f) f`))) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`[]`))) (term_tac exists_tac)));
147 (((((use_arg_then2 ("f_list_ext_table", [f_list_ext_table]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq2.size_butlast", [Seq2.size_butlast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq2.cat_butlast_last", [Seq2.cat_butlast_last]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
148 ((((use_arg_then2 ("MINIMAL", [MINIMAL]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["Pk"])) THEN (move ["Pm"]));
149 ((fun arg_tac -> arg_tac (Arg_term (`(minimal) P`))) (term_tac (set_tac "k")));
150 ((((use_arg_then2 ("Pk", [])) (disch_tac [])) THEN (clear_assumption "Pk") THEN BETA_TAC) THEN (((((use_arg_then2 ("P_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["s1"])) THEN (case THEN (move ["x"])) THEN (case THEN (move ["s2"])) THEN (case THEN (move ["f_eq"])) THEN (case THEN (move ["size_s1"])) THEN (move ["h_s2"])));
151 (((fun arg_tac -> arg_tac (Arg_term (`k = 0`))) (disch_eq_tac "k_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
152 ((((use_arg_then2 ("size_s1", [])) (disch_tac [])) THEN (clear_assumption "size_s1") THEN BETA_TAC) THEN (((((use_arg_then2 ("k_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] []))))) THEN (move ["s1_eq"])));
153 (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("s1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("f_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
154 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`P (k - 1)`))) (term_tac (have_gen_tac []ALL_TAC)))) (((((use_arg_then2 ("Pm", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("k_eq", [])) (disch_tac [])) THEN (clear_assumption "k_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
155 ((((use_arg_then2 ("P_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
156 (((fun arg_tac -> arg_tac (Arg_term (`butlast s1`))) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`last (HD f) s1`))) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`x :: s2`))) (term_tac exists_tac)));
157 ((((use_arg_then2 ("Seq2.size_butlast", [Seq2.size_butlast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("f_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)));
158 ((((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq2.cat_butlast_last", [Seq2.cat_butlast_last]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 1 (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_s1", []))(thm_tac (new_rewrite [] [])))));
159 ((((use_arg_then2 ("k_eq", [])) (disch_tac [])) THEN (clear_assumption "k_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
162 (* Section Contravening *)
163 Sections.begin_section "Contravening";;
164 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
165 (Sections.add_section_var (mk_var ("L", (`:((num)list)list`))));;
166 (Sections.add_section_var (mk_var ("h", (`:num->real^3`))));;
167 (Sections.add_section_var (mk_var ("g", (`:num#num->real^3#real^3`))));;
169 (* Lemma mem_list_of_darts_imp_mem_list_of_elements *)
170 let mem_list_of_darts_imp_mem_list_of_elements = Sections.section_proof ["a";"b"]
171 `MEM (a,b) (list_of_darts L)
172 ==> MEM a (list_of_elements L) /\ MEM b (list_of_elements L)`
174 ((((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["mem_l"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["mem_ab"]));
175 ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_undup", [mem_undup]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Seq2.mem_flatten", [Seq2.mem_flatten]))(thm_tac (new_rewrite [] []))))));
176 ((split_tac) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
178 (Sections.add_section_hyp "contrV" (`contravening V`));;
181 Sections.add_section_lemma "fanV" (Sections.section_proof []
182 `FAN (vec 0,V,ESTD V)`
184 ((((use_arg_then2 ("CONTRAVENING_FAN", [CONTRAVENING_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
188 Sections.begin_section "Norm";;
189 (Sections.add_section_hyp "bij_h" (`BIJ h (elements_of_list L) V`));;
191 (* Lemma contravening_norm_le *)
192 let contravening_norm_le = Sections.section_proof []
193 `ALL (\x. norm (h x) <= #2.52) (list_of_elements L)`
195 ((((use_arg_then2 ("bij_h", [])) (disch_tac [])) THEN (clear_assumption "bij_h") THEN BETA_TAC) THEN ((((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
196 (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in"])) THEN (move ["_"]) THEN (move ["_"]) THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("x_in", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["inV"]));
197 (((((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((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 (done_tac));
200 (* Lemma contravening_norm_ge *)
201 let contravening_norm_ge = Sections.section_proof []
202 `ALL (\x. &2 <= norm (h x)) (list_of_elements L)`
204 ((((use_arg_then2 ("bij_h", [])) (disch_tac [])) THEN (clear_assumption "bij_h") THEN BETA_TAC) THEN ((((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
205 ((BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in"])) THEN (move ["_"]) THEN (move ["_"]) THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("x_in", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["inV"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `&2 = #2.0`)))(thm_tac (new_rewrite [] [])))));
206 (((((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((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 (done_tac));
209 (* Finalization of the section Norm *)
210 let contravening_norm_le = Sections.finalize_theorem contravening_norm_le;;
211 let contravening_norm_ge = Sections.finalize_theorem contravening_norm_ge;;
212 Sections.end_section "Norm";;
214 (* Lemma contravening_dart_eq_dart1 *)
215 let contravening_dart_eq_dart1 = Sections.section_proof []
216 `dart_of_fan (V,ESTD V) = dart1_of_fan (V,ESTD V)`
218 ((((fun arg_tac -> (use_arg_then2 ("Add_triangle.fully_surrounded_dart_of_fan_eq", [Add_triangle.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)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
219 ((((use_arg_then2 ("CONTRAVENING_IMP_FULLY_SURROUNDED", [CONTRAVENING_IMP_FULLY_SURROUNDED]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
221 (Sections.add_section_hyp "goodL" (`good_list L`));;
222 (Sections.add_section_hyp "iso_g" (`hyp_iso g (hypermap_of_list L, hypermap_of_fan (V,ESTD V))`));;
225 Sections.add_section_lemma "mem_dartsL" (Sections.section_proof ["d"]
226 `MEM d (list_of_darts L) <=> d IN dart (hypermap_of_list L)`
228 (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
232 Sections.add_section_lemma "in_dartsH" (Sections.section_proof ["x"]
233 `x IN dart (hypermap_of_fan (V,ESTD V)) <=> x IN dart_of_fan (V,ESTD V)`
235 ((((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)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
238 (* Lemma contravening_dist_dart_ge *)
239 let contravening_dist_dart_ge = Sections.section_proof []
240 `ALL (\d. &2 <= dist (g d)) (list_of_darts L)`
242 (((((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_dartsL", []))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("iso_g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (simp_tac));
243 (((((use_arg_then2 ("in_dartsH", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (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 (match_mp_then snd_th MP_TAC))))) THEN (arith_tac) THEN (done_tac));
246 (* Lemma contravening_dist_dart_le *)
247 let contravening_dist_dart_le = Sections.section_proof []
248 `ALL (\d. dist (g d) <= #2.52) (list_of_darts L)`
250 (((((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_dartsL", []))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("iso_g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (simp_tac));
251 (((((use_arg_then2 ("in_dartsH", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (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 (match_mp_then snd_th MP_TAC))))) THEN (arith_tac) THEN (done_tac));
253 (Sections.add_section_hyp "bij_h" (`BIJ h (elements_of_list L) V`));;
254 (Sections.add_section_hyp "g_eq" (`g = \d. h (FST d), h (SND d)`));;
256 (* Lemma contravening_dist_not_dart *)
257 let contravening_dist_not_dart = Sections.section_proof ["s"]
258 `ALL (\d. MEM (FST d) (list_of_elements L) /\ MEM (SND d) (list_of_elements L)
259 /\ (FST d = SND d <=> F)) s
260 /\ ALL (\d. MEM d (list_of_darts L) <=> F) s
261 ==> ALL (\d. #2.52 <= dist (g d)) s`
263 ((repeat_tactic 1 9 (((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (simp_tac) THEN (case THEN (move ["h1"])) THEN (move ["h2"]) THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["mem_ds"]));
264 ((fun arg_tac -> arg_tac (Arg_term (`h a IN V /\ h b IN V /\ ~(h a = h b)`))) (term_tac (have_gen_tac [](move ["hab_in"]))));
265 ((((use_arg_then2 ("bij_h", [])) (disch_tac [])) THEN (clear_assumption "bij_h") THEN BETA_TAC) THEN (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in"])) THEN (move ["h_inj"]) THEN (move ["_"])));
266 (((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("mem_ds", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac) THEN (move ["h1"]));
267 ((repeat_tactic 1 9 (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("elements_of_list", [elements_of_list]))(fun tmp_arg1 -> (use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(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 (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
268 (((((use_arg_then2 ("implybF", [implybF]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("h_inj", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
269 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`~(g (a,b) IN dart_of_fan (V,ESTD V))`))) (term_tac (have_gen_tac [](move ["mem_gd"])))));
270 ((((use_arg_then2 ("mem_gd", [])) (disch_tac [])) THEN (clear_assumption "mem_gd") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (move ["ineq"])));
271 ((((use_arg_then2 ("contravening_dart_eq_dart1", [contravening_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Add_triangle.inE_eq_in_dart1", [Add_triangle.inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))));
272 (((((use_arg_then2 ("IN_ESTD", [IN_ESTD]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hab_in", []))(thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("ineq", [ineq])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
273 (((fun arg_tac -> (use_arg_then2 ("h2", [])) (fun fst_arg -> (use_arg_then2 ("mem_ds", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (move ["g_in"]));
274 ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("iso_g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("in_dartsH", []))(thm_tac (new_rewrite [] [])))));
275 ((((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("g_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC THEN (case THEN (case THEN ((move ["a'"]) THEN (move ["b'"]))))) THEN ((((use_arg_then2 ("mem_dartsL", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["ab'_in"]))));
276 (((((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["eq_a"]) THEN (move ["eq_b"]))));
277 ((((use_arg_then2 ("bij_h", [])) (disch_tac [])) THEN (clear_assumption "bij_h") THEN BETA_TAC) THEN (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (move ["inj"]) THEN (move ["_"])));
278 (((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("mem_ds", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac) THEN (move ["mem_ab"]));
279 (((fun arg_tac -> (use_arg_then2 ("mem_list_of_darts_imp_mem_list_of_elements", [mem_list_of_darts_imp_mem_list_of_elements])) (fun fst_arg -> (use_arg_then2 ("ab'_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["mem_ab'"]));
280 ((((fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (use_arg_then2 ("eq_a", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (use_arg_then2 ("eq_b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
283 (* Finalization of the section Contravening *)
284 let mem_list_of_darts_imp_mem_list_of_elements = Sections.finalize_theorem mem_list_of_darts_imp_mem_list_of_elements;;
285 let contravening_norm_le = Sections.finalize_theorem contravening_norm_le;;
286 let contravening_norm_ge = Sections.finalize_theorem contravening_norm_ge;;
287 let contravening_dart_eq_dart1 = Sections.finalize_theorem contravening_dart_eq_dart1;;
288 let contravening_dist_dart_ge = Sections.finalize_theorem contravening_dist_dart_ge;;
289 let contravening_dist_dart_le = Sections.finalize_theorem contravening_dist_dart_le;;
290 let contravening_dist_not_dart = Sections.finalize_theorem contravening_dist_not_dart;;
291 Sections.end_section "Contravening";;
293 (* Close the module *)