This file is indexed.

/usr/share/hol88-2.02.19940316/ml/num.ml is in hol88-source 2.02.19940316-28.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
%=============================================================================%
%                               HOL 88 Version 2.0                            %
%                                                                             %
%     FILE NAME:        num.ml                                                %
%                                                                             %
%     DESCRIPTION:      Derived rules/tactics for :num.  Assumes that theorems%
%                       from arithmetic.th are already loaded.                %
%                                                                             %
%                       Provied for compatibility with old HOL:               %
%                          - INDUCT_TAC                                       %
%                          - new_prim_rec_definition                          %
%                          - new_infix_prim_rec_definition                    %
%                                                                             %
%     AUTHOR:           MJCG and TFM                                          %
%                                                                             %
%     USES FILES:       ind.ml, prim_rec.ml, numconv.ml                       %
%                                                                             %
%                       University of Cambridge                               %
%                       Hardware Verification Group                           %
%                       Computer Laboratory                                   %
%                       New Museums Site                                      %
%                       Pembroke Street                                       %
%                       Cambridge  CB2 3QG                                    %
%                       England                                               %
%                                                                             %
%     COPYRIGHT:        University of Edinburgh                               %
%     COPYRIGHT:        University of Cambridge                               %
%     COPYRIGHT:        INRIA                                                 %
%                                                                             %
%     REVISION HISTORY: (none)                                                %
%=============================================================================%

if compiling then (loadf `ml/ind`;loadf `ml/prim_rec`;loadf `ml/numconv`);;


