formal_lp/hypermap/ineqs/lp_ineqs_defs.hl

   1 module Lp_ineqs_def = struct
   2
   3 open Sphere;;
   4 open Fan_defs;;
   5
   6 (* Definitions of all fan variables *)
   7
   8 let azim2_fan = new_definition `azim2_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (f_fan_pair_ext (V,E) x)`;;
   9 let azim3_fan = new_definition `azim3_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
  10
  11 let yn_fan = new_definition `yn_fan (v:real^3) = norm v`;;
  12 let ln_fan = new_definition `ln_fan (v:real^3) = lmfun (yn_fan v / &2)`;;
  13 let rho_fan = new_definition `rho_fan (v:real^3) = abs (&1 + const1 * (&1 - ln_fan v))`;;
  14 let ye_fan = new_definition `ye_fan (x:real^3#real^3) = dist x`;;
  15
  16 let y1_fan = new_definition `y1_fan (x:real^3#real^3) = norm (FST x)`;;
  17 let y2_fan = new_definition `y2_fan (x:real^3#real^3) = norm (SND x)`;;
  18 let y3_fan = new_definition `y3_fan (V,E) (x:real^3#real^3) = norm (FST (inverse (f_fan_pair_ext (V,E)) x))`;;
  19 let y4_fan = new_definition `y4_fan (V,E) (x:real^3#real^3) = dist (f_fan_pair_ext (V,E) x)`;;
  20 let y5_fan = new_definition `y5_fan (V,E) (x:real^3#real^3) = dist (inverse (f_fan_pair_ext (V,E)) x)`;;
  21 let y6_fan = new_definition `y6_fan (x:real^3#real^3) = dist x`;;
  22 let y8_fan = new_definition `y8_fan (V,E) (x:real^3#real^3) = y5_fan (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
  23 let y9_fan = new_definition `y9_fan (V,E) (x:real^3#real^3) = dist (f_fan_pair_ext (V,E) x)`;;
  24
  25 let rhazim_fan = new_definition `rhazim_fan (V,E) (x:real^3#real^3) = abs (&1 + const1 * (&1 - lmfun (h_dart x))) * azim_dart (V,E) x`;;
  26 let rhazim2_fan = new_definition `rhazim2_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (f_fan_pair_ext (V,E) x)`;;
  27 let rhazim3_fan = new_definition `rhazim3_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
  28
  29 (* All variables must be positive without any side conditions *)
  30 let sol_fan = new_definition `sol_fan (V,E) f = abs (sum f (\x. azim_dart (V,E) x - pi) + &2 * pi)`;;
  31 let tau_fan = new_definition `tau_fan (V,E) f = abs (tauVEF (V,E,f))`;;
  32
  33 (* A diagonal *)
  34 let y4'_fan = new_definition `y4'_fan (V,E) (x:real^3#real^3) = dist (SND x, FST (inverse (f_fan_pair_ext (V,E)) x))`;;
  35 let y7_fan = new_definition
  36         `y7_fan (V,E) (x:real^3#real^3) = norm (FST ((inverse (f_fan_pair_ext (V,E)) POWER 2) x))`;;
  37
  38 let fan_defs =
  39 [
  40   azim2_fan; azim3_fan; yn_fan; ln_fan; ye_fan;
  41   rho_fan; sol_fan; tau_fan; rhazim_fan; rhazim2_fan; rhazim3_fan;
  42   y1_fan; y2_fan; y3_fan; y4_fan; y5_fan; y6_fan; y8_fan; y9_fan; y4'_fan;
  43 ]
  44
  45
  46 (* Variables for lists *)
  47 (* g - an isomorphism from hypermap_of_list to hypermap_of_fan *)
  48 (* fan = (V,E) - a fan *)
  49 (* g x = h (FST x), h (SND x) *)
  50
  51 let list_defs = map new_definition
  52   [
  53     `azim_list (g,fan) = (azim_dart fan o g):num#num->real`;
  54     `azim2_list (g,fan) = (azim2_fan fan o g):num#num->real`;
  55     `azim3_list (g,fan) = (azim3_fan fan o g):num#num->real`;
  56     `yn_list h = (yn_fan o h):num->real`;
  57     `ln_list h = (ln_fan o h):num->real`;
  58     `rho_list h = (rho_fan o h):num->real`;
  59     `rhazim_list (g,fan) = (rhazim_fan fan o g):num#num->real`;
  60     `rhazim2_list (g,fan) = (rhazim2_fan fan o g):num#num->real`;
  61     `rhazim3_list (g,fan) = (rhazim3_fan fan o g):num#num->real`;
  62     `(ye_list g):(num#num->real) = ye_fan o g`;
  63     `(sol_list (g,fan)):(num#num->bool)->real = sol_fan fan o IMAGE g`;
  64     `(tau_list (g,fan)):(num#num->bool)->real = tau_fan fan o IMAGE g`;
  65     `(y1_list g):(num#num->real) = y1_fan o g`;
  66     `(y2_list g):(num#num->real) = y2_fan o g`;
  67     `(y3_list (g,fan)):(num#num->real) = y3_fan fan o g`;
  68     `(y4_list (g,fan)):(num#num->real) = y4_fan fan o g`;
  69     `(y5_list (g,fan)):(num#num->real) = y5_fan fan o g`;
  70     `(y6_list g):(num#num->real) = y6_fan o g`;
  71     `(y8_list (g,fan)):(num#num->real) = y8_fan fan o g`;
  72     `(y9_list (g,fan)):(num#num->real) = y9_fan fan o g`;
  73     `(y4'_list (g,fan)):(num#num->real) = y4'_fan fan o g`;
  74   ];;
  75
  76
  77 let list_defs2 = map (REWRITE_RULE[FUN_EQ_THM; o_THM]) list_defs;;
  78
  79 let list_defs_th = end_itlist CONJ list_defs;;
  80
  81 let list_var_rewrites =
  82   map GSYM list_defs @ map GSYM list_defs2;;
  83
  84
  85 (* All variables are nonnegative *)
  86
  87 let AZIM_DART_POS = prove(`&0 <= azim_dart (V,E) x`,
  88    MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
  89      STRIP_TAC THEN
  90      ASM_REWRITE_TAC[azim_dart] THEN
  91      COND_CASES_TAC THENL
  92      [
  93        MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC;
  94        ALL_TAC
  95      ] THEN
  96      REWRITE_TAC[azim_fan] THEN
  97      COND_CASES_TAC THEN REWRITE_TAC[azim] THEN
  98      MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;
  99
 100
 101 let DIST_POS = prove(`!x:(real^3#real^3). &0 <= dist x`,
 102    GEN_TAC THEN MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
 103      STRIP_TAC THEN ASM_REWRITE_TAC[dist; NORM_POS_LE]);;
 104
 105
 106 let list_var_pos = map (fun tm -> prove(tm,
 107                         GEN_TAC THEN REWRITE_TAC list_defs2 THEN
 108                           MP_TAC (ISPEC `fan:(real^3->bool)#((real^3->bool)->bool)` PAIR_SURJECTIVE) THEN
 109                           STRIP_TAC THEN ASM_REWRITE_TAC fan_defs THEN
 110                           TRY (MATCH_MP_TAC REAL_LE_MUL) THEN
 111                           REWRITE_TAC[AZIM_DART_POS; REAL_ABS_POS; NORM_POS_LE; DIST_POS; Fnjlbxs.lmfun_ge0]))
 112 [
 113   `!x. &0 <= azim_list (g,fan) x`;
 114   `!x. &0 <= azim2_list (g,fan) x`;
 115   `!x. &0 <= azim3_list (g,fan) x`;
 116   `!x. &0 <= rhazim_list (g,fan) x`;
 117   `!x. &0 <= rhazim2_list (g,fan) x`;
 118   `!x. &0 <= rhazim3_list (g,fan) x`;
 119   `!v. &0 <= yn_list h v`;
 120   `!v. &0 <= ln_list h v`;
 121   `!v. &0 <= rho_list h v`;
 122   `!f. &0 <= sol_list (g,fan) f`;
 123   `!f. &0 <= tau_list (g,fan) f`;
 124   `!x. &0 <= ye_list g x`;
 125   `!x. &0 <= y1_list g x`;
 126   `!x. &0 <= y2_list g x`;
 127   `!x. &0 <= y3_list (g,fan) x`;
 128   `!x. &0 <= y4_list (g,fan) x`;
 129   `!x. &0 <= y5_list (g,fan) x`;
 130   `!x. &0 <= y6_list g x`;
 131   `!x. &0 <= y8_list (g,fan) x`;
 132   `!x. &0 <= y9_list (g,fan) x`;
 133   `!x. &0 <= y4'_list (g,fan) x`;
 134 ];;
 135
 136
 137 end;;