Rqe/pdivides_thms.ml

   1 let neg_odd_lem = prove_by_refinement(
   2   `!a n p c q d.
   3      (a pow n * p x = c x * q x + d x) ==>
   4      ODD n ==>
   5        ((-- a) pow n * p x = (-- c x) * q x + (-- d x))`,
   6 (* {{{ Proof *)
   7
   8 [
   9   REPEAT STRIP_TAC;
  10   REWRITE_TAC[REAL_ARITH `-- x * y = -- (x * y)`];
  11   REWRITE_TAC[REAL_ARITH `-- x + -- y = -- (x + y)`];
  12   CLAIM `-- a pow n = -- (a pow n)`;
  13   DISJ_CASES_TAC (ARITH_RULE `a < &0 \/ (a = &0) \/ a > &0`);
  14   MP_TAC (ISPECL[`a:real`;`n:num`] REAL_POW_NEG);
  15   ASM_REWRITE_TAC[GSYM NOT_ODD];
  16   POP_ASSUM DISJ_CASES_TAC;
  17   ASM_REWRITE_TAC[real_pow];
  18   CLAIM `~(n = 0)`;
  19   ASM_MESON_TAC[ODD];
  20   STRIP_TAC;
  21   CLAIM `?n'. n = SUC n'`;
  22   ASM_MESON_TAC[num_CASES];
  23   STRIP_TAC;
  24   ASM_REWRITE_TAC[real_pow];
  25   REAL_ARITH_TAC;
  26   MP_TAC (ISPECL[`a:real`;`n:num`] REAL_POW_NEG);
  27   ASM_REWRITE_TAC[GSYM NOT_ODD];
  28   STRIP_TAC;
  29   ASM_REWRITE_TAC[];
  30   REWRITE_TAC[ARITH_RULE `-- x * y = -- (x * y)`];
  31   REWRITE_TAC[ARITH_RULE `(-- x = -- y) <=> (x = y)`];
  32   FIRST_ASSUM MATCH_ACCEPT_TAC;
  33 ]);;
  34
  35 (* }}} *)
  36
  37 let mul_odd_lem = prove_by_refinement(
  38   `!a n p c q d.
  39      (a pow n * p x = c x * q x + d x) ==>
  40      ODD n ==>
  41        ((a * a pow n) * p x = (a * c x) * q x + (a * d x))`,
  42 (* {{{ Proof *)
  43 [
  44   REPEAT STRIP_TAC;
  45   REWRITE_TAC[REAL_ARITH `(a * x) * y = a * (x * y)`];
  46   REWRITE_TAC[REAL_ARITH `a * x + a *  y = a *  (x + y)`];
  47   AP_TERM_TAC;
  48   FIRST_ASSUM MATCH_ACCEPT_TAC;
  49 ]);;
  50 (* }}} *)