← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2007/gordon/support/PureLisp.ml

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2007/gordon/support/PureLisp.ml
 
1
(*****************************************************************************)
 
2
(* Relational and clocked semantics of Pure Lisp                             *)
 
3
(*****************************************************************************)
 
4
 
 
5
quietdec := true;
 
6
map 
 
7
 load 
 
8
 ["stringLib","finite_mapTheory","intLib"];
 
9
open sumTheory finite_mapTheory pred_setTheory optionTheory;
 
10
Globals.checking_const_names := false;
 
11
set_trace "Subgoal number" 1000;
 
12
quietdec := false;
 
13
 
 
14
(******************************************************************************
 
15
* Set default parsing to natural numbers rather than integers 
 
16
******************************************************************************)
 
17
val _ = intLib.deprecate_int();
 
18
 
 
19
(*****************************************************************************)
 
20
(* Start new theory "PureLISP"                                               *)
 
21
(*****************************************************************************)
 
22
val _ = new_theory "PureLISP";
 
23
 
 
24
(*****************************************************************************)
 
25
(* An atom is Nil or a number or a string                                    *)
 
26
(*****************************************************************************)
 
27
val _ =
 
28
 Hol_datatype
 
29
  `atom = Nil | Number of num | String of string`;
 
30
 
 
31
(*****************************************************************************)
 
32
(* An S-expression is an atom or a dotted pair (cons-cell)                   *)
 
33
(*****************************************************************************)
 
34
val _ =
 
35
 Hol_datatype
 
36
  `sexpression = A of atom | Cons of sexpression => sexpression`;
 
37
 
 
38
(*****************************************************************************)
 
39
(* Printing utilities                                                        *)
 
40
(*****************************************************************************)
 
41
val int_of_term = numSyntax.int_of_term;
 
42
 
 
43
fun strip_quotes s = implode(tl(butlast(explode s)));
 
44
 
 
45
fun isCons tm =
 
46
 is_comb tm andalso is_comb(rator tm)
 
47
            andalso is_const(rator(rator tm))
 
48
            andalso (fst(dest_const(rator(rator tm)))) = "Cons";
 
49
 
 
50
fun isAtom tm =
 
51
 is_comb tm andalso is_const(rator tm)
 
52
            andalso fst(dest_const(rator tm)) = "A";
 
53
 
 
54
fun isNil tm =
 
55
 isAtom tm andalso rand tm = ``Nil``;
 
56
 
 
57
fun isSing tm =
 
58
 isCons tm andalso isNil(rand tm);
 
59
 
 
60
fun isList tm =
 
61
 isCons tm andalso (isNil(rand tm) orelse isList(rand tm));
 
62
 
 
63
val Split_def =
 
64
 Define
 
65
  `(Split(A _) = [])
 
66
   /\
 
67
   (Split(Cons e1 e2) = e1 :: Split e2)`;
 
68
 
 
69
(*****************************************************************************)
 
70
(* Some utility values and functions                                         *)
 
71
(*****************************************************************************)
 
72
val Num_def =
 
73
 Define
 
74
  `Num n = A(Number n)`;
 
75
 
 
76
val False_def =
 
77
 Define
 
78
  `False = A Nil`;
 
79
 
 
80
val isTrue_def =
 
81
 Define
 
82
  `isTrue s = ~(s = False)`;
 
83
 
 
84
val True_def =
 
85
 Define
 
86
  `True = A(String "T")`;
 
87
 
 
88
val Car_def =
 
89
 Define
 
90
  `Car(Cons s1 s2) = s1`;
 
91
 
 
92
val Cdr_def =
 
93
 Define
 
94
  `Cdr(Cons s1 s2) = s2`;
 
95
 
 
96
val List_def = 
 
97
 Define 
 
98
  `(List [] = A Nil) /\
 
99
   (List (s::sl) = Cons s (List sl))`;
 
100
 
 
101
val isList_def =
 
102
 Define
 
103
  `(isList (A a) = (a = Nil))
 
104
   /\
 
105
   (isList (Cons s1 s2) = isList s2)`;
 
106
 
 
107
val ListListEq =
 
108
 store_thm
 
109
  ("ListListEq",
 
110
   ``!sl1 sl2. (List sl1 = List sl2) = (sl1 = sl2)``,
 
111
   Induct 
 
112
    THEN RW_TAC list_ss [List_def]
 
113
    THENL
 
114
     [Induct_on `sl2`
 
115
       THEN RW_TAC list_ss [List_def],
 
116
      EQ_TAC
 
117
       THEN RW_TAC list_ss [List_def]
 
118
       THENL
 
119
        [Induct_on `sl2`
 
120
          THEN RW_TAC list_ss [List_def],
 
121
         METIS_TAC[List_def]]]);
 
122
 
 
123
val SplitList =
 
