needs "../formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl";;

(* Module Lp_gen_theory*)
module Lp_gen_theory = struct

open Ssrbool;;
open Ssrnat;;
open Seq;;
open Seq2;;
open Fan_defs;;
open Hypermap;;
open Hypermap_and_fan;;
open Hypermap_iso;;
open List_hypermap;;
let list_dart_pairs = new_definition
	`list_dart_pairs L = allpairs (\x y. (x,y)) (list_of_darts L) (list_of_darts L)`;;

(* Lemma mem_list_dart_pairs *)
let mem_list_dart_pairs = Sections.section_proof ["L";"p"]
`MEM p (list_dart_pairs L)
	<=> MEM (FST p) (list_of_darts L) /\ MEM (SND p) (list_of_darts L)`
[
   (((((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));
   ((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));
   ((BETA_TAC THEN (move ["h"])) THEN ((use_arg_then2 ("p", [])) (term_tac exists_tac)) THEN (done_tac));
];;

(* Lemma set_of_list_list_dart_pairs *)
let set_of_list_list_dart_pairs = Sections.section_proof ["L"]
`set_of_list (list_dart_pairs L) = (darts_of_list L) CROSS (darts_of_list L)`
[
   ((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["x"]) THEN (move ["y"]))));
   (((((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));
];;

(* Lemma ALL_list_dart_pairs_split *)
let ALL_list_dart_pairs_split = Sections.section_proof ["L";"P"]
`ALL P (list_dart_pairs L) 
	<=> ALL (\d1. ALL (\d2. P (d1, d2)) (list_of_darts L)) (list_of_darts L)`
[
   (((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));
   ((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));
   ((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));
];;

(* Section IsoLemmas *)
Sections.begin_section "IsoLemmas";;
(Sections.add_section_var (mk_var ("G", (`:(B)hypermap`))));;
(Sections.add_section_var (mk_var ("H", (`:(A)hypermap`))));;
(Sections.add_section_var (mk_var ("g", (`:B->A`))));;

(* Lemma darts_k_subset *)
let darts_k_subset = Sections.section_proof ["k";"d"]
`d IN darts_k k G ==> d IN dart G`
[
   ((((((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));
];;

(* Lemma face_set_k_subset *)
let face_set_k_subset = Sections.section_proof ["k";"f"]
`f IN face_set_k k G ==> f IN face_set G`
[
   ((((((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));
];;
(Sections.add_section_hyp "g_iso" (`hyp_iso g (G,H)`));;

(* Lemma components_iso_image *)
let components_iso_image = Sections.section_proof ["d"]
`d IN dart G ==>
	node H (g d) = IMAGE g (node G d)
	/\ face H (g d) = IMAGE g (face G d)`
[
   (((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));
];;

(* Lemma components_iso_image_face_map *)
let components_iso_image_face_map = Sections.section_proof ["d"]
`d IN dart G
	==> node H (g (face_map G d)) = IMAGE g (node G (face_map G d))
	/\ face H (g (face_map G d)) = IMAGE g (face G (face_map G d))
	/\ node H (g (inverse (face_map G) d)) = IMAGE g (node G (inverse (face_map G) d))
	/\ face H (g (inverse (face_map G) d)) = IMAGE g (face G (inverse (face_map G) d))`
[
   ((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));
];;

(* Lemma hyp_iso_comm_special *)
let hyp_iso_comm_special = Sections.section_proof ["d"]
`d IN dart G
	==> face_map H (g d) = g (face_map G d)
	   /\ node_map H (g d) = g (node_map G d)
	   /\ edge_map H (g d) = g (edge_map G d)
	   /\ (!k. (face_map H POWER k) (g d) = g ((face_map G POWER k) d))`
[
   ((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))));
   ((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)));
   (((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));
];;

(* Lemma hyp_iso_inv_comm *)
let hyp_iso_inv_comm = Sections.section_proof ["d"]
`d IN dart G
	==> inverse (face_map H) (g d) = g (inverse (face_map G) d)
            /\ inverse (node_map H) (g d) = g (inverse (node_map G) d)`
[
   (((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));
];;

(* Lemma card_face_iso *)
let card_face_iso = Sections.section_proof ["f"]
`f IN face_set G ==> CARD (IMAGE g f) = CARD f`
[
   ((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 [] [])))));
   (((((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));
];;

(* Lemma card_face_dart_iso *)
let card_face_dart_iso = Sections.section_proof ["d"]
`d IN dart G ==> CARD (IMAGE g (face G d)) = CARD (face G d)`
[
   ((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));
];;

(* Lemma hyp_iso_face_set_k *)
let hyp_iso_face_set_k = Sections.section_proof ["k"]
`face_set_k k H = IMAGE (IMAGE g) (face_set_k k G)`
[
   (((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"]));
   ((((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 [] [])))));
   ((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"]))]);
   (((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));
   (((((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));
];;

(* Lemma hyp_iso_darts_k_eq *)
let hyp_iso_darts_k_eq = Sections.section_proof ["k"]
`darts_k k H = IMAGE g (darts_k k G)`
[
   (((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));
];;

(* Lemma hyp_iso_darts_k *)
let hyp_iso_darts_k = Sections.section_proof ["k";"d"]
`d IN darts_k k G ==> g d IN darts_k k H`
[
   ((((((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));
];;

(* Lemma sum_node_iso *)
let sum_node_iso = Sections.section_proof ["r";"n"]
`n IN node_set G ==> sum (IMAGE g n) r = sum n (r o g)`
[
   ((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 [] [])))));
   ((((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"])));
   ((((((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));
];;

(* Lemma sum_face_iso *)
let sum_face_iso = Sections.section_proof ["r";"f"]
`f IN face_set G ==> sum (IMAGE g f) r = sum f (r o g)`
[
   ((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 [] [])))));
   ((((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"])));
   ((((((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));
];;

(* Lemma iso_dart_trans *)
let iso_dart_trans = Sections.section_proof ["P"]
`(!d. d IN dart H ==> P d) ==> (!d. d IN dart G ==> P (g d))`
[
   ((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));
];;

(* Lemma iso_darts_k_trans *)
let iso_darts_k_trans = Sections.section_proof ["k";"P"]
`(!d. d IN darts_k k H ==> P d) 
	==> (!d. d IN darts_k k G ==> P (g d))`
[
   ((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));
];;

(* Lemma iso_dart_pairs_trans *)
let iso_dart_pairs_trans = Sections.section_proof ["P"]
`(!p. p IN dart H CROSS dart H ==> P p)
	==> (!p. p IN dart G CROSS dart G ==> P (g (FST p), g (SND p)))`
[
   ((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)));
   (((((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));
];;

(* Lemma iso_face_trans *)
let iso_face_trans = Sections.section_proof ["P"]
`(!f. f IN face_set H ==> P f) 
	==> (!f. f IN face_set G ==> P (IMAGE g f))`
[
   ((((((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));
];;

(* Lemma iso_node_trans *)
let iso_node_trans = Sections.section_proof ["P"]
`(!n. n IN node_set H ==> P n) 
	==> (!n. n IN node_set G ==> P (IMAGE g n))`
[
   ((((((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));
];;

(* Lemma iso_face_k_trans *)
let iso_face_k_trans = Sections.section_proof ["k";"P"]
`(!f. f IN face_set_k k H ==> P f) 
	==> (!f. f IN face_set_k k G ==> P (IMAGE g f))`
[
   ((((((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));
];;

(* Finalization of the section IsoLemmas *)
let darts_k_subset = Sections.finalize_theorem darts_k_subset;;
let face_set_k_subset = Sections.finalize_theorem face_set_k_subset;;
let components_iso_image = Sections.finalize_theorem components_iso_image;;
let components_iso_image_face_map = Sections.finalize_theorem components_iso_image_face_map;;
let hyp_iso_comm_special = Sections.finalize_theorem hyp_iso_comm_special;;
let hyp_iso_inv_comm = Sections.finalize_theorem hyp_iso_inv_comm;;
let card_face_iso = Sections.finalize_theorem card_face_iso;;
let card_face_dart_iso = Sections.finalize_theorem card_face_dart_iso;;
let hyp_iso_face_set_k = Sections.finalize_theorem hyp_iso_face_set_k;;
let hyp_iso_darts_k_eq = Sections.finalize_theorem hyp_iso_darts_k_eq;;
let hyp_iso_darts_k = Sections.finalize_theorem hyp_iso_darts_k;;
let sum_node_iso = Sections.finalize_theorem sum_node_iso;;
let sum_face_iso = Sections.finalize_theorem sum_face_iso;;
let iso_dart_trans = Sections.finalize_theorem iso_dart_trans;;
let iso_darts_k_trans = Sections.finalize_theorem iso_darts_k_trans;;
let iso_dart_pairs_trans = Sections.finalize_theorem iso_dart_pairs_trans;;
let iso_face_trans = Sections.finalize_theorem iso_face_trans;;
let iso_node_trans = Sections.finalize_theorem iso_node_trans;;
let iso_face_k_trans = Sections.finalize_theorem iso_face_k_trans;;
Sections.end_section "IsoLemmas";;

(* Section BijLemmas *)
Sections.begin_section "BijLemmas";;
(Sections.add_section_var (mk_var ("h", (`:D->C`))));;

(* Lemma bij_trans *)
let bij_trans = Sections.section_proof ["R";"V"]
`BIJ h R V
	==> !P. (!x. x IN V ==> P x) ==> (!x. x IN R ==> P (h x))`
[
   ((((((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));
];;

(* Lemma fst_iso_trans *)
let fst_iso_trans = Sections.section_proof ["g"]
`(!d. g d = h (FST d), h (SND d))
	==> (!d. FST (g d) = h (FST d))`
[
   ((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));
];;

(* Finalization of the section BijLemmas *)
let bij_trans = Sections.finalize_theorem bij_trans;;
let fst_iso_trans = Sections.finalize_theorem fst_iso_trans;;
Sections.end_section "BijLemmas";;

(* Lemma list_sum_set_of_list_gen *)
let list_sum_set_of_list_gen = Sections.section_proof ["s"]
`uniq s ==> list_sum s = sum (set_of_list s)`
[
   ((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));
];;

(* Section ListLemmas *)
Sections.begin_section "ListLemmas";;
(Sections.add_section_var (mk_var ("L", (`:((A)list)list`))));;

(* Lemma list_of_faces3_subset *)
let list_of_faces3_subset = Sections.section_proof ["f"]
`MEM f (list_of_faces3 L) ==> MEM f (list_of_faces L)`
[
   ((((((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));
];;

(* Lemma list_of_faces4_subset *)
let list_of_faces4_subset = Sections.section_proof ["f"]
`MEM f (list_of_faces4 L) ==> MEM f (list_of_faces L)`
[
   ((((((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));
];;

(* Lemma list_of_faces5_subset *)
let list_of_faces5_subset = Sections.section_proof ["f"]
`MEM f (list_of_faces5 L) ==> MEM f (list_of_faces L)`
[
   ((((((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));
];;

(* Lemma list_of_faces6_subset *)
let list_of_faces6_subset = Sections.section_proof ["f"]
`MEM f (list_of_faces6 L) ==> MEM f (list_of_faces L)`
[
   ((((((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));
];;

(* Lemma list_of_darts3_subset *)
let list_of_darts3_subset = Sections.section_proof ["d"]
`MEM d (list_of_darts3 L) ==> MEM d (list_of_darts L)`
[
   ((((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 [] [])))));
   ((((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));
];;

(* Lemma list_of_darts4_subset *)
let list_of_darts4_subset = Sections.section_proof ["d"]
`MEM d (list_of_darts4 L) ==> MEM d (list_of_darts L)`
[
   ((((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 [] [])))));
   ((((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));
];;

(* Lemma list_of_darts5_subset *)
let list_of_darts5_subset = Sections.section_proof ["d"]
`MEM d (list_of_darts5 L) ==> MEM d (list_of_darts L)`
[
   ((((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 [] [])))));
   ((((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));
];;

(* Lemma list_of_darts6_subset *)
let list_of_darts6_subset = Sections.section_proof ["d"]
`MEM d (list_of_darts6 L) ==> MEM d (list_of_darts L)`
[
   ((((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 [] [])))));
   ((((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));
];;

(* Lemma list_of_dart_pairs_subset *)
let list_of_dart_pairs_subset = Sections.section_proof ["p"]
`MEM p (list_dart_pairs L) 
	==> MEM (FST p) (list_of_darts L) /\ MEM (SND p) (list_of_darts L)`
[
   ((((((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));
];;

(* Lemma e_list_ext_eq_e_list *)
let e_list_ext_eq_e_list = Sections.section_proof ["d"]
`MEM d (list_of_darts L) ==> e_list_ext L d = e_list d`
[
   ((((((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));
];;

(* Lemma fst_choice_of_list_node *)
let fst_choice_of_list_node = Sections.section_proof ["g";"h";"n"]
`MEM n (list_of_nodes L)
	/\ (!d. g d = h (FST d), h (SND d):C)
	==> FST (CHOICE (IMAGE g (set_of_list n))) = FST (g (HD n))`
[
   (BETA_TAC THEN (case THEN (move ["mem_n"])) THEN (move ["g_eq"]));
   ((fun arg_tac -> arg_tac (Arg_term (`CHOICE _`))) (term_tac (set_tac "x")));
   ((fun arg_tac -> arg_tac (Arg_term (`HD n`))) (term_tac (set_tac "y")));
   ((fun arg_tac -> arg_tac (Arg_term (`x IN IMAGE g (set_of_list n)`))) (term_tac (have_gen_tac []ALL_TAC)));
   (((((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));
   (((((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"]));
   ((fun arg_tac -> arg_tac (Arg_term (`MEM y n`))) (term_tac (have_gen_tac [](move ["mem_y"]))));
   (((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] [])))));
   ((((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));
   ((((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"])));
   ((((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));
];;
(Sections.add_section_hyp "goodL" (`good_list L`));;

(* Lemma card_set_of_list_node *)
let card_set_of_list_node = Sections.section_proof ["n"]
`MEM n (list_of_nodes L) ==> CARD (set_of_list n) = LENGTH n`
[
   ((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));
];;

(* Lemma card_set_of_list_face *)
let card_set_of_list_face = Sections.section_proof ["f"]
`MEM f (list_of_faces L) ==> CARD (set_of_list f) = LENGTH f`
[
   ((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));
];;

(* Lemma card_face_eq_length_find_face *)
let card_face_eq_length_find_face = Sections.section_proof ["d"]
`MEM d (list_of_darts L)
	==> CARD (face (hypermap_of_list L) d) = LENGTH (find_face L d)`
[
   ((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))));
   ((((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));
];;

(* Lemma dart_list_all *)
let dart_list_all = Sections.section_proof ["P"]
`(!d. d IN dart (hypermap_of_list L) ==> P d)
	<=> (!d. MEM d (list_of_darts L) ==> P d)`
[
   (((((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));
];;

(* Lemma dart3_list_all *)
let dart3_list_all = Sections.section_proof ["P"]
`(!d. d IN darts_k 3 (hypermap_of_list L) ==> P d)
	<=> (!d. MEM d (list_of_darts3 L) ==> P d)`
[
   (((((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));
];;

(* Lemma dart4_list_all *)
let dart4_list_all = Sections.section_proof ["P"]
`(!d. d IN darts_k 4 (hypermap_of_list L) ==> P d)
	<=> (!d. MEM d (list_of_darts4 L) ==> P d)`
[
   (((((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));
];;

(* Lemma dart5_list_all *)
let dart5_list_all = Sections.section_proof ["P"]
`(!d. d IN darts_k 5 (hypermap_of_list L) ==> P d)
	<=> (!d. MEM d (list_of_darts5 L) ==> P d)`
[
   (((((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));
];;

(* Lemma dart6_list_all *)
let dart6_list_all = Sections.section_proof ["P"]
`(!d. d IN darts_k 6 (hypermap_of_list L) ==> P d)
	<=> (!d. MEM d (list_of_darts6 L) ==> P d)`
[
   (((((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));
];;

(* Lemma dart_pairs_list_all *)
let dart_pairs_list_all = Sections.section_proof ["P"]
`(!p. p IN dart (hypermap_of_list L) CROSS dart (hypermap_of_list L) ==> P p)
	<=> (!p. MEM p (list_dart_pairs L) ==> P p)`
[
   (((((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));
];;

(* Lemma elements_list_all *)
let elements_list_all = Sections.section_proof ["P"]
`(!x. x IN elements_of_list L ==> P x)
	<=> (!x. MEM x (list_of_elements L) ==> P x)`
[
   (((((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));
];;

(* Lemma sum_node_list_all *)
let sum_node_list_all = Sections.section_proof ["P"]
`good_list_nodes L
	==> ((!n. n IN node_set (hypermap_of_list L) ==> P n (sum n))
		<=> (!n. MEM n (list_of_nodes L) ==> P (set_of_list n) (list_sum n)))`
[
   (((((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 [] []))))));
   ((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 [] [])))))]);
   (((((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));
   (((((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));
];;

(* Lemma sum_face_list_all *)
let sum_face_list_all = Sections.section_proof ["P"]
`(!f. f IN face_set (hypermap_of_list L) ==> P f (sum f))
		<=> (!f. MEM f (list_of_faces L) ==> P (set_of_list f) (list_sum f))`
[
   ((((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 [] [])))));
   ((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 [] [])))))]);
   (((((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));
   (((((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));
];;

(* Finalization of the section ListLemmas *)
let list_of_faces3_subset = Sections.finalize_theorem list_of_faces3_subset;;
let list_of_faces4_subset = Sections.finalize_theorem list_of_faces4_subset;;
let list_of_faces5_subset = Sections.finalize_theorem list_of_faces5_subset;;
let list_of_faces6_subset = Sections.finalize_theorem list_of_faces6_subset;;
let list_of_darts3_subset = Sections.finalize_theorem list_of_darts3_subset;;
let list_of_darts4_subset = Sections.finalize_theorem list_of_darts4_subset;;
let list_of_darts5_subset = Sections.finalize_theorem list_of_darts5_subset;;
let list_of_darts6_subset = Sections.finalize_theorem list_of_darts6_subset;;
let list_of_dart_pairs_subset = Sections.finalize_theorem list_of_dart_pairs_subset;;
let e_list_ext_eq_e_list = Sections.finalize_theorem e_list_ext_eq_e_list;;
let fst_choice_of_list_node = Sections.finalize_theorem fst_choice_of_list_node;;
let card_set_of_list_node = Sections.finalize_theorem card_set_of_list_node;;
let card_set_of_list_face = Sections.finalize_theorem card_set_of_list_face;;
let card_face_eq_length_find_face = Sections.finalize_theorem card_face_eq_length_find_face;;
let dart_list_all = Sections.finalize_theorem dart_list_all;;
let dart3_list_all = Sections.finalize_theorem dart3_list_all;;
let dart4_list_all = Sections.finalize_theorem dart4_list_all;;
let dart5_list_all = Sections.finalize_theorem dart5_list_all;;
let dart6_list_all = Sections.finalize_theorem dart6_list_all;;
let dart_pairs_list_all = Sections.finalize_theorem dart_pairs_list_all;;
let elements_list_all = Sections.finalize_theorem elements_list_all;;
let sum_node_list_all = Sections.finalize_theorem sum_node_list_all;;
let sum_face_list_all = Sections.finalize_theorem sum_face_list_all;;
Sections.end_section "ListLemmas";;

(* Close the module *)
end;;