needs "../formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl";; needs "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";; (* Module List_hypermap_iso*) module List_hypermap_iso = struct parse_as_infix ("::", (12, "right"));; override_interface ("::", `CONS`);; make_overloadable "++" `:A -> A -> A`;; overload_interface ("++", `cat`);; let split_list_face = new_definition `split_list_face f = if sizel f <= 3 then [f] else [take 3 f; HD f :: dropl 2 f]`;; let split_list_hyp = (GEN_ALL o define) `split_list_hyp [] d = [] /\ split_list_hyp (f :: t) d = if MEM d (list_pairs f) then split_list_face (rotr 1 (rot (indexl d (list_pairs f)) f)) ++ t else f :: split_list_hyp t d`;; let list_hyp_diag = new_definition `list_hyp_diag L d = (SND d, FST (prev_el (find_face L d) d))`;; let fan_list_nodes_iso = new_definition `fan_list_nodes_iso (f, (V,E)) x = FST (f (x, if set_of_edge x V E = {} then x else CHOICE (set_of_edge x V E)))`;; let fan_list_iso = new_definition `fan_list_iso (f, (V,E)) (v,w) = fan_list_nodes_iso (f, (V,E)) v, fan_list_nodes_iso (f, (V,E)) w`;; open Ssrbool;; open Ssrnat;; open Seq;; open Seq2;; open Hypermap;; open Hypermap_and_fan;; open Fan_defs;; open List_hypermap;; open Add_triangle;; open Hypermap_iso;; (* Section MoreFan *) Sections.begin_section "MoreFan";; (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));; (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));; (* Lemma fan_imp_finite_set *) let fan_imp_finite_set = Sections.section_proof ["V";"E"] `FAN (vec 0,V,E) ==> FINITE V` [ ((((((use_arg_then2 ("FAN", [FAN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fan1", [fan1]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma e_fan_pair_ext_explicit *) let e_fan_pair_ext_explicit = Sections.section_proof ["v";"w"] `(v,w) IN dart_of_fan (V,E) ==> e_fan_pair_ext (V,E) (v,w) = (w,v)` [ ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext", [e_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`v,w IN _`))) (disch_eq_tac "vw_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("e_fan_pair", [e_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((BETA_TAC THEN (case THEN (move ["z"])) THEN (case THEN (move ["_"]))) THEN ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) THEN (done_tac)); ];; (* Lemma fan_number_of_nodes *) let fan_number_of_nodes = Sections.section_proof ["V";"E"] `FAN (vec 0,V,E) ==> number_of_nodes (hypermap_of_fan (V,E)) = CARD V` [ ((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (move ["fanV"])); (((fun arg_tac -> (use_arg_then2 ("NODE_SET_AS_IMAGE", [NODE_SET_AS_IMAGE])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["f"])) THEN (case THEN (move ["inj"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((((((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("fan_imp_finite_set", [fan_imp_finite_set])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)); ];; (* Finalization of the section MoreFan *) let fan_imp_finite_set = Sections.finalize_theorem fan_imp_finite_set;; let e_fan_pair_ext_explicit = Sections.finalize_theorem e_fan_pair_ext_explicit;; let fan_number_of_nodes = Sections.finalize_theorem fan_number_of_nodes;; Sections.end_section "MoreFan";; (* Section SplitListHyp *) Sections.begin_section "SplitListHyp";; (Sections.add_section_type (mk_var ("d", (`:A#A`))));; (* Lemma split_list_hyp_alt *) let split_list_hyp_alt = Sections.section_proof ["L";"d"] `MEM d (list_of_darts L) ==> (let f = find_pair_list L d and n = indexl (find_pair_list L d) L in split_list_hyp L d = take n L ++ (split_list_face (rotr 1 (rot (indexl d (list_pairs f)) f))) ++ dropl (n + 1) L)` [ ((BETA_TAC THEN (move ["mem_d"])) THEN (CONV_TAC let_CONV) THEN (((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC)); ((THENL_FIRST) ((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 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (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 ("find_pair_list", [find_pair_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)); ((((use_arg_then2 ("Seq.index_head", [Seq.index_head]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop1", [drop1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("behead", [behead]))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("split_list_hyp", [split_list_hyp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (BETA_TAC THEN (move ["mem_dt"])); ((((use_arg_then2 ("split_list_hyp", [split_list_hyp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 (CONS h t)`))) (term_tac (set_tac "m"))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`m = SUC n`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) (((((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop", [drop]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((use_arg_then2 ("m_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_cons", [index_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))); (((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 ("mem_dt", [])) (disch_tac [])) THEN (clear_assumption "mem_dt") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma d_not_in_dart_split_eq *) let d_not_in_dart_split_eq = Sections.section_proof ["L";"d"] `~(MEM d (list_of_darts L)) ==> split_list_hyp L d = L` [ ((((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(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 ("split_list_hyp", [split_list_hyp]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["mem_d"]))); ((((fun arg_tac -> (use_arg_then2 ("mem_d", [])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL MEM)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["x"]))); ((((fun arg_tac -> (use_arg_then2 ("mem_d", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL MEM)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))))); ((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_eq_cat_find_pair_list *) let list_eq_cat_find_pair_list = Sections.section_proof ["L";"d"] `MEM d (list_of_darts L) ==> (let f = find_pair_list L d and n = indexl (find_pair_list L d) L in L = take n L ++ [f] ++ dropl (n + 1) L)` [ ((BETA_TAC THEN (move ["mem_d"])) THEN (CONV_TAC let_CONV) THEN (((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC)); ((THENL_FIRST) ((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 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (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 ("find_pair_list", [find_pair_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)); (((((use_arg_then2 ("Seq.index_head", [Seq.index_head]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop1", [drop1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("behead", [behead]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((BETA_TAC THEN (move ["mem_dt"])) THEN ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [1] [])))) THEN ((TRY done_tac)))); ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 (CONS h t)`))) (term_tac (set_tac "m"))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`m = SUC n`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) (((((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop", [drop]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac))); ((((use_arg_then2 ("m_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_cons", [index_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))); (((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 ("mem_dt", [])) (disch_tac [])) THEN (clear_assumption "mem_dt") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma list_eq_cat_list_diag *) let list_eq_cat_list_diag = Sections.section_proof ["f";"d"] `MEM d (list_pairs f) /\ 2 <= sizel f ==> (let k = indexl d (list_pairs f) and y = FST (prev_el (list_pairs f) d) in rot k f = [FST d] ++ belast (SND d) (dropl 2 (rot k f)) ++ [y])` [ ((BETA_TAC THEN (case THEN ((move ["mem_d"]) THEN (move ["f_size"])))) THEN (CONV_TAC let_CONV)); ((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k"))); ((fun arg_tac -> arg_tac (Arg_term (`FST (_1 _2 d)`))) (term_tac (set_tac "y"))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`k < sizel f`))) (term_tac (have_gen_tac [](move ["k_lt"])))) (((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((fun arg_tac -> (use_arg_then2 ("eq_from_nth", [eq_from_nth])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cat", [size_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size1", [size1]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) ((THENL) (split_tac) [ALL_TAC; (move ["i"])]) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`2 <= sizel f /\ 1 < sizel f /\ 0 < sizel f /\ k <= sizel f /\ 0 < sizel f - 1 /\ 1 <= sizel f`))) (term_tac (have_gen_tac [](move ["size_ineqs"])))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN ((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((THENL) (((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN case) [(move ["_"]); (move ["i"])]); ((((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MOD_LT", [MOD_LT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (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 BETA_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 (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) 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)); (((fun arg_tac -> arg_tac (Arg_term (`sizel f = 2`))) (disch_eq_tac "size_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); (((((use_arg_then2 ("drop_oversize", [drop_oversize]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("belast", [belast]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (move ["i_lt"])); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`i = 0`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] []))))); (((repeat_tactic 1 9 (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))))) THEN (TRY (((((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("size_ineqs", [])) (disch_tac [])) THEN (clear_assumption "size_ineqs") THEN BETA_TAC) THEN (arith_tac))))); ((((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 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] []))))); (((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`2 - 1 + k = k + 1`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`0 < sizel f - 2 /\ 2 < sizel f`))) (term_tac (have_gen_tac [](move ["size_ineqs2"])))) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN ((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((THENL) (((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN case) [(move ["_"]); (move ["i"])]); ((((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("nth0", [nth0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("head_belast", [head_belast]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (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 BETA_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 (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((BETA_TAC THEN (move ["i_lt"])) THEN ((((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))); (((fun arg_tac -> arg_tac (Arg_term (`SUC i < sizel f - 2`))) (disch_eq_tac "i_lt2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (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 [1] []))))) THEN (((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`SUC (SUC i) < 2 <=> F`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((arith_tac) THEN (done_tac))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`SUC (SUC i) - 2 = i`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac))); ((((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("i_lt2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); (((((use_arg_then2 ("nth_belast", [nth_belast]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("succnK", [succnK]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("eqS0", [eqS0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`SUC i = sizel f - 2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN ((use_arg_then2 ("i_lt2", [])) (disch_tac [])) THEN (clear_assumption "i_lt2") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnn", [ltnn]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("subnn", [subnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] []))))); (((repeat_tactic 1 9 (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))))) THEN (TRY (((((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("size_ineqs", [])) (disch_tac [])) THEN (clear_assumption "size_ineqs") THEN BETA_TAC) THEN (arith_tac))))); ((((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 ("FST", [FST]))(thm_tac (new_rewrite [] []))))); (((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`k + SUC (sizel f - 2) = sizel f - 1 + k`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))) THEN (done_tac)); ];; (* Lemma split_list_explicit *) let split_list_explicit = Sections.section_proof ["L";"d"] `let f = find_pair_list L d in (let y = FST (prev_el (list_pairs f) d) and k = indexl d (list_pairs f) in 3 < sizel f ==> split_list_face (rotr 1 (rot k f)) = [[y; FST d; SND d]; [y; SND d] ++ dropl 3 (rotr 1 (rot k f))] /\ perm_eq (list_of_darts (split_list_face (rotr 1 (rot k f)))) ([list_hyp_diag L d; e_list (list_hyp_diag L d)] ++ list_pairs f))` [ (repeat_tactic 1 9 ((CONV_TAC let_CONV))); ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac))); ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_pair_list_empty", [find_pair_list_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); (BETA_TAC THEN (move ["f_size"])); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`FST _`))) (term_tac (set_tac "y"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k"))); ((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'"))); (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_list_diag))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC)); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); (((((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(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 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] []))))) THEN (move ["rot_eq"])); ((((use_arg_then2 ("rot_eq", [])) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`rotr 1`))) (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 (((((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr1_rcons", [rotr1_rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (move ["f'_eq"]))); ((fun arg_tac -> arg_tac (Arg_term (`belast (SND d) (dropl 2 (rot k f)) = SND d :: dropl 3 f'`))) (term_tac (have_gen_tac [](move ["eqX"])))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`1 <= sizel (dropl 2 (rot k f))`))) (term_tac (have_gen_tac []ALL_TAC))) (((((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((THENL_FIRST) ((((use_arg_then2 ("f'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((THENL) (((fun arg_tac -> arg_tac (Arg_term (`dropl 2 (rot k f)`))) (disch_tac [])) THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))])) ((((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac))); ((((use_arg_then2 ("belast", [belast]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["h1"])))); ((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); (congr_tac (`[_1; _2]`)); (((((use_arg_then2 ("f'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqX", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("take_size_cat", [take_size_cat]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((THENL_FIRST) ((((use_arg_then2 ("f'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqX", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("size_cons", [size_cons]))(fun tmp_arg1 -> (use_arg_then2 ("size_nil", [size_nil]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac))); ((((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("catA", [catA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] []))))); (((((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))); ((repeat_tactic 2 0 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`FST d,SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))); ((repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2l", [perm_cat2l]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> (use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`list_pairs (rot k f)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((use_arg_then2 ("list_pairs_rot", [list_pairs_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqX", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons_cat", [rcons_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cons", [perm_cons]))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("y", [])) (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)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] [(`SND d :: _1 ++ [y]`)]))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("zip_cat", [zip_cat]))(thm_tac (new_rewrite [] []))))); (((repeat_tactic 1 9 (((use_arg_then2 ("size_cat", [size_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma darts_of_list_split *) let darts_of_list_split = Sections.section_proof ["L";"d"] `3 < sizel (find_pair_list L d) ==> perm_eq (list_of_darts (split_list_hyp L d)) ([list_hyp_diag L d; e_list (list_hyp_diag L d)] ++ list_of_darts L)` [ ((BETA_TAC THEN (move ["f_size"])) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_d"])))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("find_pair_list_empty", [find_pair_list_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("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)))(thm_tac (new_rewrite [3] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_explicit))) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["split_eq"]) THEN (move ["darts_perm"]))))); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'"))); ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cat", [list_of_darts_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catCA", [perm_catCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2l", [perm_cat2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2r", [perm_cat2r]))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_perm", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma darts_of_list_split_same *) let darts_of_list_split_same = Sections.section_proof ["L";"d"] `sizel (find_pair_list L d) <= 3 ==> perm_eq (list_of_darts (split_list_hyp L d)) (list_of_darts L)` [ ((BETA_TAC THEN (move ["f_size"])) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] []))))); ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac))); (((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("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)))(thm_tac (new_rewrite [1] [])))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'"))); ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cat", [list_of_darts_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_cat2l", [perm_cat2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2r", [perm_cat2r]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k"))); ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))))); (((fun arg_tac -> (use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`rot k _`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(fun tmp_arg1 -> (use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(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)); ];; (* Lemma list_of_elements_split *) let list_of_elements_split = Sections.section_proof ["L";"d"] `perm_eq (list_of_elements L) (list_of_elements (split_list_hyp L d))` [ (((use_arg_then2 ("uniq_perm_eq", [uniq_perm_eq])) (thm_tac apply_tac)) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["i"]))); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] []))))); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n"))); ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("flatten_cat", [flatten_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_undup", [mem_undup]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("orb_id2l", [orb_id2l])) (disch_tac [])) THEN (clear_assumption "orb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("orb_id2r", [orb_id2r])) (disch_tac [])) THEN (clear_assumption "orb_id2r") THEN (DISCH_THEN apply_tac) THEN (move ["_"]))); ((((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten0", [flatten0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> arg_tac (Arg_term (`_ <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("flatten0", [flatten0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("mem_rotr", [mem_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_rot", [mem_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "s"))); ((fun arg_tac -> arg_tac (Arg_term (`?k. s = rot k f`))) (term_tac (have_gen_tac [](case THEN ((move ["k"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))))); ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("rot_rot_eq_rot", [rot_rot_eq_rot])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`sizel f - 1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`indexl d (list_pairs f)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["k"]) THEN (move ["eq"]))))); (((use_arg_then2 ("k", [])) (term_tac exists_tac)) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`3 < sizel f /\ 2 < 3`))) (term_tac (have_gen_tac [](move ["ineqs"])))) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_rot", [mem_rot])) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (split_tac)); ((((fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))); ((case THEN (simp_tac) THEN (move ["mem_i"])) THEN (DISJ2_TAC) THEN (DISJ2_TAC)); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`rot k f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("drop_cat", [drop_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); (((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_i", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (((THENL) case [(DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_take", [mem_take])) (thm_tac (match_mp_then snd_th MP_TAC)))); ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_drop", [mem_drop])) (thm_tac (match_mp_then snd_th MP_TAC))))])]) THEN ((TRY done_tac)))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`0 < sizel (rot k f)`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); (((THENL) (((fun arg_tac -> arg_tac (Arg_term (`rot k f`))) (disch_tac [])) THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("size_nil", [size_nil]))(fun tmp_arg1 -> (use_arg_then2 ("ltn0", [ltn0]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL HD)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mem_list_hyp_diag *) let mem_list_hyp_diag = Sections.section_proof ["L";"d"] `MEM d (list_of_darts L) /\ (sizel (find_pair_list L d) = 1 \/ sizel (find_pair_list L d) = 3) ==> MEM (list_hyp_diag L d) (find_face L d)` [ ((BETA_TAC THEN (case THEN ((move ["mem_d"]) THEN (move ["size_eq"])))) THEN ((((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl d (list_pairs f)`))) (term_tac (set_tac "k"))); ((fun arg_tac -> arg_tac (Arg_term (`FST _`))) (term_tac (set_tac "y"))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs f)`))) (term_tac (have_gen_tac [](move ["mem_d2"])))) (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`k < sizel f`))) (term_tac (have_gen_tac [](move ["k_lt"])))) (((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN case THEN (move ["size_eq"])); ((((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size1_eq", [size1_eq]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (move ["f_eq"]))); ((((use_arg_then2 ("mem_d2", [])) (disch_tac [])) THEN (clear_assumption "mem_d2") THEN BETA_TAC) THEN (((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_seq1", [mem_seq1]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("prev_el", [prev_el]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("Seq.index_head", [Seq.index_head]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_pairs_rot", [list_pairs_rot])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`2 <= sizel f`))) (term_tac (have_gen_tac [](move ["size_ineq"])))) ((((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_list_diag))) (fun fst_arg -> (use_arg_then2 ("mem_d2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("size_ineq", [])) (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 ("y_def", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`dropl 2 _`))) (term_tac (set_tac "l"))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`belast (SND d) l = [SND d]`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`sizel l = 1`))) (term_tac (have_gen_tac []ALL_TAC))) (((((use_arg_then2 ("l_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac))); (((((use_arg_then2 ("size1_eq", [size1_eq]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("belast", [belast]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma good_list_split *) let good_list_split = Sections.section_proof ["L";"d"] `good_list L /\ (sizel (find_pair_list L d) <= 3 \/ ~(MEM (list_hyp_diag L d) (list_of_darts L)) /\ ~(FST (list_hyp_diag L d) = SND (list_hyp_diag L d))) ==> good_list (split_list_hyp L d)` [ (BETA_TAC THEN (case THEN ((move ["goodL"]) THEN (move ["hyp"])))); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'"))); ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((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 ["symL"]) THEN (move ["L_eq"]) THEN (move ["split_eq"]))); (((fun arg_tac -> arg_tac (Arg_term (`sizel (find_pair_list L d) <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE darts_of_list_split_same))) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"]))); ((THENL_ROT (-1)) (((((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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniqL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (split_tac))); ((BETA_TAC THEN (move ["y"])) 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)))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("symL", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)); ((((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN BETA_TAC) THEN (((((use_arg_then2 ("L_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all_cat", [all_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["f_neq"])) THEN (move ["_"]))); (((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("hyp", [])) (disch_tac [])) THEN (clear_assumption "hyp") THEN BETA_TAC) THEN (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["n_mem"])) THEN (move ["neq"]))); (in_tac ["f_size"] false (((use_arg_then2 ("NOT_LE", [NOT_LE]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE darts_of_list_split))) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"]))); (split_tac); ((THENL_ROT (-1)) (((((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)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL uniq)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniqL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (split_tac))); ((((use_arg_then2 ("n_mem", [])) (disch_tac [])) THEN (clear_assumption "n_mem") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("symL", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((((use_arg_then2 ("n_mem", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbF", [orbF]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("neq", [])) (disch_tac [])) THEN (clear_assumption "neq") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [1] [])))) 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)); (split_tac); ((((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN BETA_TAC) THEN ((((use_arg_then2 ("L_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all_cat", [all_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`3 < sizel f'`))) (term_tac (have_gen_tac [](move ["f'_size"])))) (((((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["_"])); (((repeat_tactic 1 9 (((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((BETA_TAC THEN (move ["y"])) 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)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`list_hyp_diag L d`))) (term_tac (set_tac "h"))); ((THENL_LAST) case (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("symL", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma hypermap_of_list_perm *) let hypermap_of_list_perm = Sections.section_proof ["L1";"L2"] `perm_eq L1 L2 /\ good_list L1 ==> hypermap_of_list L1 = hypermap_of_list L2` [ (BETA_TAC THEN (case THEN ((move ["perm"]) THEN (move ["good1"])))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("good_list_perm", [good_list_perm])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("good1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["good2"]))); ((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_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["mem_eq"]))); ((repeat_tactic 1 9 (((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`hypermap _`))); ((repeat_tactic 1 9 (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_set_of_list_eq", [perm_eq_set_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)); ((fun arg_tac -> arg_tac (Arg_term (`(!d. MEM d (list_of_darts L1) ==> f1 d = f2 d) ==> res f1 (darts_of_list L1) = res f2 (darts_of_list L2)`))) (term_tac (have_gen_tac ["f1"; "f2"](move ["res_eq"])))); ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["eq"]) THEN (move ["d"])); ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((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 [] []))))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((THENL_FIRST) (split_tac) ((repeat_tactic 1 9 (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L1) ==> find_face L2 d = find_face L1 d`))) (term_tac (have_gen_tac ["d"](move ["face_eq"])))); ((BETA_TAC THEN (move ["mem_d"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`list_pairs _`))); ((((use_arg_then2 ("good1", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq1"])) THEN (move ["_"]))); (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq1", [])) (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 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))); (((((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((split_tac) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("n_list_ext", [n_list_ext]))(fun tmp_arg1 -> (use_arg_then2 ("f_list_ext", [f_list_ext]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"]))); (((repeat_tactic 1 9 (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma find_face_rot *) let find_face_rot = Sections.section_proof ["L1";"L2";"d"] `ALL2 (\f1 f2. ?n. f2 = rot n f1) L1 L2 ==> ?n. find_face L2 d = rot n (find_face L1 d)` [ ((((THENL) (((use_arg_then2 ("L2", [])) (disch_tac [])) THEN (clear_assumption "L2") THEN ((use_arg_then2 ("L1", [])) (disch_tac [])) THEN (clear_assumption "L1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["Ih"]))]) THEN ((THENL) case [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]))])) THEN ((((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)))); (((((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 (((use_arg_then2 ("rot_nil", [rot_nil]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["n"])) THEN (move ["h2_eq"]) THEN (move ["all2"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_cons", [find_face_cons]))(thm_tac (new_rewrite [] [])))))); (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h1)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); (((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_pairs_rot", [list_pairs_rot])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (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 [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((fun arg_tac -> (use_arg_then2 ("Ih", [])) (fun fst_arg -> (use_arg_then2 ("all2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["m"])) THEN (move ["eq"])) THEN ((use_arg_then2 ("m", [])) (term_tac exists_tac))); (((((use_arg_then2 ("h2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_pairs_rot", [list_pairs_rot])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (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 [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma rot_list_of_darts_perm *) let rot_list_of_darts_perm = Sections.section_proof ["L1";"L2"] `ALL2 (\f1 f2. ?n. f2 = rot n f1) L1 L2 ==> perm_eq (list_of_darts L1) (list_of_darts L2)` [ ((((THENL) (((use_arg_then2 ("L2", [])) (disch_tac [])) THEN (clear_assumption "L2") THEN ((use_arg_then2 ("L1", [])) (disch_tac [])) THEN (clear_assumption "L1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["Ih"]))]) THEN ((THENL) case [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]))])) THEN ((((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) 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 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)))); (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["n"]) THEN (move ["h2_eq"]))) THEN (move ["all2"])); ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_cat", [perm_eq_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((((use_arg_then2 ("h2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs_rot", [list_pairs_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma rot_hypermap_of_list_eq *) let rot_hypermap_of_list_eq = Sections.section_proof ["L1";"L2"] `ALL2 (\f1 f2. ?n. f2 = rot n f1) L1 L2 /\ uniq (list_of_darts L1) ==> hypermap_of_list L2 = hypermap_of_list L1` [ (BETA_TAC THEN (case THEN ((move ["all2"]) THEN (move ["uniq1"])))); ((repeat_tactic 1 9 (((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`hypermap _`))); ((fun arg_tac -> (use_arg_then2 ("rot_list_of_darts_perm", [rot_list_of_darts_perm])) (fun fst_arg -> (use_arg_then2 ("all2", [])) (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_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["mem_eq"]))); ((fun arg_tac -> (use_arg_then2 ("find_face_rot", [find_face_rot])) (fun fst_arg -> (use_arg_then2 ("all2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["face_eq"]))); ((repeat_tactic 1 9 (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_set_of_list_eq", [perm_eq_set_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)); ((fun arg_tac -> arg_tac (Arg_term (`(!d. MEM d (list_of_darts L1) ==> f1 d = f2 d) ==> res f2 (darts_of_list L2) = res f1 (darts_of_list L1)`))) (term_tac (have_gen_tac ["f1"; "f2"](move ["res_eq"])))); ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["eq"]) THEN (move ["y"])); ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((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 [] []))))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (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)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((THENL_FIRST) (split_tac) ((repeat_tactic 1 9 (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["y"]) THEN (move ["mem_y"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (split_tac); ((repeat_tactic 1 9 (((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"]))); (((fun arg_tac -> (use_arg_then2 ("face_eq", [])) (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 (case THEN (move ["n"])) THEN (move ["f_eq"])); ((repeat_tactic 1 9 (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("prev_el_rot_eq", [prev_el_rot_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((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)); ((repeat_tactic 1 9 (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"]))); (((fun arg_tac -> (use_arg_then2 ("face_eq", [])) (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 (case THEN (move ["n"])) THEN (move ["f_eq"])); (((repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq]))(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)); ];; (* Lemma hypermap_of_split_list_eq3 *) let hypermap_of_split_list_eq3 = Sections.section_proof ["L";"d"] `sizel (find_face L d) <= 3 /\ uniq (list_of_darts L) ==> hypermap_of_list (split_list_hyp L d) = hypermap_of_list L` [ (BETA_TAC THEN (case THEN ((move ["f_size"]) THEN (move ["uniq_darts"])))); ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`!s:((A)list)list. ALL2 (\f1 f2. ?n. f2 = rot n f1) s s`))) (term_tac (have_gen_tac [](move ["all2_refl"])))); (((THENL) elim [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`0`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("rot0", [rot0]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((fun arg_tac -> (use_arg_then2 ("rot_hypermap_of_list_eq", [rot_hypermap_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("uniq_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)); ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("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)))(thm_tac (new_rewrite [1] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n"))); (BETA_TAC THEN (move ["f_size"])); ((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((repeat_tactic 1 9 (((use_arg_then2 ("ALL2_cat", [ALL2_cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all2_refl", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> arg_tac (Arg_term (`sizel _ - 1`))) (term_tac (set_tac "i"))) THEN ((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "j")))); ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("rot_rot_eq_rot", [rot_rot_eq_rot])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["k"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("k", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Lemma f_split_list *) let f_split_list = Sections.section_proof ["L";"d"] `let L2 = split_list_hyp L d and g = list_hyp_diag L d and f = find_face L d in good_list L /\ 3 < sizel f /\ ~(MEM g (list_of_darts L)) /\ ~(FST g = SND g) ==> f_list L2 d = g /\ f_list L2 g = prev_el f d /\ f_list L2 (e_list g) = f_list L d /\ f_list L2 (prev_el f (prev_el f d)) = e_list g /\ (!x. MEM x (list_of_darts L2) /\ ~(x = d \/ x = g \/ x = e_list g \/ x = prev_el f (prev_el f d)) ==> f_list L2 x = f_list L x)` [ (CONV_TAC let_CONV); (BETA_TAC THEN (case THEN (move ["goodL"])) THEN (case THEN (move ["f_size"])) THEN (case THEN (move ["g_n_mem"])) THEN (move ["g_neq"])); ((fun arg_tac -> arg_tac (Arg_term (`3 < sizel (find_pair_list L d)`))) (term_tac (have_gen_tac [](move ["size_gt3"])))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_d"])))); ((((use_arg_then2 ("size_gt3", [])) (disch_tac [])) THEN (clear_assumption "size_gt3") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("find_pair_list_empty", [find_pair_list_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ((fun arg_tac -> (use_arg_then2 ("darts_of_list_split", [darts_of_list_split])) (fun fst_arg -> (use_arg_then2 ("size_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_explicit))) (fun fst_arg -> (use_arg_then2 ("size_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("good_list_split", [good_list_split])) (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 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN ((THENL) (ANTS_TAC) [((TRY done_tac)); (move ["goodL2"])])); (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "s"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl s _`))) (term_tac (set_tac "n"))); ((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k"))); ((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "s'"))); ((fun arg_tac -> arg_tac (Arg_term (`split_list_hyp L d`))) (term_tac (set_tac "L2"))); ((fun arg_tac -> arg_tac (Arg_term (`list_hyp_diag L d`))) (term_tac (set_tac "g"))); ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f"))); ((fun arg_tac -> arg_tac (Arg_term (`FST _ :: _2`))) (term_tac (set_tac "s1"))); ((fun arg_tac -> arg_tac (Arg_term (`cat _1 _2`))) (term_tac (set_tac "s2"))); (BETA_TAC THEN (case THEN ((move ["split_s'_eq"]) THEN (move ["darts_s'"]))) THEN (move ["L2_eq"]) THEN (move ["dartsL2"])); ((((use_arg_then2 ("goodL2", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL2"])) THEN (move ["_"]))); ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"]))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`list_pairs s = f`))) (term_tac (have_gen_tac [](move ["fs_eq"])))) (((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`list_pairs s1 = [prev_el f d; d; g]`))) (term_tac (have_gen_tac [](move ["s1_pairs_eq"])))); ((((use_arg_then2 ("s1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("g_def", []))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`[_; d; g]`))); ((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (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 fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC)); (((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] [])))) 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 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["z"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`uniq f`))) (term_tac (have_gen_tac [](move ["uniq_f"])))) (((((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 (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`MEM s1 L2 /\ MEM s2 L2`))) (term_tac (have_gen_tac [](move ["s12_mem"])))); (((((use_arg_then2 ("L2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("split_s'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`MEM (list_pairs s1) (list_of_faces L2) /\ MEM (list_pairs s2) (list_of_faces L2)`))) (term_tac (have_gen_tac [](move ["s12_pairs_mem"])))); (((THENL) (((((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 (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))))) THEN (split_tac)) [((use_arg_then2 ("s1", [])) (term_tac exists_tac)); ((use_arg_then2 ("s2", [])) (term_tac exists_tac))]) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`uniq (list_pairs s1) /\ uniq (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["s12_pairs_uniq"])))); ((split_tac) THEN (((fun arg_tac -> (use_arg_then2 ("uniq_face", [uniq_face])) (fun fst_arg -> (use_arg_then2 ("goodL2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`next_el f x = next_el (list_pairs s') x`))) (term_tac (have_gen_tac ["x"](move ["next_el_fs'"])))); ((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr_list_pairs", [rotr_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("next_el_rotr_eq", [next_el_rotr_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("rot_uniq", [rot_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`prev_el f x = prev_el (list_pairs s') x`))) (term_tac (have_gen_tac ["x"](move ["prev_el_fs'"])))); ((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr_list_pairs", [rotr_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("prev_el_rotr_eq", [prev_el_rotr_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("rot_uniq", [rot_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("prev_el_rot_eq", [prev_el_rot_eq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`MEM x f ==> MEM x (list_of_darts L)`))) (term_tac (have_gen_tac ["x"](move ["mem_f_darts"])))); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM d f`))) (term_tac (have_gen_tac [](move ["mem_df"])))) (((((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 (`perm_eq (list_pairs s') f`))) (term_tac (have_gen_tac [](move ["p_eq_f_s'"])))); ((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr_list_pairs", [rotr_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`sizel _ - 1`))) (term_tac (set_tac "r"))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("rot_rot_eq_rot", [rot_rot_eq_rot])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`list_pairs s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("r", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["i"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); ((((use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`sizel s' = sizel s`))) (term_tac (have_gen_tac [](move ["size_s'"])))) (((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`s' = s1 ++ dropl 3 s'`))) (term_tac (have_gen_tac [](move ["s'_eq1"])))); ((((use_arg_then2 ("split_s'_eq", [])) (disch_tac [])) THEN (clear_assumption "split_s'_eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s'", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_gt3", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); ((((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (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 [4] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (injectivity "list")))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`list_pairs s' = prev_el f d :: d :: dropl 2 (list_pairs s')`))) (term_tac (have_gen_tac [](move ["s'_pairs_eq"])))); (((((fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (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 [1] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 ++ _2`)) THEN ((TRY done_tac)))); ((((use_arg_then2 ("s'_eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("TWO", [TWO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))))); ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (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 fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC)); (((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] [])))) 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)); ((BETA_TAC THEN (case THEN (move ["z"]))) THEN (((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`list_pairs s2 = e_list g :: dropl 2 (list_pairs s')`))) (term_tac (have_gen_tac [](move ["s2_pairs_eq"])))); ((((use_arg_then2 ("s'_eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("s2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("TWO", [TWO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("drop", [drop]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("g_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`0 < sizel (dropl 2 (list_pairs s')) /\ 1 < sizel (dropl 2 (list_pairs s')) /\ 0 < sizel (list_pairs s') /\ 2 < sizel (list_pairs s')`))) (term_tac (have_gen_tac [](move ["size_uneqs"])))); (((((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s'", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_gt3", [])) (disch_tac [])) THEN (clear_assumption "size_gt3") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`sizel (list_pairs s2) = sizel (list_pairs s') - 1 /\ 0 < sizel (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["size_ineqs_s2"])))); (((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s'", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_gt3", [])) (disch_tac [])) THEN (clear_assumption "size_gt3") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`last d (list_pairs s') = prev_el f (prev_el f d)`))) (term_tac (have_gen_tac [](move ["last_s'"])))); (((((use_arg_then2 ("prev_el_hd", [prev_el_hd]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL HD)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("prev_el_fs'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`last d (list_pairs s2) = prev_el f (prev_el f d)`))) (term_tac (have_gen_tac [](move ["last_s2"])))); (((((use_arg_then2 ("last_s'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last_drop", [last_drop]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((use_arg_then2 ("last_eq", [last_eq])) (thm_tac apply_tac)) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`MEM x (list_of_darts L2) <=> x = g \/ x = e_list g \/ MEM x (list_of_darts L)`))) (term_tac (have_gen_tac ["x"](move ["memL2"])))); (((((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("dartsL2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("orbF", [orbF]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("orbA", [orbA]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`find_face L2 d = list_pairs s1 /\ find_face L2 g = list_pairs s1 /\ find_face L2 (prev_el f d) = list_pairs s1`))) (term_tac (have_gen_tac [](move ["find_s1"])))); ((repeat_tactic 1 9 (((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("uniqL2", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("memL2", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("mem_d", []))(fun tmp_arg1 -> (use_arg_then2 ("s12_pairs_mem", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_f_darts", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`find_face L2 (e_list g) = list_pairs s2 /\ find_face L2 (prev_el f (prev_el f d)) = list_pairs s2`))) (term_tac (have_gen_tac [](move ["find_s2"])))); ((repeat_tactic 1 9 (((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("uniqL2", []))(fun tmp_arg1 -> (use_arg_then2 ("memL2", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_f_darts", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("s12_pairs_mem", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("last_s'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("last_drop", [last_drop])) (fun fst_arg -> (use_arg_then2 ("d", [])) (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)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("last_eq", [last_eq])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`e_list g`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_last", [mem_last]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_s1", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_s2", []))(thm_tac (new_rewrite [] [])))))); (split_tac); (((((fun arg_tac -> (use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("next_el_hd_cons2", [next_el_hd_cons2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (split_tac); ((((fun arg_tac -> (use_arg_then2 ("next_el_rotr_eq", [next_el_rotr_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr1_rcons", [rotr1_rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons2", [next_el_hd_cons2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (split_tac); ((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons", [next_el_hd_cons]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_fs'", []))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> (use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("p_eq_f_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons", [next_el_hd_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rcons", [size_rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("gtS0", [gtS0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((use_arg_then2 ("headI", [headI]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("head_HD", [head_HD]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (split_tac); (((((use_arg_then2 ("last_s2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("next_el_last", [next_el_last]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((repeat_tactic 1 9 (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["mem_x"])) THEN (move ["x_neq"])); ((((use_arg_then2 ("mem_x", [])) (disch_tac [])) THEN (clear_assumption "mem_x") THEN BETA_TAC) THEN (((((use_arg_then2 ("memL2", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("x_neq", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))))) THEN (move ["mem_x"]))); ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`MEM x f`))) (disch_eq_tac "mem_x_f" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac))); (congr_tac (`next_el _ x`)); ((((use_arg_then2 ("find_face_eq", [find_face_eq]))(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 (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("mem_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 ("s_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))) THEN (move ["L_eq"])); ((((fun arg_tac -> (use_arg_then2 ("mem_find_face", [mem_find_face])) (fun fst_arg -> (use_arg_then2 ("mem_x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("L_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("L2_eq", []))(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", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))))); ((BETA_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["mem_l"])) THEN (move ["eq"])) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac))); ((((THENL) (((use_arg_then2 ("mem_l", [])) (disch_tac [])) THEN (clear_assumption "mem_l") THEN case) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ((THENL) case [ALL_TAC; (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))])]) THEN ((TRY done_tac))) THEN ((((use_arg_then2 ("mem_seq1", [mem_seq1]))(thm_tac (new_rewrite [] [])))) THEN (move ["l_eq"]))); ((((use_arg_then2 ("mem_x_f", [])) (disch_tac [])) THEN (clear_assumption "mem_x_f") THEN ((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (((((use_arg_then2 ("l_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(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 x = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))); (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) 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 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((fun arg_tac -> arg_tac (Arg_term (`x = prev_el f d`))) (disch_eq_tac "x_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); (((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_s1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons2", [next_el_hd_cons2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`MEM x (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["mem_x_s2"])))); ((((fun arg_tac -> (use_arg_then2 ("iffRL", [iffRL])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("darts_s'", [])) (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 snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); ((((use_arg_then2 ("split_s'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))); ((case THEN ((TRY done_tac))) THEN ((((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`find_face L2 x = list_pairs s2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) (((((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s12_pairs_mem", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((use_arg_then2 ("next_el_fs'", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`indexl x _`))) (term_tac (set_tac "i"))); ((fun arg_tac -> arg_tac (Arg_term (`1 <= i /\ i < sizel (list_pairs s2) - 1`))) (term_tac (have_gen_tac [](move ["i_ineqs"])))); ((((use_arg_then2 ("mem_x_s2", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("index_mem", [index_mem]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_def", []))(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`~(i = 0) /\ ~(i = sizel (list_pairs s2) - 1)`))) (term_tac (have_gen_tac []ALL_TAC)))) ((arith_tac) THEN (done_tac))); ((((fun arg_tac ->(use_arg_then2 ("x_eq", []))(fun tmp_arg1 -> (use_arg_then2 ("x_neq", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2)))))) (disch_tac [])) THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))))); ((case THEN (move ["i_eq"])) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_x_s2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("i_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))))); ((((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`i = indexl (last d (list_pairs s2)) (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["i_eq2"])))); (((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_last", [index_last]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("s2_pairs_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((((use_arg_then2 ("i_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last_s2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); (((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_last", [mem_last]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(i = sizel (list_pairs s2) - 1)`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] []))))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`indexl x (list_pairs s') = i + 1`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(i + 1 = sizel (list_pairs s') - 1)`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN BETA_TAC) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac))); (((repeat_tactic 1 9 (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`nth x (list_pairs s') (i + 1) = x`))) (term_tac (have_gen_tac [](move ["nth_eq"]))))); ((((use_arg_then2 ("nth_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("p_eq_f_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniq_f", []))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN BETA_TAC) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_x_s2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("i_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) ((THENL) (((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN ((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN case) [ALL_TAC; ((move ["j"]) THEN (move ["j_ineq"]))]) ((arith_tac) THEN (done_tac))); ((repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [2] [])))))); (((use_arg_then2 ("set_nth_default", [set_nth_default])) (thm_tac apply_tac)) THEN (((use_arg_then2 ("j_ineq", [])) (disch_tac [])) THEN (clear_assumption "j_ineq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ];; (* Finalization of the section SplitListHyp *) let split_list_hyp_alt = Sections.finalize_theorem split_list_hyp_alt;; let d_not_in_dart_split_eq = Sections.finalize_theorem d_not_in_dart_split_eq;; let list_eq_cat_find_pair_list = Sections.finalize_theorem list_eq_cat_find_pair_list;; let list_eq_cat_list_diag = Sections.finalize_theorem list_eq_cat_list_diag;; let split_list_explicit = Sections.finalize_theorem split_list_explicit;; let darts_of_list_split = Sections.finalize_theorem darts_of_list_split;; let darts_of_list_split_same = Sections.finalize_theorem darts_of_list_split_same;; let list_of_elements_split = Sections.finalize_theorem list_of_elements_split;; let mem_list_hyp_diag = Sections.finalize_theorem mem_list_hyp_diag;; let good_list_split = Sections.finalize_theorem good_list_split;; let hypermap_of_list_perm = Sections.finalize_theorem hypermap_of_list_perm;; let find_face_rot = Sections.finalize_theorem find_face_rot;; let rot_list_of_darts_perm = Sections.finalize_theorem rot_list_of_darts_perm;; let rot_hypermap_of_list_eq = Sections.finalize_theorem rot_hypermap_of_list_eq;; let hypermap_of_split_list_eq3 = Sections.finalize_theorem hypermap_of_split_list_eq3;; let f_split_list = Sections.finalize_theorem f_split_list;; Sections.end_section "SplitListHyp";; (* Section FanAndList *) Sections.begin_section "FanAndList";; (* Lemma set_of_edge_subset *) let set_of_edge_subset = Sections.section_proof ["V";"E";"E'";"x"] `E SUBSET E' ==> set_of_edge x V E SUBSET set_of_edge x V E'` [ ((((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["subE"]) THEN (move ["y"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("subE", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma fan_list_iso_invariant *) let fan_list_iso_invariant = Sections.section_proof ["F1";"F2";"f"] `fan_list_iso (fan_list_iso (f, F1), F2) = fan_list_iso (f, F1)` [ ((((use_arg_then2 ("F2", [])) (disch_tac [])) THEN (clear_assumption "F2") THEN ((use_arg_then2 ("F1", [])) (disch_tac [])) THEN (clear_assumption "F1") THEN BETA_TAC THEN (case THEN ((move ["V"]) THEN (move ["E"]))) THEN (case THEN ((move ["V'"]) THEN (move ["E'"])))) THEN ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["v"]) THEN (move ["w"]))))); ((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("fan_list_iso", [fan_list_iso]))(fun tmp_arg1 -> (use_arg_then2 ("fan_list_nodes_iso", [fan_list_nodes_iso]))(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)); ];; (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));; (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));; (Sections.add_section_var (mk_var ("L", (`:((A)list)list`))));; (Sections.add_section_var (mk_var ("f", (`:real^3#real^3 -> A#A`))));; (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));; (Sections.add_section_hyp "goodL" (`good_list L`));; (Sections.add_section_hyp "f_iso" (`hyp_iso f (hypermap_of_fan (V,E), hypermap_of_list L)`));; (* Lemma hyp_iso_eq_fan_list_iso *) let hyp_iso_eq_fan_list_iso = Sections.section_proof ["y"] `y IN dart_of_fan (V,E) ==> f y = fan_list_iso (f, (V,E)) y` [ ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH"]) THEN (move ["mapsH"]))))); ((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 (case THEN ((move ["dartG"]) THEN (move ["mapsG"]))))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G"))); ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (V,E) ==> f d IN darts_of_list L`))) (term_tac (have_gen_tac ["d"](move ["f_in"])))); ((((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartG", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["d_in"])) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((use_arg_then2 ("y", [])) (disch_tac [])) THEN (clear_assumption "y") THEN case THEN ((move ["a"]) THEN (move ["b"])) THEN (move ["ab_in"])); (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] [])))); ((fun arg_tac -> arg_tac (Arg_term (`fan_list_nodes_iso _`))) (term_tac (set_tac "h"))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?g. !v w. (v,w) IN dart_of_fan (V,E) ==> f(v,w) = (h v:A, g (v,w):A)`))) (term_tac (have_gen_tac [](case THEN ((move ["g"]) THEN (move ["f_eq"]))))))); (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("IN_DART_OF_FAN", [IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["vw_eq"])) THEN (move ["vw_in"])); ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac))); ((((use_arg_then2 ("mapsG", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mapsH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext_explicit", [e_fan_pair_ext_explicit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("dartG", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))); ((((repeat_tactic 1 9 (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 1 (((use_arg_then2 ("dart_switch", [dart_switch]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) 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)); ((fun arg_tac -> arg_tac (Arg_term (`\d. SND (f d)`))) (term_tac exists_tac)); ((BETA_TAC THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"])) THEN ((((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("h_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fan_list_nodes_iso", [fan_list_nodes_iso]))(thm_tac (new_rewrite [] [])))))); (((fun arg_tac -> arg_tac (Arg_term (`set_of_edge v V E = {}`))) (disch_eq_tac "set_empty" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(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 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))); ((THENL_FIRST) case (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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 ((((use_arg_then2 ("set_empty", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((BETA_TAC THEN (case THEN (move ["u"])) THEN (case THEN (move ["_"])) THEN (case THEN ((move ["eq1"]) THEN (move ["eq2"])))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in1"])))); ((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(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 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))); (case THEN ((TRY done_tac)) THEN (case THEN (move ["u"])) THEN (case THEN (move ["empty"])) THEN (move ["eq"])); ((((use_arg_then2 ("empty", [])) (disch_tac [])) THEN (clear_assumption "empty") THEN BETA_TAC) THEN ((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_empty", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`CHOICE _`))) (term_tac (set_tac "w'"))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f (v,w') IN node G (f (v,w))`))) (term_tac (have_gen_tac []ALL_TAC)))); ((((use_arg_then2 ("Hypermap.node", [Hypermap.node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Hypermap.orbit_map", [Hypermap.orbit_map]))(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 ("mapsG", []))(thm_tac (new_rewrite [] []))))); (BETA_TAC THEN (case THEN (move ["n"])) THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("fst_n_list_ext_power", [fst_n_list_ext_power]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); (((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartG", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (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 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FUN_IN_IMAGE", [FUN_IN_IMAGE]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("NODE_HYPERMAP_OF_FAN_ALT", [NODE_HYPERMAP_OF_FAN_ALT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); (((use_arg_then2 ("w'", [])) (term_tac exists_tac)) THEN ((split_tac) THEN ((TRY done_tac))) THEN (((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CHOICE_DEF", [CHOICE_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ssrbool.implybF", [Ssrbool.implybF]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["eq"]))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (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 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma fan_list_nodes_iso_surj *) let fan_list_nodes_iso_surj = Sections.section_proof [] `SURJ (fan_list_nodes_iso (f,(V,E))) V (elements_of_list L)` [ ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypV"]))); ((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 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso_eq"]))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G"))); ((((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 (repeat_tactic 1 9 (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))))); ((THENL) (split_tac) [(move ["v"]); ((move ["a"]) THEN (case THEN (move ["b"])))]); ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("DART_EXISTS", [DART_EXISTS])) (fun fst_arg -> (use_arg_then2 ("E", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["w"])) THEN (move ["vw_in"])); ((fun arg_tac -> arg_tac (Arg_term (`fan_list_nodes_iso (f,V,E) w`))) (term_tac exists_tac)); ((((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(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 ("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 ("iso_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(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 ("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 (`res_inv f (dart H) (a,b)`))) (term_tac (set_tac "d"))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inv", [hyp_iso_inv])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); (((((use_arg_then2 ("d_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (move ["d_in"])); (((fun arg_tac -> arg_tac (Arg_term (`FST d`))) (term_tac exists_tac)) THEN (split_tac)); (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (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)))(thm_tac (new_rewrite [] [])))) 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 (`f d = a,b`))) (term_tac (have_gen_tac []ALL_TAC)))); ((((((use_arg_then2 ("iso_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] [])))) 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 ("d_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("surj_res_inv_right", [surj_res_inv_right])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_SURJ", [hyp_iso_SURJ])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (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 [] []))))) THEN (done_tac)); ];; (* Lemma fan_list_nodes_to *) let fan_list_nodes_to = Sections.section_proof ["v"] `v IN V ==> fan_list_nodes_iso (f,(V,E)) v IN elements_of_list L` [ ((((use_arg_then2 ("fan_list_nodes_iso_surj", [fan_list_nodes_iso_surj])) (disch_tac [])) THEN (clear_assumption "fan_list_nodes_iso_surj") THEN BETA_TAC) THEN ((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (move ["surj"]) THEN (move ["vV"])) THEN (((use_arg_then2 ("surj", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma fan_list_diag_eq *) let fan_list_diag_eq = Sections.section_proof ["v";"w"] `(v,w) IN dart1_of_fan (V,E) ==> fan_list_iso (f,(V,E)) (w, sigma_fan (vec 0) V E v w) = list_hyp_diag L (f (v,w))` [ ((((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])); ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"]))); ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in"])))); (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fan_hyp"]))); ((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 ["list_hyp"]))); ((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (fun arg -> thm_tac MP_TAC arg THEN (move ["f_eq"]))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G"))); ((fun arg_tac -> arg_tac (Arg_term (`FST _`))) (term_tac (set_tac "y"))); ((fun arg_tac -> arg_tac (Arg_term (`y = FST (inverse (face_map G) (f (v,w)))`))) (term_tac (have_gen_tac [](move ["y_eq"])))); (((((use_arg_then2 ("list_hyp", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_hyp", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fan_hyp", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fan_hyp", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("Hypermap_and_fan.INVERSE_F_FAN_PAIR_EXT_EXPLICIT", [Hypermap_and_fan.INVERSE_F_FAN_PAIR_EXT_EXPLICIT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_switch", [dart_switch]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("in_dart1_in_dart", [in_dart1_in_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (Sections.add_section_hyp "good_nodes" (`good_list_nodes L`));; (* Lemma fan_list_nodes_iso_BIJ *) let fan_list_nodes_iso_BIJ = Sections.section_proof [] `BIJ (fan_list_nodes_iso (f,(V,E))) V (elements_of_list L)` [ ((((use_arg_then2 ("finite_surj_eq_bij", [finite_surj_eq_bij]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fan_list_nodes_iso_surj", [fan_list_nodes_iso_surj]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((fun arg_tac -> (use_arg_then2 ("fan_imp_finite_set", [fan_imp_finite_set])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_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_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((fun arg_tac -> (use_arg_then2 ("iffLR", [iffLR])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (use_arg_then2 ("NODE_SET_AS_IMAGE", [NODE_SET_AS_IMAGE])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["f"]) THEN (case THEN (move ["inj"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))); (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ])) (thm_tac apply_tac)) THEN (((((fun arg_tac -> (use_arg_then2 ("fan_imp_finite_set", [fan_imp_finite_set])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)); ];; (* Lemma fan_list_nodes_iso_inj *) let fan_list_nodes_iso_inj = Sections.section_proof ["x";"y"] `x IN V /\ y IN V /\ fan_list_nodes_iso (f,(V,E)) x = fan_list_nodes_iso (f,(V,E)) y ==> x = y` [ (BETA_TAC THEN (case THEN (move ["x_in"])) THEN (case THEN (move ["y_in"])) THEN (move ["eq"])); ((((use_arg_then2 ("fan_list_nodes_iso_BIJ", [fan_list_nodes_iso_BIJ])) (disch_tac [])) THEN (clear_assumption "fan_list_nodes_iso_BIJ") THEN BETA_TAC) THEN (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (move ["inj"]) THEN (move ["_"]))); (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (exact_tac)); ];; (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));; (* Lemma iso_imp_good_conditions *) let iso_imp_good_conditions = Sections.section_proof ["d"] `MEM d (list_of_darts L) /\ 3 < sizel (find_face L d) ==> ~MEM (list_hyp_diag L d) (list_of_darts L) /\ ~(FST (list_hyp_diag L d) = SND (list_hyp_diag L d))` [ (BETA_TAC THEN (case THEN ((move ["mem_d"]) THEN (move ["f_size"])))); ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypV"]))); ((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_fan (V,E)`))) (term_tac (set_tac "H"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G"))); ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN BETA_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 (move ["d_in"]))); ((fun arg_tac -> arg_tac (Arg_term (`?x. f x = d /\ x IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((case THEN ((move ["v"]) THEN (move ["w"]))) THEN (case THEN ((move ["d_eq"]) THEN (move ["vw_in"])))))))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["x"]) THEN (case THEN ((move ["x_in"]) THEN (move ["f_eq"]))))))); (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E) /\ v,w IN dart H`))) (term_tac (have_gen_tac [](move ["vw_in1"])))); (((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`3 < CARD (face H (v,w))`))) (term_tac (have_gen_tac [](move ["card_f"])))); (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_card_components", [hyp_iso_card_components])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("G_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_face_of_list", [card_face_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_ROT (-1)) (((((use_arg_then2 ("d_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fan_list_diag_eq", [fan_list_diag_eq]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (split_tac))); (((repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("implybF", [implybF]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))); ((((use_arg_then2 ("sigma_fan_inV", [sigma_fan_inV]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))); ((((use_arg_then2 ("sigma_fan_not_fixed", [sigma_fan_not_fixed]))(gsym_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 ("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 -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_diag_not_in_dart", [fully_surrounded_diag_not_in_dart])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC); (((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (move ["ww'_in"]))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'"))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ww'_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN (case THEN ((move ["a"]) THEN (move ["b"])))))); ((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["ab_in"]))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a IN V /\ b IN V`))) (term_tac (have_gen_tac [](move ["ab_inV"])))) ((repeat_tactic 1 9 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("a", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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 (`w IN V /\ w' IN V`))) (term_tac (have_gen_tac [](move ["ww'_inV"])))); (((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sigma_fan_inV", [sigma_fan_inV]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))); (BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["eq1"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["eq2"])); (((((use_arg_then2 ("eq1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma iso_imp_good_list_split *) let iso_imp_good_list_split = Sections.section_proof ["d"] `good_list (split_list_hyp L d)` [ ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); (((fun arg_tac -> (use_arg_then2 ("good_list_split", [good_list_split])) (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)); (((fun arg_tac -> arg_tac (Arg_term (`sizel (find_pair_list L d) <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); (((use_arg_then2 ("iso_imp_good_conditions", [iso_imp_good_conditions])) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma split_list_hyp_iso *) let split_list_hyp_iso = Sections.section_proof ["d"] `d IN dart_of_fan (V,E) ==> hyp_iso (fan_list_iso (f,(V,E))) (hypermap_of_fan (split_fan_face (V,E) d), hypermap_of_list (split_list_hyp L (f d)))` [ (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN BETA_TAC THEN (case THEN ((move ["v"]) THEN (move ["w"]))) THEN (move ["vw_in"])); ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypV"]))); ((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_fan (V,E)`))) (term_tac (set_tac "H"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G"))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["d1_eq"]))); ((fun arg_tac -> arg_tac (Arg_term (`MEM (f (v,w)) (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_fd"])))); (((((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 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`CARD (face H (v,w)) = sizel (find_face L (f (v,w)))`))) (term_tac (have_gen_tac [](move ["card_f"])))); (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_card_components", [hyp_iso_card_components])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(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)); ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"]))); (((fun arg_tac -> arg_tac (Arg_term (`sizel (find_face L (f (v,w))) <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((fun arg_tac -> (use_arg_then2 ("hypermap_of_split_list_eq3", [hypermap_of_split_list_eq3])) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("G_def", []))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("split_fan_face_eq", [split_fan_face_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fanV", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FULLY_SURROUNDED_IMP_CARD_FACE_GE_3", [FULLY_SURROUNDED_IMP_CARD_FACE_GE_3])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac)); (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_ext", [hyp_iso_ext])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (move ["x_in"])); ((((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`3 < CARD (face (hypermap_of_fan (V,E)) (v,w))`))) (term_tac (have_gen_tac [](move ["card_f3"])))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["fan_split"]) THEN (case THEN (move ["dart_splitV_eq"])) THEN (move ["f_split_surr"]))))); ((fun arg_tac -> arg_tac (Arg_term (`split_fan_face (V,E) (v,w)`))) (term_tac (set_tac "F1"))); (in_tac ["f_split_surr"; "fan_split"] false (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (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 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_split_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (simp_tac))) THEN (move ["split1_eq"])); ((fun arg_tac -> (use_arg_then2 ("iso_imp_good_list_split", [iso_imp_good_list_split])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["good_split"]))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in1"])))) ((((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> (use_arg_then2 ("fan_list_diag_eq", [fan_list_diag_eq])) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["diag_eq"]))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac (set_tac "w'"))); ((fun arg_tac -> arg_tac (Arg_term (`fan_list_iso _`))) (term_tac (set_tac "R"))); ((fun arg_tac -> arg_tac (Arg_term (`dart (hypermap_of_list (split_list_hyp L (f (v,w)))) = darts_of_list L UNION {R (w',w), R (w, w')}`))) (term_tac (have_gen_tac [](move ["dart_splitL_eq"])))); ((((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("good_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`3 < sizel (find_pair_list L (f (v,w)))`))) (term_tac (have_gen_tac [](move ["gt3"])))); ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); (((fun arg_tac -> (use_arg_then2 ("perm_eq_set_of_list_eq", [perm_eq_set_of_list_eq])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("darts_of_list_split", [darts_of_list_split])) (fun fst_arg -> (use_arg_then2 ("gt3", [])) (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 ("APPEND_cat", [APPEND_cat]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SET_OF_LIST_APPEND", [SET_OF_LIST_APPEND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("UNION_COMM", [UNION_COMM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] []))))); ((congr_tac (`_1 UNION _2`)) THEN ((TRY done_tac))); ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL set_of_list)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("diag_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("R_def", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.PER_SET2)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (simp_tac))); ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("good_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H1"))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list _`))) (term_tac (set_tac "G1"))); (BETA_TAC THEN (move ["hypL1"]) THEN (move ["hypV1"])); ((fun arg_tac -> arg_tac (Arg_term (`dart G1 = IMAGE R (dart H1)`))) (term_tac (have_gen_tac [](move ["dartG1_eq"])))); ((((use_arg_then2 ("dart_splitL_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_splitV_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((use_arg_then2 ("IMAGE_UNION", [IMAGE_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMAGE_CLAUSES)))(thm_tac (new_rewrite [] [])))))) THEN ((congr_tac (`_1 UNION _2`)) THEN ((TRY done_tac)))); (((((fun arg_tac -> (use_arg_then2 ("iso_dart", [iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("image_ext_eq", [image_ext_eq])) (thm_tac apply_tac)) THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("hyp_iso_edge_face", [hyp_iso_edge_face]))(thm_tac (new_rewrite [] [])))) THEN (split_tac)); ((((use_arg_then2 ("dartG1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Misc_defs_and_lemmas.IMAGE_SURJ", [Misc_defs_and_lemmas.IMAGE_SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))); ((THENL_FIRST) (split_tac) ((BETA_TAC THEN (move ["x"]) THEN (move ["x_in"])) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac))); (BETA_TAC THEN (case THEN ((move ["v1"]) THEN (move ["w1"]))) THEN (case THEN ((move ["v2"]) THEN (move ["w2"]))) THEN (case THEN (move ["vw1_in"])) THEN (case THEN (move ["vw2_in"])) THEN (move ["eq"])); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`v1 IN V /\ v2 IN V /\ w1 IN V /\ w2 IN V`))) (term_tac (have_gen_tac [](move ["inV"]))))); ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))); ((BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("vw2_in", [])) (disch_tac [])) THEN (clear_assumption "vw2_in") THEN ((use_arg_then2 ("vw1_in", [])) (disch_tac [])) THEN (clear_assumption "vw1_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))); (BETA_TAC THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["vw1_in"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC))))); ((((use_arg_then2 ("vw1_in", [])) (disch_tac [])) THEN (clear_assumption "vw1_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("F1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac)); (case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["ab_in"])); ((fun arg_tac -> arg_tac (Arg_term (`R (a,b) IN dart G1`))) (term_tac (have_gen_tac [](move ["Rab_in"])))); (((((use_arg_then2 ("dartG1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac)) THEN (done_tac)); (split_tac); ((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL1", []))(thm_tac (new_rewrite [] [])))) 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 ("hypL1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext_explicit", [e_fan_pair_ext_explicit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV1", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_split_fan_face))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_f3", [])) (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 ("F1_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "u"))); (BETA_TAC THEN (move ["f_fan_eq"])); (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_split_list))) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC)); (((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("iso_imp_good_conditions", [iso_imp_good_conditions])) (thm_tac apply_tac))); ((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`split_list_hyp L _`))) (term_tac (set_tac "L2"))); ((((use_arg_then2 ("diag_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (BETA_TAC THEN (move ["f_list_eq"]))); ((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("split1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((((use_arg_then2 ("hypL1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,E) ==> R x = f x`))) (term_tac (have_gen_tac ["x"](move ["R_eq_f"])))); (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((((use_arg_then2 ("R_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`a,b = v,w`))) (disch_eq_tac "eq1" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`w',v = inverse (face_map H) (v,w)`))) (term_tac (have_gen_tac [](move ["w'v_eq"])))); (((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INVERSE_F_FAN_PAIR_EXT_EXPLICIT", [INVERSE_F_FAN_PAIR_EXT_EXPLICIT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`w',v IN dart H`))) (term_tac (have_gen_tac [](move ["w'v_in"])))); (((((use_arg_then2 ("w'v_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`u,w' = inverse (face_map H) (w',v)`))) (term_tac (have_gen_tac [](move ["uw'_eq"])))); ((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INVERSE_F_FAN_PAIR_EXT_EXPLICIT", [INVERSE_F_FAN_PAIR_EXT_EXPLICIT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'v_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("u_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((fun arg_tac -> arg_tac (Arg_term (`a,b = w,w'`))) (disch_eq_tac "eq2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'v_eq", []))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`R (w',w) = e_list (R (w,w'))`))) (term_tac (have_gen_tac [](move ["Rw'w_eq"])))); (((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((fun arg_tac -> arg_tac (Arg_term (`a,b = w',w`))) (disch_eq_tac "eq3" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); ((((use_arg_then2 ("eq3", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Rw'w_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`f_fan_pair (V,E) (v,w) = face_map H (v,w)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))); (((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((fun arg_tac -> arg_tac (Arg_term (`find_face L (f (v,w))`))) (term_tac (set_tac "ff"))); ((fun arg_tac -> arg_tac (Arg_term (`R (u,w') = prev_el ff (prev_el ff (f (v,w)))`))) (term_tac (have_gen_tac [](move ["Ruw'_eq"])))); ((((use_arg_then2 ("uw'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("w'v_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [2] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_fd", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ff_def", []))(thm_tac (new_rewrite [] []))))); (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`prev_el ff (f (v,w)) IN darts_of_list L`))) (term_tac (have_gen_tac [](move ["mem_ff"]))))); ((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_ff", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el ff (f (v,w))) = ff`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac))); ((((fun arg_tac -> (use_arg_then2 ("find_face_eq", [find_face_eq])) (fun fst_arg -> (use_arg_then2 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))); ((repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ff_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac))); (((fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("ff_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ff_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 (`a,b = u,w'`))) (disch_eq_tac "eq4" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)); (((((use_arg_then2 ("eq4", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ruw'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Rw'w_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) (((((use_arg_then2 ("hypV1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ab_in", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart H`))) (term_tac (have_gen_tac [](move ["ab_in0"])))); ((((use_arg_then2 ("ab_in", [])) (disch_tac [])) THEN (clear_assumption "ab_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_splitV_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))))); (((((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq3", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_ROT (-1)) (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`f_fan_pair (V,E) (a,b) = face_map H (a,b)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))); (((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ab_in0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypV", []))(gsym_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 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rab_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("Ruw'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rw'w_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("R_eq_f", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`a IN V /\ b IN V /\ u IN V /\ v IN V /\ w' IN V /\ w IN V`))) (term_tac (have_gen_tac [](move ["in_all"])))); ((((use_arg_then2 ("ab_in0", [])) (disch_tac [])) THEN (clear_assumption "ab_in0") THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (simp_tac))); ((((use_arg_then2 ("w'v_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (simp_tac))); (((fun arg_tac -> (use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps])) (fun fst_arg -> (use_arg_then2 ("w'v_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC); (((((use_arg_then2 ("uw'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (((fun arg_tac ->(use_arg_then2 ("eq1", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("eq2", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("eq3", []))(fun tmp_arg1 -> (use_arg_then2 ("eq4", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2)))))) (disch_tac [])) THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)); ((repeat_tactic 1 9 (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))); ((repeat_tactic 1 9 (case)) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["h1"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["h2"])) THEN ((((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h2", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma iso_imp_good_list_nodes_split *) let iso_imp_good_list_nodes_split = Sections.section_proof ["d"] `good_list_nodes (split_list_hyp L d)` [ ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_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 (((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)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["d_in"]))); ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((case THEN ((move ["v"]) THEN (move ["w"]))) THEN (case THEN ((move ["vw_in"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))))))))); (in_tac ["vw_in"] false (((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (use_arg_then2 ("split_list_hyp_iso", [split_list_hyp_iso])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso_th"]))); ((((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("iso_imp_good_list_split", [iso_imp_good_list_split]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))); ((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("iso_th", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))); (((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_of_elements_split", [list_of_elements_split])) (fun fst_arg -> (use_arg_then2 ("L", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["fan_split"]) THEN (move ["_"]))))); (in_tac ["fan_split"] true (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("fan_number_of_nodes", [fan_number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("fan_number_of_nodes", [fan_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))); (((((fun arg_tac -> (use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Finalization of the section FanAndList *) let set_of_edge_subset = Sections.finalize_theorem set_of_edge_subset;; let fan_list_iso_invariant = Sections.finalize_theorem fan_list_iso_invariant;; let hyp_iso_eq_fan_list_iso = Sections.finalize_theorem hyp_iso_eq_fan_list_iso;; let fan_list_nodes_iso_surj = Sections.finalize_theorem fan_list_nodes_iso_surj;; let fan_list_nodes_to = Sections.finalize_theorem fan_list_nodes_to;; let fan_list_diag_eq = Sections.finalize_theorem fan_list_diag_eq;; let fan_list_nodes_iso_BIJ = Sections.finalize_theorem fan_list_nodes_iso_BIJ;; let fan_list_nodes_iso_inj = Sections.finalize_theorem fan_list_nodes_iso_inj;; let iso_imp_good_conditions = Sections.finalize_theorem iso_imp_good_conditions;; let iso_imp_good_list_split = Sections.finalize_theorem iso_imp_good_list_split;; let split_list_hyp_iso = Sections.finalize_theorem split_list_hyp_iso;; let iso_imp_good_list_nodes_split = Sections.finalize_theorem iso_imp_good_list_nodes_split;; Sections.end_section "FanAndList";; (* Close the module *) end;;