124
 store_thm
 
125
  ("SplitList",
 
126
   ``!sl. Split(List sl) = sl``,
 
127
   Induct
 
128
    THEN RW_TAC std_ss [Split_def,List_def]);
 
129
 
 
130
val ListSplit =
 
131
 store_thm
 
132
  ("ListSplit",
 
133
   ``!s. isList s ==> (List(Split s) = s)``,
 
134
   Induct
 
135
    THEN RW_TAC std_ss [Split_def,List_def,isList_def]);
 
136
 
 
137
val Eq_def =
 
138
 Define
 
139
  `Eq ((A a1),(A a2)) = if a1 = a2 then True else False`;
 
140
 
 
141
val Atom_def =
 
142
 Define
 
143
  `(Atom (A a) = True)
 
144
   /\
 
145
   (Atom _ = False)`;
 
146
 
 
147
val Add_def =
 
148
 Define
 
149
  `Add ((A(Number m)),(A(Number n))) = A(Number(m+n))`;
 
150
 
 
151
val Add1_def =
 
152
 Define
 
153
  `Add1 (A(Number m)) = A(Number(m+1))`;
 
154
 
 
155
val Sub_def =
 
156
 Define
 
157
  `Sub ((A(Number m)),(A(Number n))) = A(Number(m-n))`;
 
158
 
 
159
val Sub1_def =
 
160
 Define
 
161
  `Sub1 (A(Number m)) = A(Number(m-1))`;
 
162
 
 
163
val Mult_def =
 
164
 Define
 
165
  `Mult ((A(Number m)),(A(Number n))) = A(Number(m*n))`;
 
166
 
 
167
val FunConSem_def =
 
168
 Define
 
169
  `FunConSem s sl =
 
170
    if s = "car"  then Car(EL 0 sl)            else
 
171
    if s = "cdr"  then Cdr(EL 0 sl)            else 
 
172
    if s = "atom" then Atom(EL 0 sl)           else 
 
173
    if s = "eq"   then Eq(EL 0 sl,EL 1 sl)     else 
 
174
    if s = "cons" then Cons(EL 0 sl) (EL 1 sl) else 
 
175
    if s = "add"  then Add(EL 0 sl,EL 1 sl)    else 
 
176
    if s = "add1" then Add1(EL 0 sl)           else 
 
177
    if s = "sub"  then Sub(EL 0 sl,EL 1 sl)    else 
 
178
    if s = "sub1" then Sub1(EL 0 sl)           else 
 
179
    if s = "mult" then Mult(EL 0 sl,EL 1 sl)   else 
 
180
    ARB`;
 
181
 
 
182
(*****************************************************************************)
 
183
(* Syntax of Pure Lisp                                                       *)
 
184
(*****************************************************************************)
 
185
val _ =
 
186
 Hol_datatype
 
187
  `term = Con of sexpression
 
188
        | Var of string
 
189
        | App of func => term list
 
190
        | Ite of (term # term)list;
 
191
 
 
192
   func = FunCon of string
 
193
        | FunVar of string
 
194
        | Lambda of string list => term
 
195
        | Label  of string => func`;
 
196
 
 
197
(*****************************************************************************)
 
198
(* An environment (alist) is a finite function from names (strings) to       *)
 
199
(* values of type ``:sexpression + func`` (so variables and                  *)
 
200
(* Label-defined functions share the same namespace).                        *)
 
201
(*****************************************************************************)
 
202
 
 
203
(*****************************************************************************)
 
204
(* VarBind a xl sl extends a by binding each string in xl to the             *)
 
205
(* S-expression at the corresponding position in sl. If xl is shorter than   *)
 
206
(* sl, then only the first n elements of sl are used, where n is the         *)
 
207
(* length of x. If xl is longer than sl, than sl is padded with NILs.        *)
 
208
(*                                                                           *)
 
209
(* Subtle point: with the semantics in which clock timeout returns NONE      *)
 
210
(* having VarBind  only partially specified is no problem, but               *)
 
211
(* with the semantics in which timeout returns an S-expression it is         *)
 
212
(* tricky to distinguish the arbitrary value returned when VarBind is        *)
 
213
(* applied to lists of different lists from a real value.                    *)
 
214
(* We thus totalise VarBind as described above.                              *)
 
215
(*****************************************************************************)
 
216
val VarBind_def =
 
217
 Define
 
218
  `(VarBind a [] sl = (a : (string |-> sexpression + func)))
 
219
   /\
 
220
   (VarBind a (x::xl) [] = (VarBind a xl []) |+ (x, INL(A Nil)))
 
221
   /\
 
222
   (VarBind a (x::xl) (s::sl) = (VarBind a xl sl) |+ (x, INL s))`;
 
223
 
 
224
(*****************************************************************************)
 
