needs "list_hypermap_iso.hl";;

(* Basic variables *)


let inv_iso = new_definition `inv_iso (V,E) f = res_inverse f (dart_of_fan (V,E))`;;

let INV_ISO = 
prove(`!V E L f. FAN (vec 0,V,E) /\ good_list L /\
		      isomorphism f (hypermap_of_fan (V,E), hypermap_of_list L)
		    ==> isomorphism (inv_iso (V,E) f) (hypermap_of_list L, hypermap_of_fan (V,E)) /\
		        (!d. d IN dart_of_fan (V,E) ==> inv_iso (V,E) f (f d) = d) /\
			(!d. d IN darts_of_list L ==> f (inv_iso (V,E) f d) = d) /\
			(!d:A#A. d IN darts_of_list L ==> inv_iso (V,E) f d IN dart_of_fan (V,E))`,

   REPEAT GEN_TAC THEN STRIP_TAC THEN
     SUBGOAL_THEN `isomorphism (inv_iso (V,E) f) (hypermap_of_list (L:((A)list)list), hypermap_of_fan (V,E))` ASSUME_TAC THENL
     [
       REWRITE_TAC[inv_iso] THEN
	 ASM_SIMP_TAC[GSYM COMPONENTS_HYPERMAP_OF_FAN] THEN
	 MATCH_MP_TAC ISOMORPHISM_INVERSE THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[inv_iso] THEN
     MATCH_MP_TAC BIJ_IMP_RES_INVERSE THEN
     REMOVE_ASSUM THEN
     POP_ASSUM MP_TAC THEN
     ASM_SIMP_TAC[isomorphism; COMPONENTS_HYPERMAP_OF_FAN; COMPONENTS_HYPERMAP_OF_LIST]);;
     



(* azim *)
let azim_list = new_definition `azim_list (V,E,g) = azim_dart (V,E) o g`;;

let SUM_ISOMORPHISM = 
prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
			    ==> (!d. d IN dart G ==> sum(node G d) (r o g) = sum(node H (g d)) r)`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `sum(node G d) (r o (g:B->A)) = sum(IMAGE g (node G d)) r` (fun th -> REWRITE_TAC[th]) THENL
     [
       MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
	 REPEAT STRIP_TAC THEN
	 UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
	 REWRITE_TAC[isomorphism; BIJ; INJ] THEN
	 DISCH_THEN (MP_TAC o CONJUNCT1) THEN
	 DISCH_THEN (MP_TAC o CONJUNCT1) THEN
	 DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
	 ASM_REWRITE_TAC[] THEN
	 CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `node G (d:B)` THEN ASM_SIMP_TAC[Hypermap.lemma_node_subset];
       ALL_TAC
     ] THEN
     MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]));;




search [`sum`; `azim_dart`];;


let yn = `yn_list (V,E,f) = norm o FST o inv_iso (V,E) f`;;

let y1_list = new_definition `y1_list (V,E,f) = norm o FST o inv_iso (V,E) f`;;
let y2 = new_definition `y2_list (V,E,f) = norm o SND o inv_iso (V,E) f`;;
let y3 = new_definition `y3_list (V,E,f) = norm o SND o n_fan_pair_ext (V,E) o inv_iso (V,E) f`;;
let y4 = new_definition `y4_list (V,E,f) = `;;
let y5 = v13;;
let y6 = v23;;



let DART_EXISTS_EQ = 
prove(`!V E v. FAN (vec 0,V,E) ==> 
			     (v IN V <=> (?w. v,w IN dart_of_fan (V,E)))`,

   REPEAT STRIP_TAC THEN EQ_TAC THENL
     [
       REWRITE_TAC[DART_EXISTS];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3,w:real^3`] IN_DART_OF_FAN) THEN
     ASM_REWRITE_TAC[PAIR_EQ] THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[]);;




prove(`!V f (L:((A)list)list). contravening V /\ good_list L /\ 
	isomorphism f (hypermap_of_fan (V,ESTD V), hypermap_of_list L)
	==> (!d. d IN darts_of_list L ==> 
	     #2.0 <= y1_list (V,ESTD V,f) d /\ y1_list (V,ESTD V,f) d <= #2.52)`,
   REWRITE_TAC[y1_list; o_THM] THEN
     REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
     MP_TAC (SPEC_ALL Tame_general.CONTRAVENING_FAN) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     SUBGOAL_THEN `FST (inv_iso (V,ESTD V) f (d:A#A)) IN V` ASSUME_TAC THENL
     [
       MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `FST (inv_iso (V,ESTD V) f (d:A#A))`] DART_EXISTS_EQ) THEN
	 ASM_REWRITE_TAC[] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 EXISTS_TAC `SND (inv_iso (V,ESTD V) f (d:A#A))` THEN
	 REWRITE_TAC[PAIR] THEN
	 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `L:((A)list)list`; `f:real^3#real^3->A#A`] INV_ISO) THEN
	 ASM_SIMP_TAC[INV_ISO];
       ALL_TAC
     ] THEN
     REWRITE_TAC[GSYM DIST_0] THEN
     ABBREV_TAC `v = FST (inv_iso (V,ESTD V) f (d:A#A))` THEN
     MP_TAC (SPEC_ALL Tame_general.CONTRAVENING_DIST) THEN
     ASM_SIMP_TAC[]);;