hol88-contrib-source 2.02.19940316-35 / usr / share / hol88-2.02.19940316 / contrib / Tarski / recbool.ml

This file is indexed.

/usr/share/hol88-2.02.19940316/contrib/Tarski/recbool.ml is in hol88-contrib-source 2.02.19940316-35.

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
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
%----- -*- Emacs Mode: fundamental -*- -------------------------------

  File:		recbool.ml

  Authors:	(c) Flemming Andersen & Kim Dam Petersen
  Date:		26/7-1991.
  Last Updated:	29/10-1992.

  Description:
		Defines operations for constructing recursive predicates.
  Dependicies:
		tarski
  Usage:
		loadt`recbool`;;
---------------------------------------------------------------------%

loadt`curry`;;
loadt`tarski`;;

let FORALL_PAIR_EQ = TAC_PROOF(([],
  "(!P. (!p. P p) = (!(x:*) (y:**). P (x,y)))"),
  GEN_TAC THEN
  EQ_TAC THEN REPEAT STRIP_TAC THENL
  [ ASM_REWRITE_TAC[]
  ; POP_ASSUM(\thm.
      ACCEPT_TAC (ONCE_REWRITE_RULE[PAIR]
         (SPECL["FST(p:*#**)";"SND(p:*#**)"]thm)))
  ]);;