225
(* FunBind a f fn extends a by binding fn to f                               *)
 
226
(*****************************************************************************)
 
227
val FunBind_def =
 
228
 Define
 
229
  `FunBind (a:string|->sexpression+func) f fn = a |+ (f, INR fn)`;
 
230
 
 
231
(*****************************************************************************)
 
232
(* Operational semantics of Pure Lisp using three inductive relations:       *)
 
233
(*                                                                           *)
 
234
(*  R_ap (fn,args,a) s - fn applied to args evaluates to s with alist a      *)
 
235
(*  R_ev (e,a) s        - term e evaluates to S-expression s with alist a    *)
 
236
(*  R_evl (el,a) sl     - term list el evaluates to S-expression list sl     *)
 
237
(*                                                                           *)
 
238
(* The names R_evl_rules, R_evl_ind, R_evl_cases are the ones                *)
 
239
(* automatically generated to name the theorems in the theory.               *)
 
240
(*                                                                           *)
 
241
(*****************************************************************************)
 
242
val (R_ap_rules,R_ap_ind,R_ap_cases) =
 
243
 Hol_reln
 
244
 `(!fc args a.
 
245
    R_ap (FunCon fc,args,a) (FunConSem fc args))
 
246
  /\
 
247
  (!fv args s a.
 
248
    R_ap (OUTR(a ' fv),args,a) s ==> R_ap (FunVar fv,args,a) s)
 
249
  /\
 
250
  (!xl e args s a.
 
251
    R_ev (e,VarBind a xl args) s 
 
252
     ==> R_ap (Lambda xl e,args,a) s)
 
253
  /\
 
254
  (!x fn args s a. 
 
255
    R_ap (fn,args,FunBind a x fn) s ==> R_ap(Label x fn,args,a) s)
 
256
  /\
 
257
  (!s a. 
 
258
    R_ev (Con s, a) s)
 
259
  /\
 
260
  (!x a. 
 
261
    R_ev (Var x, a) (OUTL(a ' x)))
 
262
  /\
 
263
  (!a.
 
264
    R_ev (Ite [], a) False)
 
265
  /\
 
266
  (!e1 e2 el s a. 
 
267
    R_ev (e1,a) False /\ R_ev (Ite el,a) s
 
268
    ==> R_ev (Ite ((e1,e2)::el),a) s)
 
269
  /\
 
270
  (!e1 e2 el s1 s a.
 
271
    R_ev (e1,a) s1 /\ isTrue s1 /\ R_ev (e2,a) s 
 
272
    ==>
 
273
    R_ev (Ite ((e1,e2)::el),a) s)
 
274
  /\
 
275
  (!fn el args s a. 
 
276
    R_evl (el,a) args /\ R_ap (fn,args,a) s
 
277
    ==> R_ev (App fn el,a) s)
 
278
  /\
 
279
  (!a.
 
280
    R_evl ([],a) [])
 
281
  /\
 
282
  (!e el s sl a.
 
283
    R_ev (e,a) s /\ R_evl (el,a) sl
 
284
    ==> R_evl (e::el,a) (s::sl))`;
 
285
 
 
286
val EvalquoteR_def =
 
287
 Define
 
288
  `EvalquoteR (fn,args) s = R_ap (fn,args,FEMPTY) s`;
 
289
 
 
290
(* Test example
 
291
computeLib.add_funs[FAPPLY_FUPDATE_THM];
 
292
computeLib.add_funs[FUPDATE_LIST_THM];
 
293
computeLib.add_funs[OUTL];
 
294
computeLib.add_funs[OUTR];
 
295
 
 
296
val Fact_def =
 
297
 Define
 
298
 `Fact =
 
299
   Label "fact"
 
300
    (Lambda ["n"]
 
301
       (Ite
 
302
          [(App (FunCon "eq") [Var "n"; Con (Num 0)],
 
303
            Con (Num 1));
 
304
           (Con True,
 
305
            App (FunCon "mult")
 
306
              [Var "n"; App (FunVar "fact") [App (FunCon "sub1") [Var "n"]]])]))`;
 
307
 
 
308
evalquote ``Fact`` ``[Num 6]``;
 
309
 
 
310
evalquote ``FunCon "car"`` ``[Cons x y]``;
 
311
evalquote ``FunCon "cdr"`` ``[Cons x y]``;
 
312
*)
 
313
 
 
314
(*****************************************************************************)
 
315
(* Encode options in S-expressions                                           *)
 
316
(*****************************************************************************)
 
317
 
 
318
val none_def =
 
319
 Define
 
320
  `none = A(String "NONE")`;
 
321
 
 
322
val some_def =
 
323
 Define
 
324
  `some s = Cons s (A Nil)`;
 
325
 
 
326
val issome_def =
 
327
 Define
 
