formal_lp/hypermap/ineqs/lp_gen_ineqs.hl

   1 needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
   2 needs "../formal_lp/hypermap/ineqs/lp_gen_theory-compiled.hl";;
   3
   4 module Lp_gen_ineqs = struct
   5
   6
   7 open Lp_ineqs_def;;
   8 open Hypermap_and_fan;;
   9 open Hypermap_iso;;
  10 open List_hypermap;;
  11 open Lp_gen_theory;;
  12
  13
  14 (* mod-file variables and definitions *)
  15
  16 let var_inst_list =
  17   let sets =
  18     [
  19       "dart", `:real^3#real^3`;
  20       "face", `:real^3#real^3->bool`;
  21       "node", `:real^3`;
  22     ] in
  23   let mk_mod name set = mk_var (name, mk_fun_ty (assoc set sets) `:real`) in
  24     [
  25       `hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
  26       `FST:real^3#real^3->real^3`, `node_mod:real^3#real^3->real^3`;
  27       `azim_dart (V,E)`, mk_mod "azim_mod" "dart";
  28       `azim2_fan (V,E)`, mk_mod "azim2_mod" "dart";
  29       `azim3_fan (V,E)`, mk_mod "azim3_mod" "dart";
  30       `rhazim_fan (V,E)`, mk_mod "rhazim_mod" "dart";
  31       `rhazim2_fan (V,E)`, mk_mod "rhazim2_mod" "dart";
  32       `rhazim3_fan (V,E)`, mk_mod "rhazim3_mod" "dart";
  33       `ln_fan`, mk_mod "ln_mod" "node";
  34       `yn_fan`, mk_mod "yn_mod" "node";
  35       `rho_fan`, mk_mod "rho_mod" "node";
  36       `ye_fan`, mk_mod "ye_mod" "dart";
  37       `y1_fan`, mk_mod "y1_mod" "dart";
  38       `y2_fan`, mk_mod "y2_mod" "dart";
  39       `y3_fan (V,E)`, mk_mod "y3_mod" "dart";
  40       `y4_fan (V,E)`, mk_mod "y4_mod" "dart";
  41       `y5_fan (V,E)`, mk_mod "y5_mod" "dart";
  42       `y6_fan`, mk_mod "y6_mod" "dart";
  43       `y8_fan (V,E)`, mk_mod "y8_mod" "dart";
  44       `y9_fan (V,E)`, mk_mod "y9_mod" "dart";
  45       `y4'_fan (V,E)`, mk_mod "y4'_mod" "dart";
  46       `sol_fan (V,E)`, mk_mod "sol_mod" "face";
  47       `tau_fan (V,E)`, mk_mod "tau_mod" "face";
  48     ];;
  49
  50
  51 (*****************)
  52
  53
  54
  55 (* For a term in the form `!x. x IN set H ==> P x` returns a theorem
  56    hyp_iso g (G,H), !x. x IN set H ==> P x |- !y. y IN set G ==> P (g y) *)
  57 let get_iso_thm =
  58   let iso_list0 =
  59     [
  60       `darts_k 6 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `6`;
  61       `darts_k 5 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `5`;
  62       `darts_k 4 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `4`;
  63       `darts_k 3 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `3`;
  64       `dart (H:(A)hypermap)`, iso_dart_trans;
  65       `face_set (H:(A)hypermap)`, iso_face_trans;
  66       `node_set (H:(A)hypermap)`, iso_node_trans;
  67       `V:C->bool`, bij_trans;
  68     ] in
  69   let cty = `:C` in
  70     fun ineq ->
  71       let x_tm, tm = dest_forall ineq in
  72       let x_ty =
  73         try (fst o dest_fun_ty o type_of) x_tm with Failure _ -> type_of x_tm in
  74       let ty_list = [x_ty, aty; x_ty, cty] in
  75       let iso_list = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) iso_list0 in
  76       let set, p_tm' = dest_binary "==>" tm in
  77       let set_th = assoc (rand set) iso_list in
  78       let p_tm = mk_abs (x_tm, p_tm') in
  79       let p_var = mk_var ("P", type_of (rand set)) in
  80       let th1 = (SPEC_ALL o ONCE_REWRITE_RULE[RIGHT_IMP_FORALL_THM] o REWRITE_RULE[IMP_IMP]) set_th in
  81         BETA_RULE (INST[p_tm, p_var] th1), ty_list;;
  82
  83
  84 (* For an inequality term returns an isomorphism theorem *)
  85 let build_iso_th =
  86   let th_rule th = (UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[RIGHT_IMP_FORALL_THM]) th in
  87   let ths0 = [
  88     th_rule components_iso_image;
  89     th_rule hyp_iso_comm_special;
  90     th_rule hyp_iso_inv_comm;
  91     th_rule card_face_iso;
  92     th_rule card_face_dart_iso;
  93     th_rule sum_node_iso;
  94     th_rule sum_face_iso;
  95   ] in
  96   let sub_ths0 = [
  97     `d IN darts_k 3 (G:(B)hypermap)`, (INST[`3`, `k:num`] o th_rule) darts_k_subset;
  98     `d IN darts_k 4 (G:(B)hypermap)`, (INST[`4`, `k:num`] o th_rule) darts_k_subset;
  99     `d IN darts_k 5 (G:(B)hypermap)`, (INST[`5`, `k:num`] o th_rule) darts_k_subset;
 100     `d IN darts_k 6 (G:(B)hypermap)`, (INST[`6`, `k:num`] o th_rule) darts_k_subset;
 101   ] in
 102
 103     fun ineq ->
 104       let iso_trans_th, ty_list = get_iso_thm ineq in
 105       let th0 = UNDISCH_ALL (PURE_REWRITE_RULE[GSYM IMP_IMP] iso_trans_th) in
 106       let gen_var, rtm = dest_forall(concl th0) in
 107       let ths = map (INST_TYPE ty_list) ths0 and
 108           sub_ths = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) sub_ths0 in
 109       let ants = lhand rtm in
 110       let th1 = UNDISCH (SPEC_ALL th0) in
 111         (* General isomorphism rewrites *)
 112       let th2 = PURE_REWRITE_RULE ths th1 in
 113       let th3 =
 114         try
 115           let sub_th = assoc ants sub_ths in
 116             PROVE_HYP sub_th th2
 117         with Failure _ -> th2 in
 118         GEN gen_var (DISCH ants th3);;
 119
 120
 121 let build_list_th =
 122   let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o
 123                    SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in
 124   (* |- !d. d IN set_of_list s ==> P d <=> !d. MEM d s ==> P d *)
 125   let ths_all = map th_rule
 126     [
 127       sum_node_list_all;
 128       sum_face_list_all;
 129       dart_list_all;
 130       dart3_list_all;
 131       dart4_list_all;
 132       dart5_list_all;
 133       dart6_list_all;
 134       elements_list_all;
 135     ] in
 136
 137   let ths_more =
 138   [
 139     th_rule card_face_eq_length_find_face;
 140     th_rule card_set_of_list_face;
 141     th_rule card_set_of_list_node;
 142     th_rule fst_choice_of_list_node;
 143     UNDISCH_ALL (ISPEC `L:((num)list)list` components_hypermap_of_list);
 144     th_rule e_list_ext_eq_e_list;
 145     th_rule fst_iso_trans;
 146   ] in
 147
 148   let ths_mem =
 149     [
 150       `MEM (d:num#num) (list_of_darts3 L)`, th_rule list_of_darts3_subset;
 151       `MEM (d:num#num) (list_of_darts4 L)`, th_rule list_of_darts4_subset;
 152       `MEM (d:num#num) (list_of_darts5 L)`, th_rule list_of_darts5_subset;
 153       `MEM (d:num#num) (list_of_darts6 L)`, th_rule list_of_darts6_subset;
 154     ] in
 155
 156     fun iso_th ->
 157       (* G -> hypermap_of_list (L:((num)list)list) *)
 158       let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty; `:real^3`, `:C`; `:num`, `:D`] iso_th in
 159       let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`; `elements_of_list L:num->bool`, `R:num->bool`] s1 in
 160         (* Convert conditions in the form !d. d IN set_of_list s to !d. MEM d s *)
 161       let s3 = PURE_REWRITE_RULE ths_all s2 in
 162       let gen_var2, rtm = dest_forall (concl s3) in
 163       let ants2 = lhand rtm in
 164       let s4 = UNDISCH (SPEC_ALL s3) in
 165         (* Instantiate all variables *)
 166       let s5 = INST var_inst_list s4 in
 167         (* Additional rewrites *)
 168       let s6 = PURE_REWRITE_RULE ths_more s5 in
 169       let s7 =
 170         try
 171           let mem_th = assoc ants2 ths_mem in
 172             PROVE_HYP mem_th s6
 173         with Failure _ -> s6 in
 174       let s8 = GEN gen_var2 (DISCH ants2 s7) in
 175       let s9 = PURE_REWRITE_RULE list_var_rewrites s8 in
 176       let s10 = PURE_REWRITE_RULE[ALL_MEM] s9 in
 177         (* Rewrite the main inequality hypothesis with the COMPONENTS_HYPERMAP_OF_FAN theorem *)
 178       let gen_hyp = find is_forall (hyp s10) in
 179       let eq_th = REWRITE_CONV[UNDISCH_ALL (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] COMPONENTS_HYPERMAP_OF_FAN)] gen_hyp in
 180       let imp_th = if (rand (concl eq_th) = `T`) then EQT_ELIM eq_th else UNDISCH (MATCH_MP EQ_IMP (SYM eq_th)) in
 181         PROVE_HYP imp_th s10;;
 182
 183
 184 let generate_ineq ineq_tm =
 185   let th1 = build_iso_th ineq_tm in
 186     build_list_th th1;;
 187
 188
 189
 190 end;;
 191
 192
 193 (*
 194 open Lp_gen_ineqs;;
 195
 196 let test_ineq1 = `!d. d IN dart (H:(A)hypermap) ==> rhazim3_mod d <= pi + sol0`;;
 197 let test_ineq2 = `!f. f IN face_set (H:(A)hypermap) ==> sol_mod f <= &4 * pi`;;
 198 let test_ineq3 = `!f. f IN face_set (H:(A)hypermap) ==> (CARD f = 5 ==>
 199     sum f azim_mod = sol_mod f + &3 * pi)`;;
 200 let test_ineq4 = `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;;
 201 let test_ineq5 = `!x. x IN (V:C->bool) ==> ln_mod x = (#2.52 - yn_mod x) / #0.52`;;
 202 let edge_sym = `!d. d IN dart (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
 203 let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node_mod d:C):real`;;
 204 let y2_def = `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node_mod (face_map H d):C):real`;;
 205 let y8_def = `!d. d IN dart (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;;
 206 let rhazim_sum = `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod (node_mod (CHOICE n):C)`;;
 207 let test_ineq6 = `!d. d IN darts_k 4 (H:(A)hypermap) ==>
 208         (((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;;
 209 let test_ineq7 = `!d. d IN dart (H:(A)hypermap) ==> CARD (face H d) = 3 ==> y4_mod d = y8_mod d:real`;;
 210 let test_ineq8 = `!d. d IN dart (H:(A)hypermap) ==> &2 <= y4'_mod d`;;
 211 let test_ineq9 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;;
 212 let test_ineq10 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
 213 let test_ineq11 = `!d. d IN darts_k 5 (H:(A)hypermap) ==> tau_mod (face H d) >= #0.4819`;;
 214 let test_ineq12 = `!d. d IN dart (H:(A)hypermap) ==> 3 < CARD (face H d) ==> #2.52 <= y4_mod d`;;
 215
 216 generate_ineq test_ineq1;;
 217 generate_ineq test_ineq2;;
 218 generate_ineq test_ineq3;;
 219 generate_ineq test_ineq4;;
 220 generate_ineq test_ineq5;;
 221 generate_ineq test_ineq6;;
 222 generate_ineq test_ineq7;;
 223 generate_ineq test_ineq8;;
 224 generate_ineq test_ineq9;;
 225 generate_ineq test_ineq10;;
 226 generate_ineq test_ineq11;;
 227 generate_ineq test_ineq12;;
 228
 229 generate_ineq edge_sym;;
 230 generate_ineq y1_def;;
 231 generate_ineq y2_def;;
 232 generate_ineq y8_def;;
 233 generate_ineq rhazim_sum;;
 234 *)
 235