text_formalization/jordan/num_ext_nabs.hl

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