328
  `(issome (Cons s0 s1) = (s1 = A Nil))
 
329
   /\
 
330
   (issome _ = F)`;
 
331
 
 
332
val somesomeEq =
 
333
 store_thm
 
334
 ("somesomeEq",
 
335
  ``(some s1 = some s2) = (s1 = s2)``,
 
336
  RW_TAC std_ss [DB.theorem "sexpression_11",some_def]);
 
337
 
 
338
val ListsomeEq =
 
339
 store_thm
 
340
 ("ListsomeEq",
 
341
  ``(List(s1::sl1) = Cons s2 (List sl2)) = (s1 = s2) /\ (sl1 = sl2)``,
 
342
  RW_TAC std_ss [DB.theorem "sexpression_11",some_def,List_def,ListListEq]);
 
343
 
 
344
val issomenone =
 
345
 store_thm
 
346
  ("issomenone",
 
347
   ``~(issome none) /\ ~(issome(A a)) /\ (issome s ==> ~(s = none))``,
 
348
   CONV_TAC EVAL
 
349
    THEN Cases_on `s`
 
350
    THEN RW_TAC std_ss [issome_def]);
 
351
 
 
352
val issomesome =
 
353
 store_thm
 
354
  ("issomesome",
 
355
   ``issome(some s)``,
 
356
   CONV_TAC EVAL);
 
357
 
 
358
val issomeExists =
 
359
 store_thm
 
360
  ("issomeExists",
 
361
   ``!x. issome x = ?s. x = some s``,
 
362
   Cases
 
363
    THEN RW_TAC std_ss [issome_def,some_def]);
 
364
 
 
365
val someNotEqnone =
 
366
 store_thm
 
367
  ("someNotEqnone",
 
368
   ``~(some s = none) /\ ~(none = some s)``,
 
369
   CONV_TAC EVAL);
 
370
 
 
371
val noneNONE =
 
372
 store_thm
 
373
  ("noneNONE",
 
374
   ``((A a = none) = (a = String "NONE")) 
 
375
     /\ 
 
376
     ((none = A a) = (a = String "NONE"))``,
 
377
   CONV_TAC EVAL
 
378
    THEN METIS_TAC[]);
 
379
 
 
380
val the_def =
 
381
 Define
 
382
  `the s = Car s`;
 
383
 
 
384
val thesome =
 
385
 store_thm
 
386
  ("thesome",
 
387
   ``the(some s) = s``,
 
388
   CONV_TAC EVAL);
 
389
 
 
390
val apply_c_def =
 
391
 tDefine
 
392
  "apply_c"
 
393
  `(apply_c n (fn,args,a) =
 
394
     if n=0 
 
395
      then none
 
396
      else case fn of
 
397
              FunCon fc   -> some(FunConSem fc args)
 
398
           || FunVar fv   -> apply_c (n-1) (OUTR(a ' fv),args,a)
 
399
           || Lambda xl e -> eval_c (n-1) (e,VarBind a xl args)
 
400
           || Label x fn  -> apply_c (n-1) (fn,args,FunBind a x fn))
 
401
   /\
 
402
   (eval_c n (e,a) =
 
403
     if n=0
 
404
      then none
 
405
      else case e of
 
406
              Con s              -> some s
 
407
           || Var v              -> some(OUTL(a ' v))
 
408
           || Ite []             -> some False
 
409
           || Ite ((e1,e2)::eel) -> (let s = eval_c (n-1) (e1,a) in
 
410
                                     if s = none
 
411
                                      then none
 
412
                                      else if the s = False
 
413
                                            then eval_c (n-1) (Ite eel,a)
 
414
                                            else eval_c (n-1) (e2,a))
 
415
           || App fn el          -> let sl = evlis_c (n-1) (el,a) in
 
416
                                     if  sl = none
 
417
                                      then none
 
418
                                      else apply_c (n-1) (fn,Split(the sl),a))
 
419
   /\
 
420
   (evlis_c n (el,a) =
 
421
     if n=0 
 
422
      then none
 
423
      else if NULL el
 
424
            then some(List[])
 
425
            else let s = eval_c (n-1) (HD el,a) in
 
426
                 if s = none
 
427
                  then none 
 
428
                  else let sl = evlis_c (n-1) (TL el, a) in
 
429
                       if sl = none then none else some(Cons (the s) (the sl)))`
 
430
 (WF_REL_TAC
 
431
   `measure 
 
432
     \x. if ISL x 
 
433
          then FST(OUTL x) else
 
434
         if ISR x /\ ISL(OUTR x) 
 
435
          then FST(OUTL(OUTR x)) 
 
436
          else FST(OUTR(OUTR x))`
 
437
    THEN RW_TAC arith_ss []);   
 
438
 
 
439
val EvalquoteEnc_def =
 
440
 Define
 
