formal_lp/hypermap/ineqs/lp_gen_theory-compiled.hl

   1 needs "../formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl";;
   2
   3 (* Module Lp_gen_theory*)
   4 module Lp_gen_theory = struct
   5
   6 open Ssrbool;;
   7 open Ssrnat;;
   8 open Seq;;
   9 open Seq2;;
  10 open Fan_defs;;
  11 open Hypermap;;
  12 open Hypermap_and_fan;;
  13 open Hypermap_iso;;
  14 open List_hypermap;;
  15 let list_dart_pairs = new_definition
  16         `list_dart_pairs L = allpairs (\x y. (x,y)) (list_of_darts L) (list_of_darts L)`;;
  17
  18 (* Lemma mem_list_dart_pairs *)
  19 let mem_list_dart_pairs = Sections.section_proof ["L";"p"]
  20 `MEM p (list_dart_pairs L)
  21         <=> MEM (FST p) (list_of_darts L) /\ MEM (SND p) (list_of_darts L)`
  22 [
  23    (((((use_arg_then2 ("list_dart_pairs", [list_dart_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("allpairsP", [allpairsP]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
  24    ((BETA_TAC THEN (case THEN (move ["p'"])) THEN (case THEN (move ["mem1"])) THEN (case THEN (move ["mem2"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  25    ((BETA_TAC THEN (move ["h"])) THEN ((use_arg_then2 ("p", [])) (term_tac exists_tac)) THEN (done_tac));
  26 ];;
  27
  28 (* Lemma set_of_list_list_dart_pairs *)
  29 let set_of_list_list_dart_pairs = Sections.section_proof ["L"]
  30 `set_of_list (list_dart_pairs L) = (darts_of_list L) CROSS (darts_of_list L)`
  31 [
  32    ((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["x"]) THEN (move ["y"]))));
  33    (((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_CROSS", [IN_CROSS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_list_dart_pairs", [mem_list_dart_pairs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  34 ];;
  35
  36 (* Lemma ALL_list_dart_pairs_split *)
  37 let ALL_list_dart_pairs_split = Sections.section_proof ["L";"P"]
  38 `ALL P (list_dart_pairs L)
  39         <=> ALL (\d1. ALL (\d2. P (d1, d2)) (list_of_darts L)) (list_of_darts L)`
  40 [
  41    (((repeat_tactic 1 9 (((use_arg_then2 ("ALL_MEM", [ALL_MEM]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_list_dart_pairs", [mem_list_dart_pairs]))(thm_tac (new_rewrite [] []))))) THEN (split_tac));
  42    ((BETA_TAC THEN (move ["h"]) THEN (move ["d1"]) THEN (move ["mem_d1"]) THEN (move ["d2"]) THEN (move ["mem_d2"])) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  43    ((BETA_TAC THEN (move ["h"]) THEN (case THEN ((move ["d1"]) THEN (move ["d2"]))) THEN (simp_tac) THEN (move ["mem_ds"])) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  44 ];;
  45
  46 (* Section IsoLemmas *)
  47 Sections.begin_section "IsoLemmas";;
  48 (Sections.add_section_var (mk_var ("G", (`:(B)hypermap`))));;
  49 (Sections.add_section_var (mk_var ("H", (`:(A)hypermap`))));;
  50 (Sections.add_section_var (mk_var ("g", (`:B->A`))));;
  51
  52 (* Lemma darts_k_subset *)
  53 let darts_k_subset = Sections.section_proof ["k";"d"]
  54 `d IN darts_k k G ==> d IN dart G`
  55 [
  56    ((((((use_arg_then2 ("darts_k", [darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  57 ];;
  58
  59 (* Lemma face_set_k_subset *)
  60 let face_set_k_subset = Sections.section_proof ["k";"f"]
  61 `f IN face_set_k k G ==> f IN face_set G`
  62 [
  63    ((((((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  64 ];;
  65 (Sections.add_section_hyp "g_iso" (`hyp_iso g (G,H)`));;
  66
  67 (* Lemma components_iso_image *)
  68 let components_iso_image = Sections.section_proof ["d"]
  69 `d IN dart G ==>
  70         node H (g d) = IMAGE g (node G d)
  71         /\ face H (g d) = IMAGE g (face G d)`
  72 [
  73    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (simp_tac)) THEN (done_tac));
  74 ];;
  75
  76 (* Lemma components_iso_image_face_map *)
  77 let components_iso_image_face_map = Sections.section_proof ["d"]
  78 `d IN dart G
  79         ==> node H (g (face_map G d)) = IMAGE g (node G (face_map G d))
  80         /\ face H (g (face_map G d)) = IMAGE g (face G (face_map G d))
  81         /\ node H (g (inverse (face_map G) d)) = IMAGE g (node G (inverse (face_map G) d))
  82         /\ face H (g (inverse (face_map G) d)) = IMAGE g (face G (inverse (face_map G) d))`
  83 [
  84    ((BETA_TAC THEN (move ["d_in"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("components_iso_image", [components_iso_image]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac ->(use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(fun tmp_arg1 -> (use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(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));
  85 ];;
  86
  87 (* Lemma hyp_iso_comm_special *)
  88 let hyp_iso_comm_special = Sections.section_proof ["d"]
  89 `d IN dart G
  90         ==> face_map H (g d) = g (face_map G d)
  91            /\ node_map H (g d) = g (node_map G d)
  92            /\ edge_map H (g d) = g (edge_map G d)
  93            /\ (!k. (face_map H POWER k) (g d) = g ((face_map G POWER k) d))`
  94 [
  95    ((BETA_TAC THEN (move ["d_in"])) THEN ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))));
  96    ((THENL_FIRST) ((THENL) elim [ALL_TAC; ((move ["k"]) 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)));
  97    (((repeat_tactic 1 9 (((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_dart_invariant_power_face", [lemma_dart_invariant_power_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  98 ];;
  99
 100 (* Lemma hyp_iso_inv_comm *)
 101 let hyp_iso_inv_comm = Sections.section_proof ["d"]
 102 `d IN dart G
 103         ==> inverse (face_map H) (g d) = g (inverse (face_map G) d)
 104             /\ inverse (node_map H) (g d) = g (inverse (node_map G) d)`
 105 [
 106    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (simp_tac)) THEN (done_tac));
 107 ];;
 108
 109 (* Lemma card_face_iso *)
 110 let card_face_iso = Sections.section_proof ["f"]
 111 `f IN face_set G ==> CARD (IMAGE g f) = CARD f`
 112 [
 113    ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 114    (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_card_components", [hyp_iso_card_components])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 115 ];;
 116
 117 (* Lemma card_face_dart_iso *)
 118 let card_face_dart_iso = Sections.section_proof ["d"]
 119 `d IN dart G ==> CARD (IMAGE g (face G d)) = CARD (face G d)`
 120 [
 121    ((BETA_TAC THEN (move ["d_in"])) THEN ((((use_arg_then2 ("card_face_iso", [card_face_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 122 ];;
 123
 124 (* Lemma hyp_iso_face_set_k *)
 125 let hyp_iso_face_set_k = Sections.section_proof ["k"]
 126 `face_set_k k H = IMAGE (IMAGE g) (face_set_k k G)`
 127 [
 128    (((repeat_tactic 1 9 (((use_arg_then2 ("face_set_k", [face_set_k]))(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 ("inE", [inE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["f"]));
 129    ((((fun arg_tac -> (use_arg_then2 ("iso_face_set", [iso_face_set])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))));
 130    ((THENL) (split_tac) [((case THEN ALL_TAC) THEN (case THEN (move ["f'"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["f'_in"]) THEN (move ["card_f'"])); ((case THEN (move ["f'"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["h"]))]);
 131    (((use_arg_then2 ("f'", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("card_face_iso", [card_face_iso]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 132    (((((use_arg_then2 ("card_face_iso", [card_face_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("f'", [])) (term_tac exists_tac)) THEN (done_tac));
 133 ];;
 134
 135 (* Lemma hyp_iso_darts_k_eq *)
 136 let hyp_iso_darts_k_eq = Sections.section_proof ["k"]
 137 `darts_k k H = IMAGE g (darts_k k G)`
 138 [
 139    (((repeat_tactic 1 9 (((use_arg_then2 ("darts_k_union_face_set_k", [darts_k_union_face_set_k]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IMAGE_UNIONS", [IMAGE_UNIONS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso_face_set_k", [hyp_iso_face_set_k]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 140 ];;
 141
 142 (* Lemma hyp_iso_darts_k *)
 143 let hyp_iso_darts_k = Sections.section_proof ["k";"d"]
 144 `d IN darts_k k G ==> g d IN darts_k k H`
 145 [
 146    ((((((use_arg_then2 ("hyp_iso_darts_k_eq", [hyp_iso_darts_k_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["d_in"])) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac));
 147 ];;
 148
 149 (* Lemma sum_node_iso *)
 150 let sum_node_iso = Sections.section_proof ["r";"n"]
 151 `n IN node_set G ==> sum (IMAGE g n) r = sum n (r o g)`
 152 [
 153    ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 154    ((((fun arg_tac -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (move ["x_in"])));
 155    ((((((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("x_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["xG"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("x_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["yG"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 156 ];;
 157
 158 (* Lemma sum_face_iso *)
 159 let sum_face_iso = Sections.section_proof ["r";"f"]
 160 `f IN face_set G ==> sum (IMAGE g f) r = sum f (r o g)`
 161 [
 162    ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 163    ((((fun arg_tac -> (use_arg_then2 ("lemma_face_subset", [lemma_face_subset])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (move ["x_in"])));
 164    ((((((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("x_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["xG"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("x_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["yG"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 165 ];;
 166
 167 (* Lemma iso_dart_trans *)
 168 let iso_dart_trans = Sections.section_proof ["P"]
 169 `(!d. d IN dart H ==> P d) ==> (!d. d IN dart G ==> P (g d))`
 170 [
 171    ((BETA_TAC THEN (move ["h"]) THEN (move ["d"]) THEN (move ["d_in"])) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 172 ];;
 173
 174 (* Lemma iso_darts_k_trans *)
 175 let iso_darts_k_trans = Sections.section_proof ["k";"P"]
 176 `(!d. d IN darts_k k H ==> P d)
 177         ==> (!d. d IN darts_k k G ==> P (g d))`
 178 [
 179    ((BETA_TAC THEN (move ["h"]) THEN (move ["d"]) THEN (move ["d_in"])) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hyp_iso_darts_k", [hyp_iso_darts_k]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 180 ];;
 181
 182 (* Lemma iso_dart_pairs_trans *)
 183 let iso_dart_pairs_trans = Sections.section_proof ["P"]
 184 `(!p. p IN dart H CROSS dart H ==> P p)
 185         ==> (!p. p IN dart G CROSS dart G ==> P (g (FST p), g (SND p)))`
 186 [
 187    ((BETA_TAC THEN (move ["h"]) THEN (case THEN ((move ["x"]) THEN (move ["y"])))) THEN ((((use_arg_then2 ("IN_CROSS", [IN_CROSS]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["x_in"]) THEN (move ["y_in"]))) THEN (simp_tac)));
 188    (((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_CROSS", [IN_CROSS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 189 ];;
 190
 191 (* Lemma iso_face_trans *)
 192 let iso_face_trans = Sections.section_proof ["P"]
 193 `(!f. f IN face_set H ==> P f)
 194         ==> (!f. f IN face_set G ==> P (IMAGE g f))`
 195 [
 196    ((((((fun arg_tac -> (use_arg_then2 ("iso_face_set", [iso_face_set])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["f"]) THEN (move ["f_in"])) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
 197 ];;
 198
 199 (* Lemma iso_node_trans *)
 200 let iso_node_trans = Sections.section_proof ["P"]
 201 `(!n. n IN node_set H ==> P n)
 202         ==> (!n. n IN node_set G ==> P (IMAGE g n))`
 203 [
 204    ((((((fun arg_tac -> (use_arg_then2 ("iso_node_set", [iso_node_set])) (fun fst_arg -> (use_arg_then2 ("g_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["n"]) THEN (move ["n_in"])) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN (done_tac));
 205 ];;
 206
 207 (* Lemma iso_face_k_trans *)
 208 let iso_face_k_trans = Sections.section_proof ["k";"P"]
 209 `(!f. f IN face_set_k k H ==> P f)
 210         ==> (!f. f IN face_set_k k G ==> P (IMAGE g f))`
 211 [
 212    ((((((use_arg_then2 ("hyp_iso_face_set_k", [hyp_iso_face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["f"]) THEN (move ["f_in"])) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
 213 ];;
 214
 215 (* Finalization of the section IsoLemmas *)
 216 let darts_k_subset = Sections.finalize_theorem darts_k_subset;;
 217 let face_set_k_subset = Sections.finalize_theorem face_set_k_subset;;
 218 let components_iso_image = Sections.finalize_theorem components_iso_image;;
 219 let components_iso_image_face_map = Sections.finalize_theorem components_iso_image_face_map;;
 220 let hyp_iso_comm_special = Sections.finalize_theorem hyp_iso_comm_special;;
 221 let hyp_iso_inv_comm = Sections.finalize_theorem hyp_iso_inv_comm;;
 222 let card_face_iso = Sections.finalize_theorem card_face_iso;;
 223 let card_face_dart_iso = Sections.finalize_theorem card_face_dart_iso;;
 224 let hyp_iso_face_set_k = Sections.finalize_theorem hyp_iso_face_set_k;;
 225 let hyp_iso_darts_k_eq = Sections.finalize_theorem hyp_iso_darts_k_eq;;
 226 let hyp_iso_darts_k = Sections.finalize_theorem hyp_iso_darts_k;;
 227 let sum_node_iso = Sections.finalize_theorem sum_node_iso;;
 228 let sum_face_iso = Sections.finalize_theorem sum_face_iso;;
 229 let iso_dart_trans = Sections.finalize_theorem iso_dart_trans;;
 230 let iso_darts_k_trans = Sections.finalize_theorem iso_darts_k_trans;;
 231 let iso_dart_pairs_trans = Sections.finalize_theorem iso_dart_pairs_trans;;
 232 let iso_face_trans = Sections.finalize_theorem iso_face_trans;;
 233 let iso_node_trans = Sections.finalize_theorem iso_node_trans;;
 234 let iso_face_k_trans = Sections.finalize_theorem iso_face_k_trans;;
 235 Sections.end_section "IsoLemmas";;
 236
 237 (* Section BijLemmas *)
 238 Sections.begin_section "BijLemmas";;
 239 (Sections.add_section_var (mk_var ("h", (`:D->C`))));;
 240
 241 (* Lemma bij_trans *)
 242 let bij_trans = Sections.section_proof ["R";"V"]
 243 `BIJ h R V
 244         ==> !P. (!x. x IN V ==> P x) ==> (!x. x IN R ==> P (h x))`
 245 [
 246    ((((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN (move ["bij_h"]) THEN (move ["p"]) THEN (move ["h"]) THEN (move ["x"]) THEN (move ["x_in"])) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("bij_h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 247 ];;
 248
 249 (* Lemma fst_iso_trans *)
 250 let fst_iso_trans = Sections.section_proof ["g"]
 251 `(!d. g d = h (FST d), h (SND d))
 252         ==> (!d. FST (g d) = h (FST d))`
 253 [
 254    ((BETA_TAC THEN (move ["g_eq"]) THEN (move ["d"])) THEN ((((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 255 ];;
 256
 257 (* Finalization of the section BijLemmas *)
 258 let bij_trans = Sections.finalize_theorem bij_trans;;
 259 let fst_iso_trans = Sections.finalize_theorem fst_iso_trans;;
 260 Sections.end_section "BijLemmas";;
 261
 262 (* Lemma list_sum_set_of_list_gen *)
 263 let list_sum_set_of_list_gen = Sections.section_proof ["s"]
 264 `uniq s ==> list_sum s = sum (set_of_list s)`
 265 [
 266    ((BETA_TAC THEN (move ["uniq_s"])) THEN ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["f"])) THEN (((use_arg_then2 ("list_sum_set_of_list", [list_sum_set_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 267 ];;
 268
 269 (* Section ListLemmas *)
 270 Sections.begin_section "ListLemmas";;
 271 (Sections.add_section_var (mk_var ("L", (`:((A)list)list`))));;
 272
 273 (* Lemma list_of_faces3_subset *)
 274 let list_of_faces3_subset = Sections.section_proof ["f"]
 275 `MEM f (list_of_faces3 L) ==> MEM f (list_of_faces L)`
 276 [
 277    ((((((use_arg_then2 ("list_of_faces3", [list_of_faces3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 278 ];;
 279
 280 (* Lemma list_of_faces4_subset *)
 281 let list_of_faces4_subset = Sections.section_proof ["f"]
 282 `MEM f (list_of_faces4 L) ==> MEM f (list_of_faces L)`
 283 [
 284    ((((((use_arg_then2 ("list_of_faces4", [list_of_faces4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 285 ];;
 286
 287 (* Lemma list_of_faces5_subset *)
 288 let list_of_faces5_subset = Sections.section_proof ["f"]
 289 `MEM f (list_of_faces5 L) ==> MEM f (list_of_faces L)`
 290 [
 291    ((((((use_arg_then2 ("list_of_faces5", [list_of_faces5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 292 ];;
 293
 294 (* Lemma list_of_faces6_subset *)
 295 let list_of_faces6_subset = Sections.section_proof ["f"]
 296 `MEM f (list_of_faces6 L) ==> MEM f (list_of_faces L)`
 297 [
 298    ((((((use_arg_then2 ("list_of_faces6", [list_of_faces6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 299 ];;
 300
 301 (* Lemma list_of_darts3_subset *)
 302 let list_of_darts3_subset = Sections.section_proof ["d"]
 303 `MEM d (list_of_darts3 L) ==> MEM d (list_of_darts L)`
 304 [
 305    ((((use_arg_then2 ("list_of_darts3", [list_of_darts3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces3", [list_of_faces3]))(thm_tac (new_rewrite [] [])))));
 306    ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (move ["h"])) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
 307 ];;
 308
 309 (* Lemma list_of_darts4_subset *)
 310 let list_of_darts4_subset = Sections.section_proof ["d"]
 311 `MEM d (list_of_darts4 L) ==> MEM d (list_of_darts L)`
 312 [
 313    ((((use_arg_then2 ("list_of_darts4", [list_of_darts4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces4", [list_of_faces4]))(thm_tac (new_rewrite [] [])))));
 314    ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (move ["h"])) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
 315 ];;
 316
 317 (* Lemma list_of_darts5_subset *)
 318 let list_of_darts5_subset = Sections.section_proof ["d"]
 319 `MEM d (list_of_darts5 L) ==> MEM d (list_of_darts L)`
 320 [
 321    ((((use_arg_then2 ("list_of_darts5", [list_of_darts5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces5", [list_of_faces5]))(thm_tac (new_rewrite [] [])))));
 322    ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (move ["h"])) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
 323 ];;
 324
 325 (* Lemma list_of_darts6_subset *)
 326 let list_of_darts6_subset = Sections.section_proof ["d"]
 327 `MEM d (list_of_darts6 L) ==> MEM d (list_of_darts L)`
 328 [
 329    ((((use_arg_then2 ("list_of_darts6", [list_of_darts6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces6", [list_of_faces6]))(thm_tac (new_rewrite [] [])))));
 330    ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (move ["h"])) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
 331 ];;
 332
 333 (* Lemma list_of_dart_pairs_subset *)
 334 let list_of_dart_pairs_subset = Sections.section_proof ["p"]
 335 `MEM p (list_dart_pairs L)
 336         ==> MEM (FST p) (list_of_darts L) /\ MEM (SND p) (list_of_darts L)`
 337 [
 338    ((((((use_arg_then2 ("list_dart_pairs", [list_dart_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("allpairsP", [allpairsP]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["p'"])) THEN (case THEN (move ["mem1"])) THEN (case THEN (move ["mem2"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 339 ];;
 340
 341 (* Lemma e_list_ext_eq_e_list *)
 342 let e_list_ext_eq_e_list = Sections.section_proof ["d"]
 343 `MEM d (list_of_darts L) ==> e_list_ext L d = e_list d`
 344 [
 345    ((((((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 346 ];;
 347
 348 (* Lemma fst_choice_of_list_node *)
 349 let fst_choice_of_list_node = Sections.section_proof ["g";"h";"n"]
 350 `MEM n (list_of_nodes L)
 351         /\ (!d. g d = h (FST d), h (SND d):C)
 352         ==> FST (CHOICE (IMAGE g (set_of_list n))) = FST (g (HD n))`
 353 [
 354    (BETA_TAC THEN (case THEN (move ["mem_n"])) THEN (move ["g_eq"]));
 355    ((fun arg_tac -> arg_tac (Arg_term (`CHOICE _`))) (term_tac (set_tac "x")));
 356    ((fun arg_tac -> arg_tac (Arg_term (`HD n`))) (term_tac (set_tac "y")));
 357    ((fun arg_tac -> arg_tac (Arg_term (`x IN IMAGE g (set_of_list n)`))) (term_tac (have_gen_tac []ALL_TAC)));
 358    (((((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CHOICE_DEF", [CHOICE_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IMAGE_EQ_EMPTY", [IMAGE_EQ_EMPTY]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SET_OF_LIST_EQ_EMPTY", [SET_OF_LIST_EQ_EMPTY]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("node_of_list_not_nil", [node_of_list_not_nil])) (fun fst_arg -> (use_arg_then2 ("mem_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 359    (((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["d"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["mem_d"]));
 360    ((fun arg_tac -> arg_tac (Arg_term (`MEM y n`))) (term_tac (have_gen_tac [](move ["mem_y"]))));
 361    (((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] [])))));
 362    ((((THENL) (((fun arg_tac -> (use_arg_then2 ("node_of_list_not_nil", [node_of_list_not_nil])) (fun fst_arg -> (use_arg_then2 ("mem_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) THEN ((TRY done_tac))) THEN ((((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 363    ((((use_arg_then2 ("mem_n", [])) (disch_tac [])) THEN (clear_assumption "mem_n") THEN BETA_TAC) THEN (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["t"])) THEN (case THEN (move ["_"])) THEN (simp_tac) THEN (move ["n_eq"])));
 364    ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN ((use_arg_then2 ("mem_y", [])) (disch_tac [])) THEN (clear_assumption "mem_y") THEN BETA_TAC) THEN (((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 365 ];;
 366 (Sections.add_section_hyp "goodL" (`good_list L`));;
 367
 368 (* Lemma card_set_of_list_node *)
 369 let card_set_of_list_node = Sections.section_proof ["n"]
 370 `MEM n (list_of_nodes L) ==> CARD (set_of_list n) = LENGTH n`
 371 [
 372    ((BETA_TAC THEN (move ["mem_n"])) THEN ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("uniq_node", [uniq_node])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 373 ];;
 374
 375 (* Lemma card_set_of_list_face *)
 376 let card_set_of_list_face = Sections.section_proof ["f"]
 377 `MEM f (list_of_faces L) ==> CARD (set_of_list f) = LENGTH f`
 378 [
 379    ((BETA_TAC THEN (move ["mem_n"])) THEN ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("uniq_face", [uniq_face])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 380 ];;
 381
 382 (* Lemma card_face_eq_length_find_face *)
 383 let card_face_eq_length_find_face = Sections.section_proof ["d"]
 384 `MEM d (list_of_darts L)
 385         ==> CARD (face (hypermap_of_list L) d) = LENGTH (find_face L d)`
 386 [
 387    ((BETA_TAC THEN (move ["mem_d"])) THEN ((((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
 388    ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN (clear_assumption "goodL") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 389 ];;
 390
 391 (* Lemma dart_list_all *)
 392 let dart_list_all = Sections.section_proof ["P"]
 393 `(!d. d IN dart (hypermap_of_list L) ==> P d)
 394         <=> (!d. MEM d (list_of_darts L) ==> P d)`
 395 [
 396    (((((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 397 ];;
 398
 399 (* Lemma dart3_list_all *)
 400 let dart3_list_all = Sections.section_proof ["P"]
 401 `(!d. d IN darts_k 3 (hypermap_of_list L) ==> P d)
 402         <=> (!d. MEM d (list_of_darts3 L) ==> P d)`
 403 [
 404    (((((use_arg_then2 ("darts3_eq_list_of_darts3", [darts3_eq_list_of_darts3]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 405 ];;
 406
 407 (* Lemma dart4_list_all *)
 408 let dart4_list_all = Sections.section_proof ["P"]
 409 `(!d. d IN darts_k 4 (hypermap_of_list L) ==> P d)
 410         <=> (!d. MEM d (list_of_darts4 L) ==> P d)`
 411 [
 412    (((((use_arg_then2 ("darts4_eq_list_of_darts4", [darts4_eq_list_of_darts4]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 413 ];;
 414
 415 (* Lemma dart5_list_all *)
 416 let dart5_list_all = Sections.section_proof ["P"]
 417 `(!d. d IN darts_k 5 (hypermap_of_list L) ==> P d)
 418         <=> (!d. MEM d (list_of_darts5 L) ==> P d)`
 419 [
 420    (((((use_arg_then2 ("darts5_eq_list_of_darts5", [darts5_eq_list_of_darts5]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 421 ];;
 422
 423 (* Lemma dart6_list_all *)
 424 let dart6_list_all = Sections.section_proof ["P"]
 425 `(!d. d IN darts_k 6 (hypermap_of_list L) ==> P d)
 426         <=> (!d. MEM d (list_of_darts6 L) ==> P d)`
 427 [
 428    (((((use_arg_then2 ("darts6_eq_list_of_darts6", [darts6_eq_list_of_darts6]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 429 ];;
 430
 431 (* Lemma dart_pairs_list_all *)
 432 let dart_pairs_list_all = Sections.section_proof ["P"]
 433 `(!p. p IN dart (hypermap_of_list L) CROSS dart (hypermap_of_list L) ==> P p)
 434         <=> (!p. MEM p (list_dart_pairs L) ==> P p)`
 435 [
 436    (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_of_list_list_dart_pairs", [set_of_list_list_dart_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 437 ];;
 438
 439 (* Lemma elements_list_all *)
 440 let elements_list_all = Sections.section_proof ["P"]
 441 `(!x. x IN elements_of_list L ==> P x)
 442         <=> (!x. MEM x (list_of_elements L) ==> P x)`
 443 [
 444    (((((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 445 ];;
 446
 447 (* Lemma sum_node_list_all *)
 448 let sum_node_list_all = Sections.section_proof ["P"]
 449 `good_list_nodes L
 450         ==> ((!n. n IN node_set (hypermap_of_list L) ==> P n (sum n))
 451                 <=> (!n. MEM n (list_of_nodes L) ==> P (set_of_list n) (list_sum n)))`
 452 [
 453    (((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))));
 454    ((THENL) (split_tac) [((move ["h"]) THEN (move ["n"]) THEN (move ["mem_n"])); ((move ["h"]) THEN (move ["t"]) THEN (case THEN (move ["n"])) THEN (case THEN (move ["mem_n"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
 455    (((((use_arg_then2 ("list_sum_set_of_list_gen", [list_sum_set_of_list_gen]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("uniq_node", [uniq_node])) (fun fst_arg -> (use_arg_then2 ("mem_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN (done_tac));
 456    (((((use_arg_then2 ("list_sum_set_of_list_gen", [list_sum_set_of_list_gen]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("uniq_node", [uniq_node])) (fun fst_arg -> (use_arg_then2 ("mem_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 457 ];;
 458
 459 (* Lemma sum_face_list_all *)
 460 let sum_face_list_all = Sections.section_proof ["P"]
 461 `(!f. f IN face_set (hypermap_of_list L) ==> P f (sum f))
 462                 <=> (!f. MEM f (list_of_faces L) ==> P (set_of_list f) (list_sum f))`
 463 [
 464    ((((use_arg_then2 ("face_set_eq_list", [face_set_eq_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))));
 465    ((THENL) (split_tac) [((move ["h"]) THEN (move ["f"]) THEN (move ["mem_f"])); ((move ["h"]) THEN (move ["t"]) THEN (case THEN (move ["f"])) THEN (case THEN (move ["mem_f"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
 466    (((((use_arg_then2 ("list_sum_set_of_list_gen", [list_sum_set_of_list_gen]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("uniq_face", [uniq_face])) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
 467    (((((use_arg_then2 ("list_sum_set_of_list_gen", [list_sum_set_of_list_gen]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("uniq_face", [uniq_face])) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 468 ];;
 469
 470 (* Finalization of the section ListLemmas *)
 471 let list_of_faces3_subset = Sections.finalize_theorem list_of_faces3_subset;;
 472 let list_of_faces4_subset = Sections.finalize_theorem list_of_faces4_subset;;
 473 let list_of_faces5_subset = Sections.finalize_theorem list_of_faces5_subset;;
 474 let list_of_faces6_subset = Sections.finalize_theorem list_of_faces6_subset;;
 475 let list_of_darts3_subset = Sections.finalize_theorem list_of_darts3_subset;;
 476 let list_of_darts4_subset = Sections.finalize_theorem list_of_darts4_subset;;
 477 let list_of_darts5_subset = Sections.finalize_theorem list_of_darts5_subset;;
 478 let list_of_darts6_subset = Sections.finalize_theorem list_of_darts6_subset;;
 479 let list_of_dart_pairs_subset = Sections.finalize_theorem list_of_dart_pairs_subset;;
 480 let e_list_ext_eq_e_list = Sections.finalize_theorem e_list_ext_eq_e_list;;
 481 let fst_choice_of_list_node = Sections.finalize_theorem fst_choice_of_list_node;;
 482 let card_set_of_list_node = Sections.finalize_theorem card_set_of_list_node;;
 483 let card_set_of_list_face = Sections.finalize_theorem card_set_of_list_face;;
 484 let card_face_eq_length_find_face = Sections.finalize_theorem card_face_eq_length_find_face;;
 485 let dart_list_all = Sections.finalize_theorem dart_list_all;;
 486 let dart3_list_all = Sections.finalize_theorem dart3_list_all;;
 487 let dart4_list_all = Sections.finalize_theorem dart4_list_all;;
 488 let dart5_list_all = Sections.finalize_theorem dart5_list_all;;
 489 let dart6_list_all = Sections.finalize_theorem dart6_list_all;;
 490 let dart_pairs_list_all = Sections.finalize_theorem dart_pairs_list_all;;
 491 let elements_list_all = Sections.finalize_theorem elements_list_all;;
 492 let sum_node_list_all = Sections.finalize_theorem sum_node_list_all;;
 493 let sum_face_list_all = Sections.finalize_theorem sum_face_list_all;;
 494 Sections.end_section "ListLemmas";;
 495
 496 (* Close the module *)
 497 end;;