development/thales/examples/workshop2010_ky_lemma_negligible.hl

   1
   2
   3 let pos_lemma = prove_by_refinement(
   4    `!Q. (?C. (&0 <= C /\  (!r. &1 <= r ==> Q r <= C * r pow 2))) <=>
   5     (?C. (  (!r. &1 <= r ==> Q r <= C * r pow 2)))`,
   6 [
   7 GEN_TAC;
   8 EQ_TAC;
   9 REPEAT STRIP_TAC;
  10 EXISTS_TAC `C:real`;
  11 ASM_REWRITE_TAC[];
  12 REPEAT STRIP_TAC;
  13 EXISTS_TAC `abs(C)`;search[`negligible_fun_0`];;
  14 REWRITE_TAC[REAL_ARITH `&0 <= abs C`];
  15 REPEAT STRIP_TAC;
  16 ASSUME_TAC (REAL_ARITH `C <= abs C`);
  17 MATCH_MP_TAC REAL_LE_TRANS;
  18 EXISTS_TAC `C * r pow 2`;
  19 CONJ_TAC;
  20 ASM_SIMP_TAC[];
  21 MATCH_MP_TAC REAL_LE_RMUL_IMP;
  22 ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2];
  23 ]);;
  24
  25 let negligible_fun_any_C = prove(
  26    `!f S. negligible_fun_0 f S <=>
  27     (?C.  (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`,
  28   REWRITE_TAC[Pack_defs.negligible_fun_0;Pack_defs.negligible_fun_p;pos_lemma]);;
  29
  30