441
  `EvalquoteEnc n (fn,args) = apply_c n (fn,args,FEMPTY)`;
 
442
 
 
443
(* Factorial function
 
444
 
 
445
computeLib.add_funs[FAPPLY_FUPDATE_THM];
 
446
computeLib.add_funs[FUPDATE_LIST_THM];
 
447
computeLib.add_funs[OUTL];
 
448
computeLib.add_funs[OUTR];
 
449
 
 
450
 
 
451
val fact_tm =
 
452
 ``Label "fact"
 
453
    (Lambda ["n"]
 
454
       (Ite
 
455
          [(App (FunCon "eq") [Var "n"; Con (Num 0)],
 
456
            Con (Num 1));
 
457
           (Con True,
 
458
            App (FunCon "mult")
 
459
              [Var "n"; App (FunVar "fact") [App (FunCon "sub1") [Var "n"]]])]))`` ;
 
460
 
 
461
EVAL ``eval_c 63 (App ^fact_tm [Con(Num 1)],a)``;
 
462
 
 
463
EVAL ``eval_c 63 (App ^fact_tm [Con(Num 7)],a)``;
 
464
EVAL ``eval_c 64 (App ^fact_tm [Con(Num 7)],a)``;
 
465
 
 
466
EVAL ``EvalquoteEnc 62 (^fact_tm, [Num 7])``;
 
467
EVAL ``EvalquoteEnc 63 (^fact_tm, [Num 7])``;
 
468
 
 
469
EVAL ``EvalquoteEnc 10000 (APP Car [Cons x y])``;
 
470
*)
 
471
 
 
472
val apply_cCases =
 
473
 store_thm
 
474
  ("apply_cCases",
 
475
   ``(!fn args a. issome(apply_c n (fn,args,a)) \/ (apply_c n (fn,args,a) = none))
 
476
     /\
 
477
     (!e a. issome(eval_c n (e,a)) \/ (eval_c n (e,a) = none))
 
478
     /\
 
479
     (!el a. issome(evlis_c n (el,a)) \/ (evlis_c n (el,a) = none))``,
 
480
   Induct_on `n`
 
481
    THEN RW_TAC list_ss
 
482
          [SIMP_RULE arith_ss [] (INST[``n:num``|->``SUC n``]apply_c_def),
 
483
           SIMP_RULE arith_ss [] (INST[``n:num``|->``0``]apply_c_def),
 
484
           issomesome,someNotEqnone,LET_DEF]
 
485
    THENL
 
486
     [Cases_on `fn` 
 
487
       THEN RW_TAC std_ss [issomesome],
 
488
      Cases_on `e` 
 
489
       THEN RW_TAC std_ss [issomesome]
 
490
       THEN Induct_on `l`
 
491
       THEN RW_TAC std_ss [issomesome]
 
492
       THEN Cases_on `h`
 
493
       THEN RW_TAC std_ss [issomesome]]);
 
494
 
 
495
val apply_cCasesCor =
 
496
 store_thm
 
497
  ("apply_cCasesCor",
 
498
   ``(!fn n args a. issome(apply_c n (fn,args,a)) \/ (apply_c n (fn,args,a) = none))
 
499
     /\
 
500
     (!e n a. issome(eval_c n (e,a)) \/ (eval_c n (e,a) = none))
 
501
     /\
 
502
     (!el n a. issome(evlis_c n (el,a)) \/ (evlis_c n (el,a) = none))``,
 
503
    METIS_TAC[apply_cCases]);
 
504
 
 
505
val apply_c =
 
506
 store_thm
 
