nums.ml

   1 (* ========================================================================= *)
   2 (* The axiom of infinity; construction of the natural numbers.               *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "pair.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Declare a new type "ind" of individuals.                                  *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 new_type ("ind",0);;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* We assert the axiom of infinity as in HOL88, but then we can forget it!   *)
  20 (* ------------------------------------------------------------------------- *)
  21
  22 let ONE_ONE = new_definition
  23   `ONE_ONE(f:A->B) = !x1 x2. (f x1 = f x2) ==> (x1 = x2)`;;
  24
  25 let ONTO = new_definition
  26   `ONTO(f:A->B) = !y. ?x. y = f x`;;
  27
  28 let INFINITY_AX = new_axiom
  29   `?f:ind->ind. ONE_ONE f /\ ~(ONTO f)`;;
  30
  31 (* ------------------------------------------------------------------------- *)
  32 (* Actually introduce constants.                                             *)
  33 (* ------------------------------------------------------------------------- *)
  34
  35 let IND_SUC_0_EXISTS = prove
  36  (`?(f:ind->ind) z. (!x1 x2. (f x1 = f x2) = (x1 = x2)) /\ (!x. ~(f x = z))`,
  37   X_CHOOSE_TAC `f:ind->ind` INFINITY_AX THEN EXISTS_TAC `f:ind->ind` THEN
  38   POP_ASSUM MP_TAC THEN REWRITE_TAC[ONE_ONE; ONTO] THEN MESON_TAC[]);;
  39
  40 let IND_SUC_SPEC =
  41   let th1 = new_definition
  42    `IND_SUC = @f:ind->ind. ?z. (!x1 x2. (f x1 = f x2) = (x1 = x2)) /\
  43                                 (!x. ~(f x = z))` in
  44   let th2 = REWRITE_RULE[GSYM th1] (SELECT_RULE IND_SUC_0_EXISTS) in
  45   let th3 = new_definition
  46    `IND_0 = @z:ind. (!x1 x2. IND_SUC x1 = IND_SUC x2 <=> x1 = x2) /\
  47                     (!x. ~(IND_SUC x = z))` in
  48   REWRITE_RULE[GSYM th3] (SELECT_RULE th2);;
  49
  50 let IND_SUC_INJ,IND_SUC_0 = CONJ_PAIR IND_SUC_SPEC;;
  51
  52 (* ------------------------------------------------------------------------- *)
  53 (* Carve out the natural numbers inductively.                                *)
  54 (* ------------------------------------------------------------------------- *)
  55
  56 let NUM_REP_RULES,NUM_REP_INDUCT,NUM_REP_CASES =
  57   new_inductive_definition
  58    `NUM_REP IND_0 /\
  59     (!i. NUM_REP i ==> NUM_REP (IND_SUC i))`;;
  60
  61 let num_tydef = new_basic_type_definition
  62   "num" ("mk_num","dest_num")
  63     (CONJUNCT1 NUM_REP_RULES);;
  64
  65 let ZERO_DEF = new_definition
  66  `_0 = mk_num IND_0`;;
  67
  68 let SUC_DEF = new_definition
  69  `SUC n = mk_num(IND_SUC(dest_num n))`;;
  70
  71 (* ------------------------------------------------------------------------- *)
  72 (* Distinctness and injectivity of constructors.                             *)
  73 (* ------------------------------------------------------------------------- *)
  74
  75 let NOT_SUC = prove
  76  (`!n. ~(SUC n = _0)`,
  77   REWRITE_TAC[SUC_DEF; ZERO_DEF] THEN
  78   MESON_TAC[NUM_REP_RULES; fst num_tydef; snd num_tydef; IND_SUC_0]);;
  79
  80 let SUC_INJ = prove
  81  (`!m n. SUC m = SUC n <=> m = n`,
  82   REPEAT GEN_TAC THEN REWRITE_TAC[SUC_DEF] THEN
  83   EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  84   POP_ASSUM(MP_TAC o AP_TERM `dest_num`) THEN
  85   SUBGOAL_THEN `!p. NUM_REP (IND_SUC (dest_num p))` MP_TAC THENL
  86    [GEN_TAC THEN MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES); ALL_TAC] THEN
  87   REWRITE_TAC[fst num_tydef; snd num_tydef] THEN
  88   DISCH_TAC THEN ASM_REWRITE_TAC[IND_SUC_INJ] THEN
  89   DISCH_THEN(MP_TAC o AP_TERM `mk_num`) THEN
  90   REWRITE_TAC[fst num_tydef]);;
  91
  92 (* ------------------------------------------------------------------------- *)
  93 (* Induction.                                                                *)
  94 (* ------------------------------------------------------------------------- *)
  95
  96 let num_INDUCTION = prove
  97  (`!P. P(_0) /\ (!n. P(n) ==> P(SUC n)) ==> !n. P n`,
  98   REPEAT STRIP_TAC THEN
  99   MP_TAC(SPEC `\i. NUM_REP i /\ P(mk_num i):bool` NUM_REP_INDUCT) THEN
 100   ASM_REWRITE_TAC[GSYM ZERO_DEF; NUM_REP_RULES] THEN
 101   W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
 102    [REPEAT STRIP_TAC THENL
 103      [MATCH_MP_TAC(CONJUNCT2 NUM_REP_RULES) THEN ASM_REWRITE_TAC[];
 104       SUBGOAL_THEN `mk_num(IND_SUC i) = SUC(mk_num i)` SUBST1_TAC THENL
 105        [REWRITE_TAC[SUC_DEF] THEN REPEAT AP_TERM_TAC THEN
 106         CONV_TAC SYM_CONV THEN REWRITE_TAC[GSYM(snd num_tydef)] THEN
 107         FIRST_ASSUM MATCH_ACCEPT_TAC;
 108         FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC]];
 109     DISCH_THEN(MP_TAC o SPEC `dest_num n`) THEN
 110     REWRITE_TAC[fst num_tydef; snd num_tydef]]);;
 111
 112 (* ------------------------------------------------------------------------- *)
 113 (* Recursion.                                                                *)
 114 (* ------------------------------------------------------------------------- *)
 115
 116 let num_Axiom = prove
 117  (`!(e:A) f. ?!fn. (fn _0 = e) /\
 118                    (!n. fn (SUC n) = f (fn n) n)`,
 119   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL
 120    [(MP_TAC o prove_inductive_relations_exist)
 121       `PRG _0 e /\ (!b:A n:num. PRG n b ==> PRG (SUC n) (f b n))` THEN
 122     DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 123     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN
 124     SUBGOAL_THEN `!n:num. ?!y:A. PRG n y` MP_TAC THENL
 125      [MATCH_MP_TAC num_INDUCTION THEN REPEAT STRIP_TAC THEN
 126       FIRST_ASSUM(fun th -> GEN_REWRITE_TAC BINDER_CONV [GSYM th]) THEN
 127       REWRITE_TAC[GSYM NOT_SUC; NOT_SUC; SUC_INJ; EXISTS_UNIQUE_REFL] THEN
 128       REWRITE_TAC[UNWIND_THM1] THEN
 129       UNDISCH_TAC `?!y. PRG (n:num) (y:A)` THEN
 130       REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 131       DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `y:A`) ASSUME_TAC) THEN
 132       REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 133        [MAP_EVERY EXISTS_TAC [`(f:A->num->A) y n`; `y:A`];
 134         AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC] THEN
 135       ASM_REWRITE_TAC[];
 136       REWRITE_TAC[UNIQUE_SKOLEM_ALT] THEN
 137       DISCH_THEN(X_CHOOSE_THEN `fn:num->A` (ASSUME_TAC o GSYM)) THEN
 138       EXISTS_TAC `fn:num->A` THEN ASM_REWRITE_TAC[] THEN
 139       GEN_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o CONJUNCT2) THEN
 140       FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN REFL_TAC];
 141     REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
 142     MATCH_MP_TAC num_INDUCTION THEN ASM_REWRITE_TAC[] THEN
 143     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]]);;
 144
 145 (* ------------------------------------------------------------------------- *)
 146 (* The basic numeral tag; rewrite existing instances of "_0".                *)
 147 (* ------------------------------------------------------------------------- *)
 148
 149 let NUMERAL = new_definition
 150  `NUMERAL (n:num) = n`;;
 151
 152 let [NOT_SUC; num_INDUCTION; num_Axiom] =
 153   let th = prove(`_0 = 0`,REWRITE_TAC[NUMERAL]) in
 154   map (GEN_REWRITE_RULE DEPTH_CONV [th])
 155     [NOT_SUC; num_INDUCTION; num_Axiom];;
 156
 157 (* ------------------------------------------------------------------------- *)
 158 (* Induction tactic.                                                         *)
 159 (* ------------------------------------------------------------------------- *)
 160
 161 let (INDUCT_TAC:tactic) =
 162   MATCH_MP_TAC num_INDUCTION THEN
 163   CONJ_TAC THENL [ALL_TAC; GEN_TAC THEN DISCH_TAC];;
 164
 165 let num_RECURSION =
 166   let avs = fst(strip_forall(concl num_Axiom)) in
 167   GENL avs (EXISTENCE (SPECL avs num_Axiom));;
 168
 169 (* ------------------------------------------------------------------------- *)
 170 (* Cases theorem.                                                            *)
 171 (* ------------------------------------------------------------------------- *)
 172
 173 let num_CASES = prove
 174  (`!m. (m = 0) \/ (?n. m = SUC n)`,
 175   INDUCT_TAC THEN MESON_TAC[]);;
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* Augmenting inductive type store.                                          *)
 179 (* ------------------------------------------------------------------------- *)
 180
 181 let num_RECURSION_STD = prove
 182  (`!e:Z f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f n (fn n))`,
 183   REPEAT GEN_TAC THEN
 184   MP_TAC(ISPECL [`e:Z`; `(\z n. (f:num->Z->Z) n z)`] num_RECURSION) THEN
 185   REWRITE_TAC[]);;
 186
 187 inductive_type_store :=
 188  ("num",(2,num_INDUCTION,num_RECURSION_STD))::(!inductive_type_store);;
 189
 190 (* ------------------------------------------------------------------------- *)
 191 (* "Bitwise" binary representation of numerals.                              *)
 192 (* ------------------------------------------------------------------------- *)
 193
 194 let BIT0_DEF =
 195   let def = new_definition
 196    `BIT0 = @fn. fn 0 = 0 /\ (!n. fn (SUC n) = SUC (SUC(fn n)))`
 197   and th = BETA_RULE(ISPECL [`0`; `\m n:num. SUC(SUC m)`] num_RECURSION) in
 198   REWRITE_RULE[GSYM def] (SELECT_RULE th);;
 199
 200 let BIT1_DEF = new_definition
 201  `BIT1 n = SUC (BIT0 n)`;;
 202
 203 (* ------------------------------------------------------------------------- *)
 204 (* Syntax operations on numerals.                                            *)
 205 (* ------------------------------------------------------------------------- *)
 206
 207 let mk_numeral =
 208   let pow24 = pow2 24 and num_0 = Int 0
 209   and zero_tm = mk_const("_0",[])
 210   and BIT0_tm = mk_const("BIT0",[])
 211   and BIT1_tm = mk_const("BIT1",[])
 212   and NUMERAL_tm = mk_const("NUMERAL",[]) in
 213   let rec stripzeros l = match l with false::t -> stripzeros t | _ -> l in
 214   let rec raw_list_of_num l n =
 215     if n =/ num_0 then stripzeros l else
 216     let h = Num.int_of_num(mod_num n pow24) in
 217     raw_list_of_num
 218      ((h land 8388608 <> 0)::(h land 4194304 <> 0)::(h land 2097152 <> 0)::
 219       (h land 1048576 <> 0)::(h land 524288 <> 0)::(h land 262144 <> 0)::
 220       (h land 131072 <> 0)::(h land 65536 <> 0)::(h land 32768 <> 0)::
 221       (h land 16384 <> 0)::(h land 8192 <> 0)::(h land 4096 <> 0)::
 222       (h land 2048 <> 0)::(h land 1024 <> 0)::(h land 512 <> 0)::
 223       (h land 256 <> 0)::(h land 128 <> 0)::(h land 64 <> 0)::
 224       (h land 32 <> 0)::(h land 16 <> 0)::(h land 8 <> 0)::(h land 4 <> 0)::
 225       (h land 2 <> 0)::(h land 1 <> 0)::l) (quo_num n pow24) in
 226   let rec numeral_of_list t l =
 227     match l with
 228       [] -> t
 229     | b::r -> numeral_of_list(mk_comb((if b then BIT1_tm else BIT0_tm),t)) r in
 230   let mk_raw_numeral n = numeral_of_list zero_tm (raw_list_of_num [] n) in
 231   fun n -> if n </ num_0 then failwith "mk_numeral: negative argument" else
 232            mk_comb(NUMERAL_tm,mk_raw_numeral n);;
 233
 234 let mk_small_numeral n = mk_numeral(Int n);;
 235
 236 let dest_small_numeral t = Num.int_of_num(dest_numeral t);;
 237
 238 let is_numeral = can dest_numeral;;
 239
 240 (* ------------------------------------------------------------------------- *)
 241 (* Derived principles of definition based on existence.                      *)
 242 (*                                                                           *)
 243 (* This is put here because we use numerals as tags to force different       *)
 244 (* constants specified with equivalent theorems to have different underlying *)
 245 (* definitions, ensuring that there are no provable equalities between them  *)
 246 (* and so in some sense the constants are "underspecified" as the user might *)
 247 (* want for some applications.                                               *)
 248 (* ------------------------------------------------------------------------- *)
 249
 250 let the_specifications = ref [];;
 251
 252 let new_specification =
 253   let code c = mk_small_numeral (Char.code (c.[0])) in
 254   let mk_code name =
 255       end_itlist (curry mk_pair) (map code (explode name)) in
 256   let check_distinct l =
 257     try itlist (fun t res -> if mem t res then fail() else t::res) l []; true
 258     with Failure _ -> false in
 259   let specify name th =
 260     let ntm = mk_code name in
 261     let gv = genvar(type_of ntm) in
 262     let th0 = CONV_RULE(REWR_CONV SKOLEM_THM) (GEN gv th) in
 263     let th1 = CONV_RULE(RATOR_CONV (REWR_CONV EXISTS_THM) THENC
 264                         BETA_CONV) th0 in
 265     let l,r = dest_comb(concl th1) in
 266     let rn = mk_comb(r,ntm) in
 267     let ty = type_of rn in
 268     let th2 = new_definition(mk_eq(mk_var(name,ty),rn)) in
 269     GEN_REWRITE_RULE ONCE_DEPTH_CONV [GSYM th2]
 270      (SPEC ntm (CONV_RULE BETA_CONV th1)) in
 271   let rec specifies names th =
 272     match names with
 273       [] -> th
 274     | name::onames -> let th' = specify name th in
 275                       specifies onames th' in
 276   fun names th ->
 277     let asl,c = dest_thm th in
 278     if not (asl = []) then
 279       failwith "new_specification: Assumptions not allowed in theorem" else
 280     if not (frees c = []) then
 281       failwith "new_specification: Free variables in predicate" else
 282     let avs = fst(strip_exists c) in
 283     if length names = 0 or length names > length avs then
 284       failwith "new_specification: Unsuitable number of constant names" else
 285     if not (check_distinct names) then
 286       failwith "new_specification: Constant names not distinct"
 287     else
 288       try let sth = snd(find (fun ((names',th'),sth') ->
 289                                names' = names & aconv (concl th') (concl th))
 290                              (!the_specifications)) in
 291           warn true ("Benign respecification"); sth
 292       with Failure _ ->
 293           let sth = specifies names th in
 294           the_specifications := ((names,th),sth)::(!the_specifications);
 295           sth;;