needs "tame/ssreflect/seq2-compiled.hl";; needs "hypermap/hypermap.hl";; needs "fan/HypermapAndFan.hl";; needs "fan/hypermap_iso-compiled.hl";; (* Module List_hypermap*) module List_hypermap = struct open Ssrbool;; open Ssrnat;; open Seq;; open Seq2;; open Hypermap;; open Hypermap_and_fan;; parse_as_infix ("::", (12, "right"));; override_interface ("::", `CONS`);; make_overloadable "++" `:A -> A -> A`;; overload_interface ("++", `cat`);; let darts_k = new_definition `darts_k k H = {d:A | d IN dart H /\ CARD (face H d) = k}`;; let face_set_k = new_definition `face_set_k k (H:(A)hypermap) = {f | f IN face_set H /\ CARD f = k}`;; let list_pairs = new_definition `list_pairs list = zip list (rot 1 list)`;; let list_of_darts = new_definition `list_of_darts L = foldr (\list all. (list_pairs list) ++ all) [] L`;; let darts_of_list = new_definition `darts_of_list L = set_of_list (list_of_darts L)`;; let list_of_faces = new_definition `list_of_faces L = MAP list_pairs L`;; let faces_of_list = new_definition `faces_of_list L = MAP set_of_list (list_of_faces L)`;; let list_of_elements = new_definition `list_of_elements L = undup (flatten L)`;; let elements_of_list = new_definition `elements_of_list L = set_of_list (list_of_elements L)`;; let list_of_nodes = new_definition `list_of_nodes L = MAP (\x. filter (\d. FST d = x) (list_of_darts L)) (list_of_elements L)`;; let nodes_of_list = new_definition `nodes_of_list L = MAP set_of_list (list_of_nodes L)`;; let list_of_faces3 = new_definition `list_of_faces3 (L:((A)list)list) = filter (\f. LENGTH f = 3) (list_of_faces L)`;; let list_of_faces4 = new_definition `list_of_faces4 (L:((A)list)list) = filter (\f. LENGTH f = 4) (list_of_faces L)`;; let list_of_faces5 = new_definition `list_of_faces5 (L:((A)list)list) = filter (\f. LENGTH f = 5) (list_of_faces L)`;; let list_of_faces6 = new_definition `list_of_faces6 (L:((A)list)list) = filter (\f. LENGTH f = 6) (list_of_faces L)`;; let list_of_darts3 = new_definition `list_of_darts3 (L:((A)list)list) = flatten (list_of_faces3 L)`;; let list_of_darts4 = new_definition `list_of_darts4 (L:((A)list)list) = flatten (list_of_faces4 L)`;; let list_of_darts5 = new_definition `list_of_darts5 (L:((A)list)list) = flatten (list_of_faces5 L)`;; let list_of_darts6 = new_definition `list_of_darts6 (L:((A)list)list) = flatten (list_of_faces6 L)`;; let find_list = (GEN_ALL o define) `find_list [] x = [] /\ find_list (CONS h t) x = if (MEM x h) then h else find_list t x`;; let find_pair_list = (GEN_ALL o define) `find_pair_list [] d = [] /\ find_pair_list (CONS h t) d = if (MEM d (list_pairs h)) then h else find_pair_list t d`;; let find_face = new_definition `find_face L d = find_list (list_of_faces L) d`;; let f_list = new_definition `f_list L d = next_el (find_face L d) d`;; let e_list = new_definition `e_list d = (SND d, FST d)`;; let n_list = new_definition `n_list L d = e_list (prev_el (find_face L d) d)`;; let f_list_ext = new_definition `f_list_ext L = res (f_list L) (darts_of_list L)`;; let e_list_ext = new_definition `e_list_ext L = res (e_list) (darts_of_list L)`;; let n_list_ext = new_definition `n_list_ext L = res (n_list L) (darts_of_list L)`;; let hypermap_of_list = new_definition `hypermap_of_list (L:((A)list)list) = hypermap (darts_of_list L, e_list_ext L, n_list_ext L, f_list_ext L)`;; let good_list = new_definition `good_list L <=> uniq (list_of_darts L) /\ all (\l. ~(l = [])) L /\ (!d. MEM d (list_of_darts L) ==> MEM (SND d, FST d) (list_of_darts L))`;; let good_list_nodes = new_definition `good_list_nodes L <=> node_set (hypermap_of_list L) = set_of_list (nodes_of_list L)`;; (* Lemma list_pairs_empty *) let list_pairs_empty = Sections.section_proof ["s"] `list_pairs s = [] <=> s = []` [ (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("size1_zip", [size1_zip]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_of_darts_alt *) let list_of_darts_alt = Sections.section_proof ["L"] `list_of_darts L = flatten (list_of_faces L)` [ ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] []))))); (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma find_face_alt *) let find_face_alt = Sections.section_proof ["L";"d"] `find_face L d = list_pairs (find_pair_list L d)` [ ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] []))))); ((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]); (((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma mem_find_list *) let mem_find_list = Sections.section_proof ["x";"L"] `MEM x (flatten L) ==> MEM (find_list L x) L` [ ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"]))); (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) (BETA_TAC THEN (case THEN (((THENL) case [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); (move ["lt"])]) THEN (move ["xl"])))) (((((use_arg_then2 ("xl", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((fun arg_tac -> arg_tac (Arg_term (`MEM x h`))) (disch_eq_tac "xh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_find_face *) let mem_find_face = Sections.section_proof ["d";"L"] `MEM d (list_of_darts L) ==> MEM (find_face L d) (list_of_faces L)` [ ((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"])); (((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_list", [mem_find_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma find_list_empty *) let find_list_empty = Sections.section_proof ["d";"L"] `find_list L d = [] <=> ~(MEM d (flatten L))` [ ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))); (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))); (((fun arg_tac -> arg_tac (Arg_term (`MEM d h`))) (disch_eq_tac "dh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(h = [])`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("dh", [])) (disch_tac [])) THEN (clear_assumption "dh") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac)); ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN (move ["h1"]) THEN (move ["x"]))); ((((fun arg_tac -> arg_tac (Arg_term (`x = h`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((fun arg_tac ->(use_arg_then2 ("eq", []))(fun tmp_arg1 -> (use_arg_then2 ("h1", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac)); ];; (* Lemma mem_find_list_nonempty *) let mem_find_list_nonempty = Sections.section_proof ["x";"L"] `all (\l. ~(l = [])) L ==> (MEM x (flatten L) <=> MEM (find_list L x) L)` [ (((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["h1"])); ((THENL_FIRST) ((THENL) (split_tac) [ALL_TAC; (move ["h2"])]) (((use_arg_then2 ("mem_find_list", [mem_find_list])) (thm_tac apply_tac)) THEN (done_tac))); ((((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("find_list_empty", [find_list_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_find_face_nonempty *) let mem_find_face_nonempty = Sections.section_proof ["d";"L"] `all (\l. ~(l = [])) L ==> (MEM d (list_of_darts L) <=> MEM (find_face L d) (list_of_faces L))` [ (BETA_TAC THEN (move ["h1"])); ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_list_nonempty", [mem_find_list_nonempty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((in_tac ["h1"] true ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (simp_tac))) THEN ((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (move ["s"]))); ((((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["l_L"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs_empty", [list_pairs_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma e_list_ext_involution *) let e_list_ext_involution = Sections.section_proof ["L"] `good_list L ==> e_list_ext L o e_list_ext L = I` [ (((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h_uniq"])) THEN (case THEN (move ["all_n"])) THEN (move ["mem_snd"]) THEN (case THEN ((move ["x"]) THEN (move ["y"])))); ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_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 [] [])))))); (((fun arg_tac -> arg_tac (Arg_term (`MEM (x,y) _`))) (disch_eq_tac "xy_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((fun arg_tac -> (use_arg_then2 ("mem_snd", [])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac)) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((((use_arg_then2 ("xy_in", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; let INVERSE_EXISTS_IMP_BIJECTIVE = prove(`!(f:A->B) g. f o g = I /\ g o f = I ==> (!y. ?!x. f x = y)`, REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN EXISTS_TAC `(g:B->A) y` THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM (MP_TAC o AP_TERM `g:B->A`) THEN ASM_REWRITE_TAC[]);; (* Lemma e_list_ext_permutes_darts *) let e_list_ext_permutes_darts = Sections.section_proof ["L"] `good_list L ==> (e_list_ext L) permutes (darts_of_list L)` [ (((((use_arg_then2 ("permutes", [permutes]))(thm_tac (new_rewrite [] [])))) THEN (move ["good_l"])) THEN (split_tac)); ((BETA_TAC THEN (move ["x"]) THEN (move ["x_n"])) THEN ((((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_n", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((use_arg_then2 ("INVERSE_EXISTS_IMP_BIJECTIVE", [INVERSE_EXISTS_IMP_BIJECTIVE])) (thm_tac apply_tac)); (((fun arg_tac -> arg_tac (Arg_term (`e_list_ext L`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("ETA_AX", [ETA_AX]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma dart_in_darts *) let dart_in_darts = Sections.section_proof ["d";"l";"L"] `MEM d (list_pairs l) /\ MEM l L ==> MEM d (list_of_darts L)` [ (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"])); (((fun arg_tac -> arg_tac (Arg_term (`list_pairs l`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma mem_find_pair_list *) let mem_find_pair_list = Sections.section_proof ["d";"L"] `MEM d (list_of_darts L) ==> MEM (find_pair_list L d) L` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Ih", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma dart_in_find_pair_list *) let dart_in_find_pair_list = Sections.section_proof ["d";"L"] `MEM d (list_of_darts L) <=> MEM d (list_pairs (find_pair_list L d))` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma dart_in_face *) let dart_in_face = Sections.section_proof ["d";"L"] `MEM d (list_of_darts L) <=> MEM d (find_face L d)` [ (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_imp_unique_list *) let uniq_imp_unique_list = Sections.section_proof ["l1";"l2";"d";"L"] `uniq (list_of_darts L) /\ MEM l1 L /\ MEM l2 L /\ MEM d (list_pairs l1) /\ MEM d (list_pairs l2) ==> l1 = l2` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))); ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))); (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_mem"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["h1"])) THEN (case THEN (move ["h2"])) THEN (case THEN (move ["d_l1"])) THEN (move ["d_l2"])); ((THENL_LAST) (((use_arg_then2 ("h2", [])) (disch_tac [])) THEN (clear_assumption "h2") THEN ((use_arg_then2 ("h1", [])) (disch_tac [])) THEN (clear_assumption "h1") THEN case THEN (move ["h1"]) THEN (case THEN ALL_TAC) THEN (move ["h2"]) THEN ((TRY done_tac))) (((use_arg_then2 ("Ih", [])) (disch_tac [])) THEN (clear_assumption "Ih") THEN (exact_tac))); ((((fun arg_tac -> (use_arg_then2 ("not_mem", [])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("h1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_l1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); ((((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("d_l2", [])) (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 ("not_mem", [])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("h2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_l2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); ((((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("d_l1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma find_pair_list_unique *) let find_pair_list_unique = Sections.section_proof ["l";"d";"L"] `uniq (list_of_darts L) /\ MEM l L /\ MEM d (list_pairs l) ==> l = find_pair_list L d` [ (BETA_TAC THEN (case THEN (move ["uniq_darts"])) THEN (case THEN (move ["l_L"])) THEN (move ["mem_d"])); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_imp_unique_list", [uniq_imp_unique_list])) (fun fst_arg -> (use_arg_then2 ("uniq_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); (((((use_arg_then2 ("l_L", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_find_face *) let uniq_find_face = Sections.section_proof ["d";"L"] `uniq (list_of_darts L) ==> uniq (find_face L d)` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)))); (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face", [find_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["_"])) THEN (move ["uniq_t"])); ((((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_tac [])) THEN case THEN ((simp_tac THEN TRY done_tac))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma size_list_pairs *) let size_list_pairs = Sections.section_proof ["l"] `sizel (list_pairs l) = sizel l` [ (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size1_zip", [size1_zip]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_list_pairs *) let mem_list_pairs = Sections.section_proof ["x";"y";"l"] `MEM (x,y) (list_pairs l) ==> MEM x l /\ MEM y l` [ (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_zip", [mem_zip])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("mem_rot", [mem_rot]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma mem_f_list *) let mem_f_list = Sections.section_proof ["d";"L"] `MEM d (list_of_darts L) ==> MEM (f_list L d) (find_face L d)` [ ((BETA_TAC THEN (move ["mem_d"])) THEN ((((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_next_el", [mem_next_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma nth_list_pairs *) let nth_list_pairs = Sections.section_proof ["x0";"i";"s"] `i < sizel s ==> nth (x0, x0) (list_pairs s) i = (nth x0 s i, nth x0 s (if i = sizel s - 1 then 0 else i + 1))` [ ((BETA_TAC THEN (move ["i_lt"])) THEN ((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))); (((((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fun_if", [fun_if]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma uniq_list_pairs *) let uniq_list_pairs = Sections.section_proof ["s"] `uniq s ==> uniq (list_pairs s)` [ ((fun arg_tac -> arg_tac (Arg_term (`HD s`))) (term_tac (set_tac "x0"))); (((((fun arg_tac -> (use_arg_then2 ("uniq_nthP", [uniq_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("uniq_nthP", [uniq_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x0, x0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["i"]) THEN (move ["j"]) THEN (case THEN (move ["i_lt_j"])) THEN (move ["j_lt"])); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_lt_j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j_lt", [])) (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)); ((repeat_tactic 1 9 (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)); ((((use_arg_then2 ("j_lt", [])) (disch_tac [])) THEN (clear_assumption "j_lt") THEN ((use_arg_then2 ("i_lt_j", [])) (disch_tac [])) THEN (clear_assumption "i_lt_j") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma mem_list_pairs_explicit *) let mem_list_pairs_explicit = Sections.section_proof ["x";"y";"s"] `uniq s /\ MEM (x,y) (list_pairs s) ==> y = next_el s x` [ (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["i"]))); (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["i_lt"])) THEN (case THEN (move ["x_eq"])) THEN (move ["y_eq"])); ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (use_arg_then2 ("x", [])) (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)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN (done_tac))); (((((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_eq", []))(gsym_then (thm_tac (new_rewrite [3] []))))) THEN (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma index_fst_snd *) let index_fst_snd = Sections.section_proof ["x0";"i";"x";"y";"s"] `uniq s /\ i < sizel s /\ nth (x0,x0) (list_pairs s) i = (x,y) ==> indexl x s = i /\ indexl y s = if (i = sizel s - 1) then 0 else i + 1` [ (BETA_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["i_lt"])) THEN (simp_tac)); (((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))))); (((repeat_tactic 1 9 (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_s", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma next_el_list_pairs *) let next_el_list_pairs = Sections.section_proof ["x";"y";"s"] `uniq s /\ MEM (x,y) (list_pairs s) ==> next_el (list_pairs s) (x,y) = (y, next_el s y)` [ (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"])))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM y s`))) (term_tac (have_gen_tac [](move ["ys"])))) ((((fun arg_tac -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (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 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "i"))); ((fun arg_tac -> arg_tac (Arg_term (`nth (x,x) (list_pairs s) i = x,y`))) (term_tac (have_gen_tac [](move ["nth_i"])))); (((((use_arg_then2 ("i_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`i < sizel s`))) (term_tac (have_gen_tac [](move ["i_lt"])))); (((((use_arg_then2 ("i_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((repeat_tactic 1 9 (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 fst_arg -> (use_arg_then2 ("x", [])) (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)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((fun arg_tac -> arg_tac (Arg_term (`i = sizel s - 1`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((THENL_FIRST) (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(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))); ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (split_tac)); (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("x", [])) (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 fst_arg -> (use_arg_then2 ("s", [])) (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 -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 fst_arg -> (use_arg_then2 ("x", [])) (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)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((fun arg_tac -> arg_tac (Arg_term (`0 = sizel s - 1`))) (disch_eq_tac "eq2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN ((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (split_tac)); (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("x", [])) (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 fst_arg -> (use_arg_then2 ("s", [])) (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 -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 fst_arg -> (use_arg_then2 ("x", [])) (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)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((fun arg_tac -> arg_tac (Arg_term (`i + 1 = _`))) (disch_eq_tac "eq2" [])) THEN case THEN (process_fst_eq_tac)) THEN (done_tac)); ];; (* Lemma prev_el_list_pairs *) let prev_el_list_pairs = Sections.section_proof ["x";"y";"s"] `uniq s /\ MEM (x,y) (list_pairs s) ==> prev_el (list_pairs s) (x,y) = (prev_el s x, x)` [ (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"])))); ((fun arg_tac -> arg_tac (Arg_term (`prev_el _1 _2`))) (term_tac (set_tac "t"))); ((fun arg_tac -> arg_tac (Arg_term (`MEM t (list_pairs s)`))) (term_tac (have_gen_tac [](move ["mem_t"])))); (((((use_arg_then2 ("t_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((use_arg_then2 ("t_def", [])) (disch_tac [])) THEN (clear_assumption "t_def") THEN ((use_arg_then2 ("mem_t", [])) (disch_tac [])) THEN (clear_assumption "mem_t") THEN ((use_arg_then2 ("t", [])) (disch_tac [])) THEN (clear_assumption "t") THEN case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["mem_t"]) THEN (move ["t_def"])); ((fun arg_tac -> arg_tac (Arg_term (`b = next_el s a`))) (term_tac (have_gen_tac []ALL_TAC))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_list_pairs_explicit", [mem_list_pairs_explicit])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`prev_el s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC); (((((use_arg_then2 ("prev_next_id", [prev_next_id]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (fun fst_arg -> (use_arg_then2 ("mem_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`b = x`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))))))); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`next_el (list_pairs s)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t_def", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC); ((((((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_pairs", [uniq_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("next_el_list_pairs", [next_el_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma f_list_inverse *) let f_list_inverse = Sections.section_proof ["d";"L"] `uniq (list_of_darts L) /\ MEM d (list_of_darts L) ==> f_list L (prev_el (find_face L d) d) = d /\ prev_el (find_face L (f_list L d)) (f_list L d) = d` [ ((BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)); ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f"))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac)))); (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f"))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (next_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((((use_arg_then2 ("prev_next_id", [prev_next_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac)))); (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_next_el", [mem_next_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma find_face_f_list *) let find_face_f_list = Sections.section_proof ["d";"L"] `uniq (list_of_darts L) /\ MEM d (list_of_darts L) ==> find_face L (f_list L d) = find_face L d` [ (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"])))); (((repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac)))); (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); (((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_f_list", [mem_f_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma f_list_ext_permutes_darts *) let f_list_ext_permutes_darts = Sections.section_proof ["L"] `uniq (list_of_darts L) ==> (f_list_ext L) permutes (darts_of_list L)` [ (BETA_TAC THEN (move ["uniq_s"])); ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Hypermap_and_fan.RES_PERMUTES", [Hypermap_and_fan.RES_PERMUTES]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_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 [] [])))))); ((THENL) (split_tac) [((move ["d"]) THEN (move ["mem_d"])); ALL_TAC]); (((((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_f_list", [find_face_f_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_f_list", [mem_f_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_ROT (-1)) ((THENL) (split_tac) [((move ["d"]) THEN (move ["mem_d"])); ((move ["d1"]) THEN (move ["d2"]) THEN (case THEN (move ["mem_d1"])) THEN (case THEN (move ["mem_d2"])) THEN (move ["eq"]))])); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("f_list_inverse", [f_list_inverse])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))))))); (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("f_list_inverse", [f_list_inverse])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`prev_el (find_face L d) d`))) (term_tac exists_tac)); ((((use_arg_then2 ("f_list_inverse", [f_list_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f"))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac)))); (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma find_face_empty *) let find_face_empty = Sections.section_proof ["d";"L"] `find_face L d = [] <=> ~MEM d (list_of_darts L)` [ (((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list_empty", [find_list_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_find_face_imp_faces_eq *) let mem_find_face_imp_faces_eq = Sections.section_proof ["d1";"d2";"L"] `uniq (list_of_darts L) /\ MEM d1 (find_face L d2) ==> find_face L d1 = find_face L d2` [ (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d1"])))); (((repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac)))); (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((use_arg_then2 ("mem_d1", [])) (disch_tac [])) THEN (clear_assumption "mem_d1") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)); (((((use_arg_then2 ("find_face_empty", [find_face_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma mem_find_face_imp_mem_darts *) let mem_find_face_imp_mem_darts = Sections.section_proof ["d";"y";"L"] `MEM d (find_face L y) ==> MEM d (list_of_darts L)` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))); ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`MEM y _`))) (disch_eq_tac "mem_y" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((((use_arg_then2 ("list_of_faces", [list_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face", [find_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Ih", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma f_list_ext_inverse *) let f_list_ext_inverse = Sections.section_proof ["L"] `uniq (list_of_darts L) ==> inverse (f_list_ext L) = res (\d. prev_el (find_face L d) d) (darts_of_list L)` [ ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["uniq_s"]) THEN (move ["d"])); (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))); ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("darts_of_list", [darts_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 [] [])))))); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM _1 _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))))) ((((use_arg_then2 ("f_list_inverse", [f_list_inverse]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); (((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac))); (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma f_list_ext_inverse_works *) let f_list_ext_inverse_works = Sections.section_proof ["L"] `uniq (list_of_darts L) ==> f_list_ext L o inverse (f_list_ext L) = I /\ inverse (f_list_ext L) o f_list_ext L = I` [ (BETA_TAC THEN (move ["uniq_s"])); (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSES_o", [PERMUTES_INVERSES_o])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac)); ];; (* Lemma n_eq_e_fi *) let n_eq_e_fi = Sections.section_proof ["L"] `uniq (list_of_darts L) ==> n_list_ext L = e_list_ext L o inverse (f_list_ext L)` [ (BETA_TAC THEN (move ["uniq_s"])); (((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq_ext", [eq_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"])); ((((use_arg_then2 ("darts_of_list", [darts_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 [] [])))))); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM _1 _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))))) ((((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); (((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac))); (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma n_list_ext_permutes_darts *) let n_list_ext_permutes_darts = Sections.section_proof ["L"] `good_list L ==> (n_list_ext L) permutes (darts_of_list L)` [ ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]))); ((((use_arg_then2 ("n_eq_e_fi", [n_eq_e_fi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_COMPOSE", [PERMUTES_COMPOSE]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("e_list_ext_permutes_darts", [e_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_INVERSE", [PERMUTES_INVERSE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac)); ];; (* Lemma e_n_f_id *) let e_n_f_id = Sections.section_proof ["L"] `good_list L ==> e_list_ext L o n_list_ext L o f_list_ext L = I` [ ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]))); (((((use_arg_then2 ("n_eq_e_fi", [n_eq_e_fi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_ASSOC", [o_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("I_O_ID", [I_O_ID]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext_inverse_works", [f_list_ext_inverse_works]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma tuple_hypermap_of_list *) let tuple_hypermap_of_list = Sections.section_proof ["L"] `good_list L ==> tuple_hypermap (hypermap_of_list L) = darts_of_list L, e_list_ext L, n_list_ext L, f_list_ext L` [ ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]))); ((((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (CONJUNCT2 hypermap_tybij)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)); ((((use_arg_then2 ("e_list_ext_permutes_darts", [e_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("n_list_ext_permutes_darts", [n_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((((use_arg_then2 ("e_n_f_id", [e_n_f_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma f_list_ext_orbit *) let f_list_ext_orbit = Sections.section_proof ["L";"x"] `MEM x (list_of_darts L) /\ uniq (list_of_darts L) ==> orbit_map (f_list_ext L) x = set_of_list (find_face L x)` [ (BETA_TAC THEN (case THEN ((move ["mem_x"]) THEN (move ["uniq_l"])))); ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ORBIT_MAP_RES", [ORBIT_MAP_RES]))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("f_list_ext", [f_list_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) 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 (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM x (find_face L x)`))) (term_tac (have_gen_tac [](move ["x_in_face"])))) ((((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`orbit_map (f_list L) x = orbit_map (next_el (find_face L x)) x`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((((use_arg_then2 ("next_el_orbit", [next_el_orbit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`(f_list L POWER n) x = (next_el (find_face L x) POWER n) x`))) (term_tac (have_gen_tac ["n"](move ["eq"]))))); (((repeat_tactic 1 9 (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))]) ((repeat_tactic 1 9 (((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((repeat_tactic 1 9 (((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))); ((congr_tac (`next_el _1 _2`)) THEN ((TRY done_tac))); (((fun arg_tac -> (use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (fun fst_arg -> (use_arg_then2 ("uniq_l", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((fun arg_tac -> (use_arg_then2 ("next_el_power", [next_el_power])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(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))); ((((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DIVISION", [DIVISION]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("x_in_face", [])) (disch_tac [])) THEN (clear_assumption "x_in_face") THEN BETA_TAC) THEN (((use_arg_then2 ("index_mem", [index_mem]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma uniq_flatten *) let uniq_flatten = Sections.section_proof ["L"] `uniq (flatten L) /\ all (\l. ~(l = [])) L ==> uniq L` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("uniq", [uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))))); (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_has"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["h_n0"])) THEN (move ["all_t"])); ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["ht"]))); ((((use_arg_then2 ("h_n0", [])) (disch_tac [])) THEN (clear_assumption "h_n0") THEN BETA_TAC) THEN (((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lt0n", [lt0n]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("has_predT", [has_predT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["xh"])) THEN (move ["_"]))); (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("xh", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma flatten_filter_empty *) let flatten_filter_empty = Sections.section_proof ["L"] `flatten (filter (\l. ~(l = [])) L) = flatten L` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("filter", [filter]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac))); (((fun arg_tac -> arg_tac (Arg_term (`h = []`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_sublist_unique *) let uniq_sublist_unique = Sections.section_proof ["l1";"l2";"L";"x"] `uniq (flatten L) /\ MEM l1 L /\ MEM l2 L /\ MEM x l1 /\ MEM x l2 ==> l1 = l2` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))))); (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_has"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["c1"])) THEN (case THEN (move ["c2"])) THEN (case THEN (move ["x_l1"])) THEN (move ["x_l2"])); ((THENL_LAST) (((THENL) (((use_arg_then2 ("c2", [])) (disch_tac [])) THEN (clear_assumption "c2") THEN ((use_arg_then2 ("c1", [])) (disch_tac [])) THEN (clear_assumption "c1") THEN case) [(move ["eq1"]); (move ["l1t"])]) THEN ((THENL) case [(move ["eq2"]); (move ["l2t"])]) THEN ((TRY done_tac))) ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac))); (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_l1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l2", [])) (term_tac exists_tac)) THEN (done_tac)); ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac))); (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_l2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l1", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma uniq_face_unique *) let uniq_face_unique = Sections.section_proof ["f1";"f2";"d";"L"] `uniq (list_of_darts L) /\ MEM f1 (list_of_faces L) /\ MEM f2 (list_of_faces L) /\ MEM d f1 /\ MEM d f2 ==> f1 = f2` [ (BETA_TAC THEN (case THEN (move ["uniq_l"])) THEN (case THEN (move ["mem_f1"])) THEN (case THEN (move ["mem_f2"])) THEN (case THEN (move ["mem_d1"])) THEN (move ["mem_d2"])); ((use_arg_then2 ("uniq_sublist_unique", [uniq_sublist_unique])) (thm_tac apply_tac)); (((fun arg_tac -> arg_tac (Arg_term (`list_of_faces L`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac))); ((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_face_lemma *) let mem_face_lemma = Sections.section_proof ["f";"L"] `good_list L /\ MEM f (list_of_faces L) ==> ?d. MEM d (list_of_darts L) /\ f = find_face L d` [ ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["all_n0"])) THEN (move ["_"]) THEN (move ["mem_f"])); ((fun arg_tac -> arg_tac (Arg_term (`HD f`))) (term_tac exists_tac)); ((fun arg_tac -> arg_tac (Arg_term (`~(f = [])`))) (term_tac (have_gen_tac [](move ["f_n0"])))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`all (\l. ~(l = [])) (list_of_faces L)`))) (term_tac (have_gen_tac []ALL_TAC)))); ((((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("allPn", [allPn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["f_eq"])) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac)); (((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all_map", [all_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("preim", [preim]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (move ["x_L"]) THEN (simp_tac)); (((use_arg_then2 ("list_pairs_empty", [list_pairs_empty]))(thm_tac (new_rewrite [] [])))); ((((use_arg_then2 ("all_n0", [])) (disch_tac [])) THEN (clear_assumption "all_n0") THEN BETA_TAC) THEN ((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("x_L", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`MEM (HD f) f`))) (term_tac (have_gen_tac [](move ["mem_hd"])))); ((((use_arg_then2 ("f_n0", [])) (disch_tac [])) THEN (clear_assumption "f_n0") THEN ((use_arg_then2 ("f", [])) (disch_tac [])) THEN (clear_assumption "f") THEN case THEN ((TRY done_tac)) THEN (move ["h"]) THEN (move ["t"])) THEN ((((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (HD f) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac))); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_face_unique", [uniq_face_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`HD f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM (HD f) (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_hd2"]))))); (((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma face_set_eq_list *) let face_set_eq_list = Sections.section_proof ["L"] `good_list L ==> face_set (hypermap_of_list L) = set_of_list (faces_of_list L)` [ ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["all_n0"])) THEN (move ["_"]))); ((((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_map", [face_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart", [dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("tuple_hypermap_of_list", [tuple_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))); (((((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["f"])); ((((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 [] []))))); ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ALL_TAC]); ((((use_arg_then2 ("f_list_ext_orbit", [f_list_ext_orbit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["ff"])) THEN (case THEN (move ["mem_ff"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_ff", [])) (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 (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("f_list_ext_orbit", [f_list_ext_orbit]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma components_hypermap_of_list *) let components_hypermap_of_list = Sections.section_proof ["L"] `good_list L ==> dart (hypermap_of_list L) = darts_of_list L /\ edge_map (hypermap_of_list L) = e_list_ext L /\ node_map (hypermap_of_list L) = n_list_ext L /\ face_map (hypermap_of_list L) = f_list_ext L` [ (BETA_TAC THEN (move ["good_s"])); ((((use_arg_then2 ("dart", [dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("edge_map", [edge_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_map", [node_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_map", [face_map]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("tuple_hypermap_of_list", [tuple_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma node_of_list_lemma *) let node_of_list_lemma = Sections.section_proof ["x";"L"] `set_of_list (filter (\d. FST d = x) (list_of_darts L)) = {(x, y) | y | (x, y) IN darts_of_list L}` [ (((((use_arg_then2 ("set_of_list_filter", [set_of_list_filter]))(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 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"])); ((THENL) (split_tac) [((case THEN (move ["y"])) THEN (move ["h"])); ((case THEN (move ["y"])) THEN (move ["h"]))]); (((fun arg_tac -> arg_tac (Arg_term (`SND d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma image_lemma *) let image_lemma = Sections.section_proof ["f";"s"] `{f x | x IN s} = IMAGE f s` [ (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma set_nodes_of_list *) let set_nodes_of_list = Sections.section_proof ["L"] `set_of_list (nodes_of_list L) = {{(x, y) | y | (x, y) IN darts_of_list L} | x | x IN elements_of_list L}` [ ((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SET_OF_LIST_MAP", [SET_OF_LIST_MAP]))(thm_tac (new_rewrite [] [])))))); ((repeat_tactic 1 9 (((use_arg_then2 ("image_lemma", [image_lemma]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"])); ((THENL) (split_tac) [((case THEN (move ["n"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["i"])) THEN (move ["h"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((case THEN (move ["i"])) THEN (move ["h"]))]); (((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("node_of_list_lemma", [node_of_list_lemma]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`filter (\d. FST d = i) (list_of_darts L)`))) (term_tac exists_tac)); ((((use_arg_then2 ("node_of_list_lemma", [node_of_list_lemma]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)); (((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma good_list_node *) let good_list_node = Sections.section_proof ["L";"d"] `good_list L /\ good_list_nodes L /\ d IN darts_of_list L ==> node (hypermap_of_list L) d = {(FST d, y) | y | (FST d, y) IN darts_of_list L}` [ ((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node", [node]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("set_nodes_of_list", [set_nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["good_s"])) THEN (case THEN (move ["eq"])) THEN (move ["d_in"])); (((fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`node (hypermap_of_list L) d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC); ((fun arg_tac -> arg_tac (Arg_term (`?x. _ x`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))); (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (move ["eq"])) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`x = FST d`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("node_refl", [node_refl])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["y"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma prev_el_list_pairs_general *) let prev_el_list_pairs_general = Sections.section_proof ["x";"y";"s"] `MEM (x,y) (list_pairs s) ==> ?z. prev_el (list_pairs s) (x,y) = (z,x) /\ MEM (z,x) (list_pairs s)` [ (BETA_TAC THEN (move ["mem_xy"])); ((fun arg_tac -> arg_tac (Arg_term (`FST (prev_el (list_pairs s) (x,y))`))) (term_tac (set_tac "z"))); ((use_arg_then2 ("z", [])) (term_tac exists_tac)); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["eq"]))))) (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`SND (prev_el (list_pairs s) (x,y)) = x`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [2] []))))))))) (((((use_arg_then2 ("z_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`indexl (x,y) _`))) (term_tac (set_tac "k"))); ((fun arg_tac -> arg_tac (Arg_term (`sizel s`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`k < n:num`))) (term_tac (have_gen_tac [](move ["k_lt"])))); (((((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`nth x s k = x`))) (term_tac (have_gen_tac [](move ["nth_s"])))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("mem_xy", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,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 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("nth_shift_right", [nth_shift_right]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`k = 0`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((THENL_LAST) ((((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_s", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((THENL_FIRST) ((((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] []))))) ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((THENL_FIRST) (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); (((((use_arg_then2 ("nth_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma n_list_ext_fst *) let n_list_ext_fst = Sections.section_proof ["x";"y";"L"] `good_list L /\ (x,y) IN darts_of_list L ==> ?z. n_list_ext L (x,y) = (x,z) /\ (x,z) IN darts_of_list L` [ (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["xy_in"])))); ((((use_arg_then2 ("xy_in", [])) (disch_tac [])) THEN BETA_TAC) 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 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (move ["mem_xy"]))); ((fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (fun fst_arg -> (use_arg_then2 ("mem_xy", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["z"]) THEN (case THEN ((move ["eq"]) THEN (move ["mem_zx"]))))))); ((use_arg_then2 ("z", [])) (term_tac exists_tac)); ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["n_eq"])))); (((((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("xy_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("n_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))); (((((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_ext_power_in_darts *) let list_ext_power_in_darts = Sections.section_proof ["d";"L";"n"] `good_list L /\ d IN darts_of_list L ==> (e_list_ext L POWER n) d IN darts_of_list L /\ (n_list_ext L POWER n) d IN darts_of_list L /\ (f_list_ext L POWER n) d IN darts_of_list L` [ ((BETA_TAC THEN (case THEN (move ["good_s"]))) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))) THEN (move ["d_in"]))); ((((use_arg_then2 ("lemma_dart_invariant_power_node", [lemma_dart_invariant_power_node]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("lemma_dart_invariant_power_face", [lemma_dart_invariant_power_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); (((use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`edge (hypermap_of_list L) d`))) (term_tac exists_tac))); (((((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_edge2", [lemma_in_edge2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma fst_n_list_ext_power *) let fst_n_list_ext_power = Sections.section_proof ["x";"y";"L";"n"] `good_list L /\ x,y IN darts_of_list L ==> FST ((n_list_ext L POWER n) (x,y)) = x` [ (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["xy_in"])))); ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))]) (((((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`(n_list_ext L POWER n) (x,y)`))) (term_tac (set_tac "d"))); ((((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_def", []))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("n_list_ext_fst", [n_list_ext_fst])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`FST d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (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 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] [])))) THEN (ANTS_TAC)); (((((use_arg_then2 ("d_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_ext_power_in_darts", [list_ext_power_in_darts]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((BETA_TAC THEN (case THEN (move ["z"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_list_pairs_exists *) let mem_list_pairs_exists = Sections.section_proof ["x";"l"] `MEM x l <=> ?y. MEM (x,y) (list_pairs l)` [ ((THENL) (split_tac) [(move ["mem_x"]); ((case THEN (move ["y"])) 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 (simp_tac))]); ((fun arg_tac -> arg_tac (Arg_term (`next_el l x`))) (term_tac exists_tac)); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,next_el l x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`indexl x l`))) (term_tac exists_tac)); ((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth0", [nth0]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((((fun arg_tac -> arg_tac (Arg_term (`indexl x l = _`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN (done_tac)); ];; (* Lemma mem_list_of_darts *) let mem_list_of_darts = Sections.section_proof ["d";"L"] `MEM d (list_of_darts L) <=> ?l. MEM l L /\ MEM d (list_pairs l)` [ ((THENL_LAST) ((THENL) (split_tac) [ALL_TAC; ((case THEN (move ["l"])) THEN (case THEN ((move ["mem_l"]) THEN (move ["mem_d"]))))]) (((use_arg_then2 ("dart_in_darts", [dart_in_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac))); (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))); ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))); ((THENL_FIRST) (case THEN (move ["mem_d"])) (((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac))); (((fun arg_tac -> (use_arg_then2 ("Ih", [])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["mem_l"])) THEN (move ["mem_d2"])); (((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma mem_list_of_elements *) let mem_list_of_elements = Sections.section_proof ["x";"L"] `MEM x (list_of_elements L) <=> ?y. MEM (x,y) (list_of_darts L)` [ ((((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_undup", [mem_undup]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("SWAP_EXISTS_THM", [SWAP_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("RIGHT_EXISTS_AND_THM", [RIGHT_EXISTS_AND_THM]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))); ((((use_arg_then2 ("mem_list_pairs_exists", [mem_list_pairs_exists]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_node *) let uniq_node = Sections.section_proof ["L";"n"] `good_list L /\ MEM n (list_of_nodes L) ==> uniq n` [ (((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]) THEN (case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("filter_uniq", [filter_uniq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma uniq_face *) let uniq_face = Sections.section_proof ["L";"f"] `good_list L /\ MEM f (list_of_faces L) ==> uniq f` [ ((BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_f"])))) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"]))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (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 (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); ((((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma list_of_darts_nil *) let list_of_darts_nil = Sections.section_proof [] `list_of_darts [] = []` [ (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_of_darts_cons *) let list_of_darts_cons = Sections.section_proof ["h";"t"] `list_of_darts (h :: t) = list_pairs h ++ list_of_darts t` [ (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma list_of_darts_cat *) let list_of_darts_cat = Sections.section_proof ["s1";"s2"] `list_of_darts (s1 ++ s2) = list_of_darts s1 ++ list_of_darts s2` [ (((THENL) (((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(fun tmp_arg1 -> (use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(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 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))); (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma good_list_uniq *) let good_list_uniq = Sections.section_proof ["L"] `good_list L ==> uniq L` [ ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (case THEN (move ["allL"])) THEN (move ["_"])); (((THENL) (((use_arg_then2 ("uniqL", [])) (disch_tac [])) THEN (clear_assumption "uniqL") THEN ((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN ((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL uniq)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))); (((((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hasPn", [hasPn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["h_neq"])) THEN (move ["all_t"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["mem_h"])) THEN (move ["uniq_t"])); ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`?d. MEM d (list_pairs h)`))) (term_tac (have_gen_tac [](case THEN ((move ["d"]) THEN (move ["mem_d"])))))); ((THENL_LAST) (((THENL) (((fun arg_tac -> arg_tac (Arg_term (`list_pairs h`))) (disch_eq_tac "eq" [])) THEN case) [ALL_TAC; ((move ["h'"]) THEN (move ["t'"]))]) THEN (process_fst_eq_tac)) (((use_arg_then2 ("h'", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h_neq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("mem_h", [])) (disch_tac [])) THEN (clear_assumption "mem_h") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_imply", [negb_imply]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (move ["mem_h"]))); (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma list_pairs_inj *) let list_pairs_inj = Sections.section_proof ["s1";"s2"] `list_pairs s1 = list_pairs s2 ==> s1 = s2` [ ((repeat_tactic 1 9 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`unzip1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC))))); (((repeat_tactic 1 9 (((use_arg_then2 ("unzip1_zip", [unzip1_zip]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_list_of_faces *) let uniq_list_of_faces = Sections.section_proof ["L"] `good_list L ==> uniq (list_of_faces L)` [ ((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])); ((((((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_uniq", [map_inj_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("good_list_uniq", [good_list_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["x"]) THEN (move ["y"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("list_pairs_inj", [list_pairs_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)); ];; (* Lemma uniq_faces_of_list *) let uniq_faces_of_list = Sections.section_proof ["L"] `good_list L ==> uniq (faces_of_list L)` [ ((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])); (((((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_faces", [uniq_list_of_faces]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["f1"]) THEN (move ["f2"]) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["mem1"]) THEN (move ["mem2"]))) THEN (move ["eq"])); ((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 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN (move ["d"])))); ((((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["mem_d"])) THEN (move ["f1_eq"])); (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_face_unique", [uniq_face_unique])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((THENL_FIRST) (((((use_arg_then2 ("f1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac)) ((((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 (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f1_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma card_faces_of_list *) let card_faces_of_list = Sections.section_proof ["L"] `good_list L ==> CARD (face_set (hypermap_of_list L)) = sizel (list_of_faces L)` [ ((BETA_TAC THEN (move ["goodL"])) THEN ((((use_arg_then2 ("face_set_eq_list", [face_set_eq_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))); ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_faces_of_list", [uniq_faces_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma card_darts_of_list *) let card_darts_of_list = Sections.section_proof ["L"] `good_list L ==> CARD (dart (hypermap_of_list L)) = sizel (list_of_darts L)` [ (BETA_TAC THEN (move ["goodL"])); ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((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 (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_list_of_elements *) let uniq_list_of_elements = Sections.section_proof ["L"] `uniq (list_of_elements L)` [ (((((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("undup_uniq", [undup_uniq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uniq_list_of_nodes *) let uniq_list_of_nodes = Sections.section_proof ["L"] `uniq (list_of_nodes L)` [ (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))) THEN (move ["a"]) THEN (move ["b"])); ((repeat_tactic 1 9 (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["c"]) THEN (move ["mem_a"]))) THEN (case THEN ((move ["d"]) THEN (move ["mem_b"])))); (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`MEM (a,c)`))) (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 (DISCH_THEN (fun snd_th -> (use_arg_then2 ("EQ_IMP", [EQ_IMP])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_a", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_not_nil *) let mem_not_nil = Sections.section_proof ["s"] `~(s = []) <=> (?x. MEM x s)` [ (((THENL) (((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("NOT_CONS_NIL", [NOT_CONS_NIL]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma node_of_list_not_nil *) let node_of_list_not_nil = Sections.section_proof ["L";"n"] `MEM n (list_of_nodes L) ==> ~(n = [])` [ (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["a"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["b"])) THEN (move ["mem_ab"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac))); (((((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_ab", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma nodes_of_list_eq *) let nodes_of_list_eq = Sections.section_proof ["L";"n1";"n2";"a"] `MEM n1 (list_of_nodes L) /\ MEM n2 (list_of_nodes L) /\ MEM a n1 /\ MEM a n2 ==> n1 = n2` [ ((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))); (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y"])) THEN (move ["mem_xy"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (case THEN ALL_TAC) THEN (case THEN (move ["u"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["v"])) THEN (move ["mem_uv"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma uniq_nodes_of_list *) let uniq_nodes_of_list = Sections.section_proof ["L"] `uniq (nodes_of_list L)` [ (((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_nodes", [uniq_list_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["n1"]) THEN (move ["n2"]) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["mem1"]) THEN (move ["mem2"]))) THEN (move ["eq"])); ((fun arg_tac -> arg_tac (Arg_term (`?d. d IN set_of_list n1`))) (term_tac (have_gen_tac [](case THEN ((move ["d"]) THEN (move ["d_in"])))))); (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("node_of_list_not_nil", [node_of_list_not_nil])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nodes_of_list_eq", [nodes_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma size_list_of_nodes *) let size_list_of_nodes = Sections.section_proof ["L"] `sizel (list_of_nodes L) = sizel (list_of_elements L)` [ (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma card_nodes_of_list *) let card_nodes_of_list = Sections.section_proof ["L"] `CARD (set_of_list (nodes_of_list L)) = sizel (list_of_elements L)` [ ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_nodes_of_list", [uniq_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_of_nodes", [size_list_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma surj_delete *) let surj_delete = Sections.section_proof ["f";"s";"t";"a";"b"] `SURJ f s t /\ f a = f b /\ a IN s /\ b IN s /\ ~(a = b) ==> SURJ f (s DELETE a) t` [ ((((repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_DELETE", [IN_DELETE]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["f_in"]) THEN (move ["f_surj"]))) THEN (case THEN (move ["eq"])) THEN (case THEN (move ["a_in"])) THEN (case THEN (move ["b_in"])) THEN (move ["neq"])) THEN (split_tac)); ((BETA_TAC THEN (move ["x"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("f_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (BETA_TAC THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("f_surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (move ["f_eq"])); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`y = a`))) (disch_eq_tac "y_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac))); (((use_arg_then2 ("b", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("b_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("neq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma fst_node_hypermap_of_list *) let fst_node_hypermap_of_list = Sections.section_proof ["L";"d"] `good_list L ==> (!x. x IN node (hypermap_of_list L) d ==> FST x = FST d)` [ (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN BETA_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["goodL"]) THEN (move ["x"])); ((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))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"]))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H"))); ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`a,b IN darts_of_list L`))) (disch_eq_tac "ab_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac))); ((((((use_arg_then2 ("lemma_node_exception", [lemma_node_exception]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("node", [node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["k"])) THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fst_n_list_ext_power", [fst_n_list_ext_power]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma fst_choice_node_hypermap_of_list *) let fst_choice_node_hypermap_of_list = Sections.section_proof ["L";"d"] `good_list L ==> FST (CHOICE (node (hypermap_of_list L) d)) = FST d` [ ((BETA_TAC THEN (move ["goodL"])) THEN (((fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_list", [fst_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac))); ((((use_arg_then2 ("CHOICE_DEF", [CHOICE_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma surj_fst_nodes_hypermap_of_list *) let surj_fst_nodes_hypermap_of_list = Sections.section_proof ["L"] `good_list L ==> SURJ (\n. FST (CHOICE n)) (node_set (hypermap_of_list L)) (elements_of_list L)` [ (((((use_arg_then2 ("SURJ", [SURJ]))(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 (move ["goodL"])); ((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))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"]))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H"))); (((THENL) (split_tac) [((move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (move ["a"])]) THEN (simp_tac)); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`SND d`))) (term_tac exists_tac)) THEN ((((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 (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["b"]))); (((((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 (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["ab_in"])); ((fun arg_tac -> arg_tac (Arg_term (`node H (a,b)`))) (term_tac exists_tac)); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_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 (simp_tac) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma good_list_nodes_condition *) let good_list_nodes_condition = Sections.section_proof ["L"] `good_list L ==> (good_list_nodes L <=> CARD (node_set (hypermap_of_list L)) = sizel (list_of_elements L))` [ ((THENL_FIRST) (((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])) THEN ((split_tac) THEN (move ["eq"]))) (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_nodes_of_list", [card_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then2 ("SUBSET_CARD_EQ", [SUBSET_CARD_EQ]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("card_nodes_of_list", [card_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (move ["n"])); ((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))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"]))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H"))); ((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 ["r"])) THEN (case THEN (move ["r_in"])) THEN (move ["n_eq"])); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM r (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_r"])))) (((((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 (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac))); ((((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 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`filter (\y. FST y = FST r) (list_of_darts L)`))) (term_tac exists_tac)) THEN (split_tac)); ((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> arg_tac (Arg_term (`FST r`))) (term_tac exists_tac)) THEN (simp_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`SND r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`set_of_list _`))) (term_tac (set_tac "s"))); (((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["neq"])); ((fun arg_tac -> arg_tac (Arg_term (`n PSUBSET s`))) (term_tac (have_gen_tac []ALL_TAC))); (((((use_arg_then2 ("PSUBSET", [PSUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (move ["x_in"])); ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((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 (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_list", [fst_node_hypermap_of_list])) (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 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); (((use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node H r`))) (term_tac exists_tac))); (((((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((((use_arg_then2 ("PSUBSET_ALT", [PSUBSET_ALT]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["a"])) THEN (case THEN (move ["a_in"])) THEN (move ["a_n_in"])); ((fun arg_tac -> arg_tac (Arg_term (`~(sizel (list_of_elements L) = 0)`))) (term_tac (have_gen_tac [](move ["size_gt0"])))); ((((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`FST r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`SND r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`sizel (list_of_elements L) <= CARD (node_set H DELETE n) `))) (term_tac (have_gen_tac []ALL_TAC)))); ((((use_arg_then2 ("CARD_DELETE", [CARD_DELETE]))(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 (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("r_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("size_gt0", [])) (disch_tac [])) THEN (clear_assumption "size_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.surj_imp_card_le", [Hypermap_iso.surj_imp_card_le])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`\x. FST (CHOICE x)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)); ((((use_arg_then2 ("FINITE_DELETE", [FINITE_DELETE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))); (((use_arg_then2 ("surj_delete", [surj_delete])) (thm_tac apply_tac)) THEN (((fun arg_tac -> arg_tac (Arg_term (`node H a`))) (term_tac exists_tac)) THEN (simp_tac))); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1; 2] []))))) THEN (((use_arg_then2 ("surj_fst_nodes_hypermap_of_list", [surj_fst_nodes_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`a IN dart H`))) (term_tac (have_gen_tac [](move ["a_in2"])))); ((((use_arg_then2 ("hypL", []))(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 [] []))))); ((((use_arg_then2 ("a_in", [])) (disch_tac [])) THEN (clear_assumption "a_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("s_def", []))(gsym_then (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_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("a_in2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("r_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("lemma_different_nodes", [lemma_different_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("n_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((simp_tac THEN TRY done_tac))); ((((use_arg_then2 ("a_in", [])) (disch_tac [])) THEN (clear_assumption "a_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("s_def", []))(gsym_then (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_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac)); ];; (* Lemma plain_hypermap_of_list *) let plain_hypermap_of_list = Sections.section_proof ["L"] `good_list L ==> plain_hypermap (hypermap_of_list L)` [ ((BETA_TAC THEN (move ["goodL"])) 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))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])))); (((((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma edge_CARD_dart *) let edge_CARD_dart = Sections.section_proof ["H"] `plain_hypermap H /\ is_edge_nondegenerate H ==> CARD (dart H) = 2 * number_of_edges H` [ (((((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("is_edge_nondegenerate", [is_edge_nondegenerate]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["plain"]) THEN (move ["edge_nd"])))); ((((use_arg_then2 ("number_of_edges", [number_of_edges]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_card_eq", [lemma_card_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (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 (repeat_tactic 0 10 (((use_arg_then2 ("number_of_orbits", [number_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((repeat_tactic 1 9 (((use_arg_then2 ("edge_map_and_darts", [edge_map_and_darts]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["x_in"])); ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL lemma_orbit_of_size_2))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("edge_map_and_darts", [edge_map_and_darts]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((use_arg_then2 ("edge_nd", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("plain", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma good_list_nodes_size_condition *) let good_list_nodes_size_condition = Sections.section_proof ["L"] `good_list L /\ planar_hypermap (hypermap_of_list L) /\ connected_hypermap (hypermap_of_list L) /\ is_edge_nondegenerate (hypermap_of_list L) ==> (good_list_nodes L <=> 2 * (sizel (list_of_elements L) + sizel (list_of_faces L)) = sizel (list_of_darts L) + 4)` [ (BETA_TAC THEN (case THEN (move ["goodL"])) THEN (case THEN (move ["planarL"])) THEN (case THEN (move ["connL"])) THEN (move ["nondL"])); ((((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H"))); ((THENL_FIRST) ((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("eqn_pmul2l", [eqn_pmul2l])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac))); ((((use_arg_then2 ("planarL", [])) (disch_tac [])) THEN (clear_assumption "planarL") THEN ((use_arg_then2 ("connL", [])) (disch_tac [])) THEN (clear_assumption "connL") THEN BETA_TAC) THEN (((((use_arg_then2 ("planar_hypermap", [planar_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("connected_hypermap", [connected_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("eqn_pmul2l", [eqn_pmul2l])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac))); ((repeat_tactic 1 9 (((use_arg_then2 ("muln_addr", [muln_addr]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("edge_CARD_dart", [edge_CARD_dart]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("plain_hypermap_of_list", [plain_hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("card_faces_of_list", [card_faces_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("number_of_faces", [number_of_faces]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("card_darts_of_list", [card_darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))); ((arith_tac) THEN (done_tac)); ];; (* Lemma face_of_list *) let face_of_list = Sections.section_proof ["L";"d"] `good_list L /\ MEM d (list_of_darts L) ==> face (hypermap_of_list L) d = set_of_list (find_face L d)` [ (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_d"])))); ((fun arg_tac -> (use_arg_then2 ("face_set_eq_list", [face_set_eq_list])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (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 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_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 [] [])))))); ((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`face (hypermap_of_list L) d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`face _1 d IN _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac))); (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f"])) THEN (case THEN (move ["mem_f"])) THEN (move ["face_eq"])); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (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 ["d2"]) THEN (case THEN (move ["mem_d2"])) THEN (move ["f_eq"]))))); (((((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))); ((use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (thm_tac apply_tac)); ((((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN (clear_assumption "good_s") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); (((((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma card_face_of_list *) let card_face_of_list = Sections.section_proof ["L";"d"] `good_list L /\ MEM d (list_of_darts L) ==> CARD (face (hypermap_of_list L) d) = sizel (find_face L d)` [ (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_d"])))); ((((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN (clear_assumption "good_s") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_of_faces_k *) let list_of_faces_k = Sections.section_proof ["L";"k"] `good_list L ==> face_set_k k (hypermap_of_list L) = set_of_list (MAP set_of_list (filter (\f. sizel f = k) (list_of_faces L)))` [ ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]))); ((((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) 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 [] []))))); (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (move ["f"]) THEN (simp_tac)); ((THENL) (split_tac) [((case THEN (move ["g"])) THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["card_eq"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((case THEN (move ["g"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["size_g"])) THEN (move ["mem_g"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]); ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac exists_tac)); (((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_face_of_list", [card_face_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_g", [])) (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 ["g_eq"]))))); ((((fun arg_tac -> arg_tac (Arg_term (`set_of_list g`))) (term_tac exists_tac)) THEN (simp_tac)) THEN (split_tac)); (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma darts_k_union_face_set_k *) let darts_k_union_face_set_k = Sections.section_proof ["H";"k"] `darts_k k H = UNIONS (face_set_k k H)` [ (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIONS", [IN_UNIONS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_k", [darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Hypermap_iso.inE", [Hypermap_iso.inE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["d"])); ((THENL) (split_tac) [(move ["h"]); ((case THEN (move ["t"])) THEN (case THEN ALL_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 (move ["card_eq"]) THEN (move ["d_in"]))]); (((fun arg_tac -> arg_tac (Arg_term (`face H d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`face H x = face H d`))) (term_tac (have_gen_tac [](move ["eq"]))))); (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac)); ];; (* Lemma set_of_list_flatten_map *) let set_of_list_flatten_map = Sections.section_proof ["s"] `set_of_list (flatten s) = UNIONS (set_of_list (map set_of_list s))` [ (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIONS", [IN_UNIONS]))(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 (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"])); ((THENL) (split_tac) [((case THEN (move ["l"])) THEN (move ["h"])); ((case THEN (move ["t"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["l2"])) THEN (case THEN (move ["mem_l2"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]); (((fun arg_tac -> arg_tac (Arg_term (`set_of_list l`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac)); (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (move ["mem_x"])) THEN ((use_arg_then2 ("l2", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma list_of_darts_k *) let list_of_darts_k = Sections.section_proof ["L";"k"] `good_list L ==> darts_k k (hypermap_of_list L) = set_of_list (flatten (filter (\f. sizel f = k) (list_of_faces L)))` [ ((BETA_TAC THEN (move ["goodL"])) THEN (((use_arg_then2 ("darts_k_union_face_set_k", [darts_k_union_face_set_k]))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("list_of_faces_k", [list_of_faces_k]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_of_list_flatten_map", [set_of_list_flatten_map]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma darts3_eq_list_of_darts3 *) let darts3_eq_list_of_darts3 = Sections.section_proof ["L"] `good_list L ==> darts_k 3 (hypermap_of_list L) = set_of_list (list_of_darts3 L)` [ (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (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 ((((use_arg_then2 ("list_of_darts3", [list_of_darts3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces3", [list_of_faces3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma darts4_eq_list_of_darts4 *) let darts4_eq_list_of_darts4 = Sections.section_proof ["L"] `good_list L ==> darts_k 4 (hypermap_of_list L) = set_of_list (list_of_darts4 L)` [ (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (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 ((((use_arg_then2 ("list_of_darts4", [list_of_darts4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces4", [list_of_faces4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma darts5_eq_list_of_darts5 *) let darts5_eq_list_of_darts5 = Sections.section_proof ["L"] `good_list L ==> darts_k 5 (hypermap_of_list L) = set_of_list (list_of_darts5 L)` [ (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`5`))) (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 ((((use_arg_then2 ("list_of_darts5", [list_of_darts5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces5", [list_of_faces5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma darts6_eq_list_of_darts6 *) let darts6_eq_list_of_darts6 = Sections.section_proof ["L"] `good_list L ==> darts_k 6 (hypermap_of_list L) = set_of_list (list_of_darts6 L)` [ (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`6`))) (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 ((((use_arg_then2 ("list_of_darts6", [list_of_darts6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces6", [list_of_faces6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma rot_list_pairs *) let rot_list_pairs = Sections.section_proof ["s";"n"] `rot n (list_pairs s) = list_pairs (rot n s)` [ (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_zip", [rot_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("rot_rot", [rot_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma rotr_list_pairs *) let rotr_list_pairs = Sections.section_proof ["s";"n"] `rotr n (list_pairs s) = list_pairs (rotr n s)` [ (((((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma list_pairs_rot *) let list_pairs_rot = Sections.section_proof ["s";"n"] `perm_eq (list_pairs (rot n s)) (list_pairs s)` [ (((((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma find_pair_list_empty *) let find_pair_list_empty = Sections.section_proof ["L";"d"] `find_pair_list L d = [] <=> ~(MEM d (list_of_darts L))` [ (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))); ((((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] []))))); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((((use_arg_then2 ("implybF", [implybF]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["h_eq"])); ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC) THEN ((((use_arg_then2 ("h_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_of_darts_perm *) let list_of_darts_perm = Sections.section_proof ["L1";"L2"] `perm_eq L1 L2 ==> perm_eq (list_of_darts L1) (list_of_darts L2)` [ ((BETA_TAC THEN (move ["perm"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] []))))))); (((((use_arg_then2 ("perm_eq_flatten", [perm_eq_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_map", [perm_eq_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma good_list_perm *) let good_list_perm = Sections.section_proof ["L1";"L2"] `perm_eq L1 L2 /\ good_list L1 ==> good_list L2` [ ((repeat_tactic 1 9 (((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["perm"])) THEN (case THEN (move ["uniq1"])) THEN (case THEN (move ["all1"])) THEN (move ["sym1"])); ((fun arg_tac -> (use_arg_then2 ("list_of_darts_perm", [list_of_darts_perm])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"]))); ((((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("all_perm_eq", [all_perm_eq])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all1", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))))); ((BETA_TAC THEN (move ["d"])) THEN ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("sym1", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)); ];; (* Lemma find_face_cons *) let find_face_cons = Sections.section_proof ["h";"t";"d"] `find_face (h :: t) d = if MEM d (list_pairs h) then (list_pairs h) else find_face t d` [ (((repeat_tactic 1 9 (((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma find_face_eq *) let find_face_eq = Sections.section_proof ["L";"d";"f"] `uniq (list_of_darts L) /\ MEM d (list_of_darts L) ==> (find_face L d = f <=> MEM f (list_of_faces L) /\ MEM d f)` [ ((BETA_TAC THEN (case THEN ((move ["uniqL"]) THEN (move ["mem_d"])))) THEN ((THENL) (split_tac) [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); ALL_TAC])); (((((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["s"])) THEN (case THEN (move ["mem_s"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["eq"])); (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Close the module *) end;;