text_formalization/fan/hypermap_iso-compiled.hl

   1 needs "Examples/ssrnat-compiled.hl";;
   2
   3 (* Module Hypermap_iso*)
   4 module Hypermap_iso = struct
   5
   6 let hyp_iso = new_definition `hyp_iso f (H, G) <=>
   7                            BIJ f (dart H) (dart G) /\
   8                         (!x. x IN dart H ==>
   9                         edge_map G (f x) = f (edge_map H x) /\
  10                                node_map G (f x) = f (node_map H x) /\
  11                            face_map G (f x) = f (face_map H x))`;;
  12 let res_inv = new_definition `res_inv f s = (\y. @x. f x = y /\ x IN s)`;;
  13 open Ssrfun;;
  14 open Ssrbool;;
  15 open Ssrnat;;
  16 open Fan;;
  17 open Hypermap;;
  18 open Fan_defs;;
  19 open Hypermap_and_fan;;
  20 parse_as_infix("iso",(24,"right"));;
  21 let inE = CONJUNCT2 IN_ELIM_THM;;
  22 let IN_TRANS = prove(`!(x:A) s t. t SUBSET s /\ x IN t ==> x IN s`, SET_TAC[]);;
  23
  24 (* Lemma bij_disjoint_union *)
  25 let bij_disjoint_union = Sections.section_proof ["f";"g";"s";"t";"s'";"t'"]
  26 `DISJOINT s t /\ DISJOINT s' t' /\ BIJ (f:A->B) s s' /\ BIJ (g:A->B) t t'
  27                 ==> BIJ (\x. if x IN s then f x else g x) (s UNION t) (s' UNION t')`
  28 [
  29    ((repeat_tactic 1 9 (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))));
  30    (BETA_TAC THEN (case THEN (move ["d_st"])) THEN (case THEN (move ["d_s't'"])) THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["fx"]) THEN (move ["f_inj"]))) THEN (case THEN ((move ["_"]) THEN (move ["f_surj"]))) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["gx"]) THEN (move ["g_inj"]))) THEN (case THEN ((move ["_"]) THEN (move ["g_surj"]))));
  31    ((fun arg_tac -> arg_tac (Arg_term (`x IN t ==> ~(x IN s)`))) (term_tac (have_gen_tac ["x"](move ["x_in_t"]))));
  32    ((BETA_TAC THEN (move ["xt"])) THEN (((use_arg_then2 ("d_st", [])) (disch_tac [])) THEN (clear_assumption "d_st") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (move ["xs"])));
  33    (((((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
  34    ((repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 ((split_tac))));
  35    ((THENL_FIRST) (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x_in"]))) (((((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
  36    (((((fun arg_tac -> (use_arg_then2 ("x_in_t", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  37    ((BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y_in"]))) THEN (((repeat_tactic 0 10 (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("y_in", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("x_in_t", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))) THEN (move ["eq"])));
  38    ((((fun arg_tac -> (use_arg_then2 ("f_inj", [])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  39    ((((use_arg_then2 ("d_s't'", [])) (disch_tac [])) THEN (clear_assumption "d_s't'") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
  40    (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  41    ((((use_arg_then2 ("d_s't'", [])) (disch_tac [])) THEN (clear_assumption "d_s't'") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
  42    (((fun arg_tac -> arg_tac (Arg_term (`g x`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  43    ((((fun arg_tac -> (use_arg_then2 ("g_inj", [])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  44    ((THENL_FIRST) (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x_in"]))) (((((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
  45    (((((fun arg_tac -> (use_arg_then2 ("x_in_t", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("gx", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  46    (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x_in"])));
  47    (((fun arg_tac -> (use_arg_then2 ("f_surj", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (case THEN ((move ["ys"]) THEN (move ["fy_eq"]))));
  48    (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("ys", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  49    (((fun arg_tac -> (use_arg_then2 ("g_surj", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (case THEN ((move ["yt"]) THEN (move ["gy_eq"]))));
  50    (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("yt", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("x_in_t", [])) (fun fst_arg -> (use_arg_then2 ("yt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  51 ];;
  52
  53 (* Lemma disjoint_diff *)
  54 let disjoint_diff = Sections.section_proof ["s";"t"]
  55 `DISJOINT s (t DIFF s)`
  56 [
  57    (((((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]));
  58    ((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_DIFF", [IN_DIFF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] [])))));
  59    (((((use_arg_then2 ("andbA", [andbA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbAC", [andbAC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbN", [andbN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andFb", [andFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  60 ];;
  61
  62 (* Lemma image_lemma *)
  63 let image_lemma = Sections.section_proof ["f";"P"]
  64 `IMAGE f {x | P x} = {f x | P x}`
  65 [
  66    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  67 ];;
  68
  69 (* Section PowerOrbit *)
  70 Sections.begin_section "PowerOrbit";;
  71 (Sections.add_section_var (mk_var ("f", (`:A -> B`))));;
  72 (Sections.add_section_var (mk_var ("g1", (`:A -> A`))));;
  73 (Sections.add_section_var (mk_var ("g2", (`:B -> B`))));;
  74 (Sections.add_section_var (mk_var ("s", (`:A -> bool`))));;
  75 (Sections.add_section_hyp "g1s" (`!x. x IN s ==> g1 x IN s`));;
  76
  77 (* Lemma power_in *)
  78 let power_in = Sections.section_proof ["x";"n"]
  79 `x IN s ==> (g1 POWER n) x IN s`
  80 [
  81    ((THENL_FIRST) ((BETA_TAC THEN (move ["xs"])) THEN ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))])) (((((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
  82    (((((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("g1s", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  83 ];;
  84 (Sections.add_section_hyp "fg" (`!x. x IN s ==> f (g1 x) = g2 (f x)`));;
  85
  86 (* Lemma power_comm *)
  87 let power_comm = Sections.section_proof ["x";"n"]
  88 `x IN s ==> f ((g1 POWER n) x) = (g2 POWER n) (f x)`
  89 [
  90    ((THENL_FIRST) ((BETA_TAC THEN (move ["xs"])) THEN ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))])) (((repeat_tactic 1 9 (((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
  91    (((repeat_tactic 1 9 (((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fg", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("power_in", [power_in]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
  92 ];;
  93
  94 (* Lemma orbit_comm *)
  95 let orbit_comm = Sections.section_proof ["x"]
  96 `x IN s ==> orbit_map g2 (f x) = IMAGE f (orbit_map g1 x)`
  97 [
  98    (((repeat_tactic 1 9 (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["xs"]) THEN (move ["x"]));
  99    ((THENL) (split_tac) [((case THEN (move ["n"])) THEN (move ["h"])); ((case THEN (move ["y"])) THEN (case THEN (move ["x_eq"])) THEN (case THEN (move ["n"])) THEN (move ["h"]))]);
 100    ((fun arg_tac -> arg_tac (Arg_term (`(g1 POWER n) x`))) (term_tac exists_tac));
 101    (((((use_arg_then2 ("power_comm", [power_comm]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN (done_tac));
 102    (((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("power_comm", [power_comm]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 103 ];;
 104
 105 (* Finalization of the section PowerOrbit *)
 106 let power_in = Sections.finalize_theorem power_in;;
 107 let power_comm = Sections.finalize_theorem power_comm;;
 108 let orbit_comm = Sections.finalize_theorem orbit_comm;;
 109 Sections.end_section "PowerOrbit";;
 110
 111 (* Lemma image_ext_eq *)
 112 let image_ext_eq = Sections.section_proof ["f";"g";"s"]
 113 `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`
 114 [
 115    ((BETA_TAC THEN (move ["eq"])) THEN (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["y"])));
 116    (((split_tac) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["y_eq"])) THEN (move ["xs"])) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 117 ];;
 118
 119 (* Lemma image_res *)
 120 let image_res = Sections.section_proof ["f";"s";"u"]
 121 `s SUBSET u ==> IMAGE f s = IMAGE (res f u) s`
 122 [
 123    (((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (move ["su"])) THEN (((use_arg_then2 ("image_ext_eq", [image_ext_eq])) (thm_tac apply_tac)) THEN (move ["x"]) THEN (move ["xs"])));
 124    (((((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("su", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 125 ];;
 126
 127 (* Lemma im_in_image *)
 128 let im_in_image = Sections.section_proof ["f";"s";"x"]
 129 `f x IN IMAGE f s <=> x IN s \/ ?y. y IN s /\ ~(x = y) /\ f x = f y`
 130 [
 131    ((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((THENL) (split_tac) [((case THEN (move ["y"])) THEN (move ["h"])); ALL_TAC]));
 132    (((fun arg_tac -> arg_tac (Arg_term (`x IN s`))) (disch_eq_tac "x_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 133    (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
 134    ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 135    (((THENL) (BETA_TAC THEN ((THENL) case [(move ["x_in"]); ((case THEN (move ["y"])) THEN (move ["h"]))])) [((use_arg_then2 ("x", [])) (term_tac exists_tac)); ((use_arg_then2 ("y", [])) (term_tac exists_tac))]) THEN (done_tac));
 136 ];;
 137
 138 (* Section InjProps *)
 139 Sections.begin_section "InjProps";;
 140 (Sections.add_section_var (mk_var ("u", (`:A -> bool`))));;
 141 (Sections.add_section_var (mk_var ("f", (`:A -> B`))));;
 142 (Sections.add_section_hyp "inj" (`!x y. x IN u /\ y IN u /\ f x = f y ==> x = y`));;
 143
 144 (* Lemma image_inter_inj_gen *)
 145 let image_inter_inj_gen = Sections.section_proof ["s";"t"]
 146 `s SUBSET u /\ t SUBSET u
 147         ==> IMAGE f (s INTER t) = IMAGE f s INTER IMAGE f t`
 148 [
 149    ((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["su"]) THEN (move ["tu"]))));
 150    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]));
 151    ((THENL) (split_tac) [((case THEN (move ["x"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN ((move ["xs"]) THEN (move ["xt"])))); ((case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN ((move ["y_eq"]) THEN (move ["xs"]))) THEN (case THEN (move ["x'"])) THEN (case THEN ((move ["y_eq'"]) THEN (move ["x't"]))))]);
 152    ((split_tac) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
 153    (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (repeat_tactic 1 9 (((split_tac) THEN ((TRY done_tac))))));
 154    (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("xs", [])) (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 -> (fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("x't", [])) (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 ((TRY done_tac)) THEN (((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y_eq'", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 155 ];;
 156
 157 (* Lemma image_inj_gen *)
 158 let image_inj_gen = Sections.section_proof ["s";"t"]
 159 `s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t
 160         ==> s = t`
 161 [
 162    ((((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["su"])) THEN (case THEN (move ["tu"])) THEN (move ["eq"]) THEN (move ["y"])) THEN ((split_tac) THEN (move ["y_in"])));
 163    ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then2 ("iffLR", [iffLR])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f y`))) (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 (ANTS_TAC)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)));
 164    (BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["f_eq"])) THEN (move ["xt"]));
 165    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (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 -> (fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("xt", [])) (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));
 166    ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then2 ("iffRL", [iffRL])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f y`))) (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 (ANTS_TAC)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)));
 167    (BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["f_eq"])) THEN (move ["xs"]));
 168    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (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 -> (fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("xs", [])) (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));
 169 ];;
 170
 171 (* Lemma image_set_inj_gen *)
 172 let image_set_inj_gen = Sections.section_proof ["s";"t"]
 173 `s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t ==> s = t`
 174 [
 175    ((((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["su"])) THEN (case THEN (move ["tu"])) THEN (move ["i_eq"]) THEN (move ["x"])) THEN ((split_tac) THEN (move ["x_in"])));
 176    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`f x IN IMAGE f s`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
 177    (((((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("im_in_image", [im_in_image]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN ((TRY done_tac)) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (case THEN (move ["neq"])) THEN (move ["f_eq"]));
 178    ((((use_arg_then2 ("neq", [])) (disch_tac [])) THEN (clear_assumption "neq") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)));
 179    (((((fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 180    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`f x IN IMAGE f t`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
 181    (((((use_arg_then2 ("i_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("im_in_image", [im_in_image]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN ((TRY done_tac)) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (case THEN (move ["neq"])) THEN (move ["f_eq"]));
 182    ((((use_arg_then2 ("neq", [])) (disch_tac [])) THEN (clear_assumption "neq") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (DISCH_THEN apply_tac)));
 183    (((((fun arg_tac -> (use_arg_then2 ("su", [])) (fun fst_arg -> (use_arg_then2 ("y_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("tu", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 184 ];;
 185
 186 (* Finalization of the section InjProps *)
 187 let image_inter_inj_gen = Sections.finalize_theorem image_inter_inj_gen;;
 188 let image_inj_gen = Sections.finalize_theorem image_inj_gen;;
 189 let image_set_inj_gen = Sections.finalize_theorem image_set_inj_gen;;
 190 Sections.end_section "InjProps";;
 191
 192 (* Section FiniteBijections *)
 193 Sections.begin_section "FiniteBijections";;
 194 (Sections.add_section_var (mk_var ("s", (`:A->bool`))));;
 195 (Sections.add_section_var (mk_var ("t", (`:B->bool`))));;
 196
 197 (* Lemma permutes_imp_bij *)
 198 let permutes_imp_bij = Sections.section_proof ["p"]
 199 `p permutes s ==> BIJ p s s`
 200 [
 201    ((BETA_TAC THEN (move ["perm"])) THEN ((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PERMUTES_IN_IMAGE", [PERMUTES_IN_IMAGE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
 202    ((THENL_FIRST) ((THENL) (split_tac) [((move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["xs"])) THEN (case THEN (move ["ys"])) THEN (move ["p_eq"])); ((move ["x"]) THEN (move ["xs"]))]) ((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INJECTIVE", [PERMUTES_INJECTIVE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 203    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PERMUTES_SURJECTIVE", [PERMUTES_SURJECTIVE])) (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 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (move ["p_eq"])) THEN ((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((split_tac) THEN ((TRY done_tac))));
 204    (((((fun arg_tac -> (use_arg_then2 ("PERMUTES_IN_IMAGE", [PERMUTES_IN_IMAGE])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 205 ];;
 206
 207 (* Lemma surj_image *)
 208 let surj_image = Sections.section_proof ["f"]
 209 `SURJ f s t ==> IMAGE f s = t`
 210 [
 211    (((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["surj"]))) THEN (move ["y"]));
 212    (((THENL) ((THENL) (split_tac) [((case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])); ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["x"])) THEN (case THEN ((move ["xs"]) THEN (move ["eq"]))))]) [(((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)); ((use_arg_then2 ("x", [])) (term_tac exists_tac))]) THEN (done_tac));
 213 ];;
 214
 215 (* Lemma surj_imp_finite *)
 216 let surj_imp_finite = Sections.section_proof ["f"]
 217 `FINITE s /\ SURJ f s t ==> FINITE t`
 218 [
 219    ((BETA_TAC THEN (case THEN (move ["fin_s"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj_image", [surj_image])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("FINITE_IMAGE", [FINITE_IMAGE])) (thm_tac apply_tac)) THEN (done_tac));
 220 ];;
 221
 222 (* Lemma inj_imp_finite *)
 223 let inj_imp_finite = Sections.section_proof ["f"]
 224 `FINITE t /\ INJ f s t ==> FINITE s`
 225 [
 226    ((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["fin_t"])) THEN (case THEN (move ["f_in"])) THEN (move ["inj"]));
 227    ((((fun arg_tac -> (use_arg_then2 ("FINITE_IMAGE_INJ_EQ", [FINITE_IMAGE_INJ_EQ])) (fun fst_arg -> (use_arg_then2 ("inj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("FINITE_SUBSET", [FINITE_SUBSET])) (fun fst_arg -> (use_arg_then2 ("fin_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))));
 228    ((BETA_TAC THEN (move ["y"]) THEN (case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])) THEN (((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)) THEN (done_tac));
 229 ];;
 230
 231 (* Lemma bij_finite_eq *)
 232 let bij_finite_eq = Sections.section_proof ["f"]
 233 `BIJ f s t ==> (FINITE s <=> FINITE t)`
 234 [
 235    (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (move ["bij"])) THEN ((THENL) (split_tac) [(move ["fin_s"]); (move ["fin_t"])]));
 236    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("surj_imp_finite", [surj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("fin_s", [])) (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)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 237    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inj_imp_finite", [inj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("fin_t", [])) (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)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 238 ];;
 239
 240 (* Lemma surj_imp_card_le *)
 241 let surj_imp_card_le = Sections.section_proof ["f"]
 242 `FINITE s /\ SURJ f s t ==> CARD t <= CARD s`
 243 [
 244    ((BETA_TAC THEN (case THEN (move ["fin_s"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj_image", [surj_image])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("CARD_IMAGE_LE", [CARD_IMAGE_LE])) (thm_tac apply_tac)) THEN (done_tac));
 245 ];;
 246
 247 (* Lemma inj_imp_card_le *)
 248 let inj_imp_card_le = Sections.section_proof ["f"]
 249 `FINITE t /\ INJ f s t ==> CARD s <= CARD t`
 250 [
 251    ((BETA_TAC THEN (case THEN (move ["fin_t"])) THEN (move ["inj"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["f_in"])) THEN (move ["inj2"])));
 252    ((((fun arg_tac -> (use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ])) (fun fst_arg -> (use_arg_then2 ("inj2", [])) (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 ("inj_imp_finite", [inj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("inj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 253    ((((((use_arg_then2 ("CARD_SUBSET", [CARD_SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fin_t", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]) THEN (case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])) THEN (((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)) THEN (done_tac));
 254 ];;
 255
 256 (* Lemma bij_card_eq *)
 257 let bij_card_eq = Sections.section_proof ["f"]
 258 `BIJ f s t /\ FINITE s ==> CARD t = CARD s`
 259 [
 260    (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["inj"]) THEN (move ["surj"]))) THEN (move ["fin_s"])) THEN (((use_arg_then2 ("anti_leq", [anti_leq])) (disch_tac [])) THEN (clear_assumption "anti_leq") THEN (DISCH_THEN apply_tac)));
 261    (((((fun arg_tac -> (use_arg_then2 ("surj_imp_card_le", [surj_imp_card_le])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("inj_imp_card_le", [inj_imp_card_le])) (fun fst_arg -> (use_arg_then2 ("inj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("surj_imp_finite", [surj_imp_finite])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 262 ];;
 263 (Sections.add_section_hyp "fin_s" (`FINITE s`));;
 264 (Sections.add_section_hyp "fin_t" (`FINITE t`));;
 265 (Sections.add_section_hyp "card_eq" (`CARD s = CARD t`));;
 266
 267 (* Lemma finite_inj_eq_surj *)
 268 let finite_inj_eq_surj = Sections.section_proof ["f"]
 269 `INJ f s t <=> SURJ f s t`
 270 [
 271    (((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andb_id2l", [andb_id2l])) (disch_tac [])) THEN (clear_assumption "andb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["f_in"])));
 272    ((((use_arg_then2 ("SURJECTIVE_IFF_INJECTIVE_GEN", [SURJECTIVE_IFF_INJECTIVE_GEN]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fin_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fin_t", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 273    ((((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]) THEN (case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["xs"])) THEN (((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (exact_tac)) THEN (done_tac));
 274 ];;
 275
 276 (* Lemma finite_inj_eq_bij *)
 277 let finite_inj_eq_bij = Sections.section_proof ["f"]
 278 `INJ f s t <=> BIJ f s t`
 279 [
 280    (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_inj_eq_surj", [finite_inj_eq_surj]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 281 ];;
 282
 283 (* Lemma finite_surj_eq_bij *)
 284 let finite_surj_eq_bij = Sections.section_proof ["f"]
 285 `SURJ f s t <=> BIJ f s t`
 286 [
 287    (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_inj_eq_surj", [finite_inj_eq_surj]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 288 ];;
 289
 290 (* Finalization of the section FiniteBijections *)
 291 let permutes_imp_bij = Sections.finalize_theorem permutes_imp_bij;;
 292 let surj_image = Sections.finalize_theorem surj_image;;
 293 let surj_imp_finite = Sections.finalize_theorem surj_imp_finite;;
 294 let inj_imp_finite = Sections.finalize_theorem inj_imp_finite;;
 295 let bij_finite_eq = Sections.finalize_theorem bij_finite_eq;;
 296 let surj_imp_card_le = Sections.finalize_theorem surj_imp_card_le;;
 297 let inj_imp_card_le = Sections.finalize_theorem inj_imp_card_le;;
 298 let bij_card_eq = Sections.finalize_theorem bij_card_eq;;
 299 let finite_inj_eq_surj = Sections.finalize_theorem finite_inj_eq_surj;;
 300 let finite_inj_eq_bij = Sections.finalize_theorem finite_inj_eq_bij;;
 301 let finite_surj_eq_bij = Sections.finalize_theorem finite_surj_eq_bij;;
 302 Sections.end_section "FiniteBijections";;
 303
 304 (* Section ResInverse *)
 305 Sections.begin_section "ResInverse";;
 306
 307 (* Lemma bij_alt *)
 308 let bij_alt = Sections.section_proof ["f";"s";"t"]
 309 `BIJ f s t <=>
 310         (!x. x IN s ==> f x IN t) /\
 311         (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\
 312         (!y. y IN t ==> ?x. x IN s /\ f x = y)`
 313 [
 314    (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbAC", [andbAC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbA", [andbA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbAC", [andbAC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 315 ];;
 316
 317 (* Section Ext *)
 318 Sections.begin_section "Ext";;
 319 (Sections.add_section_var (mk_var ("f", (`:A->B`))); Sections.add_section_var (mk_var ("g", (`:A->B`))));;
 320 (Sections.add_section_var (mk_var ("s", (`:A->bool`))));;
 321 (Sections.add_section_var (mk_var ("t", (`:B->bool`))));;
 322 (Sections.add_section_hyp "ext" (`!x. x IN s ==> f x = g x`));;
 323
 324 (* Lemma inj_ext *)
 325 let inj_ext = Sections.section_proof []
 326 `INJ f s t ==> INJ g s t`
 327 [
 328    (((repeat_tactic 1 9 (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["f_inj"])))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["xs"])); ((move ["x"]) THEN (move ["y"]) THEN (move ["h"]))]));
 329    (((((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 330    ((((use_arg_then2 ("f_inj", [])) (disch_tac [])) THEN (clear_assumption "f_inj") THEN (DISCH_THEN apply_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ext", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 331 ];;
 332
 333 (* Lemma surj_ext *)
 334 let surj_ext = Sections.section_proof []
 335 `SURJ f s t ==> SURJ g s t`
 336 [
 337    (((repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["f_surj"])))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["xs"])); ((move ["x"]) THEN (move ["xt"]))]));
 338    (((((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 339    (((fun arg_tac -> (use_arg_then2 ("f_surj", [])) (fun fst_arg -> (use_arg_then2 ("xt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["y"])) THEN (case THEN ((move ["ys"]) THEN (move ["eq"]))));
 340    (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 341 ];;
 342
 343 (* Lemma bij_ext *)
 344 let bij_ext = Sections.section_proof []
 345 `BIJ f s t ==> BIJ g s t`
 346 [
 347    (((THENL) (((repeat_tactic 1 9 (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"])) THEN (split_tac)) [(((use_arg_then2 ("inj_ext", [inj_ext])) (disch_tac [])) THEN (clear_assumption "inj_ext") THEN (exact_tac)); (((use_arg_then2 ("surj_ext", [surj_ext])) (disch_tac [])) THEN (clear_assumption "surj_ext") THEN (exact_tac))]) THEN (done_tac));
 348 ];;
 349
 350 (* Finalization of the section Ext *)
 351 let inj_ext = Sections.finalize_theorem inj_ext;;
 352 let surj_ext = Sections.finalize_theorem surj_ext;;
 353 let bij_ext = Sections.finalize_theorem bij_ext;;
 354 Sections.end_section "Ext";;
 355
 356 (* Lemma res_inv_left *)
 357 let res_inv_left = Sections.section_proof ["f";"s";"x"]
 358 `(!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ x IN s
 359         ==> res_inv f s (f x) = x`
 360 [
 361    (((((use_arg_then2 ("res_inv", [res_inv]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((move ["inj"]) THEN (move ["xs"]))));
 362    ((((use_arg_then2 ("SELECT_UNIQUE", [SELECT_UNIQUE])) (thm_tac apply_tac)) THEN (simp_tac) THEN (move ["y"])) THEN ((THENL) (split_tac) [(case THEN ((move ["f_eq"]) THEN (move ["ys"]))); ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]));
 363    ((((fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (use_arg_then2 ("f_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 364 ];;
 365
 366 (* Lemma res_inv_right *)
 367 let res_inv_right = Sections.section_proof ["f";"s";"t";"y"]
 368 `(!y. y IN t ==> ?x. x IN s /\ f x = y) /\ y IN t
 369         ==> f (res_inv f s y) = y /\ res_inv f s y IN s`
 370 [
 371    (((((use_arg_then2 ("res_inv", [res_inv]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["surj"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["x"])) THEN (move ["h"]));
 372    ((fun arg_tac -> (use_arg_then2 ("SELECT_AX", [SELECT_AX])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`\x. f x = y /\ x IN s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (simp_tac)));
 373    ((DISCH_THEN apply_tac) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
 374 ];;
 375
 376 (* Lemma res_inv_bij *)
 377 let res_inv_bij = Sections.section_proof ["f";"s";"t"]
 378 `BIJ f s t ==>
 379         (!x. x IN s ==> res_inv f s (f x) = x) /\
 380         (!y. y IN t ==> f (res_inv f s y) = y) /\
 381         (!y. y IN t ==> res_inv f s y IN s)`
 382 [
 383    (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]));
 384    (((THENL_FIRST) ((repeat_tactic 1 9 ((split_tac))) THEN (BETA_TAC THEN (move ["a"]) THEN (move ["a_in"]))) ((use_arg_then2 ("res_inv_left", [res_inv_left])) (thm_tac apply_tac))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (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 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 385 ];;
 386
 387 (* Lemma bij_res_inv *)
 388 let bij_res_inv = Sections.section_proof ["f";"s";"t"]
 389 `BIJ f s t ==> BIJ (res_inv f s) t s`
 390 [
 391    ((repeat_tactic 1 9 (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f_in"])) THEN (case THEN ((move ["inj"]) THEN (move ["surj"]))));
 392    ((THENL_FIRST) ((THENL) (split_tac) [((move ["x"]) THEN (move ["xt"])); ALL_TAC]) ((((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 393    ((THENL_ROT (-1)) ((THENL) (split_tac) [((move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["xt"])) THEN (case THEN (move ["yt"])) THEN (move ["inv_eq"])); ((move ["x"]) THEN (move ["xs"]))]));
 394    (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("f_in", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res_inv_left", [res_inv_left]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 395    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (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 ("inv_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
 396    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("surj", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 397 ];;
 398
 399 (* Lemma inj_res_inv_left *)
 400 let inj_res_inv_left = Sections.section_proof ["f";"s";"t";"x"]
 401 `INJ f s t /\ x IN s ==> res_inv f s (f x) = x`
 402 [
 403    (((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (move ["h"])) THEN ((((use_arg_then2 ("res_inv_left", [res_inv_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
 404 ];;
 405
 406 (* Lemma surj_res_inv_right *)
 407 let surj_res_inv_right = Sections.section_proof ["f";"s";"t";"y"]
 408 `SURJ f s t /\ y IN t ==>
 409         f (res_inv f s y) = y /\ res_inv f s y IN s`
 410 [
 411    (((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"])) THEN ((repeat_tactic 1 9 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (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 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (done_tac));
 412 ];;
 413
 414 (* Finalization of the section ResInverse *)
 415 let bij_alt = Sections.finalize_theorem bij_alt;;
 416 let inj_ext = Sections.finalize_theorem inj_ext;;
 417 let surj_ext = Sections.finalize_theorem surj_ext;;
 418 let bij_ext = Sections.finalize_theorem bij_ext;;
 419 let res_inv_left = Sections.finalize_theorem res_inv_left;;
 420 let res_inv_right = Sections.finalize_theorem res_inv_right;;
 421 let res_inv_bij = Sections.finalize_theorem res_inv_bij;;
 422 let bij_res_inv = Sections.finalize_theorem bij_res_inv;;
 423 let inj_res_inv_left = Sections.finalize_theorem inj_res_inv_left;;
 424 let surj_res_inv_right = Sections.finalize_theorem surj_res_inv_right;;
 425 Sections.end_section "ResInverse";;
 426
 427 (* Section Iso *)
 428 Sections.begin_section "Iso";;
 429
 430 (* Lemma hyp_iso_imp_iso *)
 431 let hyp_iso_imp_iso = Sections.section_proof ["H";"G";"f"]
 432 `hyp_iso f (H, G) ==> H iso G`
 433 [
 434    ((((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso", [iso]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"])) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
 435 ];;
 436
 437 (* Lemma iso_imp_hyp_iso *)
 438 let iso_imp_hyp_iso = Sections.section_proof ["H";"G"]
 439 `H iso G ==> ?f. hyp_iso f (H, G)`
 440 [
 441    (((((use_arg_then2 ("iso", [iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 442 ];;
 443
 444 (* Lemma h_map_outside *)
 445 let h_map_outside = Sections.section_proof ["H";"x"]
 446 `~(x:A IN dart H) ==>
 447         edge_map H x = x /\
 448         node_map H x = x /\
 449         face_map H x = x`
 450 [
 451    (BETA_TAC THEN (move ["x_n_dart"]));
 452    ((fun arg_tac -> (use_arg_then2 ("hypermap_lemma", [hypermap_lemma])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["h"])));
 453    ((in_tac ["h"] false (repeat_tactic 1 9 (((use_arg_then2 ("permutes", [permutes]))(thm_tac (new_rewrite [] [])))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (done_tac));
 454 ];;
 455
 456 (* Lemma hyp_path_subset *)
 457 let hyp_path_subset = Sections.section_proof ["H";"p";"n"]
 458 `p 0 IN dart H /\ is_path H p n
 459         ==> (!i. i <= n ==> p i IN dart H)`
 460 [
 461    (((((use_arg_then2 ("lemma_def_path", [lemma_def_path]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("go_one_step", [go_one_step]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["p0_in"])) THEN (move ["h"]));
 462    ((((THENL) elim [ALL_TAC; ((move ["i"]) THEN (move ["Ih"]))]) THEN ((TRY done_tac)) THEN (move ["i_le"])) THEN (in_tac ["i_le"] false (((use_arg_then2 ("LE_SUC_LT", [LE_SUC_LT]))(thm_tac (new_rewrite [] []))))));
 463    ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_le", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_IMP_LE", [LT_IMP_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 464 ];;
 465
 466 (* Section Iso1 *)
 467 Sections.begin_section "Iso1";;
 468 (Sections.add_section_var (mk_var ("H", (`:(A)hypermap`))));;
 469 (Sections.add_section_var (mk_var ("G", (`:(B)hypermap`))));;
 470 (Sections.add_section_var (mk_var ("f", (`:A->B`))));;
 471
 472 (* Lemma hyp_iso_edge_face *)
 473 let hyp_iso_edge_face = Sections.section_proof []
 474 `hyp_iso f (H,G) <=> BIJ f (dart H) (dart G) /\
 475         (!x. x IN dart H ==> edge_map G (f x) = f (edge_map H x)
 476                          /\ face_map G (f x) = f (face_map H x))`
 477 [
 478    ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andb_id2l", [andb_id2l])) (disch_tac [])) THEN (clear_assumption "andb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((split_tac) THEN (move ["eq"]) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))));
 479    ((((use_arg_then2 ("Hypermap.inverse2_hypermap_maps", [Hypermap.inverse2_hypermap_maps]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))));
 480    ((fun arg_tac -> (use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma])) (fun fst_arg -> (use_arg_then2 ("G", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypG"])));
 481    ((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart 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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 482    ((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart 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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 483    (((((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`face_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Hypermap.hypermap_cyclic", [Hypermap.hypermap_cyclic]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 484 ];;
 485
 486 (* Lemma hyp_iso_edge_node *)
 487 let hyp_iso_edge_node = Sections.section_proof []
 488 `hyp_iso f (H,G) <=> BIJ f (dart H) (dart G) /\
 489         (!x. x IN dart H ==> edge_map G (f x) = f (edge_map H x)
 490                          /\ node_map G (f x) = f (node_map H x))`
 491 [
 492    ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andb_id2l", [andb_id2l])) (disch_tac [])) THEN (clear_assumption "andb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((split_tac) THEN (move ["eq"]) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))));
 493    ((((use_arg_then2 ("Hypermap.inverse2_hypermap_maps", [Hypermap.inverse2_hypermap_maps]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))));
 494    ((fun arg_tac -> (use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma])) (fun fst_arg -> (use_arg_then2 ("G", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypG"])));
 495    ((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart 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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 496    ((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart 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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 497    (((((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`node_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 498 ];;
 499 (Sections.add_section_hyp "isoHG" (`hyp_iso f (H, G)`));;
 500
 501 (* Lemma hyp_iso_bij *)
 502 let hyp_iso_bij = Sections.section_proof []
 503 `BIJ f (dart H) (dart G)`
 504 [
 505    ((in_tac ["isoHG"] false (((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 506 ];;
 507
 508 (* Lemma hyp_iso_inj *)
 509 let hyp_iso_inj = Sections.section_proof ["x";"y"]
 510 `x IN dart H /\ y IN dart H /\ f x = f y ==> x = y`
 511 [
 512    ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (case THEN (move ["inj"])) THEN (move ["_"]) THEN (move ["_"]) THEN (move ["h"])) THEN (((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (exact_tac)) THEN (done_tac));
 513 ];;
 514
 515 (* Lemma hyp_iso_surj *)
 516 let hyp_iso_surj = Sections.section_proof ["y"]
 517 `y IN dart G ==> ?x. x IN dart H /\ f x = y`
 518 [
 519    ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (move ["surj"]) THEN (move ["_"]) THEN (move ["y"])) THEN (((use_arg_then2 ("surj", [])) (disch_tac [])) THEN (clear_assumption "surj") THEN (exact_tac)) THEN (done_tac));
 520 ];;
 521
 522 (* Lemma hyp_iso_dart *)
 523 let hyp_iso_dart = Sections.section_proof ["x"]
 524 `x IN dart H ==> f x IN dart G`
 525 [
 526    ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["h"])) THEN (move ["_"]) THEN (move ["_"])) THEN (((use_arg_then2 ("h", [])) (disch_tac [])) THEN (clear_assumption "h") THEN (exact_tac)) THEN (done_tac));
 527 ];;
 528
 529 (* Lemma hyp_iso_SURJ *)
 530 let hyp_iso_SURJ = Sections.section_proof []
 531 `SURJ f (dart H) (dart G)`
 532 [
 533    ((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN (move ["x"]) THEN (move ["x_in"])) THEN (((fun arg_tac ->(use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(fun tmp_arg1 -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj]))(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));
 534 ];;
 535
 536 (* Lemma hyp_iso_INJ *)
 537 let hyp_iso_INJ = Sections.section_proof []
 538 `INJ f (dart H) (dart G)`
 539 [
 540    ((THENL_FIRST) ((((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["x_in"])); ((move ["x"]) THEN (move ["y"]))])) ((((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 541    (((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (exact_tac));
 542 ];;
 543
 544 (* Lemma hyp_iso_comm *)
 545 let hyp_iso_comm = Sections.section_proof ["x"]
 546 `x IN dart H ==>
 547         edge_map G (f x) = f (edge_map H x) /\
 548         node_map G (f x) = f (node_map H x) /\
 549         face_map G (f x) = f (face_map H x)`
 550 [
 551    ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (move ["_"]) THEN (move ["h"]) THEN (move ["x_in"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 552 ];;
 553
 554 (* Lemma hyp_iso_inverse_comm *)
 555 let hyp_iso_inverse_comm = Sections.section_proof ["x"]
 556 `x IN dart H
 557         ==> inverse (edge_map G) (f x) = f (inverse (edge_map H) x)
 558          /\ inverse (node_map G) (f x) = f (inverse (node_map H) x)
 559          /\ inverse (face_map G) (f x) = f (inverse (face_map H) x)`
 560 [
 561    (BETA_TAC THEN (move ["x_in"]));
 562    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart G`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 563    ((repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.lemma_dart_inveriant_under_inverse_maps", [Hypermap.lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 564    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSES", [PERMUTES_INVERSES])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Hypermap.hypermap_lemma", [Hypermap.hypermap_lemma]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 565 ];;
 566
 567 (* Lemma hyp_iso_inv *)
 568 let hyp_iso_inv = Sections.section_proof []
 569 `hyp_iso (res_inv f (dart H)) (G, H)`
 570 [
 571    (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("bij_res_inv", [bij_res_inv])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (move ["d_in"]));
 572    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (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 ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["d_eq"])))))));
 573    (((((use_arg_then2 ("d_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("res_inv_bij", [res_inv_bij])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 574 ];;
 575
 576 (* Lemma hyp_iso_ext *)
 577 let hyp_iso_ext = Sections.section_proof ["g"]
 578 `(!d. d IN (dart H) ==> f d = g d)
 579         ==> hyp_iso g (H, G)`
 580 [
 581    ((BETA_TAC THEN (move ["ext"])) THEN (((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("bij_ext", [bij_ext])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (move ["d_in"])));
 582    (((repeat_tactic 1 9 (((use_arg_then2 ("ext", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Hypermap.lemma_dart_invariant", [Hypermap.lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 583 ];;
 584
 585 (* Lemma iso_components *)
 586 let iso_components = Sections.section_proof ["d"]
 587 `d IN dart H ==>
 588         node G (f d) = IMAGE f (node H d) /\
 589         face G (f d) = IMAGE f (face H d) /\
 590         edge G (f d) = IMAGE f (edge H d)`
 591 [
 592    ((((use_arg_then2 ("isoHG", [])) (disch_tac [])) THEN (clear_assumption "isoHG") THEN BETA_TAC) THEN ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["bij"])) THEN (move ["f_eq"]) THEN (move ["d_in"])));
 593    ((repeat_tactic 1 9 (((use_arg_then2 ("node", [node]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("face", [face]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("edge", [edge]))(thm_tac (new_rewrite [] []))))));
 594    ((repeat_tactic 1 9 ((split_tac))) THEN (((fun arg_tac -> (use_arg_then2 ("orbit_comm", [orbit_comm])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((split_tac) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 595 ];;
 596
 597 (* Lemma hyp_iso_card_components *)
 598 let hyp_iso_card_components = Sections.section_proof ["x"]
 599 `x IN dart H ==>
 600         CARD (face H x) = CARD (face G (f x)) /\
 601         CARD (node H x) = CARD (node G (f x)) /\
 602         CARD (edge H x) = CARD (edge G (f x))`
 603 [
 604    ((BETA_TAC THEN (move ["x_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
 605    (((repeat_tactic 1 9 (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac ->(use_arg_then2 ("EDGE_FINITE", [EDGE_FINITE]))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("FACE_FINITE", [FACE_FINITE]))(fun tmp_arg1 -> (use_arg_then2 ("NODE_FINITE", [NODE_FINITE]))(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 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (case THEN (move ["a_in"])) THEN (case THEN (move ["b_in"])) THEN (move ["eq"])) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)));
 606    ((split_tac) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`face H x`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 607    ((split_tac) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node H x`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 608    ((split_tac) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`edge H x`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 609 ];;
 610
 611 (* Lemma iso_node_set *)
 612 let iso_node_set = Sections.section_proof []
 613 `node_set G = IMAGE (IMAGE f) (node_set H)`
 614 [
 615    (((repeat_tactic 1 9 (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("node", [node]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
 616    ((THENL_ROT (-1)) ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["y_eq"])); ((case THEN (move ["n"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["n_eq"]))]));
 617    ((fun arg_tac -> arg_tac (Arg_term (`f d`))) (term_tac exists_tac));
 618    (((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 619    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (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 ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["f_eq"])))))));
 620    (((fun arg_tac -> arg_tac (Arg_term (`node H t`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
 621    (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
 622 ];;
 623
 624 (* Lemma iso_edge_set *)
 625 let iso_edge_set = Sections.section_proof []
 626 `edge_set G = IMAGE (IMAGE f) (edge_set H)`
 627 [
 628    (((repeat_tactic 1 9 (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("edge", [edge]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
 629    ((THENL_ROT (-1)) ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["y_eq"])); ((case THEN (move ["n"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["n_eq"]))]));
 630    ((fun arg_tac -> arg_tac (Arg_term (`f d`))) (term_tac exists_tac));
 631    (((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 632    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (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 ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["f_eq"])))))));
 633    (((fun arg_tac -> arg_tac (Arg_term (`edge H t`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
 634    (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
 635 ];;
 636
 637 (* Lemma iso_face_set *)
 638 let iso_face_set = Sections.section_proof []
 639 `face_set G = IMAGE (IMAGE f) (face_set H)`
 640 [
 641    (((repeat_tactic 1 9 (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
 642    ((THENL_ROT (-1)) ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["y_eq"])); ((case THEN (move ["n"])) THEN (case THEN (move ["y_eq"])) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["n_eq"]))]));
 643    ((fun arg_tac -> arg_tac (Arg_term (`f d`))) (term_tac exists_tac));
 644    (((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 645    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (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 ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["f_eq"])))))));
 646    (((fun arg_tac -> arg_tac (Arg_term (`face H t`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
 647    (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
 648 ];;
 649
 650 (* Lemma iso_number_of_nodes *)
 651 let iso_number_of_nodes = Sections.section_proof []
 652 `number_of_nodes G = number_of_nodes H`
 653 [
 654    (((repeat_tactic 1 9 (((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_node_set", [iso_node_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
 655    (((repeat_tactic 1 9 (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("node", [node]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d1"]) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d2"]) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
 656    (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 657    (((((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 658 ];;
 659
 660 (* Lemma iso_number_of_edges *)
 661 let iso_number_of_edges = Sections.section_proof []
 662 `number_of_edges G = number_of_edges H`
 663 [
 664    (((repeat_tactic 1 9 (((use_arg_then2 ("number_of_edges", [number_of_edges]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_edge_set", [iso_edge_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
 665    (((repeat_tactic 1 9 (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("edge", [edge]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d1"]) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d2"]) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
 666    (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 667    (((((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 668 ];;
 669
 670 (* Lemma iso_number_of_faces *)
 671 let iso_number_of_faces = Sections.section_proof []
 672 `number_of_faces G = number_of_faces H`
 673 [
 674    (((repeat_tactic 1 9 (((use_arg_then2 ("number_of_faces", [number_of_faces]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_face_set", [iso_face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
 675    (((repeat_tactic 1 9 (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d1"]) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN ALL_TAC) THEN (move ["d2"]) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
 676    (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 677    (((((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 678 ];;
 679
 680 (* Lemma iso_plain_imp *)
 681 let iso_plain_imp = Sections.section_proof []
 682 `plain_hypermap G ==> plain_hypermap H`
 683 [
 684    (((repeat_tactic 1 9 (((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))))) THEN (move ["g_eq"]) THEN (move ["x"]));
 685    ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`x IN dart H`))) (disch_eq_tac "x_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((repeat_tactic 1 9 (((use_arg_then2 ("h_map_outside", [h_map_outside]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 686    ((((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (DISCH_THEN apply_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(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 (done_tac));
 687 ];;
 688
 689 (* Lemma iso_edge_nondegenerate_imp *)
 690 let iso_edge_nondegenerate_imp = Sections.section_proof []
 691 `is_edge_nondegenerate G ==> is_edge_nondegenerate H`
 692 [
 693    ((repeat_tactic 1 9 (((use_arg_then2 ("is_edge_nondegenerate", [is_edge_nondegenerate]))(thm_tac (new_rewrite [] []))))) THEN (move ["g_eq"]) THEN (move ["d"]) THEN (move ["d_in"]));
 694    (((fun arg_tac -> (use_arg_then2 ("g_eq", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (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 ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac));
 695    ((((((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 696 ];;
 697
 698 (* Lemma iso_simple_imp *)
 699 let iso_simple_imp = Sections.section_proof []
 700 `simple_hypermap G ==> simple_hypermap H`
 701 [
 702    ((repeat_tactic 1 9 (((use_arg_then2 ("simple_hypermap", [simple_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["d"]) THEN (move ["d_in"]));
 703    (((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (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);
 704    ((repeat_tactic 1 9 (((use_arg_then2 ("iso_components", [iso_components]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("image_inter_inj_gen", [image_inter_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 705    ((fun arg_tac -> arg_tac (Arg_term (`{f d} = IMAGE f {d}`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 706    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))))) THEN (move ["y"]));
 707    ((((THENL) (split_tac) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ((case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]) THEN ((TRY done_tac))) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac));
 708    ((BETA_TAC THEN (move ["eq"])) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("image_inj_gen", [image_inj_gen])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)));
 709    (((((use_arg_then2 ("SING_SUBSET", [SING_SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["_"])));
 710    ((((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN BETA_TAC) THEN ((((use_arg_then2 ("SUBSET", [SUBSET]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 711 ];;
 712
 713 (* Lemma iso_path_imp *)
 714 let iso_path_imp = Sections.section_proof ["p";"n"]
 715 `p 0 IN dart H /\ is_path H p n ==> is_path G (f o p) n`
 716 [
 717    (BETA_TAC THEN (case THEN ((move ["p0_in"]) THEN (move ["p_path"]))));
 718    ((((use_arg_then2 ("p_path", [])) (disch_tac [])) THEN BETA_TAC) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("lemma_def_path", [lemma_def_path]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("go_one_step", [go_one_step]))(thm_tac (new_rewrite [] [])))))) THEN (move ["h"]) THEN (move ["i"]) THEN (move ["i_lt"])));
 719    ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_path_subset", [hyp_path_subset])) (fun fst_arg -> (use_arg_then2 ("p_path", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("p0_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_IMP_LE", [LT_IMP_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 720 ];;
 721
 722 (* Lemma iso_path_inv *)
 723 let iso_path_inv = Sections.section_proof ["q";"n"]
 724 `q 0 IN dart G /\ is_path G q n ==>
 725         ?p. (!i. i <= n ==> q i = f (p i)) /\ p 0 IN dart H /\ is_path H p n`
 726 [
 727    ((BETA_TAC THEN (case THEN ((move ["q0"]) THEN (move ["q_path"])))) THEN (((use_arg_then2 ("q_path", [])) (disch_tac [])) THEN BETA_TAC));
 728    ((repeat_tactic 1 9 (((use_arg_then2 ("lemma_def_path", [lemma_def_path]))(thm_tac (new_rewrite [] []))))) THEN (move ["q_path2"]));
 729    (((fun arg_tac -> arg_tac (Arg_term (`res_inv f (dart H) o q`))) (term_tac exists_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))));
 730    ((THENL) (split_tac) [((move ["i"]) THEN (move ["i_le"])); ALL_TAC]);
 731    (((((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_path_subset", [hyp_path_subset])) (fun fst_arg -> (use_arg_then2 ("q_path", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 732    (((((fun arg_tac -> (use_arg_then2 ("res_inv_right", [res_inv_right])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["i"]) THEN (move ["i_lt"]));
 733    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_path_subset", [hyp_path_subset])) (fun fst_arg -> (use_arg_then2 ("q_path", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("q0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("LT_IMP_LE", [LT_IMP_LE])) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 arg -> thm_tac MP_TAC arg THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN ((move ["t"]) THEN (case THEN (move ["t_in"])) THEN (move ["qi_eq"]))))));
 734    ((((use_arg_then2 ("qi_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("res_inv_left", [res_inv_left])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 735    ((((fun arg_tac -> (use_arg_then2 ("q_path2", [])) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (((use_arg_then2 ("go_one_step", [go_one_step]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("qi_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("res_inv_bij", [res_inv_bij])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_bij", [hyp_iso_bij])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 736 ];;
 737
 738 (* Lemma iso_comb_component *)
 739 let iso_comb_component = Sections.section_proof ["d"]
 740 `d IN dart H ==>
 741         comb_component G (f d) = IMAGE f (comb_component H d)`
 742 [
 743    ((repeat_tactic 1 9 (((use_arg_then2 ("comb_component", [comb_component]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("image_lemma", [image_lemma]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("is_in_component", [is_in_component]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 744    ((THENL_ROT (-1)) ((BETA_TAC THEN (move ["d_in"]) THEN (move ["z"])) THEN ((THENL) (split_tac) [((case THEN (move ["p"])) THEN (case THEN (move ["n"])) THEN (case THEN (move ["p0_eq"])) THEN (case THEN (move ["pn_eq"])) THEN (move ["pathG"])); ALL_TAC])));
 745    (BETA_TAC THEN (case THEN (move ["t"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["p"])) THEN (case THEN (move ["n"])) THEN (case THEN (move ["p0_eq"])) THEN (case THEN (move ["pn_eq"])) THEN (move ["path_p"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 746    ((((fun arg_tac -> arg_tac (Arg_term (`f o p`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_path_imp", [iso_path_imp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("p0_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 747    ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("iso_path_inv", [iso_path_inv])) (fun fst_arg -> (use_arg_then2 ("pathG", [])) (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 ("p0_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 748    (BETA_TAC THEN (case THEN (move ["q"])) THEN (case THEN (move ["p_eq"])) THEN (case THEN (move ["q0"])) THEN (move ["path_q"]));
 749    (((fun arg_tac -> arg_tac (Arg_term (`q n`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("p_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("LE_REFL", [LE_REFL]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("pn_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
 750    ((((use_arg_then2 ("q", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac))) THEN (repeat_tactic 1 9 (((split_tac) THEN ((TRY done_tac))))));
 751    ((((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("p_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("LE_0", [LE_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 752 ];;
 753
 754 (* Lemma iso_set_part_components *)
 755 let iso_set_part_components = Sections.section_proof []
 756 `set_of_components G = IMAGE (IMAGE f) (set_of_components H)`
 757 [
 758    (((repeat_tactic 1 9 (((use_arg_then2 ("set_of_components", [set_of_components]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_part_components", [set_part_components]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["c"]));
 759    ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (move ["c_eq"])); ((case THEN (move ["c2"])) THEN (case THEN (move ["c_eq"])) THEN (case THEN (move ["t"])) THEN (case THEN (move ["t_in"])) THEN (move ["c2_eq"]))]);
 760    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (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 ["t"]) THEN (case THEN ((move ["t_in"]) THEN (move ["d_eq"])))))));
 761    ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`comb_component H t`))) (term_tac exists_tac)) THEN (split_tac)) (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac)));
 762    (((((use_arg_then2 ("iso_comb_component", [iso_comb_component]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("c_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (done_tac));
 763    ((fun arg_tac -> arg_tac (Arg_term (`f t`))) (term_tac exists_tac));
 764    (((((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("c_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("c2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_comb_component", [iso_comb_component]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 765 ];;
 766
 767 (* Lemma iso_number_of_components *)
 768 let iso_number_of_components = Sections.section_proof []
 769 `number_of_components G = number_of_components H`
 770 [
 771    ((repeat_tactic 1 9 (((use_arg_then2 ("number_of_components", [number_of_components]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_set_part_components", [iso_set_part_components]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 772    (((((use_arg_then2 ("FINITE_HYPERMAP_COMPONENTS", [FINITE_HYPERMAP_COMPONENTS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (move ["n1"]) THEN (move ["n2"]));
 773    ((repeat_tactic 1 9 (((use_arg_then2 ("set_of_components", [set_of_components]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_part_components", [set_part_components]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 774    (BETA_TAC THEN (case THEN ((case THEN (move ["d1"])) THEN (move ["n1_eq"]))) THEN (case THEN ((case THEN (move ["d2"])) THEN (move ["n2_eq"]))) THEN (move ["i_eq"]));
 775    (((fun arg_tac -> (use_arg_then2 ("image_set_inj_gen", [image_set_inj_gen])) (fun fst_arg -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 776    (((((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("n1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_component_subset", [lemma_component_subset]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 777 ];;
 778
 779 (* Lemma iso_dart *)
 780 let iso_dart = Sections.section_proof []
 781 `dart G = IMAGE f (dart H)`
 782 [
 783    ((((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"])) THEN ((THENL) (split_tac) [(move ["d_in"]); ((case THEN (move ["t"])) THEN (case THEN ((move ["d_eq"]) THEN (move ["t_in"]))))]));
 784    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (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 ["t"]) THEN (move ["h"])))));
 785    (((use_arg_then2 ("t", [])) (term_tac exists_tac)) THEN (done_tac));
 786    (((((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 787 ];;
 788
 789 (* Lemma iso_card_dart *)
 790 let iso_card_dart = Sections.section_proof []
 791 `CARD (dart G) = CARD (dart H)`
 792 [
 793    (((((use_arg_then2 ("iso_dart", [iso_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypermap_lemma", [hypermap_lemma]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (disch_tac [])) THEN (clear_assumption "hyp_iso_inj") THEN (exact_tac)) THEN (done_tac));
 794 ];;
 795
 796 (* Lemma iso_planar_imp *)
 797 let iso_planar_imp = Sections.section_proof []
 798 `planar_hypermap G ==> planar_hypermap H`
 799 [
 800    ((repeat_tactic 1 9 (((use_arg_then2 ("planar_hypermap", [planar_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_card_dart", [iso_card_dart]))(thm_tac (new_rewrite [] [])))));
 801    (((((use_arg_then2 ("iso_number_of_edges", [iso_number_of_edges]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_number_of_faces", [iso_number_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("iso_number_of_components", [iso_number_of_components]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 802 ];;
 803
 804 (* Lemma iso_connected_imp *)
 805 let iso_connected_imp = Sections.section_proof []
 806 `connected_hypermap G ==> connected_hypermap H`
 807 [
 808    (((repeat_tactic 1 9 (((use_arg_then2 ("connected_hypermap", [connected_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("iso_number_of_components", [iso_number_of_components]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 809 ];;
 810
 811 (* Finalization of the section Iso1 *)
 812 let hyp_iso_edge_face = Sections.finalize_theorem hyp_iso_edge_face;;
 813 let hyp_iso_edge_node = Sections.finalize_theorem hyp_iso_edge_node;;
 814 let hyp_iso_bij = Sections.finalize_theorem hyp_iso_bij;;
 815 let hyp_iso_inj = Sections.finalize_theorem hyp_iso_inj;;
 816 let hyp_iso_surj = Sections.finalize_theorem hyp_iso_surj;;
 817 let hyp_iso_dart = Sections.finalize_theorem hyp_iso_dart;;
 818 let hyp_iso_SURJ = Sections.finalize_theorem hyp_iso_SURJ;;
 819 let hyp_iso_INJ = Sections.finalize_theorem hyp_iso_INJ;;
 820 let hyp_iso_comm = Sections.finalize_theorem hyp_iso_comm;;
 821 let hyp_iso_inverse_comm = Sections.finalize_theorem hyp_iso_inverse_comm;;
 822 let hyp_iso_inv = Sections.finalize_theorem hyp_iso_inv;;
 823 let hyp_iso_ext = Sections.finalize_theorem hyp_iso_ext;;
 824 let iso_components = Sections.finalize_theorem iso_components;;
 825 let hyp_iso_card_components = Sections.finalize_theorem hyp_iso_card_components;;
 826 let iso_node_set = Sections.finalize_theorem iso_node_set;;
 827 let iso_edge_set = Sections.finalize_theorem iso_edge_set;;
 828 let iso_face_set = Sections.finalize_theorem iso_face_set;;
 829 let iso_number_of_nodes = Sections.finalize_theorem iso_number_of_nodes;;
 830 let iso_number_of_edges = Sections.finalize_theorem iso_number_of_edges;;
 831 let iso_number_of_faces = Sections.finalize_theorem iso_number_of_faces;;
 832 let iso_plain_imp = Sections.finalize_theorem iso_plain_imp;;
 833 let iso_edge_nondegenerate_imp = Sections.finalize_theorem iso_edge_nondegenerate_imp;;
 834 let iso_simple_imp = Sections.finalize_theorem iso_simple_imp;;
 835 let iso_path_imp = Sections.finalize_theorem iso_path_imp;;
 836 let iso_path_inv = Sections.finalize_theorem iso_path_inv;;
 837 let iso_comb_component = Sections.finalize_theorem iso_comb_component;;
 838 let iso_set_part_components = Sections.finalize_theorem iso_set_part_components;;
 839 let iso_number_of_components = Sections.finalize_theorem iso_number_of_components;;
 840 let iso_dart = Sections.finalize_theorem iso_dart;;
 841 let iso_card_dart = Sections.finalize_theorem iso_card_dart;;
 842 let iso_planar_imp = Sections.finalize_theorem iso_planar_imp;;
 843 let iso_connected_imp = Sections.finalize_theorem iso_connected_imp;;
 844 Sections.end_section "Iso1";;
 845 (Sections.add_section_type (mk_var ("H", (`:(C)hypermap`))));;
 846 (Sections.add_section_type (mk_var ("G", (`:(D)hypermap`))));;
 847
 848 (* Lemma iso_plain *)
 849 let iso_plain = Sections.section_proof ["H";"G"]
 850 `H iso G ==> (plain_hypermap H <=> plain_hypermap G)`
 851 [
 852    ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_plain_imp", [iso_plain_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 853 ];;
 854
 855 (* Lemma iso_edge_nondegenerate *)
 856 let iso_edge_nondegenerate = Sections.section_proof ["H";"G"]
 857 `H iso G ==> (is_edge_nondegenerate H <=> is_edge_nondegenerate G)`
 858 [
 859    ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_edge_nondegenerate_imp", [iso_edge_nondegenerate_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 860 ];;
 861
 862 (* Lemma iso_simple *)
 863 let iso_simple = Sections.section_proof ["H";"G"]
 864 `H iso G ==> (simple_hypermap H <=> simple_hypermap G)`
 865 [
 866    ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_simple_imp", [iso_simple_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 867 ];;
 868
 869 (* Lemma iso_planar *)
 870 let iso_planar = Sections.section_proof ["H";"G"]
 871 `H iso G ==> (planar_hypermap H <=> planar_hypermap G)`
 872 [
 873    ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_planar_imp", [iso_planar_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 874 ];;
 875
 876 (* Lemma iso_connected *)
 877 let iso_connected = Sections.section_proof ["H";"G"]
 878 `H iso G ==> (connected_hypermap H <=> connected_hypermap G)`
 879 [
 880    ((BETA_TAC THEN (move ["iso"])) THEN ((split_tac) THEN (move ["h"])) THEN ((fun arg_tac -> (use_arg_then2 ("iso_connected_imp", [iso_connected_imp])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("iso_imp_hyp_iso", [iso_imp_hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("iso_sym", [iso_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 881 ];;
 882
 883 (* Finalization of the section Iso *)
 884 let hyp_iso_imp_iso = Sections.finalize_theorem hyp_iso_imp_iso;;
 885 let iso_imp_hyp_iso = Sections.finalize_theorem iso_imp_hyp_iso;;
 886 let h_map_outside = Sections.finalize_theorem h_map_outside;;
 887 let hyp_path_subset = Sections.finalize_theorem hyp_path_subset;;
 888 let hyp_iso_edge_face = Sections.finalize_theorem hyp_iso_edge_face;;
 889 let hyp_iso_edge_node = Sections.finalize_theorem hyp_iso_edge_node;;
 890 let hyp_iso_bij = Sections.finalize_theorem hyp_iso_bij;;
 891 let hyp_iso_inj = Sections.finalize_theorem hyp_iso_inj;;
 892 let hyp_iso_surj = Sections.finalize_theorem hyp_iso_surj;;
 893 let hyp_iso_dart = Sections.finalize_theorem hyp_iso_dart;;
 894 let hyp_iso_SURJ = Sections.finalize_theorem hyp_iso_SURJ;;
 895 let hyp_iso_INJ = Sections.finalize_theorem hyp_iso_INJ;;
 896 let hyp_iso_comm = Sections.finalize_theorem hyp_iso_comm;;
 897 let hyp_iso_inverse_comm = Sections.finalize_theorem hyp_iso_inverse_comm;;
 898 let hyp_iso_inv = Sections.finalize_theorem hyp_iso_inv;;
 899 let hyp_iso_ext = Sections.finalize_theorem hyp_iso_ext;;
 900 let iso_components = Sections.finalize_theorem iso_components;;
 901 let hyp_iso_card_components = Sections.finalize_theorem hyp_iso_card_components;;
 902 let iso_node_set = Sections.finalize_theorem iso_node_set;;
 903 let iso_edge_set = Sections.finalize_theorem iso_edge_set;;
 904 let iso_face_set = Sections.finalize_theorem iso_face_set;;
 905 let iso_number_of_nodes = Sections.finalize_theorem iso_number_of_nodes;;
 906 let iso_number_of_edges = Sections.finalize_theorem iso_number_of_edges;;
 907 let iso_number_of_faces = Sections.finalize_theorem iso_number_of_faces;;
 908 let iso_plain_imp = Sections.finalize_theorem iso_plain_imp;;
 909 let iso_edge_nondegenerate_imp = Sections.finalize_theorem iso_edge_nondegenerate_imp;;
 910 let iso_simple_imp = Sections.finalize_theorem iso_simple_imp;;
 911 let iso_path_imp = Sections.finalize_theorem iso_path_imp;;
 912 let iso_path_inv = Sections.finalize_theorem iso_path_inv;;
 913 let iso_comb_component = Sections.finalize_theorem iso_comb_component;;
 914 let iso_set_part_components = Sections.finalize_theorem iso_set_part_components;;
 915 let iso_number_of_components = Sections.finalize_theorem iso_number_of_components;;
 916 let iso_dart = Sections.finalize_theorem iso_dart;;
 917 let iso_card_dart = Sections.finalize_theorem iso_card_dart;;
 918 let iso_planar_imp = Sections.finalize_theorem iso_planar_imp;;
 919 let iso_connected_imp = Sections.finalize_theorem iso_connected_imp;;
 920 let iso_plain = Sections.finalize_theorem iso_plain;;
 921 let iso_edge_nondegenerate = Sections.finalize_theorem iso_edge_nondegenerate;;
 922 let iso_simple = Sections.finalize_theorem iso_simple;;
 923 let iso_planar = Sections.finalize_theorem iso_planar;;
 924 let iso_connected = Sections.finalize_theorem iso_connected;;
 925 Sections.end_section "Iso";;
 926
 927 (* Section FanHypermapsIso *)
 928 Sections.begin_section "FanHypermapsIso";;
 929
 930 (* Lemma fan_in_e_imp_neq *)
 931 let fan_in_e_imp_neq = Sections.section_proof ["V";"E";"v";"w"]
 932 `FAN (vec 0,V,E) /\ {v, w} IN E ==> ~(v = w)`
 933 [
 934    (((((use_arg_then2 ("FAN", [FAN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("graph", [graph]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HAS_SIZE", [HAS_SIZE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (case THEN (move ["size2"])) THEN (move ["_"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("size2", [])) (thm_tac (match_mp_then snd_th MP_TAC)))));
 935    (((((use_arg_then2 ("Geomdetail.CARD2", [Geomdetail.CARD2]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 936 ];;
 937
 938 (* Lemma in_set_of_edge_neq *)
 939 let in_set_of_edge_neq = Sections.section_proof ["V";"E";"v";"w"]
 940 `FAN (vec 0,V,E) /\ w IN set_of_edge v V E ==> ~(v = w)`
 941 [
 942    (((((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["fan"])) THEN (case THEN (move ["vwE"])) THEN (move ["_"]));
 943    (((fun arg_tac -> (use_arg_then2 ("fan_in_e_imp_neq", [fan_in_e_imp_neq])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
 944 ];;
 945
 946 (* Lemma dart_of_fan_eq *)
 947 let dart_of_fan_eq = Sections.section_proof ["V";"E"]
 948 `dart_of_fan (V,E) = dart1_of_fan (V,E) UNION {(v,v) | v IN V /\ set_of_edge v V E = {}}`
 949 [
 950    (((((use_arg_then2 ("dart_of_fan", [dart_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL UNION_ACI)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 951 ];;
 952
 953 (* Lemma darts_of_fan_disj *)
 954 let darts_of_fan_disj = Sections.section_proof ["V";"E"]
 955 `FAN (vec 0,V,E) ==>
 956         DISJOINT (dart1_of_fan (V,E)) {(v,v) | v IN V /\ set_of_edge v V E = {}}`
 957 [
 958    (((((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (move ["fan"]) THEN (move ["x"]));
 959    (((fun arg_tac -> arg_tac (Arg_term (`x IN _`))) (disch_eq_tac "x_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 960    ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["vw_in"])) THEN (move ["x_eq"])));
 961    (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN ALL_TAC THEN (case THEN (move ["u"])) THEN (case THEN (move ["_"])) THEN (move ["x_eq2"]));
 962    (((fun arg_tac -> (use_arg_then2 ("fan_in_e_imp_neq", [fan_in_e_imp_neq])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (move ["in_e"]));
 963    (((repeat_tactic 1 9 (((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("negb_imply", [negb_imply]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))));
 964    (((((use_arg_then2 ("in_e", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_eq2", [])) (disch_tac [])) THEN (clear_assumption "x_eq2") THEN BETA_TAC) THEN (((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) 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));
 965 ];;
 966
 967 (* Lemma dart1_of_fan_eq_image *)
 968 let dart1_of_fan_eq_image = Sections.section_proof ["V";"E"]
 969 `dart1_of_fan (V,E) = IMAGE contracted_dart (d1_fan (vec 0,V,E))`
 970 [
 971    (((((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"]));
 972    ((THENL) (split_tac) [((case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["in_e"])) THEN (move ["d_eq"])); ((case THEN (move ["x"])) THEN (case THEN (move ["d_eq"])) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN ALL_TAC) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (case THEN (move ["in_e"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["x_eq"]))]);
 973    ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, w, sigma_fan (vec 0) V E v w`))) (term_tac exists_tac));
 974    ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 975    ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac exists_tac))) THEN (done_tac));
 976    ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN ((((use_arg_then2 ("in_e", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 977 ];;
 978
 979 (* Lemma dart2_of_fan_eq_image *)
 980 let dart2_of_fan_eq_image = Sections.section_proof ["V";"E"]
 981 `{(v,v) | v IN V /\ set_of_edge v V E = {}} = IMAGE contracted_dart (d20_fan (vec 0,V,E))`
 982 [
 983    (((((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["d"]));
 984    ((THENL) (split_tac) [((case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["d_eq"])); ((case THEN (move ["x"])) THEN (case THEN (move ["d_eq"])) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]))]);
 985    ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, v, v`))) (term_tac exists_tac));
 986    ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 987    ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac))) THEN (done_tac));
 988    (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 989 ];;
 990
 991 (* Lemma disjoint_preimage *)
 992 let disjoint_preimage = Sections.section_proof ["f";"s";"t"]
 993 `DISJOINT (IMAGE f s) (IMAGE f t) ==> DISJOINT s t`
 994 [
 995    ((repeat_tactic 1 9 (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CONTRAPOS_THM", [CONTRAPOS_THM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))));
 996    (BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN ((move ["xs"]) THEN (move ["xt"]))));
 997    (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN (split_tac) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
 998 ];;
 999
1000 (* Lemma darts_of_fan_disj1 *)
1001 let darts_of_fan_disj1 = Sections.section_proof ["V";"E"]
1002 `FAN (vec 0,V,E) ==>
1003         DISJOINT (d1_fan (vec 0,V,E)) (d20_fan (vec 0,V,E))`
1004 [
1005    ((BETA_TAC THEN (move ["fan"])) THEN (((fun arg_tac -> (use_arg_then2 ("disjoint_preimage", [disjoint_preimage])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`contracted_dart`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
1006    (((((use_arg_then2 ("dart1_of_fan_eq_image", [dart1_of_fan_eq_image]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart2_of_fan_eq_image", [dart2_of_fan_eq_image]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_fan_disj", [darts_of_fan_disj]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1007 ];;
1008
1009 (* Lemma bij_contracted_dart1 *)
1010 let bij_contracted_dart1 = Sections.section_proof ["V";"E"]
1011 `BIJ contracted_dart (d1_fan (vec 0,V,E)) (dart1_of_fan (V,E))`
1012 [
1013    ((((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
1014    (repeat_tactic 1 9 ((split_tac)));
1015    (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN ALL_TAC) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (case THEN (move ["in_e"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["x_eq"]));
1016    ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN ((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1017    (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y'"])) THEN (case THEN (move ["v'"])) THEN (case THEN (move ["w'"])) THEN (case THEN (move ["w1'"])) THEN (case THEN (move ["h'"])) THEN (move ["y_eq"]));
1018    (((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["v_eq"]) THEN (move ["w_eq"]))));
1019    (((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("h'", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("v_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1020    (BETA_TAC THEN (move ["y"]) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["in_e"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
1021    ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, w, sigma_fan (vec 0) V E v w`))) (term_tac exists_tac));
1022    ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1023    ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac exists_tac))) THEN (done_tac));
1024 ];;
1025
1026 (* Lemma bij_contracted_dart2 *)
1027 let bij_contracted_dart2 = Sections.section_proof ["V";"E"]
1028 `BIJ contracted_dart (d20_fan (vec 0,V,E)) {(v,v) | v IN V /\ set_of_edge v V E = {}}`
1029 [
1030    ((((use_arg_then2 ("bij_alt", [bij_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1031    (repeat_tactic 1 9 ((split_tac)));
1032    (BETA_TAC THEN (move ["x"]) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]));
1033    (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1034    (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (move ["x_eq"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y'"])) THEN (case THEN (move ["v'"])) THEN (case THEN (move ["h'"])) THEN (move ["y_eq"]));
1035    ((((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h'", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1036    ((BETA_TAC THEN (move ["y"]) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`vec 0, v, v, v`))) (term_tac exists_tac)));
1037    ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1038    ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac))) THEN (done_tac));
1039 ];;
1040
1041 (* Section Iso *)
1042 Sections.begin_section "Iso";;
1043 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
1044 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
1045 (Sections.add_section_hyp "fan" (`FAN (vec 0,V,E)`));;
1046
1047 (* Lemma bij_contracted_dart *)
1048 let bij_contracted_dart = Sections.section_proof []
1049 `BIJ contracted_dart (d_fan (vec 0,V,E)) (dart_of_fan (V,E))`
1050 [
1051    ((fun arg_tac -> arg_tac (Arg_term (`contracted_dart = \t. if t IN d1_fan (vec 0,V,E) then contracted_dart t else contracted_dart t`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
1052    (((((use_arg_then2 ("if_same", [if_same]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ETA_AX", [ETA_AX]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1053    ((((use_arg_then2 ("d_fan", [d_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_disjoint_union", [bij_disjoint_union]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_fan_disj", [darts_of_fan_disj]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
1054    (((((use_arg_then2 ("darts_of_fan_disj1", [darts_of_fan_disj1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("bij_contracted_dart1", [bij_contracted_dart1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_contracted_dart2", [bij_contracted_dart2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1055 ];;
1056
1057 (* Lemma hypermap_of_fan_rep_alt *)
1058 let hypermap_of_fan_rep_alt = Sections.section_proof []
1059 `dart (hypermap1_of_fanx (vec 0,V,E)) = d_fan (vec 0,V,E)
1060         /\ edge_map (hypermap1_of_fanx (vec 0,V,E)) = res (e_fan (vec 0) V E) (d1_fan (vec 0,V,E))
1061         /\ node_map (hypermap1_of_fanx (vec 0,V,E)) = res (n_fan (vec 0) V E) (d1_fan (vec 0,V,E))
1062         /\ face_map (hypermap1_of_fanx (vec 0,V,E)) = res (f1_fan (vec 0) V E) (d1_fan (vec 0,V,E))`
1063 [
1064    ((fun arg_tac -> (use_arg_then2 ("hypermap_of_fan_rep", [hypermap_of_fan_rep])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
1065    (((fun arg_tac -> arg_tac (Arg_term (`\t. _ t`))) (term_tac (set_tac "p"))) THEN (((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("p", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC) THEN ((ANTS_TAC) THEN ((TRY done_tac)) THEN (move ["eq"])));
1066    (((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("p_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1067 ];;
1068
1069 (* Lemma fan_hypermaps_iso_explicit *)
1070 let fan_hypermaps_iso_explicit = Sections.section_proof []
1071 `hyp_iso contracted_dart (hypermap1_of_fanx (vec 0,V,E), hypermap_of_fan (V,E))`
1072 [
1073    ((((use_arg_then2 ("hyp_iso", [hyp_iso]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hypermap_of_fan_rep_alt", [hypermap_of_fan_rep_alt]))(thm_tac (new_rewrite [] []))))));
1074    ((((use_arg_then2 ("bij_contracted_dart", [bij_contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("d_fan", [d_fan]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
1075    ((fun arg_tac -> arg_tac (Arg_term (`x IN d20_fan (vec 0,V,E) ==> ~(x IN d1_fan (vec 0,V,E))`))) (term_tac (have_gen_tac ["x"](move ["x_in_d2"]))));
1076    ((BETA_TAC THEN (move ["x2"])) THEN (((fun arg_tac -> (use_arg_then2 ("darts_of_fan_disj1", [darts_of_fan_disj1])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (move ["x1"])));
1077    (((((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac));
1078    ((THENL_ROT (-1)) (((((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (move ["x"]) THEN (case THEN (move ["x_in"]))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("x_in_d2", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)))));
1079    ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
1080    ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext", [e_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan_pair_ext", [n_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))));
1081    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("NOT_IN_DART1_OF_FAN", [NOT_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1082    ((((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["x'"])) THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["w1"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
1083    ((((use_arg_then2 ("e_fan", [e_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan", [n_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f1_fan", [f1_fan]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] []))))));
1084    ((((use_arg_then2 ("e_fan_pair_ext", [e_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan_pair_ext", [n_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))));
1085    ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))));
1086    (((((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN (done_tac));
1087    ((((use_arg_then2 ("e_fan_pair", [e_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair", [f_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1088    (((((use_arg_then2 ("Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN", [Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.PER_SET2)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1089 ];;
1090
1091 (* Lemma fan_hypermaps_iso *)
1092 let fan_hypermaps_iso = Sections.section_proof []
1093 `(hypermap1_of_fanx (vec 0,V,E)) iso (hypermap_of_fan (V,E))`
1094 [
1095    (((fun arg_tac -> (use_arg_then2 ("hyp_iso_imp_iso", [hyp_iso_imp_iso])) (fun fst_arg -> (use_arg_then2 ("fan_hypermaps_iso_explicit", [fan_hypermaps_iso_explicit])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
1096 ];;
1097 let ext_dart = new_definition
1098         `ext_dart (V,E) (v,w) = (vec 0,v,w,extension_sigma_fan (vec 0) V E v w)`;;
1099
1100 (* Lemma ext_dart_eq_inv_contracted_dart *)
1101 let ext_dart_eq_inv_contracted_dart = Sections.section_proof ["d"]
1102 `d IN dart_of_fan (V,E)
1103         ==> ext_dart (V,E) d = res_inv contracted_dart (d_fan (vec 0,V,E)) d`
1104 [
1105    ((((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"])) THEN ((((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in"])));
1106    ((fun arg_tac -> arg_tac (Arg_term (`extension_sigma_fan _ V E v w`))) (term_tac (set_tac "w1")));
1107    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`(v,w) = contracted_dart (vec 0:real^3,v,w,w1:real^3)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("contracted_dart", [contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
1108    (((((use_arg_then2 ("res_inv_left", [res_inv_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((THENL) (split_tac) [((move ["x"]) THEN (move ["y"]) THEN (move ["h"])); ALL_TAC]));
1109    ((use_arg_then2 ("bij_contracted_dart", [bij_contracted_dart])) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
1110    ((((((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 ["h2"]) THEN (move ["_"])) THEN (((use_arg_then2 ("h2", [])) (disch_tac [])) THEN (clear_assumption "h2") THEN (DISCH_THEN apply_tac)) THEN (done_tac));
1111    ((((use_arg_then2 ("w1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("extension_sigma_fan", [extension_sigma_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_fan", [d_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))));
1112    (((fun arg_tac -> arg_tac (Arg_term (`w IN set_of_edge v V E`))) (disch_eq_tac "w_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
1113    (((((use_arg_then2 ("d1_fan", [d1_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (DISJ1_TAC));
1114    ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac exists_tac))) THEN (simp_tac));
1115    ((((fun arg_tac -> (use_arg_then2 ("properties_of_set_of_edge_fan", [properties_of_set_of_edge_fan])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1116    (((((use_arg_then2 ("d20_fan", [d20_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (DISJ2_TAC));
1117    ((((fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac))) THEN (simp_tac));
1118    ((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan", [dart_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN case);
1119    ((BETA_TAC THEN (case THEN (move ["v'"]))) THEN (((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN", [IN]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h"])) THEN (move ["eq"])));
1120    ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1121    (BETA_TAC THEN (case THEN (move ["v'"])) THEN (case THEN (move ["w'"])));
1122    (((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("properties_of_set_of_edge_fan", [properties_of_set_of_edge_fan])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h"])) THEN (move ["eq"]));
1123    ((((use_arg_then2 ("w_in", [])) (disch_tac [])) THEN (clear_assumption "w_in") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1124 ];;
1125
1126 (* Lemma fan_hypermaps_iso_explicit2 *)
1127 let fan_hypermaps_iso_explicit2 = Sections.section_proof []
1128 `hyp_iso (ext_dart (V,E)) (hypermap_of_fan (V,E),hypermap1_of_fanx (vec 0,V,E))`
1129 [
1130    ((fun arg_tac -> (use_arg_then2 ("hyp_iso_inv", [hyp_iso_inv])) (fun fst_arg -> (use_arg_then2 ("fan_hypermaps_iso_explicit", [fan_hypermaps_iso_explicit])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
1131    (((fun arg_tac -> (use_arg_then2 ("hyp_iso_ext", [hyp_iso_ext])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
1132    (((((use_arg_then2 ("hypermap_of_fan_rep_alt", [hypermap_of_fan_rep_alt]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]) THEN (move ["d_in"]));
1133    ((((use_arg_then2 ("ext_dart_eq_inv_contracted_dart", [ext_dart_eq_inv_contracted_dart]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1134 ];;
1135
1136 (* Lemma fan_hypermaps_iso2 *)
1137 let fan_hypermaps_iso2 = Sections.section_proof []
1138 `(hypermap_of_fan (V,E)) iso (hypermap1_of_fanx (vec 0,V,E))`
1139 [
1140    (((fun arg_tac -> (use_arg_then2 ("hyp_iso_imp_iso", [hyp_iso_imp_iso])) (fun fst_arg -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
1141 ];;
1142
1143 (* Finalization of the section Iso *)
1144 let bij_contracted_dart = Sections.finalize_theorem bij_contracted_dart;;
1145 let hypermap_of_fan_rep_alt = Sections.finalize_theorem hypermap_of_fan_rep_alt;;
1146 let fan_hypermaps_iso_explicit = Sections.finalize_theorem fan_hypermaps_iso_explicit;;
1147 let fan_hypermaps_iso = Sections.finalize_theorem fan_hypermaps_iso;;
1148 let ext_dart_eq_inv_contracted_dart = Sections.finalize_theorem ext_dart_eq_inv_contracted_dart;;
1149 let fan_hypermaps_iso_explicit2 = Sections.finalize_theorem fan_hypermaps_iso_explicit2;;
1150 let fan_hypermaps_iso2 = Sections.finalize_theorem fan_hypermaps_iso2;;
1151 Sections.end_section "Iso";;
1152
1153 (* Finalization of the section FanHypermapsIso *)
1154 let fan_in_e_imp_neq = Sections.finalize_theorem fan_in_e_imp_neq;;
1155 let in_set_of_edge_neq = Sections.finalize_theorem in_set_of_edge_neq;;
1156 let dart_of_fan_eq = Sections.finalize_theorem dart_of_fan_eq;;
1157 let darts_of_fan_disj = Sections.finalize_theorem darts_of_fan_disj;;
1158 let dart1_of_fan_eq_image = Sections.finalize_theorem dart1_of_fan_eq_image;;
1159 let dart2_of_fan_eq_image = Sections.finalize_theorem dart2_of_fan_eq_image;;
1160 let disjoint_preimage = Sections.finalize_theorem disjoint_preimage;;
1161 let darts_of_fan_disj1 = Sections.finalize_theorem darts_of_fan_disj1;;
1162 let bij_contracted_dart1 = Sections.finalize_theorem bij_contracted_dart1;;
1163 let bij_contracted_dart2 = Sections.finalize_theorem bij_contracted_dart2;;
1164 let bij_contracted_dart = Sections.finalize_theorem bij_contracted_dart;;
1165 let hypermap_of_fan_rep_alt = Sections.finalize_theorem hypermap_of_fan_rep_alt;;
1166 let fan_hypermaps_iso_explicit = Sections.finalize_theorem fan_hypermaps_iso_explicit;;
1167 let fan_hypermaps_iso = Sections.finalize_theorem fan_hypermaps_iso;;
1168 let ext_dart_eq_inv_contracted_dart = Sections.finalize_theorem ext_dart_eq_inv_contracted_dart;;
1169 let fan_hypermaps_iso_explicit2 = Sections.finalize_theorem fan_hypermaps_iso_explicit2;;
1170 let fan_hypermaps_iso2 = Sections.finalize_theorem fan_hypermaps_iso2;;
1171 Sections.end_section "FanHypermapsIso";;
1172
1173 (* Close the module *)
1174 end;;