formal_lp/old/ineqs/list_hypermap_vars.hl

   1 needs "list_hypermap_iso.hl";;
   2
   3 (* Basic variables *)
   4
   5
   6 let inv_iso = new_definition `inv_iso (V,E) f = res_inverse f (dart_of_fan (V,E))`;;
   7
   8
   9 let INV_ISO = prove(`!V E L f. FAN (vec 0,V,E) /\ good_list L /\
  10                       isomorphism f (hypermap_of_fan (V,E), hypermap_of_list L)
  11                     ==> isomorphism (inv_iso (V,E) f) (hypermap_of_list L, hypermap_of_fan (V,E)) /\
  12                         (!d. d IN dart_of_fan (V,E) ==> inv_iso (V,E) f (f d) = d) /\
  13                         (!d. d IN darts_of_list L ==> f (inv_iso (V,E) f d) = d) /\
  14                         (!d:A#A. d IN darts_of_list L ==> inv_iso (V,E) f d IN dart_of_fan (V,E))`,
  15    REPEAT GEN_TAC THEN STRIP_TAC THEN
  16      SUBGOAL_THEN `isomorphism (inv_iso (V,E) f) (hypermap_of_list (L:((A)list)list), hypermap_of_fan (V,E))` ASSUME_TAC THENL
  17      [
  18        REWRITE_TAC[inv_iso] THEN
  19          ASM_SIMP_TAC[GSYM COMPONENTS_HYPERMAP_OF_FAN] THEN
  20          MATCH_MP_TAC ISOMORPHISM_INVERSE THEN
  21          ASM_REWRITE_TAC[];
  22        ALL_TAC
  23      ] THEN
  24      ASM_REWRITE_TAC[inv_iso] THEN
  25      MATCH_MP_TAC BIJ_IMP_RES_INVERSE THEN
  26      REMOVE_ASSUM THEN
  27      POP_ASSUM MP_TAC THEN
  28      ASM_SIMP_TAC[isomorphism; COMPONENTS_HYPERMAP_OF_FAN; COMPONENTS_HYPERMAP_OF_LIST]);;
  29
  30
  31
  32
  33 (* azim *)
  34 let azim_list = new_definition `azim_list (V,E,g) = azim_dart (V,E) o g`;;
  35
  36
  37 let SUM_ISOMORPHISM = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
  38                             ==> (!d. d IN dart G ==> sum(node G d) (r o g) = sum(node H (g d)) r)`,
  39    REPEAT STRIP_TAC THEN
  40      SUBGOAL_THEN `sum(node G d) (r o (g:B->A)) = sum(IMAGE g (node G d)) r` (fun th -> REWRITE_TAC[th]) THENL
  41      [
  42        MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
  43          REPEAT STRIP_TAC THEN
  44          UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
  45          REWRITE_TAC[isomorphism; BIJ; INJ] THEN
  46          DISCH_THEN (MP_TAC o CONJUNCT1) THEN
  47          DISCH_THEN (MP_TAC o CONJUNCT1) THEN
  48          DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
  49          ASM_REWRITE_TAC[] THEN
  50          CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `node G (d:B)` THEN ASM_SIMP_TAC[Hypermap.lemma_node_subset];
  51        ALL_TAC
  52      ] THEN
  53      MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
  54      ASM_REWRITE_TAC[] THEN
  55      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]));;
  56
  57
  58
  59
  60
  61 search [`sum`; `azim_dart`];;
  62
  63
  64 let yn = `yn_list (V,E,f) = norm o FST o inv_iso (V,E) f`;;
  65
  66 let y1_list = new_definition `y1_list (V,E,f) = norm o FST o inv_iso (V,E) f`;;
  67 let y2 = new_definition `y2_list (V,E,f) = norm o SND o inv_iso (V,E) f`;;
  68 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`;;
  69 let y4 = new_definition `y4_list (V,E,f) = `;;
  70 let y5 = v13;;
  71 let y6 = v23;;
  72
  73
  74
  75 let DART_EXISTS_EQ = prove(`!V E v. FAN (vec 0,V,E) ==>
  76                              (v IN V <=> (?w. v,w IN dart_of_fan (V,E)))`,
  77    REPEAT STRIP_TAC THEN EQ_TAC THENL
  78      [
  79        REWRITE_TAC[DART_EXISTS];
  80        ALL_TAC
  81      ] THEN
  82      STRIP_TAC THEN
  83      MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3,w:real^3`] IN_DART_OF_FAN) THEN
  84      ASM_REWRITE_TAC[PAIR_EQ] THEN
  85      STRIP_TAC THEN
  86      ASM_REWRITE_TAC[]);;
  87
  88
  89
  90
  91
  92 prove(`!V f (L:((A)list)list). contravening V /\ good_list L /\
  93         isomorphism f (hypermap_of_fan (V,ESTD V), hypermap_of_list L)
  94         ==> (!d. d IN darts_of_list L ==>
  95              #2.0 <= y1_list (V,ESTD V,f) d /\ y1_list (V,ESTD V,f) d <= #2.52)`,
  96    REWRITE_TAC[y1_list; o_THM] THEN
  97      REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
  98      MP_TAC (SPEC_ALL Tame_general.CONTRAVENING_FAN) THEN
  99      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 100      SUBGOAL_THEN `FST (inv_iso (V,ESTD V) f (d:A#A)) IN V` ASSUME_TAC THENL
 101      [
 102        MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `FST (inv_iso (V,ESTD V) f (d:A#A))`] DART_EXISTS_EQ) THEN
 103          ASM_REWRITE_TAC[] THEN
 104          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 105          EXISTS_TAC `SND (inv_iso (V,ESTD V) f (d:A#A))` THEN
 106          REWRITE_TAC[PAIR] THEN
 107          MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `L:((A)list)list`; `f:real^3#real^3->A#A`] INV_ISO) THEN
 108          ASM_SIMP_TAC[INV_ISO];
 109        ALL_TAC
 110      ] THEN
 111      REWRITE_TAC[GSYM DIST_0] THEN
 112      ABBREV_TAC `v = FST (inv_iso (V,ESTD V) f (d:A#A))` THEN
 113      MP_TAC (SPEC_ALL Tame_general.CONTRAVENING_DIST) THEN
 114      ASM_SIMP_TAC[]);;
 115
 116