(* ========================================================================== *)
(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Jordan                                                               *)
(* Copied from HOL Light jordan directory *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-08                                                           *)
(* ========================================================================== *)
 

(* needs tactics_ext.ml *)

module Num_ext_nabs = struct

open Tactics_jordan;;

Parse_ext_override_interface.unambiguous_interface();;

let INT_NUM = 
prove(`!u. (integer (real_of_num u))`,
(REWRITE_TAC[is_int]) THEN GEN_TAC THEN (EXISTS_TAC (`u:num`)) THEN (MESON_TAC[]));;
let INT_NUM_REAL = 
prove(`!u. (real_of_int (int_of_num u) = real_of_num u)`,
(REWRITE_TAC[int_of_num]) THEN GEN_TAC THEN (MESON_TAC[INT_NUM;int_rep]));;
let INT_IS_INT = 
prove(`!(a:int). (integer (real_of_int a))`,
REWRITE_TAC[int_rep;int_abstr]);;
let INT_OF_NUM_DEST = 
prove(`!a n. ((real_of_int a = (real_of_num n)) = (a = int_of_num n))`,
(REWRITE_TAC[int_eq]) THEN (REPEAT GEN_TAC) THEN (REWRITE_TAC[int_of_num]) THEN (ASSUME_TAC (SPEC (`n:num`) INT_NUM)) THEN (UNDISCH_EL_TAC 0) THEN (SIMP_TAC[int_rep]));;
let INT_REP = 
prove(`!a. ?n m. (a = (int_of_num n) - (int_of_num m))`,
GEN_TAC THEN (let tt =(REWRITE_RULE[is_int] (SPEC (`a:int`) INT_IS_INT)) in (CHOOSE_TAC tt)) THEN (POP_ASSUM DISJ_CASES_TAC) THENL [ (EXISTS_TAC (`n:num`)) THEN (EXISTS_TAC (`0`)) THEN (ASM_REWRITE_TAC[INT_SUB_RZERO;GSYM INT_OF_NUM_DEST]); (EXISTS_TAC (`0`)) THEN (EXISTS_TAC (`n:num`)) THEN (REWRITE_TAC[INT_SUB_LZERO]) THEN (UNDISCH_EL_TAC 0) THEN (REWRITE_TAC[GSYM REAL_NEG_EQ;GSYM INT_NEG_EQ;GSYM int_neg_th;GSYM INT_OF_NUM_DEST])]);;
let INT_REP2 = 
prove( `!a. ?n. ((a = (&: n)) \/ (a = (--: (&: n))))`,
(GEN_TAC) THEN ((let tt =(REWRITE_RULE[is_int] (SPEC (`a:int`) INT_IS_INT)) in (CHOOSE_TAC tt))) THEN ((POP_ASSUM DISJ_CASES_TAC)) THENL [ ((EXISTS_TAC (`n:num`))) THEN ((ASM_REWRITE_TAC[GSYM INT_OF_NUM_DEST])); ((EXISTS_TAC (`n:num`))) (* THEN ((RULE_EL 0 (REWRITE_RULE[GSYM REAL_NEG_EQ;GSYM int_neg_th]))) *) THEN (H_REWRITE_RULE[THM (GSYM REAL_NEG_EQ);THM (GSYM int_neg_th)] (HYP_INT 0)) THEN ((ASM_REWRITE_TAC[GSYM INT_NEG_EQ;GSYM INT_OF_NUM_DEST]))]);;
(* ------------------------------------------------------------------ *) (* nabs : int -> num gives the natural number abs. value of an int *) (* ------------------------------------------------------------------ *)
let nabs = new_definition(`nabs n = @u. ((n = int_of_num u) \/ (n =
        int_neg (int_of_num u)))`);;
let NABS_POS = 
prove(`!u. (nabs (int_of_num u)) = u`,
GEN_TAC THEN (REWRITE_TAC [nabs]) THEN (MATCH_MP_TAC SELECT_UNIQUE) THEN (GEN_TAC THEN BETA_TAC) THEN (EQ_TAC) THENL [(TAUT_TAC (` ((A==>C)/\ (B==>C)) ==> (A\/B ==>C) `)); MESON_TAC[]] THEN CONJ_TAC THENL (let branch2 = (REWRITE_TAC[int_eq;int_neg_th;INT_NUM_REAL]) THEN (REWRITE_TAC[prove (`! u y.(((real_of_num u) = --(real_of_num y))= ((real_of_num u) +(real_of_num y) = (&0)))`,REAL_ARITH_TAC)]) THEN (REWRITE_TAC[REAL_OF_NUM_ADD;REAL_OF_NUM_EQ]) THEN (MESON_TAC[ADD_EQ_0]) in [(REWRITE_TAC[int_eq;INT_NUM_REAL]);branch2]) THEN (REWRITE_TAC[INT_NUM_REAL]) THEN (MESON_TAC[REAL_OF_NUM_EQ]));;
let NABS_NEG = 
prove(`!n. (nabs (-- (int_of_num n))) = n`,
GEN_TAC THEN (REWRITE_TAC [nabs]) THEN (MATCH_MP_TAC SELECT_UNIQUE) THEN (GEN_TAC THEN BETA_TAC) THEN (EQ_TAC) THENL [(TAUT_TAC (` ((A==>C)/\ (B==>C)) ==> (A\/B ==>C) `)); MESON_TAC[]] THEN CONJ_TAC THENL (let branch1 = (REWRITE_TAC[int_eq;int_neg_th;INT_NUM_REAL]) THEN (REWRITE_TAC[prove (`! u y.((--(real_of_num u) = (real_of_num y))= ((real_of_num u) +(real_of_num y) = (&0)))`,REAL_ARITH_TAC)]) THEN (REWRITE_TAC[REAL_OF_NUM_ADD;REAL_OF_NUM_EQ]) THEN (MESON_TAC[ADD_EQ_0]) in [branch1;(REWRITE_TAC[int_eq;INT_NUM_REAL])]) THEN (REWRITE_TAC[INT_NUM_REAL;int_neg_th;REAL_NEG_EQ;REAL_NEGNEG]) THEN (MESON_TAC[REAL_OF_NUM_EQ]));;
end;;