507
  ("apply_c",
 
508
   ``(apply_c 0 (fn,args,a) = none)
 
509
     /\
 
510
     (apply_c (SUC n) (FunCon fc,args,a) = some(FunConSem fc args))
 
511
     /\
 
512
     (apply_c (SUC n) (FunVar fv,args,a) = apply_c n (OUTR(a ' fv),args,a))
 
513
     /\
 
514
     (apply_c (SUC n) (Lambda xl e,args,a) = eval_c n (e,VarBind a xl args))
 
515
     /\
 
516
     (apply_c (SUC n) (Label x fn,args,a) = apply_c n (fn,args,FunBind a x fn))
 
517
     /\
 
518
     (eval_c 0 (e,a) = none)
 
519
     /\
 
520
     (eval_c (SUC n) (Con s,a) = some s)
 
521
     /\
 
522
     (eval_c (SUC n) (Var v,a) = some(OUTL(a ' v)))
 
523
     /\
 
524
     (eval_c (SUC n) (Ite [],a) = some False)
 
525
     /\
 
526
     (eval_c (SUC n) (Ite ((e1,e2)::eel),a) = 
 
527
       if issome(eval_c n (e1,a)) 
 
528
        then (if the(eval_c n (e1,a)) = False
 
529
               then eval_c n (Ite eel,a)
 
530
               else eval_c n (e2,a))
 
531
        else none)
 
532
     /\
 
533
     (eval_c (SUC n) (App fn el,a) = 
 
534
       if issome(evlis_c n (el,a)) 
 
535
        then apply_c n (fn,Split(the(evlis_c n (el,a))),a)
 
536
        else none)
 
537
     /\
 
538
     (evlis_c 0 (el,a) = none)
 
539
     /\
 
540
     (evlis_c (SUC n) ([],a) = some(List[]))
 
541
     /\
 
542
     (evlis_c (SUC n) (e::el,a) =
 
543
       if issome(eval_c n (e,a))
 
544
        then (if issome(evlis_c n (el,a))
 
545
               then some(Cons (the(eval_c n (e,a))) (the(evlis_c n (el,a))))
 
546
               else none)
 
547
        else none)``,
 
548
   RW_TAC list_ss 
 
549
    [SIMP_RULE arith_ss [] (INST[``n:num``|->``SUC n``]apply_c_def),
 
550
     SIMP_RULE arith_ss [] (INST[``n:num``|->``0``]apply_c_def)]
 
551
    THEN FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def]
 
552
    THEN TRY(DISJ_CASES_TAC (Q.SPECL [`e1`,`a`] (el 2 (CONJUNCTS apply_cCases))))
 
553
    THEN TRY(DISJ_CASES_TAC (Q.SPECL [`el`,`a`] (el 3 (CONJUNCTS apply_cCases))))
 
554
    THEN TRY(DISJ_CASES_TAC (Q.SPECL [`e`,`a`] (el 2 (CONJUNCTS apply_cCases))))
 
555
    THEN FULL_SIMP_TAC std_ss [issomenone,noneNONE]);
 
556
 
 
557
val isListevlis_c =
 
558
 store_thm
 
559
  ("isListevlis_c",
 
560
   ``!el n s. (evlis_c n (el,a) = some s) ==> isList s``,
 
561
   Induct
 
562
    THEN RW_TAC list_ss [apply_c,someNotEqnone,somesomeEq,isList_def,List_def]
 
563
    THEN Cases_on `n`
 
564
    THEN FULL_SIMP_TAC list_ss [apply_c,someNotEqnone,somesomeEq,isList_def,List_def]
 
565
    THEN RW_TAC std_ss [isList_def]
 
566
    THEN DISJ_CASES_TAC (Q.SPECL [`h`,`n'`,`a`] (el 2 (CONJUNCTS apply_cCasesCor)))
 
567
    THEN DISJ_CASES_TAC (Q.SPECL [`el`,`n'`,`a`] (el 3 (CONJUNCTS apply_cCasesCor)))
 
568
    THEN FULL_SIMP_TAC std_ss [issomenone,noneNONE,someNotEqnone,issomeExists,somesomeEq]
 
569
    THEN RW_TAC std_ss [isList_def,thesome]
 
570
    THEN METIS_TAC[]);
 
571
 
 
572
local
 
573
val TAC0 =
 
574
 Q.EXISTS_TAC `0` 
 
575
  THEN RW_TAC arith_ss []
 
576
  THEN `?m. n = SUC m` by intLib.COOPER_TAC
 
577
  THEN RW_TAC std_ss [apply_c,LET_THM]  
 
578
  THEN METIS_TAC[]
 
579
val TAC1 =
 
580
 Q.EXISTS_TAC `SUC m`
 
581
  THEN RW_TAC std_ss []
 
582
  THEN `?p. (n = SUC p) /\ m < p` by intLib.COOPER_TAC
 
583
  THEN RW_TAC std_ss [apply_c,isTrue_def,LET_THM]
 
584
  THEN METIS_TAC[]
 
585
val TAC2 =
 
586
 Q.EXISTS_TAC `SUC(m+m')`
 
587
  THEN RW_TAC std_ss []
 
588
  THEN `?p. (n = SUC p) /\ m < p /\ m' < p` by intLib.COOPER_TAC
 
589
  THEN RW_TAC std_ss [apply_c,isTrue_def,LET_THM,issomesome]
 
590
  THEN METIS_TAC
 
591
        [isTrue_def,False_def,DB.theorem "atom_distinct",apply_c,
 
592
         SplitList,DB.theorem "sexpression_11",EVAL ``True = False``,
 
593
         issomesome,thesome,somesomeEq,ListsomeEq]
 
594
in
 
595
val R_ap_apply_c_lemma =
 
596
 store_thm
 
597
  ("R_ap_apply_c_lemma",
 
598
   ``(!fnargsa s.
 
599
       R_ap fnargsa s
 
600
       ==> (\fnargsa s. ?m. !n. m < n ==> (some s = apply_c n fnargsa)) fnargsa s)
 
601
     /\
 
602
     (!ea s.
 
603
       R_ev ea s
 
604
       ==> (\ea s. ?m. !n. m < n ==> (some s = eval_c n ea)) ea s)
 
605
     /\
 
606
     (!ela sl.
 
607
       R_evl ela sl
 
608
       ==> (\ela sl. ?m. !n. m < n ==> (some(List sl) = evlis_c n ela)) ela sl)``,
 
609
   IndDefRules.RULE_TAC
 
610
    (IndDefRules.derive_mono_strong_induction [] (R_ap_rules,R_ap_ind))
 
611
    THEN RW_TAC std_ss [LET_THM]
 
612
    THEN TRY(TAC0 ORELSE TAC1 ORELSE TAC2))
 
613
end;
 
614
 
 
615
val R_ap_apply_c =
 
616
 store_thm
 
617
  ("R_ap_apply_c",
 
618
   ``(!fnargsa s. R_ap fnargsa s ==> ?n. some s = apply_c n fnargsa)
 
619
     /\
 
620
     (!ea s. R_ev ea s ==> ?n. some s = eval_c n ea)
 
621
     /\
 
622
     (!ela sl. R_evl ela sl ==> ?n. some(List sl) = evlis_c n ela)``,
 
623
   RW_TAC std_ss []
 
624
    THEN IMP_RES_TAC R_ap_apply_c_lemma
 
625
    THEN FULL_SIMP_TAC std_ss []
 
626
    THEN `m < SUC m` by DECIDE_TAC
 
627
    THEN METIS_TAC[]);
 
628
 
 
629
val apply_c_R_ap_lemma =
 
630
 store_thm
 
631
  ("apply_c_R_ap_lemma",
 
632
   ``(!fn args s a. (apply_c n (fn,args,a) = some s) ==> R_ap (fn,args,a) s)
 
633
     /\
 
634
     (!e s a. (eval_c n (e,a) = some s) ==> R_ev (e,a) s)
 
635
     /\
 
636
     (!el sl a. (evlis_c n (el,a) = some(List sl)) ==> R_evl (el,a) sl)``,
 
637
   Induct_on `n`
 
638
    THEN RW_TAC std_ss [apply_c,R_ap_rules,someNotEqnone]
 
639
    THENL
 
640
     [Cases_on `fn`
 
641
       THEN FULL_SIMP_TAC std_ss [apply_c,R_ap_rules,somesomeEq]
 
642
       THEN RW_TAC std_ss [apply_c,R_ap_rules],
 
643
      Cases_on `e`
 
644
       THEN FULL_SIMP_TAC std_ss [apply_c,R_ap_rules,somesomeEq]
 
645
       THEN RW_TAC std_ss [apply_c,R_ap_rules]
 
646
       THENL
 
647
        [DISJ_CASES_TAC (Q.SPECL [`l`,`a`] (el 3 (CONJUNCTS apply_cCases)))
 
648
          THEN FULL_SIMP_TAC std_ss [apply_c,R_ap_rules,somesomeEq,issomeExists]
 
649
          THEN RES_TAC
 
650
          THEN METIS_TAC[someNotEqnone,thesome,isListevlis_c,ListSplit,R_ap_rules],
 
651
         Induct_on `l`
 
652
          THEN RW_TAC std_ss [apply_c,R_ap_rules,somesomeEq]
 
653
          THEN RW_TAC std_ss [apply_c,R_ap_rules,somesomeEq]
 
654
          THEN Cases_on `h`
 
655
          THEN Cases_on `eval_c n (q,a) = some False`
 
656
          THENL
 
657
           [RES_TAC
 
658
             THEN FULL_SIMP_TAC std_ss [apply_c,issomesome,thesome]
 
659
             THEN METIS_TAC[R_ap_rules],
 
660
            FULL_SIMP_TAC std_ss [apply_c,issomesome,thesome]
 
661
             THEN DISJ_CASES_TAC (Q.SPECL [`q`,`a`] (el 2 (CONJUNCTS apply_cCases)))
 
662
             THEN FULL_SIMP_TAC std_ss [apply_c,R_ap_rules,somesomeEq,issomeExists]
 
663
             THEN METIS_TAC[R_ap_rules,isTrue_def,thesome,somesomeEq]]],
 
664
      Induct_on `el`
 
665
       THEN FULL_SIMP_TAC std_ss [apply_c,R_ap_rules]
 
666
       THEN RW_TAC std_ss [apply_c,R_ap_rules]
 
667
       THEN RW_TAC std_ss [apply_c,R_ap_rules]
 
668
       THENL
 
669
        [DISJ_CASES_TAC (Q.SPECL [`el`,`a`] (el 3 (CONJUNCTS apply_cCases)))
 
670
          THEN FULL_SIMP_TAC std_ss [somesomeEq,issomeExists,ListListEq]
 
671
          THEN RW_TAC std_ss [R_ap_rules],
 
672
         DISJ_CASES_TAC (Q.SPECL [`h`,`a`] (el 2 (CONJUNCTS apply_cCases)))
 
673
          THEN FULL_SIMP_TAC std_ss [somesomeEq,issomeExists,ListListEq,thesome,someNotEqnone]
 
674
          THEN `sl = Split(Cons s' s)` by METIS_TAC[thesome,SplitList]
 
675
          THEN RW_TAC std_ss [Split_def]
 
676
          THEN METIS_TAC[ListSplit,R_ap_rules,isListevlis_c],
 
677
         FULL_SIMP_TAC std_ss [someNotEqnone],
 
678
         FULL_SIMP_TAC std_ss [someNotEqnone]]]);
 
679
 
 
680
val apply_c_R_ap =
 
681
 store_thm
 
682
  ("apply_c_R_ap",
 
683
   ``(!fnargsa s. (apply_c n fnargsa = some s) ==> R_ap fnargsa s)
 
684
     /\
 
685
     (!ea s. (eval_c n ea = some s) ==> R_ev ea s)
 
686
     /\
 
687
     (!ela sl. (evlis_c n ela = some(List sl)) ==> R_evl ela sl)``,
 
688
   RW_TAC std_ss []
 
689
    THENL
 
690
     [Cases_on `fnargsa` THEN Cases_on `r`,
 
691
      Cases_on `ea`,
 
692
      Cases_on `ela`]
 
693
    THEN METIS_TAC[apply_c_R_ap_lemma]);
 
694
 
 
695
val apply_c_R_ap_EQ =
 
696
 store_thm
 
697
  ("apply_c_R_ap_EQ",
 
698
   ``(!fnargsa s. R_ap fnargsa s = ?n. some s = apply_c n fnargsa)
 
699
     /\
 
700
     (!ea s. R_ev ea s = ?n. some s = eval_c n ea)
 
701
     /\
 
702
     (!ela sl. R_evl ela sl = ?n. some(List sl) = evlis_c n ela)``,
 
703
   METIS_TAC[R_ap_apply_c,apply_c_R_ap]);
 
704
 
 
705
(*****************************************************************************)
 
706
(* Tool to compute s such that R_ap (fn,args,a) s                            *)
 
707
(*****************************************************************************)
 
708
fun apply fn_tm args_tm a =
 
709
 MATCH_MP
 
710
  (REWRITE_RULE[some_def](hd(CONJUNCTS apply_c_R_ap)))
 
711
  (EVAL ``apply_c 1000000000 (^fn_tm,^args_tm,a)``);
 
712
 
 
713
(*****************************************************************************)
 
714
(* Add some library theorems to the evaluator compset to make computation on *)
 
715
(* finite functions work.                                                    *)
 
716
(*****************************************************************************)
 
717
computeLib.add_funs[FAPPLY_FUPDATE_THM];
 
718
computeLib.add_funs[FUPDATE_LIST_THM];
 
719
computeLib.add_funs[OUTL];
 
720
computeLib.add_funs[OUTR];
 
721
 
 
722
(*****************************************************************************)
 
723
(* Example: factorial function                                               *)
 
724
(*****************************************************************************)
 
725
val Fact_def =
 
726
 Define
 
727
 `Fact =
 
728
   Label "fact"
 
729
    (Lambda ["n"]
 
730
       (Ite
 
731
          [(App (FunCon "eq") [Var "n"; Con (Num 0)],
 
732
            Con (Num 1));
 
733
           (Con True,
 
734
            App (FunCon "mult")
 
735
              [Var "n"; 
 
736
               App (FunVar "fact") [App (FunCon "sub1") [Var "n"]]])]))`;
 
737
 
 
738
(*****************************************************************************)
 
739
(* Evaluate 6!, 20!, 50! and 100! in the empty environment                   *)
 
740
(*****************************************************************************)
 
741
apply ``Fact`` ``[Num 6]``   ``FEMPTY``;
 
742
apply ``Fact`` ``[Num 20]``  ``FEMPTY``;
 
743
apply ``Fact`` ``[Num 50]``  ``FEMPTY``;
 
744
apply ``Fact`` ``[Num 100]`` ``FEMPTY``;
 
745
 
 
746
(*****************************************************************************)
 
747
(* Check (EQ (CAR(CONS X Y)) X) and (EQ (CDR(CONS X Y)) Y) by computation    *)
 
748
(*****************************************************************************)
 
749
apply ``FunCon "car"`` ``[Cons x y]`` ``FEMPTY``;
 
750
apply ``FunCon "cdr"`` ``[Cons x y]`` ``FEMPTY``;
 
751
 
 
752