%<
  FORALL_PAIR_CONV "(x1:*,..,xn:*n)" "!(p:*#...#*n). P p" -->
     |- (!(p:*#...#*n). P p) = (!(x1:*) ... (xn:*n). P(x1,...,xn))
>%
let FORALL_PAIR_CONV xp tm =
  let
    (p,Pp) = dest_forall tm and
    xv = strip_pair xp
  in letrec pairs xp =
    if is_pair xp then
      ((\p. "FST ^p") .
       (map (\fn p. fn "SND ^p") (pairs (snd(dest_pair xp)))))
    else
      [\p. p]
  in let
    thm1 = DISCH_ALL(GENL xv (SPEC xp (ASSUME tm)))
  in let
    thm2 = DISCH_ALL (PURE_REWRITE_RULE[PAIR](GEN p (SPECL 
      (map (\fn. fn p) (pairs xp))
      (ASSUME (list_mk_forall (xv, (subst[(xp,p)]Pp)))))))
  in
    if is_pair xp then
      IMP_ANTISYM_RULE thm1 thm2
    else
      failwith `FORALL_PAIR_CONV`;;

%<
  EquationToAbstraction "!x1 ... xn. f (x1,...,xn) = t"
                     --> "\f (x1,...,xn). t"
>%
let EquationToAbstraction =
  set_fail_prefix `EquationToAbstraction`
  (\tm.
     let
       (fxv, t) = dest_eq (snd(strip_forall tm))
     in let
       (f,xv)   = strip_comb fxv
     in
       mk_abs (f, list_mk_uncurry_abs (xv,t)));;

%<
   PURE_CONV conv tm --> if conv tm = |- tm = tm then fail
>%
let PURE_CONV conv =
  set_fail_prefix `PURE_CONV`
  (\tm.
    let thm = conv tm
    in
       if aconv tm (concl thm) then fail`identity conversion`
       else thm);;
%<
  MonoThmToTactic mono_thm --> Initial tactic

>%
let MonoThmToTactic eqn =
  let
    xp = snd(dest_comb(fst(dest_eq(eqn))))
  in
    (REWRITE_TAC[IsMono;Leq] THEN
     BETA_TAC THEN
     CONV_TAC(DEPTH_CONV (FORALL_PAIR_CONV xp)) THEN
     UNCURRY_BETA_TAC);;
    
%<
  CurryEquationToAbstraction "!x1 ... xn. f x1 ... xn = t"
                     --> "\f'. (\f (x1,...,xn). t)(\x1 ... xn. g(x1,...,xn))"
>%
let CurryEquationToAbstraction =
  set_fail_prefix `NewEquationToAbstraction`
  (\tm.
     let    (fxv, t) = dest_eq (snd(strip_forall tm))
     in let (f,xv)   = strip_comb fxv
     in let tpg      = type_of(list_mk_pair xv)
     in let g = variant (frees t)
                   (mk_var(fst(dest_var f),
                           mk_type(`fun`,[tpg;":bool"])))
     in let fabs = mk_abs(f, mk_uncurry_abs (list_mk_pair xv,t)) and
            gabs = list_mk_abs(xv, mk_comb(g,list_mk_pair xv))
     in
       mk_abs (g, mk_comb(fabs, gabs)));;

%<
  set_monotonic_goal "f (x1,...,xn) = Body[f,x1,...,xn]" -->
    set_goal([],"IsMono (\f. \(x1,...,xn). Body[f,x1,...,xn])")
>%

let set_monotonic_goal =
  set_fail_prefix `set_monotonic_goal`
  (\tm.
    let
      tm' = "IsMono ^(EquationToAbstraction tm)"
    in
      (set_goal([],tm');
       e(MonoThmToTactic tm)));;

%<       e(REWRITE_TAC[IsMono;Leq])));; >%

%<
  curry_set_monotonic_goal "f (x1,...,xn) = Body[f,x1,...,xn]" -->
    curry_set_goal([],"IsMono (\f. \(x1,...,xn). Body[f,x1,...,xn])")
>%

let curry_set_monotonic_goal =
  set_fail_prefix `curry_set_monotonic_goal`
  (\tm.
    let
      tm' = "IsMono ^(CurryEquationToAbstraction tm)" and
      xp = list_mk_pair(snd(strip_comb(fst(dest_eq (snd(strip_forall tm))))))
    in
      (set_goal([],tm');
       e(REWRITE_TAC[IsMono;Leq] THEN
         BETA_TAC THEN
         BETA_TAC THEN
         CONV_TAC (DEPTH_CONV UNCURRY_BETA_CONV) THEN
         CONV_TAC (DEPTH_CONV (FORALL_PAIR_CONV xp)) THEN
         CONV_TAC (DEPTH_CONV UNCURRY_BETA_CONV) )));;

%<
  prove_monotonic_thm "f (x1,...,xn) = Body[f,x1,...,xn]" tactic -->
    |- IsMono (\f. \(x1,...,xn). Body[f,x1,...,xn])
>%

let prove_monotonic_thm =
  set_fail_prefix `prove_monotonic_thm`
  (\ (str,tm,tactic). 
    let
      tm' = "IsMono ^(EquationToAbstraction tm)"
    in
      (prove_thm(str, tm', (MonoThmToTactic tm THEN tactic))));;

%<
  new_min_recursive_relation_definition name
       |- IsMono (\f. \(x1,...,xn). Body[f,x1,...,xn]) -->
    |- f = MinFix (\f. \(x1,...,xn). Body[f,x1,...,xn])
>%

let new_min_recursive_relation_definition =
  set_fail_prefix `new_min_recursive_relation_definition`
  (\(name,mono).
     let
       (r,a) = dest_abs(snd(dest_comb(snd(dest_thm mono))))
     in let
       b     = mk_abs (r,a)
     in
       new_definition (name, "^r = MinFix ^b"));;

%<
  new_max_recursive_relation_definition name
       |- IsMono (\f. \(x1,...,xn). Body[f,x1,...,xn]) -->
    |- f = MaxFix (\f. \(x1,...,xn). Body[f,x1,...,xn])
>%

let new_max_recursive_relation_definition =
  set_fail_prefix `new_max_recursive_relation_definition`
  (\(name,mono).
     let
       (r,a) = dest_abs(snd(dest_comb(snd(dest_thm mono))))
     in let
       b     = mk_abs (r,a)
     in
       new_definition (name, "^r = MaxFix ^b"));;

%<
  prove_fix_thm
       fail_str
       FixEQThm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_fix_thm fail_str FixEQThm =
  set_fail_prefix fail_str
  (\ (name,def,mono). 
    let
      thm= BETA_RULE(ONCE_REWRITE_RULE[SYM def](MATCH_MP FixEQThm mono))
    in let
      x = fst(dest_uncurry_abs(fst(dest_eq(snd(dest_thm thm)))))
    in let
      thm = AP_THM thm x
    in letrec
      curry_beta_rule (x,thm) =
        if is_pair x then
          curry_beta_rule
           (snd(dest_pair x),
            BETA_RULE(PURE_ONCE_REWRITE_RULE[UNCURRY_DEF]thm))
        else
          BETA_RULE(PURE_ONCE_REWRITE_RULE[UNCURRY_DEF]thm)
    in
      save_thm(name, GEN_ALL(SYM(curry_beta_rule(x,thm)))));;

%<
  prove_min_fix_thm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_min_fix_thm =
 prove_fix_thm `prove_min_fix_thm` MinFixEQThm;;

%<
  prove_max_fix_thm
       name
       (|- f = MaxFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_max_fix_thm =
 prove_fix_thm `prove_max_fix_thm` MaxFixEQThm;;

%<
  prove_min_min_thm name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !R. ((\ (x1,...,xn). Body[R]) = R) ==>
             (!x1 ... xn. f (x1,...,xn) = R(x1,...,xn))   
>%
let prove_min_min_thm =
  set_fail_prefix `prove_min_min_thm`
  (\ (name,def,mono). 
    let Fn = el 1 (snd (strip_comb (concl mono))) in
    let
      thm1 = BETA_RULE(ONCE_REWRITE_RULE[SYM def]
                (ISPEC Fn Min_MinFixThm))
    in let
      thm2 = ONCE_REWRITE_RULE[Leq]thm1
    in let
      x = el 2 (fst(strip_uncurry_abs
                 (snd(dest_comb(snd(dest_eq(snd(dest_thm def))))))))
    in letrec rule (x,thm) =
         if is_pair x then
            rule(snd(dest_pair x),
                 BETA_RULE(ONCE_REWRITE_RULE[UNCURRY_DEF]
                   (CONV_RULE (DEPTH_CONV (FORALL_PAIR_CONV x)) thm)))
         else
            thm
    in
      save_thm(name, rule(x,thm2)));;

%<
  prove_max_max_thm name
       (|- f = MaxFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !R. ((\ (x1,...,xn). Body[R]) = R) ==>
             (!x1 ... xn. f (x1,...,xn) = R(x1,...,xn))   
>%
let prove_max_max_thm =
  set_fail_prefix `prove_max_max_thm`
  (\ (name,def,mono). 
    let Fn = el 1 (snd (strip_comb (concl mono))) in
    let
      thm1 = BETA_RULE(ONCE_REWRITE_RULE[SYM def]
                        (ISPEC Fn Max_MaxFixThm))
    in let
      thm2 = ONCE_REWRITE_RULE[Leq]thm1
    in let
      x = el 2 (fst(strip_uncurry_abs
                 (snd(dest_comb(snd(dest_eq(snd(dest_thm def))))))))
    in letrec rule (x,thm) =
         if is_pair x then
            rule(snd(dest_pair x),
                 BETA_RULE(ONCE_REWRITE_RULE[UNCURRY_DEF]
                   (CONV_RULE (DEPTH_CONV (FORALL_PAIR_CONV x)) thm)))
         else
            thm
    in
      save_thm(name, rule(x,thm2)));;

let OR_IMP = TAC_PROOF(([],
  "!t1 t2 t. ((t1 \/ t2) ==> t) = ((t1 ==> t) /\ (t2 ==> t))"),
  REPEAT GEN_TAC THEN
  EQ_TAC THEN REPEAT STRIP_TAC THEN
  RES_TAC);;

%<
   FORALL_CONJ_CONV "!x1 ... xn. P1 /\ ... /\ Pm" -->
     |- (!x1...xn. P1  /\ ... /\ Pm) =
        (!x1...xk1. P1) /\ ... /\ (!x1...xkm. Pm)
   , where x1...xki = intersect [x1...xn] (frees Pi)
>%

let FORALL_CONJ_CONV tm =
  letrec
     conjs tm =
       if can dest_conj tm then
          (let (x,tm') = dest_conj tm in (x.(conjs tm')))
       else
          [tm]
  in let
    (xv,PC) = strip_forall tm
  in let
    Pv      = conjs PC
  in if (length Pv) < 2 or (length xv) < 1 then
            failwith `FORALL_CONJ_CONV` else
  let
    fPv     = map (\tm. intersect xv (frees tm)) Pv
  in let
    thm1 = LIST_CONJ (map
                       (\ (fv,thm). GENL fv thm)
                       (combine (fPv,
                          (CONJ_LIST (length Pv) (SPECL xv (ASSUME tm)))))) and
    thm2 = GENL xv (LIST_CONJ(map (\ (fv,thm). SPECL fv thm)
     (combine (fPv,
       (CONJ_LIST (length Pv) (ASSUME (list_mk_conj
         (map (\ (fv,tm). list_mk_forall(fv,tm)) (combine (fPv,Pv))))))))))
  in
   IMP_ANTISYM_RULE (DISCH_ALL thm1) (DISCH_ALL thm2);;


%<
  prove_intro_thm
       fail_str
       IntroThm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_intro_thm fail_str IntroThm =
  set_fail_prefix fail_str
  (\ (name,def,mono). 
    let Fn = el 1 (snd (strip_comb (concl mono))) in
    let
      thm1 = ONCE_REWRITE_RULE [mono] (BETA_RULE(ONCE_REWRITE_RULE[SYM def]
               (ISPEC Fn IntroThm)))
    in let
      thm2 = REWRITE_RULE[Leq]thm1
    in let
      x = el 2 (fst(strip_uncurry_abs
                 (snd(dest_comb(snd(dest_eq(snd(dest_thm def))))))))
    in letrec rule (x,thm) =
         if is_pair x then
            rule(snd(dest_pair x),
                 BETA_RULE(ONCE_REWRITE_RULE[UNCURRY_DEF]
                   (CONV_RULE (DEPTH_CONV (FORALL_PAIR_CONV x)) thm)))
         else
            thm
    in let
      thm3 = PURE_REWRITE_RULE[OR_IMP](rule(x,thm2))
    in let
      thm4 = CONV_RULE (DEPTH_CONV FORALL_CONJ_CONV) thm3
    in let
      thm5 = BETA_RULE (REWRITE_RULE[And;Or]thm4)
    in
      save_thm(name, thm5));;

%<
  prove_min_intro_thm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_min_intro_thm =
  prove_intro_thm `prove_min_intro_thm` MinFixIntroductThm;;

%<
  prove_extended_min_intro_thm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%

let prove_extended_min_intro_thm =
  prove_intro_thm `prove_extended_min_intro_thm` ExtMinFixIntroductThm;;

%<
  prove_max_intro_thm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_max_intro_thm =
  prove_intro_thm `prove_max_intro_thm` MaxFixIntroductThm;;

%<
  prove_extended_max_intro_thm
       name
       (|- f = MinFix (\f. \ (x1,...,xn). Body[f,x1,...,xn]))
       (|- IsMono (\f...))
    |- !x1 ... xn. f (x1,...,xn) = Body[f,x1,...,xn]
>%
let prove_extended_max_intro_thm =
  prove_intro_thm `prove_extended_max_intro_thm` ExtMaxFixIntroductThm;;

APT Browse - Built by Thomas Orozco.