Jordan/num_ext_nabs.ml

   1 unambiguous_interface();;
   2
   3 let INT_NUM = prove(`!u. (integer (real_of_num u))`,
   4         (REWRITE_TAC[is_int]) THEN GEN_TAC THEN
   5         (EXISTS_TAC (`u:num`)) THEN (MESON_TAC[]));;
   6
   7 let INT_NUM_REAL = prove(`!u. (real_of_int (int_of_num u) = real_of_num u)`,
   8         (REWRITE_TAC[int_of_num]) THEN
   9         GEN_TAC THEN (MESON_TAC[INT_NUM;int_rep]));;
  10
  11 let INT_IS_INT = prove(`!(a:int). (integer (real_of_int a))`,
  12         REWRITE_TAC[int_rep;int_abstr]);;
  13
  14 let INT_OF_NUM_DEST = prove(`!a n. ((real_of_int a = (real_of_num n)) =
  15                 (a = int_of_num n))`,
  16         (REWRITE_TAC[int_eq])
  17         THEN (REPEAT GEN_TAC)
  18         THEN (REWRITE_TAC[int_of_num])
  19         THEN (ASSUME_TAC (SPEC (`n:num`) INT_NUM))
  20         THEN (UNDISCH_EL_TAC 0)
  21         THEN (SIMP_TAC[int_rep]));;
  22
  23 let INT_REP = prove(`!a. ?n m. (a = (int_of_num n) - (int_of_num m))`,
  24         GEN_TAC
  25         THEN (let tt =(REWRITE_RULE[is_int] (SPEC (`a:int`) INT_IS_INT)) in
  26                 (CHOOSE_TAC tt))
  27         THEN (POP_ASSUM DISJ_CASES_TAC)
  28         THENL [
  29          (EXISTS_TAC (`n:num`)) THEN (EXISTS_TAC (`0`)) THEN
  30          (ASM_REWRITE_TAC[INT_SUB_RZERO;GSYM INT_OF_NUM_DEST]);
  31          (EXISTS_TAC (`0`)) THEN (EXISTS_TAC (`n:num`)) THEN
  32          (REWRITE_TAC[INT_SUB_LZERO]) THEN
  33          (UNDISCH_EL_TAC 0) THEN
  34          (REWRITE_TAC[GSYM REAL_NEG_EQ;GSYM INT_NEG_EQ;GSYM int_neg_th;GSYM
  35         INT_OF_NUM_DEST])]);;
  36
  37 let INT_REP2 = prove( `!a. ?n. ((a = (&: n)) \/ (a = (--: (&: n))))`,
  38 (GEN_TAC)
  39    THEN ((let tt =(REWRITE_RULE[is_int] (SPEC (`a:int`) INT_IS_INT)) in
  40       (CHOOSE_TAC tt)))
  41    THEN ((POP_ASSUM DISJ_CASES_TAC))
  42    THENL
  43    [ ((EXISTS_TAC (`n:num`)))
  44    THEN ((ASM_REWRITE_TAC[GSYM INT_OF_NUM_DEST]));
  45      ((EXISTS_TAC (`n:num`)))
  46    (* THEN ((RULE_EL 0 (REWRITE_RULE[GSYM REAL_NEG_EQ;GSYM int_neg_th]))) *)
  47    THEN (H_REWRITE_RULE[THM (GSYM REAL_NEG_EQ);THM (GSYM int_neg_th)] (HYP_INT 0))
  48    THEN ((ASM_REWRITE_TAC[GSYM INT_NEG_EQ;GSYM INT_OF_NUM_DEST]))]);;
  49
  50
  51
  52 (* ------------------------------------------------------------------ *)
  53 (* nabs : int -> num gives the natural number abs. value of an int *)
  54 (* ------------------------------------------------------------------ *)
  55
  56
  57 let nabs = new_definition(`nabs n = @u. ((n = int_of_num u) \/ (n =
  58         int_neg (int_of_num u)))`);;
  59
  60 let NABS_POS = prove(`!u. (nabs (int_of_num u)) = u`,
  61         GEN_TAC
  62         THEN (REWRITE_TAC [nabs])
  63         THEN (MATCH_MP_TAC SELECT_UNIQUE)
  64         THEN (GEN_TAC THEN BETA_TAC)
  65         THEN (EQ_TAC)
  66         THENL [(TAUT_TAC (` ((A==>C)/\ (B==>C)) ==> (A\/B ==>C) `));
  67                 MESON_TAC[]]
  68         THEN CONJ_TAC THENL
  69         (let branch2 =  (REWRITE_TAC[int_eq;int_neg_th;INT_NUM_REAL])
  70         THEN (REWRITE_TAC[prove (`! u y.(((real_of_num u) = --(real_of_num y))=
  71                 ((real_of_num u) +(real_of_num y) = (&0)))`,REAL_ARITH_TAC)])
  72         THEN (REWRITE_TAC[REAL_OF_NUM_ADD;REAL_OF_NUM_EQ])
  73         THEN (MESON_TAC[ADD_EQ_0]) in
  74         [(REWRITE_TAC[int_eq;INT_NUM_REAL]);branch2])
  75         THEN (REWRITE_TAC[INT_NUM_REAL])
  76         THEN (MESON_TAC[REAL_OF_NUM_EQ]));;
  77
  78 let NABS_NEG = prove(`!n. (nabs (-- (int_of_num n))) = n`,
  79         GEN_TAC
  80         THEN (REWRITE_TAC [nabs])
  81         THEN (MATCH_MP_TAC SELECT_UNIQUE)
  82         THEN (GEN_TAC THEN BETA_TAC)
  83         THEN (EQ_TAC)
  84         THENL [(TAUT_TAC (` ((A==>C)/\ (B==>C)) ==> (A\/B ==>C) `));
  85                 MESON_TAC[]]
  86         THEN CONJ_TAC THENL
  87         (let branch1 =  (REWRITE_TAC[int_eq;int_neg_th;INT_NUM_REAL])
  88         THEN (REWRITE_TAC[prove (`! u y.((--(real_of_num u) = (real_of_num y))=
  89                 ((real_of_num u) +(real_of_num y) = (&0)))`,REAL_ARITH_TAC)])
  90         THEN (REWRITE_TAC[REAL_OF_NUM_ADD;REAL_OF_NUM_EQ])
  91         THEN (MESON_TAC[ADD_EQ_0]) in
  92         [branch1;(REWRITE_TAC[int_eq;INT_NUM_REAL])])
  93         THEN (REWRITE_TAC[INT_NUM_REAL;int_neg_th;REAL_NEG_EQ;REAL_NEGNEG])
  94         THEN (MESON_TAC[REAL_OF_NUM_EQ]));;
  95
  96