text_formalization/usr/thales/init_search.hl

   1 (* initialization of search structures *)
   2
   3 (* module Init = struct *)
   4
   5
   6 flyspeck_needs "usr/thales/searching.hl";;
   7
   8 module Init_search = struct
   9
  10   open Hales_tactic;;
  11   open Searching;;
  12
  13 (* ========================================================================== *)
  14 (* REWRITE SUGGEST *)
  15
  16 update_database();;
  17
  18 (*
  19 let search_result_dump_march7_2012_8am =
  20   ["Trigonometry2.COLLINEAR_TRANSABLE"; "Trigonometry2.COLLINEAR_TRANSABLE";
  21    "Trigonometry2.COLLINEAR_TRANSABLE"; "Trigonometry2.COLLINEAR_TRANSABLE";
  22    "COLLINEAR_LEMMA_ALT"; "WEDGE_LUNE_GT"; "COLLINEAR_3_AFFINE_HULL";
  23    "Sphere.aff"; "AFFINE_HULL_2_ALT";
  24    "Marchal_cells_2.RADIAL_VS_RADIAL_NORM"; "Conforming.SOL_UNIONS";
  25    "Vol1.sol"; "AFF_DIM_CONVEX_HULL"; "Hypermap.lemma_in_disjoint";
  26    "FACE_OF_DISJOINT_INTERIOR"; "real_div"; "SUM_RMUL"; "VECTOR_MUL_RZERO";
  27    "SUM_CLAUSES"; "Packing3.SING_UNION_EQ_INSERT"; "VSUM_LMUL";
  28    "Collect_geom.IN_AFFINE_HULL_IMP_COLLINEAR"; "AFF_DIM_2";
  29    "AFF_DIM_INSERT"; "AFF_DIM_SUBSET"; "Polyhedron.AFF_DIM_INTERIOR_EQ_3";
  30    "AFF_DIM_EQ_AFFINE_HULL"; "CONVEX_HULL_EQ";
  31    "Marchal_cells.CONVEX_HULL_SUBSET";
  32    "Upfzbzm_support_lemmas.SUM_SET_OF_2_ELEMENTS"; "SUM_SUBSET_SIMPLE";
  33    "HAS_SIZE_1_EXISTS"; "HAS_SIZE_0"; "SUM_UNION"; "SUM_POS_LE"; "sgn_gt";
  34    "FACE_OF_IMP_CONVEX"; "POLYTOPE_UNION_CONVEX_HULL_FACETS";
  35    "SUBSET_RELATIVE_INTERIOR";
  36    "EXPLICIT_SUBSET_RELATIVE_INTERIOR_CONVEX_HULL"; "Geomdetail.SUM_DIS3";
  37    "face_of"; "FACE_OF_CONVEX_HULL_SUBSET"; "Geomdetail.VSUM_DIS3";
  38    "Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL";
  39    "Marchal_cells_2.VSUM_CLAUSES_alt"; "NOT_IN_EMPTY"; "UNION_EMPTY";
  40    "aff_gt_def"; "CONVEX_AFF_GT"; "affsign"; "Sphere.aff_gt_def";
  41    "AZIM_REFL"; "AZIM_BASE_SHIFT_LT"; "Counting_spheres.EMPTY_NOT_EXISTS_IN";
  42    "wedge"; "NORM_NEG"; "dist"; "IN_BALL"; "VECTOR_MUL_ASSOC";
  43    "Polyhedron.fchanged"; "NORMBALL_BALL"; "Sphere.radial";
  44    "Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON";
  45    "Polyhedron.POLYTOPE_FAN80"; "Conforming.PIIJBJK";
  46    "Polyhedron.POLYHEDRON_FAN";
  47    "Conforming.MEASURABLE_TOPOLOGICAL_COMPONENT_YFAN_INTER_BALL";
  48    "Polyhedron.FCHANGED_IN_COMPONENT"; "primitive"; "MEASURABLE_RULES";
  49    "Sphere.cone0"; "solid_triangle"; "Vol1.volume_prop_fix";
  50    "Sphere.eventually_radial"; "MEASURABLE_BALL_WEDGE"; "MEASURE_SUBSET";
  51    "NORM_EQ_0"; "DOT_EQ_0"; "NORM_POS_LE"; "Real_ext.REAL_PROP_NN_MUL2";
  52    "Calc_derivative.invert_den_le"; "DOT_SYM"; "Collect_geom.EQ_POW2_COND";
  53    "Trigonometry2.DIV_POW2"; "DOT_LZERO"; "Calc_derivative.invert_den_eq";
  54    "VECTOR_MUL_EQ_0"; "REAL_EQ_MUL_LCANCEL"; "NORM_POS_LT"; "SQRT_POS_LT";
  55    "ABS_SQUARE_LT_1"; "Calc_derivative.invert_den_lt"; "REAL_LT_MUL";
  56    "Trigonometry1.DOT_COS"; "Trigonometry2.NOT_ZERO_EQ_POW2_LT";
  57    "REAL_LT_MUL"; "REAL_LT_RMUL"; "Trigonometry2.UNIT_BOUNDED_IN_TOW_FORMS";
  58    "SQRT_POW_2"; "NORM_EQ_0"; "Collect_geom.DIST_POW2_DOT";
  59    "Tarjjuw.CHANGE_TARJJUW_4"; "NORM_POS_LE"; "Real_ext.REAL_PROP_NN_MUL2";
  60    "NORM_POW_2"; "DOT_SQUARE_NORM"; "Trigonometry2.MUL_POW2";
  61    "Tactics_jordan.REAL_POW_2_LT"; "DOT_SYM";
  62    "Polyhedron.INTERIOR_AFFINIE_HUL_EQ_UNIV";
  63    "Counting_spheres.affine_facet_hyper"; "RELATIVE_INTERIOR_SUBSET";
  64    "INTERIOR_SUBSET_RELATIVE_INTERIOR"; "facet_of"; "POLYHEDRON_IMP_CONVEX";
  65    "Ldurdpn.SUBSET_P_HULL"; "HULL_HULL"; "HULL_MONO"; "VECTOR_MUL_LID";
  66    "Marchal_cells_2.AFFINE_SUBSET_KY_LEMMA"; "RELATIVE_INTERIOR_SUBSET";
  67    "FACE_OF_STILLCONVEX"; "FACE_OF_DISJOINT_RELATIVE_INTERIOR";
  68    "REAL_LT_MUL"; "REAL_LT_LMUL"; "REAL_LT_DIV";
  69    "Local_lemmas.REAL_LT_DIV_NEG"; "Trigonometry2.LT_IMP_ABS_REFL";
  70    "NORM_POW_2"; "NORM_MUL"; "DOT_LMUL"; "DIST_0"; "VECTOR_SUB_RZERO";
  71    "rconesgn"; "rcone_gt"; "Polyhedron.REDUCE_POINT_FACET_EXISTS";
  72    "POLYHEDRON_COLLINEAR_FACES"; "DOT_POS_LT"; "DOT_RZERO"; "facet_of";
  73    "DOT_LMUL"; "Trigonometry2.EXISTS_OTHOR_VECTOR_DIFFF_VEC0";
  74    "Trigonometry2.EXISTS_UNIT_OTHOR_VECTOR"; "INJECTIVE_PAD2D3D";
  75    "COMPLEX_VEC_0"; "COMPLEX_VEC_0"; "Counting_spheres.facet_rep_def";
  76    "CX_INJ"; "COMPLEX_NORM_CX"; "POLYTOPE_EQ_BOUNDED_POLYHEDRON";
  77    "POLYTOPE_IMP_CONVEX"; "POLYTOPE_IMP_COMPACT";
  78    "EXTREME_POINT_EXISTS_CONVEX"; "FACE_OF_SING";
  79    "FACE_OF_POLYHEDRON_SUBSET_FACET"; "POLYTOPE_FACET_EXISTS"];;
  80
  81 let remove_work_in_progress =
  82   Lib.subtract search_result_dump_march7_2012_8am ["AZIM_BASE_SHIFT_LT"];;
  83
  84 map refresh_rewrite_stag remove_work_in_progress;;
  85
  86 (* augment_search_results search_result_dump_march7_2012_8am;; *)
  87
  88 remove_rewrite_tag "POLYHEDRON_COLLINEAR_FACES";;
  89
  90
  91
  92 map refresh_rewrite_stag
  93   ["SQRT_POS_LE";"SUBSET_INTER";"VECTOR_MUL_RZERO";"VECTOR_ADD_RID";
  94    "VECTOR_SUB_RZERO";"VECTOR_ADD_LID";"VECTOR_SUB_LZERO";"IN_UNIV";
  95    "Local_lemmas.EXISTS_IN";"Collect_geom.IN_SET2";"DOT_RMUL";"DOT_LMUL";
  96    "FORALL_PAIR_THM";"EXISTS_PAIRED_THM";"Hales_tactic.GSYM_EXISTS_PAIRED_THM";
  97   "IN_SING"];;
  98 *)
  99
 100
 101 (* ========================================================================== *)
 102 (* tactic patterns *)
 103
 104 map add_tactic_pattern
 105  [(match_g[`(@):(A->bool)->A`],"SELECT_ELIM_TAC","remove @",
 106    fun t-> SELECT_ELIM_TAC);
 107 (match_g[`(@):(A->bool)->A`],"SELECT_TAC","remove @ with subgoals",
 108  fun t-> SELECT_TAC);
 109 (match_g[full `(\x. f x = \x. g x)`],"ABS_TAC","strip abstractions from equality",
 110  fun t-> ABS_TAC);
 111 (match_g[full ` ((p ==> q) ==> r)`],"ANTS_TAC","ants",
 112  fun t-> ANTS_TAC);
 113 (match_g_no_ho[full ` (f x = g x)`],"AP_THM_TAC","drop the function argument",
 114  fun t-> AP_THM_TAC);
 115 (match_g_no_ho[full ` (f x y = f x' y)`],"AP_THM_TAC THEN AP_TERM_TAC","show first args of a binary function are equal",
 116  fun t-> AP_THM_TAC THEN AP_TERM_TAC);
 117 (match_g[`(\x. f) y`],"BETA_TAC","beta reduce",
 118  fun t-> BETA_TAC);
 119 (match_g[full ` (f x y = f x' y')`],"BINOP_TAC","show binary function args equal",
 120  fun t-> BINOP_TAC);
 121 (match_g[full ` (f x  = f x' )`],"AP_TERM_TAC","show function args equal",
 122  fun t-> AP_TERM_TAC);
 123 (match_g[full `(a /\ b)`],"CONJ_TAC","split into two subgoals",
 124  fun t-> CONJ_TAC);
 125 (match_g[full `(a ==>b)`],"DISCH_TAC","discharge antecedent",
 126  fun t -> DISCH_TAC);
 127 (match_g[full `(a <=> b)`],"EQ_TAC","split <=> into two conditionals",
 128  fun t -> EQ_TAC);
 129 (match_g[full `(?x. t)`],"EXISTS_TAC","specify existence",
 130  fun t -> failwith "syntax: EXISTS_TAC `u`");
 131 (match_g[full `(!x. t)`],"GEN_TAC","remove universal",
 132  fun t-> GEN_TAC);
 133 (match_g[full `((f:A->B) = g)`],"MATCH_MP_TAC EQ_EXT","apply to arg",
 134  fun t-> MATCH_MP_TAC EQ_EXT);
 135 (* was ONCE_REWRITE_TAC[FUN_EQ_THM] *)
 136 (match_g[full `(!(x:num). t)`],"INDUCT_TAC","induction",
 137  fun t->INDUCT_TAC);
 138 (match_g[full `(!(n:A list). P)`],"LIST_INDUCT_TAC","structure induction on lists",
 139  fun t->LIST_INDUCT_TAC);
 140 (match_g[full `(f x = g y)`],"MK_COMB_TAC","show equality of functions and args",
 141  fun t->MK_COMB_TAC);
 142 (match_g[full`x <= (z:real)`],"MATCH_MP_TAC REAL_LE_TRANS","x <= y /\ y <= z ",
 143  fun t -> MATCH_MP_TAC REAL_LE_TRANS);
 144 (match_g[full`x < (z:real)`],"MATCH_MP_TAC REAL_LET_TRANS","x <= y /\ y < z ",
 145  fun t -> MATCH_MP_TAC REAL_LET_TRANS);
 146 (match_g[full`x < (z:real)`],"MATCH_MP_TAC REAL_LTE_TRANS","x < y /\ y <= z",
 147  fun t -> MATCH_MP_TAC REAL_LTE_TRANS);
 148 (match_asm[ full `x \/ y`],"FIRST_X_ASSUM DISJ_CASES_TAC","split x \/ y assumption",
 149  fun t -> FIRST_X_ASSUM DISJ_CASES_TAC);
 150 (match_asm[full `?(x:A). y`],"FIRST_X_ASSUM CHOOSE_TAC","choose existential quant in assumption list",
 151  fun t-> FIRST_X_ASSUM CHOOSE_TAC);
 152 (match_asm[full `x /\ y`],"FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC)","split asumption conjunction",
 153  fun t->FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC));
 154 ];;
 155
 156 add_tactic_pattern (match_g[`let x = (y:A) in (z:B)`],"LET_TAC","let elimination",
 157                     fun t -> LET_TAC);;
 158
 159 add_tactic_pattern (match_g[full `(a:A->bool) = b`],"MATCH_MP_TAC SUBSET_ANTISYM",
 160                     "subset conjunction",
 161                     fun t -> MATCH_MP_TAC SUBSET_ANTISYM);;
 162
 163
 164 (* ========================================================================== *)
 165 (*
 166 ABBREVIATIONS OF TACTICS
 167 *)
 168
 169 tactic_abbreviations:= [
 170   ("fun","fun");
 171   ("then","THEN");
 172   ("real","REAL_ARITH_TAC");
 173   ("se","SELECT_TAC");
 174   ("if","COND_CASES_TAC");
 175   ("cc","COND_CASES_TAC");
 176   ("r","REWRITE_TAC");
 177   ("mp","MP_TAC");
 178 ("ra","REAL_ARITH");
 179 ("aru","ARITH_RULE");
 180 ("field","REAL_FIELD");
 181 ("fieldt","(CONV_TAC REAL_FIELD)");
 182 ("ar","ASM_REWRITE_TAC");
 183 ("hc","HYP_CONJ_TAC");
 184 ("rt/a","ASM_REWRITE_TAC");
 185 ("r/a","ASM_REWRITE_TAC");
 186 ("r/o","ONCE_REWRITE_TAC");
 187 ("rt/o","ONCE_REWRITE_TAC");
 188 ("mmp","MATCH_MP_TAC");
 189 ("st","WEAKER_STRIP_TAC");
 190 ("st/r","REPEAT WEAKER_STRIP_TAC");
 191 ("str","STRIP_TAC");
 192 ("str/r","REPEAT STRIP_TAC");
 193 ("e","EXISTS_TAC");
 194 ("m","MESON_TAC");
 195 ("mt/a","ASM_MESON_TAC");
 196 ("m/a","ASM_MESON_TAC");
 197 ("am","ASM_MESON_TAC");
 198 ("c","CONJ_TAC");
 199 ("a","ASSUME_TAC");
 200 ("g","GEN_TAC");
 201 ("g/r","REPEAT GEN_TAC");
 202 ("sc","SUBCONJ_TAC");
 203 ("su","SUBST1_TAC");
 204 ("si","SIMP_TAC");
 205 ("si/a","ASM_SIMP_TAC");
 206 ("asi","ASM_SIMP_TAC");
 207 ("sg","SUBGOAL_THEN");
 208 ("d","DISCH_TAC");
 209 ("an","ANTS_TAC");
 210 ("le","LET_TAC");
 211 ("l","LET_TAC");
 212 ("rat","REAL_ARITH_TAC");
 213 ("p","POP_ASSUM");
 214 ("p/r","REPEAT POP_ASSUM");
 215 ("by","BY");
 216 ("exv","EXISTSv_TAC");
 217 ("mu", "MESON");
 218 ("gv","X_GENv_TAC");
 219 ("sym","GSYM");
 220 ("specl","ISPECL");
 221 ("spec","ISPEC");
 222 ("o","o");
 223 ("rr","REWRITE_RULE");
 224 ("orr","ONCE_REWRITE_RULE");
 225 ("pbc","PROOF_BY_CONTR_TAC");
 226 ("taut","TAUT");
 227 ("snd","snd");
 228 ("asl","asl");
 229 ("let","let");
 230 ("in","in");
 231 ("@","SELECT_TAC");
 232 ("/\\","CONJ_TAC");
 233 ("!","GEN_TAC");
 234 ];;
 235
 236 abbrev ("fexp","FULL_EXPAND_TAC");;
 237 abbrev ("ispecl","ISPECL");;
 238 abbrev ("ispec","ISPEC");;
 239 abbrev ("t","t");;
 240 abbrev ("beta","BETA_TAC");;
 241 abbrev ("subconj","SUBCONJ_TAC");;
 242 abbrev ("fassum","FIRST_ASSUM");;
 243 abbrev ("fa","FIRST_ASSUM");;
 244 abbrev ("d/r","REPEAT DISCH_TAC");;
 245 abbrev ("comment","COMMENT");;
 246 abbrev ("name","NAME");;
 247 abbrev ("rot","ROT_TAC");;
 248 unabbrev ("rau");;
 249 abbrev ("arith","arith");;
 250 abbrev ("aa","ARITH_TAC");;
 251 abbrev ("rep","REPLICATE_TAC");;
 252 abbrev ("simp","SIMP_TAC");;
 253 abbrev ("contr","PROOF_BY_CONTR_TAC");;
 254 abbrev ("set","SET_TAC");;
 255 (* abbrev ("sth","SEARCH_THEN");;*)
 256 abbrev ("ets","ENOUGH_TO_SHOW_TAC");;
 257 abbrev ("mm","MATCH_MP");;
 258 abbrev ("calc","Calc_derivative.CALC_ID_TAC");;
 259 abbrev ("gm","GMATCH_SIMP_TAC");;
 260 abbrev ("w","w");;
 261 abbrev ("asl","asl");;
 262 abbrev ("replicate","replicate");;
 263 abbrev ("2","2");;
 264 abbrev ("fxast","FIRST_X_ASSUM_ST");;
 265 abbrev ("fast","FIRST_ASSUM_ST");;
 266 abbrev ("@","@");;
 267 abbrev ("map","map");;
 268 abbrev ("dt/r","REPEAT DISCH_TAC");;
 269 abbrev ("1","1");;
 270 abbrev ("2","2");;
 271 abbrev ("3","3");;
 272 abbrev ("4","4");;
 273 abbrev ("5","5");;
 274 abbrev ("uni","uni");;
 275 abbrev ("intro","INTRO_TAC");;
 276 abbrev ("conj2","CONJ2_TAC");;
 277 abbrev ("subconj2","SUBCONJ2_TAC");;
 278 abbrev ("name","RENAME_FREE_VAR");;
 279 abbrev ("rebind","REBIND_TAC");;
 280 abbrev ("s","s");;
 281 abbrev ("copy","COPY_TAC");;
 282 abbrev ("exl","GEXISTL_TAC");;
 283 abbrev ("orelse","ORELSE");;
 284 abbrev ("t","t");;
 285 abbrev ("typ","TYPIFY");;
 286 abbrev ("vat","VECTOR_ARITH_TAC");;
 287 abbrev ("smp","(C SUBGOAL_THEN MP_TAC)");;
 288 abbrev ("sat","(C SUBGOAL_THEN ASSUME_TAC)");;
 289 abbrev ("s1","(C SUBGOAL_THEN SUBST1_TAC)");;
 290 abbrev ("e","");;
 291 abbrev ("abbrev","TYPED_ABBREV_TAC");;
 292 abbrev ("strip/r","REPEAT STRIP_TAC");;
 293 abbrev ("act","act");;
 294 abbrev ("ls","LOCAL_STEP_TAC()");;
 295 abbrev ("ra","RULE_ASSUM_TAC");;
 296 abbrev ("rule","RULE_ASSUM_TAC");;
 297 abbrev ("asm","ASM_TAC");;
 298 abbrev ("gtyp","TYPIFY_GOAL_THEN");;
 299 abbrev ("setr","SET_RULE");;
 300 abbrev ("nconj","nCONJ_TAC");;
 301 abbrev ("nrt","NUM_REDUCE_TAC");;
 302 abbrev ("grt","GEN_REWRITE_TAC");;
 303 abbrev ("land","LAND_CONV");;
 304 abbrev ("rand","RAND_CONV");;
 305 abbrev ("odc","ONCE_DEPTH_CONV");;
 306 abbrev ("the","the");;
 307
 308 (* follow your nose, type "fyn" to use *)
 309
 310 add_your_nose(match_g[`&a + &b`],"REWRITE_TAC[REAL_OF_NUM_ADD]","&m + &n");;
 311 add_your_nose(match_g[`&a = &b`],"REWRITE_TAC[REAL_OF_NUM_EQ]","&m = &n");;
 312 add_your_nose(match_g[`&x < &y`],"REWRITE_TAC[ REAL_OF_NUM_LT]","&x < &y");;
 313 add_your_nose(match_g[`&x <= &y`],"REWRITE_TAC[ REAL_OF_NUM_LE]","&x <= &y");;
 314
 315 add_your_nose(match_g[full `(!(x:A). t)`],"GEN_TAC","GEN_TAC");;
 316 add_your_nose(match_g[`&0 < sqrt x`],"GMATCH_SIMP_TAC SQRT_POS_LT","&0 < sqrt _");;
 317 add_your_nose(match_g[`&0 <= sqrt x`],"GMATCH_SIMP_TAC SQRT_POS_LE","&0 <= sqrt _");;
 318 add_your_nose(match_g[`x IN {}`],"REWRITE_TAC[NOT_IN_EMPTY]","_ IN {}");;
 319 add_your_nose(match_g[`sqrt x <= sqrt y`],"GMATCH_SIMP_TAC SQRT_MONO_LE_EQ","sqrt _ <= sqrt _");;
 320 add_your_nose(match_g[`sqrt x < sqrt y`],"GMATCH_SIMP_TAC SQRT_MONO_LT_EQ","sqrt _ < sqrt _");;
 321 add_your_nose(match_g[`&0 < x * y`],"GMATCH_SIMP_TAC REAL_LT_MUL_EQ","&0 < pos1 * pow2");;
 322 add_your_nose(match_g[`x * x <= y * y`],"GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE","x * x <= y * y");;
 323 add_your_nose(match_g[`&0 <= x/y`],"GMATCH_SIMP_TAC REAL_LE_DIV","&0 <= x/y");;
 324 add_your_nose(match_g[`&0 <= x * y`],"GMATCH_SIMP_TAC REAL_LE_MUL","&0 <= x *y");;
 325 add_your_nose(match_g[`&0 <= x * x`],"REWRITE_TAC[ REAL_LE_SQUARE]","&0 <= x *y");;
 326 add_your_nose(match_g[`sqrt x pow 2`],"GMATCH_SIMP_TAC SQRT_POW_2","sqrt x pow 2");;
 327 add_your_nose(match_g[`x /z <= y`],"GMATCH_SIMP_TAC REAL_LE_LDIV_EQ","x /z <= y");;
 328 add_your_nose(match_g[`&0 <= x pow 2`],"REWRITE_TAC[ REAL_LE_POW_2]","&0 <= x pow 2");;
 329 add_your_nose(match_g[`x < sqrt y`],"GMATCH_SIMP_TAC REAL_LT_RSQRT","x < sqrt y");;
 330 add_your_nose(match_g[`x /z <= y/ z`],"GMATCH_SIMP_TAC REAL_LE_DIV2_EQ","x/z <= y/z");;
 331 add_your_nose(match_g[`sqrt(y*y)`],"GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx","sqrt(x*x)");;
 332 add_your_nose(match_g[`x * y <= x * z`],"GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP","x * y <= x * z");;
 333 add_your_nose(match_g[`x < y/ z`],"GMATCH_SIMP_TAC REAL_LT_RDIV_EQ","x < y/z");;
 334 add_your_nose(match_g[`&0 < x/y`],"GMATCH_SIMP_TAC REAL_LT_DIV","&0 < x/y");;
 335 add_your_nose(match_g[`sqrt x * sqrt y`],"GMATCH_SIMP_TAC (GSYM SQRT_MUL)","sqrt x * sqrt y");;
 336 add_your_nose(match_g[`x * x < y * y`],"GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE","x * x < y*y");;
 337 add_your_nose(match_g[`&0 < y pow 2`],"REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]","&0 < x pow 2");;
 338 add_your_nose(match_g[`x * y < x * z`],"GMATCH_SIMP_TAC REAL_LT_LMUL_EQ","x * y < x*z");;
 339 add_your_nose(match_g[`sqrt x = &0`],"GMATCH_SIMP_TAC SQRT_EQ_0","sqrt x = &0");;
 340  add_your_nose(match_g[`x <= y/z`],"GMATCH_SIMP_TAC REAL_LE_RDIV_EQ","x <= y/z");;
 341  add_your_nose(match_g[`x * x < y * y`],"GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE","x * x < y * y");;
 342 add_your_nose(match_g[`inv y <= inv x`],"GMATCH_SIMP_TAC REAL_LE_INV2","inv y <= inv x");;
 343 add_your_nose(match_g[`&0 < inv x`],"GMATCH_SIMP_TAC REAL_LT_INV","&0 < inv x");;
 344 add_your_nose(match_g[`&0 <= inv x`],"REWRITE_TAC[REAL_LE_INV_EQ]","&0 <= inv x");;
 345 add_your_nose(match_g[`abs(a*b)`],"REWRITE_TAC[REAL_ABS_MUL]","abs(a*b)");;
 346
 347   let gnose s t prompt = add_your_nose(match_g[t],"GMATCH_SIMP_TAC "^s,prompt);;
 348   let wnose s t prompt = add_your_nose(match_g[t],"REWRITE_TAC["^s^"]",prompt);;
 349   let mnose s t prompt = add_your_nose(match_g[t],"MATCH_MP_TAC "^s,prompt);;
 350
 351 wnose "VECTOR_MUL_LCANCEL" `a % v = a % w` "a % v = a % w";;
 352 wnose "VECTOR_MUL_ASSOC" `a % b % w` "a % b % w";;
 353 wnose "VECTOR_MUL_LID" `&1 % w` "&1 % w`";;
 354 wnose "Counting_spheres.AZIM_NN" `&0 <= azim a b c d` "0 <= azim";;
 355 wnose "DIST_EQ_0" `dist(x,y) = &0` "dist(x,y) = &0";;
 356 wnose "DIST_REFL" `dist(x,x) = &0` "dist(x,x) = &0";;
 357 wnose "DIST_POS_LE" `&0 <= dist(x,y)` "&0 <= dist(x,y)";;
 358 wnose "VECTOR_SUB_RZERO" `v - vec 0` "v - vec 0";;
 359 wnose "GSYM DIST_NZ" `&0 < dist(x,y)` "&0 < dist(x,y)";;
 360 wnose "NORM_POS_LE" `&0 <= norm x` "&0 <= norm x";;
 361 wnose "NORM_MUL" `norm (a % w)` "norm (a % w)";;
 362 wnose "DOT_EQ_0" `w dot w = &0` "w dot w = &0";;
 363 wnose "GSYM REAL_EQ_SQUARE_ABS" `a pow 2 = b pow 2` "a pow 2 = b pow 2 <=> abs a = abs b";;
 364 wnose "NORM_EQ_0" `norm v = &0` "norm v = &0";;
 365 wnose "DOT_POS_LT" `&0 < x dot x` "&0 < x dot x";;
 366 wnose "WITHINREAL_UNIV" `net within (:real)` "within (:real)";;
 367 gnose "Merge_ineq.sqrtpow2" `sqrt x * sqrt x` "sqrt x * sqrt x";;
 368 gnose "(GSYM Trigonometry2.POW2_COND)" `a pow 2 <= b pow 2` "a pow 2 <= b pow 2";;
 369 wnose "POW_2_SQRT_ABS" `sqrt(x pow 2)` "sqrt (x pow 2)";;
 370 mnose "REAL_LE_RSQRT" `y <= sqrt x` "y <= sqrt x";;
 371
 372 end;;