1 needs "../formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl";;
3 (* Module Lp_gen_theory*)
4 module Lp_gen_theory = struct
12 open Hypermap_and_fan;;
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)`;;
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)`
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));
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)`
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));
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)`
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));
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`))));;
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`
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));
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`
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));
65 (Sections.add_section_hyp "g_iso" (`hyp_iso g (G,H)`));;
67 (* Lemma components_iso_image *)
68 let components_iso_image = Sections.section_proof ["d"]
70 node H (g d) = IMAGE g (node G d)
71 /\ face H (g d) = IMAGE g (face G d)`
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));
76 (* Lemma components_iso_image_face_map *)
77 let components_iso_image_face_map = Sections.section_proof ["d"]
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))`
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));
87 (* Lemma hyp_iso_comm_special *)
88 let hyp_iso_comm_special = Sections.section_proof ["d"]
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))`
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));
100 (* Lemma hyp_iso_inv_comm *)
101 let hyp_iso_inv_comm = Sections.section_proof ["d"]
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)`
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));
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`
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));
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)`
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));
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)`
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));
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)`
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));
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`
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));
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)`
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));
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)`
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));
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))`
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));
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))`
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));
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)))`
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));
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))`
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));
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))`
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));
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))`
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));
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";;
237 (* Section BijLemmas *)
238 Sections.begin_section "BijLemmas";;
239 (Sections.add_section_var (mk_var ("h", (`:D->C`))));;
241 (* Lemma bij_trans *)
242 let bij_trans = Sections.section_proof ["R";"V"]
244 ==> !P. (!x. x IN V ==> P x) ==> (!x. x IN R ==> P (h x))`
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));
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))`
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));
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";;
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)`
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));
269 (* Section ListLemmas *)
270 Sections.begin_section "ListLemmas";;
271 (Sections.add_section_var (mk_var ("L", (`:((A)list)list`))));;
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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`
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));
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))`
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));
366 (Sections.add_section_hyp "goodL" (`good_list L`));;
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`
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));
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`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
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)`
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));
447 (* Lemma sum_node_list_all *)
448 let sum_node_list_all = Sections.section_proof ["P"]
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)))`
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));
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))`
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));
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";;
496 (* Close the module *)