% --------------------------------------------------------------------- %
% INDUCT: (thm # thm) -> thm                                            %
%                                                                       %
%   A1 |- t[0]      A2 |- !n. t[n] ==> t[SUC n]                         %
% -----------------------------------------------                       %
%             A1 u A2 |- !n. t[n]                                       %
% --------------------------------------------------------------------- %

let INDUCT =
    let INDUCTION = theorem `num` `INDUCTION` in
    \(base,step).
     (let n,body = dest_forall(concl step) in
      let assm,conc = dest_imp body in
      let P  = "\^n.^assm" and
          v1 = genvar bool_ty and
          v2 = genvar bool_ty in
     let base'  = EQ_MP (SYM(BETA_CONV "^P 0")) base and
         step'  = SPEC n step and
         hypth  = SYM(RIGHT_BETA(REFL "^P ^n")) and
         concth = SYM(RIGHT_BETA(REFL "^P(SUC ^n)")) and
         IND    = SPEC P INDUCTION in
     let th1 = SUBST [hypth,v1;concth,v2]
                     "^(concl step') = (^v1 ==> ^v2)"
                     (REFL (concl step')) in
     let th2 = GEN n (EQ_MP th1 step') in
     let th3 = SPEC n (MP IND (CONJ base' th2)) in
         GEN n (EQ_MP (BETA_CONV(concl th3)) th3)) ? failwith`INDUCT`;;

% --------------------------------------------------------------------- %
%             [A] !n.t[n]                                               %
%  ================================                                     %
%   [A] t[0]  ,  [A,t[n]] t[SUC x]                                      %
% --------------------------------------------------------------------- %

let INDUCT_TAC =
    let INDUCTION = theorem `num` `INDUCTION` in
    let tac = INDUCT_THEN INDUCTION ASSUME_TAC in
        \g. tac g ? failwith `INDUCT_TAC`;;

% --------------------------------------------------------------------- %
% For compatibility of new/old HOL.                                     %
% --------------------------------------------------------------------- %

let new_prim_rec_definition =
    let num_Axiom = theorem `prim_rec` `num_Axiom` in
        \(name,tm). new_recursive_definition false num_Axiom name tm;;

let new_infix_prim_rec_definition =
    let num_Axiom = theorem `prim_rec` `num_Axiom` in
        \(name,tm). new_recursive_definition true num_Axiom name tm;;

% --------------------------------------------------------------------- %
% ADD_CONV: addition of natural number constants (numerals).            %
%                                                                       %
% If n and m are numerals (i.e 0,1,2,3,...) then:                       %
%                                                                       %
%      ADD_CONV "n + m"                                                 %
%                                                                       %
% returns                                                               %
%                                                                       %
%      |- n + m = s                                                     %
%                                                                       %
% where s is the numeral denoting the sum of n and m.                   %
%                                                                       %
% NOTE: iterative version.                                              %
% --------------------------------------------------------------------- %

let ADD_CONV =
    let nv = "n:num" and mv = "m:num" and numty = ":num" in
    let asym = SPECL [nv;mv] (theorem `arithmetic` `ADD_SYM`) in
    let Sth = let addc = theorem `arithmetic` `ADD_CLAUSES` in
              let t1,t2 = CONJ_PAIR (CONJUNCT2(CONJUNCT2 addc)) in
                  (TRANS t1 (SYM t2)) in
    let ladd0 = let addc = theorem `arithmetic` `ADD_CLAUSES` in
                    GEN "n:num" (CONJUNCT1 addc) in
    let v1 = genvar ":num" and v2 = genvar ":num" in
    let int_of_tm tm = int_of_string(fst(dest_const tm)) and
        tm_of_int i  = mk_const(string_of_int i,numty) in
    let mk_pat =
        let pl = "$+" in
        let lra = mk_comb(pl,v1) in
        \(n,m). mk_eq(mk_comb(lra,m),mk_comb(mk_comb(pl,n),v2)) in
    let trans (c,mi) th =
        let n,m = (rand # I) (dest_comb(rand (concl th))) in
        let nint = tm_of_int c and mint = tm_of_int mi in
        let nth = SYM(num_CONV n) and mth = SYM(num_CONV mint) in
        let thm1 = INST [nint,mv;m,nv] Sth in
            (SUBST [nth,v1;mth,v2] (mk_pat(nint,m)) thm1) in
    let zconv = RAND_CONV(REWR_CONV ladd0) in
    let conv th (n,m) =
        letref thm,count,mint = th,n,m in
        if (count=0)
           then CONV_RULE zconv thm
           loop (count := count - 1 ;
                 mint := mint + 1;
                 thm := TRANS thm (trans (count,mint) thm)) in
    \tm. (let c,[n;m] = (assert (\c.c="+") # I) (strip_comb tm) in
          let nint = int_of_tm n and mint = int_of_tm m in
          if not(mint < nint) then conv (REFL tm) (nint,mint) else
             let th1 = conv (REFL(mk_comb(mk_comb(c,m),n))) (mint,nint) in
                 TRANS (INST [n,nv;m,mv] asym) th1) ?
         failwith `ADD_CONV`;;

% --------------------------------------------------------------------- %
% num_EQ_CONV: equality of natural number constants.                    %
%                                                                       %
% If n and m are numerals (i.e 0,1,2,3,...) or sucessors of numerals    %
% (e.g. SUC 0, SUC(SUC 2), etc), then:                                  %
%                                                                       %
%      num_EQ_CONV "n = m"                                              %
%                                                                       %
% returns                                                               %
%                                                                       %
%      |- (n = m) = T           if n=m                                  %
%      |- (n = m) = F           if ~(n=m)                               %
%                                                                       %
% and if n and m are syntactically identical terms of type :num, then   %
%                                                                       %
%      num_EQ_CONV "n = m"  returns |- (n = m) = T                      %
%                                                                       %
% NOTE: runs out of stack for large numbers.                            %
%									%
% Fixed Bug: 5 May 1993, TFM.						%
% --------------------------------------------------------------------- %

let num_EQ_CONV =
    let nv = genvar ":num" and mv = genvar ":num" in
    let rth = SPEC nv (theorem `prim_rec` `LESS_SUC_REFL`) and
        lnth = SPECL [nv;mv] (theorem `prim_rec` `LESS_NOT_EQ`) and
        lmth = SPECL [nv;mv] (theorem `prim_rec` `LESS_MONO`) and
        lz = SPEC  nv (theorem `prim_rec` `LESS_0`) in
    let checkty = assert (\t. type_of t = ":num") in
    let check = let tm = "SUC" in assert (\t. t = tm) in
    let Suc = AP_TERM "SUC" in
    let int_of_tm tm = int_of_string(fst(dest_const tm)) in
    letrec val n = (int_of_tm n) ? val (snd((check # I) (dest_comb n)))+1 in
    let mk_pat = let less = "$<" in \n. mk_comb(mk_comb(less,n),mv) in
    let mk_pat2 = let less = "$<" in \m. mk_comb(mk_comb(less,nv),m) in
    letrec eqconv n m =
       if (n=m) then REFL n else
       if (is_const n) then
           let th = num_CONV n in
               TRANS th (eqconv (rand(concl th)) m) else
       if (is_const m) then
           let th = num_CONV m in
               TRANS (eqconv n (rand(concl th))) (SYM th) else
       Suc (eqconv (rand n) (rand m)) in
    letrec neqconv n m =
       if (is_const m) then
            let th = num_CONV m in
            let thm = (neqconv n (rand(concl th))) in
                SUBST [SYM th,mv] (mk_pat n) thm else
       let m' = rand m in
       if (n=m') then INST [n,nv] rth else
       if (is_const n) then
           if (n="0") then INST [m',nv] lz else
           let th = num_CONV n in
           let n' = rand(rand(concl th)) in
           let th2 = MP (INST [n',nv;m',mv] lmth) (neqconv n' m') in
               SUBST [SYM th,nv] (mk_pat2 m) th2 else
       let n' = rand n in
           MP (INST [n',nv;m',mv] lmth) (neqconv n' m') in
    \tm. (let n,m = (checkty # I) (dest_eq tm) in
          if (n=m) then EQT_INTRO (REFL n) else
          let nint = val n and mint = val m in
          if (mint=nint) then EQT_INTRO(eqconv n m) else
          if (nint<mint) then
             let thm = INST [n,nv;m,mv] lnth in
                 EQF_INTRO (MP thm (neqconv n m)) else
             let thm = INST [m,nv;n,mv] lnth in
             let thm2 = MP thm (neqconv m n) in
                 EQF_INTRO(NOT_EQ_SYM thm2)) ?
         failwith `num_EQ_CONV`;;


% --------------------------------------------------------------------- %
% EXISTS_LEAST_CONV: applies the well-ordering property to non-empty    %
% sets of numbers specified by predicates.                              %
%                                                                       %
% A call to EXISTS_LEAST_CONV "?n:num. P[n]" returns:                   %
%                                                                       %
%   |- (?n. P[n]) = ?n. P[n] /\ !n'. (n' < n) ==> ~P[n']                %
%                                                                       %
% --------------------------------------------------------------------- %

let EXISTS_LEAST_CONV =
    let wop = theorem `arithmetic` `WOP` in
    let wth = CONV_RULE (ONCE_DEPTH_CONV ETA_CONV) wop in
    let check = let ty = ":num" in assert (\tm. type_of tm = ty) in
    let acnv = RAND_CONV o ABS_CONV in
    \tm. (let n,P = (check # I) (dest_exists tm) in
          let thm1 = UNDISCH (SPEC (rand tm) wth) in
          let thm2 = CONV_RULE (GEN_ALPHA_CONV n) thm1 in
          let c1,c2 = dest_comb (snd(dest_exists(concl thm2))) in
          let bth1 = RAND_CONV BETA_CONV c1 in
          let bth2 = acnv (RAND_CONV (RAND_CONV BETA_CONV)) c2 in
          let n' = variant (n. frees tm) n in
          let abth2 = CONV_RULE (RAND_CONV (GEN_ALPHA_CONV n')) bth2 in
          let thm3 = EXISTS_EQ n (MK_COMB(bth1,abth2)) in
          let imp1 = DISCH tm (EQ_MP thm3 thm2) in
          let eltm = rand(concl thm3) in
          let thm4 = CONJUNCT1 (ASSUME (snd(dest_exists eltm))) in
          let thm5 = CHOOSE (n,ASSUME eltm) (EXISTS (tm,n) thm4) in
              IMP_ANTISYM_RULE imp1 (DISCH eltm thm5)) ?
         failwith `EXISTS_LEAST_CONV`;;

%---------------------------------------------------------------------------%
% EXISTS_GREATEST_CONV - Proves existence of greatest element satisfying P. %
%                                                                           %
% EXISTS_GREATEST_CONV "(?x. P[x]) /\ (?y. !z. z > y ==> ~(P[z]))" =        %
%    |- (?x. P[x]) /\ (?y. !z. z > y ==> ~(P[z])) =                         %
%        ?x. P[x] /\ !z. z > x ==> ~(P[z])                                  %
%                                                                           %
% If the variables x and z are the same, the "z" instance will be primed.   %
% [JRH 91.07.17]                                                            %
%---------------------------------------------------------------------------%

let EXISTS_GREATEST_CONV =
  let LESS_EQ' = theorem `arithmetic` `LESS_EQ`
  and LESS_EQUAL_ANTISYM' = theorem `arithmetic` `LESS_EQUAL_ANTISYM`
  and NOT_LESS' = theorem `arithmetic` `NOT_LESS`
  and LESS_SUC_REFL' = theorem `prim_rec` `LESS_SUC_REFL`
  and LESS_0_CASES' = theorem `arithmetic` `LESS_0_CASES`
  and NOT_LESS_0' = theorem `prim_rec` `NOT_LESS_0`
  and num_CASES' = theorem `arithmetic` `num_CASES`
  and GREATER' = definition `arithmetic` `GREATER` in
  let EXISTS_GREATEST = PROVE
   ("!P.(?x. P x) /\ (?x. !y. y > x ==> ~P y) = ?x. P x /\ !y. y > x ==> ~P y",
    GEN_TAC THEN EQ_TAC THENL
     [REWRITE_TAC[GREATER'] THEN DISCH_THEN (CONJUNCTS_THEN2 STRIP_ASSUME_TAC
      (X_CHOOSE_THEN "g:num" MP_TAC o CONV_RULE EXISTS_LEAST_CONV)) THEN
      DISCH_THEN (\th. EXISTS_TAC "g:num" THEN REWRITE_TAC[th] THEN MP_TAC th)
      THEN STRUCT_CASES_TAC (SPEC "g:num" num_CASES') THENL
       [REWRITE_TAC[NOT_LESS_0'] THEN DISCH_THEN (MP_TAC o SPEC "x:num") THEN
        DISJ_CASES_TAC (SPEC "x:num" LESS_0_CASES');
        POP_ASSUM (K ALL_TAC) THEN DISCH_THEN (CONJUNCTS_THEN2
        (MP_TAC o REWRITE_RULE[] o CONV_RULE (ONCE_DEPTH_CONV CONTRAPOS_CONV))
        (X_CHOOSE_TAC "y:num" o REWRITE_RULE[NOT_IMP] o CONV_RULE
        NOT_FORALL_CONV o REWRITE_RULE[LESS_SUC_REFL'] o SPEC "n:num")) THEN
        DISCH_THEN (MP_TAC o SPEC "y:num") THEN ASM_REWRITE_TAC[NOT_LESS'] THEN
        POP_ASSUM (CONJUNCTS_THEN2 (\th. DISCH_THEN (SUBST1_TAC o MATCH_MP
        LESS_EQUAL_ANTISYM' o CONJ (REWRITE_RULE[LESS_EQ'] th))) ASSUME_TAC)];
      DISCH_THEN CHOOSE_TAC THEN CONJ_TAC THEN EXISTS_TAC "x:num"]
    THEN ASM_REWRITE_TAC[]) in
 let t = RATOR_CONV and n = RAND_CONV and b = ABS_CONV in
 let red1 = t o n o t o n o n o b and red2 = t o n o n o n o b o n o b o n o n
 and red3 = n o n o b o t o n and red4 = n o n o b o n o n o b o n o n in
 \tm. (let (lc,rc) = dest_conj tm in let pred = rand lc in
       let (xv,xb) = dest_exists lc in let (yv,yb) = dest_exists rc in
       let zv = fst (dest_forall yb) in
       let prealpha = CONV_RULE (red1 BETA_CONV THENC red2 BETA_CONV THENC
          red3 BETA_CONV THENC red4 BETA_CONV) (SPEC pred EXISTS_GREATEST) in
       let rqd = mk_eq(tm,mk_exists(xv,mk_conj(xb,subst[(xv,yv)] yb))) in
       S (C EQ_MP) (C ALPHA rqd o concl) prealpha)
      ? failwith `EXISTS_GREATEST_CONV`;;

%---------------------------------------------------------------------------%
% A couple of useful function for converting between  ML integers and 	    %
% numeric terms, e.g., "2" <---> 2  					    %
%---------------------------------------------------------------------------%

let term_of_int =  
      \n. mk_const(string_of_int n, mk_type(`num`,[])) ;;

let int_of_term = int_of_string o fst o dest_const ;;