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;;