1 (* ========================================================================== *)
2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Copied from HOL Light jordan directory *)
7 (* Author: Thomas C. Hales *)
9 (* ========================================================================== *)
12 (* needs tactics_ext.ml *)
14 module Num_ext_nabs = struct
18 Parse_ext_override_interface.unambiguous_interface();;
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[]));;
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]));;
28 let INT_IS_INT = prove(`!(a:int). (integer (real_of_int a))`,
29 REWRITE_TAC[int_rep;int_abstr]);;
31 let INT_OF_NUM_DEST = prove(`!a n. ((real_of_int a = (real_of_num n)) =
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]));;
40 let INT_REP = prove(`!a. ?n m. (a = (int_of_num n) - (int_of_num m))`,
42 THEN (let tt =(REWRITE_RULE[is_int] (SPEC (`a:int`) INT_IS_INT)) in
44 THEN (POP_ASSUM DISJ_CASES_TAC)
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
54 let INT_REP2 = prove( `!a. ?n. ((a = (&: n)) \/ (a = (--: (&: n))))`,
56 THEN ((let tt =(REWRITE_RULE[is_int] (SPEC (`a:int`) INT_IS_INT)) in
58 THEN ((POP_ASSUM DISJ_CASES_TAC))
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]))]);;
69 (* ------------------------------------------------------------------ *)
70 (* nabs : int -> num gives the natural number abs. value of an int *)
71 (* ------------------------------------------------------------------ *)
74 let nabs = new_definition(`nabs n = @u. ((n = int_of_num u) \/ (n =
75 int_neg (int_of_num u)))`);;
77 let NABS_POS = prove(`!u. (nabs (int_of_num u)) = u`,
79 THEN (REWRITE_TAC [nabs])
80 THEN (MATCH_MP_TAC SELECT_UNIQUE)
81 THEN (GEN_TAC THEN BETA_TAC)
83 THENL [(TAUT_TAC (` ((A==>C)/\ (B==>C)) ==> (A\/B ==>C) `));
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]));;
95 let NABS_NEG = prove(`!n. (nabs (-- (int_of_num n))) = n`,
97 THEN (REWRITE_TAC [nabs])
98 THEN (MATCH_MP_TAC SELECT_UNIQUE)
99 THEN (GEN_TAC THEN BETA_TAC)
101 THENL [(TAUT_TAC (` ((A==>C)/\ (B==>C)) ==> (A\/B ==>C) `));
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]));;