-
Notifications
You must be signed in to change notification settings - Fork 129
/
Defn.sml
1888 lines (1686 loc) · 71.9 KB
/
Defn.sml
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
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
structure Defn :> Defn =
struct
open HolKernel Parse boolLib;
open pairLib Rules wfrecUtils Pmatch Induction DefnBase;
type thry = TypeBasePure.typeBase
type proofs = Manager.proofs
type absyn = Absyn.absyn;
val ERR = mk_HOL_ERR "Defn";
val ERRloc = mk_HOL_ERRloc "Defn";
val monitoring = ref false;
(* Interactively:
val const_eq_ref = ref (!Defn.const_eq_ref);
*)
val const_eq_ref = ref Conv.NO_CONV;
(*---------------------------------------------------------------------------
Miscellaneous support
---------------------------------------------------------------------------*)
fun enumerate l = map (fn (x,y) => (y,x)) (Lib.enumerate 0 l);
fun drop [] x = x
| drop (_::t) (_::rst) = drop t rst
| drop _ _ = raise ERR "drop" "";
fun variants FV vlist =
fst
(rev_itlist
(fn v => fn (V,W) =>
let val v' = variant W v in (v'::V, v'::W) end) vlist ([],FV));
fun make_definition thry s tm = (new_definition(s,tm), thry)
fun head tm = head (rator tm) handle HOL_ERR _ => tm;
fun all_fns eqns =
mk_set (map (head o lhs o #2 o strip_forall) (strip_conj eqns));
fun dest_hd_eqn eqs =
let val hd_eqn = if is_conj eqs then fst(dest_conj eqs) else eqs
val (lhs,rhs) = dest_eq (snd(strip_forall hd_eqn))
in (strip_comb lhs, rhs)
end;
fun dest_hd_eqnl (hd_eqn::_) =
let val (lhs,rhs) = dest_eq (snd (strip_forall (concl hd_eqn)))
in (strip_comb lhs, rhs)
end
| dest_hd_eqnl _ = raise Match
fun extract_info constset db =
let open TypeBasePure
fun foldthis (tyinfo, (R, C)) =
if List.exists
(fn x => same_const (case_const_of tyinfo) x
handle HOL_ERR _ => false) constset then
(case_def_of tyinfo::R, case_cong_of tyinfo::C)
else (R, C)
val (rws,congs) = foldl foldthis ([], []) (listItems db)
in {case_congs=congs, case_rewrites=rws}
end;
(*---------------------------------------------------------------------------
Support for automatically building names to store definitions
(and the consequences thereof) with in the current theory. Somewhat
ad hoc, but I don't know a better way!
---------------------------------------------------------------------------*)
val ind_suffix = ref "_ind";
val def_suffix = boolLib.def_suffix
fun indSuffix s = (s ^ !ind_suffix);
fun defSuffix s = (s ^ !def_suffix);
fun defPrim s = defSuffix(s^"_primitive");
fun defExtract(s,n) = defSuffix(s^"_extract"^Lib.int_to_string n);
fun argMunge s = defSuffix(s^"_curried");
fun auxStem stem = stem^"_AUX";
fun unionStem stem = stem^"_UNION";
val imp_elim =
let val P = mk_var("P",bool)
val Q = mk_var("Q",bool)
val R = mk_var("R",bool)
val PimpQ = mk_imp(P,Q)
val PimpR = mk_imp(P,R)
val tm = mk_eq(PimpQ,PimpR)
val tm1 = mk_imp(P,tm)
val th1 = DISCH tm (DISCH P (ASSUME tm))
val th2 = ASSUME tm1
val th2a = ASSUME P
val th3 = MP th2 th2a
val th3a = EQ_MP (SPECL[PimpQ, PimpR] boolTheory.EQ_IMP_THM) th3
val (th4,th5) = (CONJUNCT1 th3a,CONJUNCT2 th3a)
fun pmap f (x,y) = (f x, f y)
val (th4a,th5a) = pmap (DISCH P o funpow 2 UNDISCH) (th4,th5)
val th4b = DISCH PimpQ th4a
val th5b = DISCH PimpR th5a
val th6 = DISCH tm1 (IMP_ANTISYM_RULE th4b th5b)
val th7 = DISCH tm (DISCH P (ASSUME tm))
in GENL [P,Q,R]
(IMP_ANTISYM_RULE th6 th7)
end;
fun inject ty [v] = [v]
| inject ty (v::vs) =
let val (lty,rty) = case dest_type ty of
(_, [x,y]) => (x,y)
| _ => raise Bind
val res = mk_comb(mk_const("INL", lty-->ty),v)
val inr = curry mk_comb (mk_const("INR", rty-->ty))
in
res::map inr (inject rty vs)
end
| inject ty [] = raise Match
fun project [] _ _ = raise ERR "project" "catastrophic invariant failure (eqns was empty!?)"
| project [_] ty M = [M]
| project (_::ls) ty M = let
val (lty,rty) = sumSyntax.dest_sum ty
in mk_comb(mk_const("OUTL", type_of M-->lty),M)
:: project ls rty (mk_comb(mk_const("OUTR", type_of M-->rty),M))
end
(*---------------------------------------------------------------------------*
* We need a "smart" MP. th1 can be less quantified than th2, so th2 has *
* to be specialized appropriately. We assume that all the "local" *
* variables are quantified first. *
*---------------------------------------------------------------------------*)
fun ModusPonens th1 th2 =
let val V1 = #1(strip_forall(fst(dest_imp(concl th1))))
val V2 = #1(strip_forall(concl th2))
val diff = Lib.op_set_diff Term.aconv V2 V1
fun loop th =
if is_forall(concl th)
then let val (Bvar,Body) = dest_forall (concl th)
in if Lib.op_mem Term.aconv Bvar diff
then loop (SPEC Bvar th) else th
end
else th
in
MP th1 (loop th2)
end
handle _ => raise ERR "ModusPonens" "failed";
(*---------------------------------------------------------------------------*)
(* Version of PROVE_HYP that works modulo permuting outer universal quants. *)
(*---------------------------------------------------------------------------*)
fun ALPHA_PROVE_HYP th1 th2 =
let val c1 = concl th1
val asl = hyp th2
val tm = snd(strip_forall c1)
val a = Lib.first (fn t => aconv tm (snd(strip_forall t))) asl
val V = fst(strip_forall a)
val th1' = GENL V (SPEC_ALL th1)
in
PROVE_HYP th1' th2
end;
fun name_of (ABBREV {bind, ...}) = bind
| name_of (PRIMREC{bind, ...}) = bind
| name_of (NONREC {eqs, ind, stem, ...}) = stem
| name_of (STDREC {eqs, ind, stem, ...}) = stem
| name_of (MUTREC {eqs,ind,stem,...}) = stem
| name_of (NESTREC{eqs,ind,stem, ...}) = stem
| name_of (TAILREC{eqs,ind,stem, ...}) = stem
fun eqns_of (ABBREV {eqn, ...}) = [eqn]
| eqns_of (NONREC {eqs, ...}) = [eqs]
| eqns_of (PRIMREC {eqs, ...}) = [eqs]
| eqns_of (STDREC {eqs, ...}) = eqs
| eqns_of (NESTREC {eqs, ...}) = eqs
| eqns_of (MUTREC {eqs, ...}) = eqs
| eqns_of (TAILREC {eqs, ...}) = eqs;
fun aux_defn (NESTREC {aux, ...}) = SOME aux
| aux_defn _ = NONE;
fun union_defn (MUTREC {union, ...}) = SOME union
| union_defn _ = NONE;
fun ind_of (ABBREV _) = NONE
| ind_of (NONREC {ind, ...}) = SOME ind
| ind_of (PRIMREC {ind, ...}) = SOME ind
| ind_of (STDREC {ind, ...}) = SOME ind
| ind_of (NESTREC {ind, ...}) = SOME ind
| ind_of (MUTREC {ind, ...}) = SOME ind
| ind_of (TAILREC {ind, ...}) = SOME ind;
fun params_of (ABBREV _) = []
| params_of (PRIMREC _) = []
| params_of (NONREC {SV, ...}) = SV
| params_of (STDREC {SV, ...}) = SV
| params_of (NESTREC{SV, ...}) = SV
| params_of (MUTREC {SV, ...}) = SV
| params_of (TAILREC {SV, ...}) = SV
fun schematic defn = not(List.null (params_of defn));
fun tcs_of (ABBREV _) = []
| tcs_of (NONREC _) = []
| tcs_of (PRIMREC _) = []
| tcs_of (STDREC {eqs,...}) = op_U aconv (map hyp eqs)
| tcs_of (NESTREC {eqs,...}) = op_U aconv (map hyp eqs)
| tcs_of (MUTREC {eqs,...}) = op_U aconv (map hyp eqs)
| tcs_of (TAILREC {eqs,...}) = raise ERR "tcs_of" "Tail recursive definition"
fun reln_of (ABBREV _) = NONE
| reln_of (NONREC _) = NONE
| reln_of (PRIMREC _) = NONE
| reln_of (STDREC {R, ...}) = SOME R
| reln_of (NESTREC {R, ...}) = SOME R
| reln_of (MUTREC {R, ...}) = SOME R
| reln_of (TAILREC {R, ...}) = SOME R;
fun nUNDISCH n th = if n<1 then th else nUNDISCH (n-1) (UNDISCH th)
fun INST_THM theta th =
let val asl = hyp th
val th1 = rev_itlist DISCH asl th
val th2 = INST_TY_TERM theta th1
in
nUNDISCH (length asl) th2
end;
fun isubst (tmtheta,tytheta) tm = subst tmtheta (inst tytheta tm);
fun inst_defn (STDREC{eqs,ind,R,SV,stem}) theta =
STDREC {eqs=map (INST_THM theta) eqs,
ind=INST_THM theta ind,
R=isubst theta R,
SV=map (isubst theta) SV, stem=stem}
| inst_defn (NESTREC{eqs,ind,R,SV,aux,stem}) theta =
NESTREC {eqs=map (INST_THM theta) eqs,
ind=INST_THM theta ind,
R=isubst theta R,
SV=map (isubst theta) SV,
aux=inst_defn aux theta, stem=stem}
| inst_defn (MUTREC{eqs,ind,R,SV,union,stem}) theta =
MUTREC {eqs=map (INST_THM theta) eqs,
ind=INST_THM theta ind,
R=isubst theta R,
SV=map (isubst theta) SV,
union=inst_defn union theta, stem=stem}
| inst_defn (PRIMREC{eqs,ind,bind}) theta =
PRIMREC{eqs=INST_THM theta eqs,
ind=INST_THM theta ind, bind=bind}
| inst_defn (NONREC {eqs,ind,SV,stem}) theta =
NONREC {eqs=INST_THM theta eqs,
ind=INST_THM theta ind,
SV=map (isubst theta) SV,stem=stem}
| inst_defn (ABBREV {eqn,bind}) theta = ABBREV {eqn=INST_THM theta eqn,bind=bind}
| inst_defn (TAILREC{eqs,ind,R,SV,stem}) theta =
TAILREC {eqs=map (INST_THM theta) eqs,
ind=INST_THM theta ind,
R=isubst theta R,
SV=map (isubst theta) SV, stem=stem};
fun set_reln def R =
case reln_of def
of NONE => def
| SOME Rpat => inst_defn def (Term.match_term Rpat R)
handle e => (HOL_MESG"set_reln: unable"; raise e);
fun PROVE_HYPL thl th = itlist PROVE_HYP thl th
fun MATCH_HYPL thms th =
let val aslthms = mapfilter (EQT_ELIM o REWRITE_CONV thms) (hyp th)
in itlist PROVE_HYP aslthms th
end;
(* We use PROVE_HYPL on induction theorems, since their tcs are fully
quantified. We use MATCH_HYPL on equations, since their tcs are
bare.
*)
fun elim_tcs (STDREC {eqs, ind, R, SV,stem}) thms =
STDREC{R=R, SV=SV, stem=stem,
eqs=map (MATCH_HYPL thms) eqs,
ind=PROVE_HYPL thms ind}
| elim_tcs (NESTREC {eqs, ind, R, SV, aux, stem}) thms =
NESTREC{R=R, SV=SV, stem=stem,
eqs=map (MATCH_HYPL thms) eqs,
ind=PROVE_HYPL thms ind,
aux=elim_tcs aux thms}
| elim_tcs (MUTREC {eqs, ind, R, SV, union, stem}) thms =
MUTREC{R=R, SV=SV, stem=stem,
eqs=map (MATCH_HYPL thms) eqs,
ind=PROVE_HYPL thms ind,
union=elim_tcs union thms}
| elim_tcs (TAILREC {eqs, ind, R, SV,stem}) thms =
TAILREC{R=R, SV=SV, stem=stem,
eqs=map (MATCH_HYPL thms) eqs,
ind=PROVE_HYPL thms ind}
| elim_tcs x _ = x;
local
val lem =
let val M = mk_var("M",bool)
val P = mk_var("P",bool)
val M1 = mk_var("M1",bool)
val tm1 = mk_eq(M,M1)
val tm2 = mk_imp(M,P)
in DISCH tm1 (DISCH tm2 (SUBS [ASSUME tm1] (ASSUME tm2)))
end
in
fun simp_assum conv tm th =
let val th' = DISCH tm th
val tmeq = conv tm
val tm' = rhs(concl tmeq)
in
if tm' = T then MP th' (EQT_ELIM tmeq)
else UNDISCH(MATCH_MP (MATCH_MP lem tmeq) th')
end
end;
fun SIMP_HYPL conv th = itlist (simp_assum conv) (hyp th) th;
fun simp_tcs (STDREC {eqs, ind, R, SV, stem}) conv =
STDREC{R=rhs(concl(conv R)), SV=SV, stem=stem,
eqs=map (SIMP_HYPL conv) eqs,
ind=SIMP_HYPL conv ind}
| simp_tcs (NESTREC {eqs, ind, R, SV, aux, stem}) conv =
NESTREC{R=rhs(concl(conv R)), SV=SV, stem=stem,
eqs=map (SIMP_HYPL conv) eqs,
ind=SIMP_HYPL conv ind,
aux=simp_tcs aux conv}
| simp_tcs (MUTREC {eqs, ind, R, SV, union, stem}) conv =
MUTREC{R=rhs(concl(conv R)), SV=SV, stem=stem,
eqs=map (SIMP_HYPL conv) eqs,
ind=SIMP_HYPL conv ind,
union=simp_tcs union conv}
| simp_tcs x _ = x;
fun TAC_HYPL tac th =
PROVE_HYPL (mapfilter (C (curry Tactical.prove) tac) (hyp th)) th;
fun prove_tcs (STDREC {eqs, ind, R, SV, stem}) tac =
STDREC{R=R, SV=SV, stem=stem,
eqs=map (TAC_HYPL tac) eqs,
ind=TAC_HYPL tac ind}
| prove_tcs (NESTREC {eqs, ind, R, SV, aux, stem}) tac =
NESTREC{R=R, SV=SV, stem=stem,
eqs=map (TAC_HYPL tac) eqs,
ind=TAC_HYPL tac ind,
aux=prove_tcs aux tac}
| prove_tcs (MUTREC {eqs, ind, R, SV, union, stem}) tac =
MUTREC{R=R, SV=SV, stem=stem,
eqs=map (TAC_HYPL tac) eqs,
ind=TAC_HYPL tac ind,
union=prove_tcs union tac}
| prove_tcs x _ = x;
(*---------------------------------------------------------------------------*)
(* Deal with basic definitions. *)
(*---------------------------------------------------------------------------*)
fun triv_defn (ABBREV _) = true
| triv_defn (PRIMREC _) = true
| triv_defn otherwise = false
fun fetch_eqns (ABBREV{eqn,...}) = eqn
| fetch_eqns (PRIMREC{eqs,...}) = eqs
| fetch_eqns otherwise = raise ERR "fetch_eqns" "shouldn't happen"
(*---------------------------------------------------------------------------
Store definition information to disk. Currently, just writes out the
eqns and induction theorem. A more advanced implementation would
write things out so that, when the exported theory is reloaded, the
defn datastructure is rebuilt. This would give a seamless view of
things.
Note that we would need to save union and aux info only when
termination has not been proved for a nested recursion.
Another (easier) way to look at it would be to require termination
and suchlike to be taken care of in the current theory. That is
what is assumed at present.
---------------------------------------------------------------------------*)
local fun is_suc tm =
case total dest_thy_const tm
of NONE => false
| SOME{Name,Thy,...} => Name="SUC" andalso Thy="num"
in
val SUC_TO_NUMERAL_DEFN_CONV_hook =
ref (fn _ => raise ERR "SUC_TO_NUMERAL_DEFN_CONV_hook" "not initialized")
fun add_persistent_funs l =
if not (!computeLib.auto_import_definitions) then () else
let val has_lhs_SUC = List.exists
(can (find_term is_suc) o lhs o #2 o strip_forall)
o strip_conj o concl
fun f (s, th) =
[s] @
(if has_lhs_SUC th then let
val name = s^"_compute"
val name = let
val used = Lib.C Lib.mem (#1 (Lib.unzip (current_theorems())))
fun loop n = let val x = (name^(Int.toString n)) in if used x then loop (n+1) else x end
in if used name then loop 0 else name end
val th_compute = CONV_RULE (!SUC_TO_NUMERAL_DEFN_CONV_hook) th
val _ = save_thm(name,th_compute)
in [name] end
else [])
in
computeLib.add_persistent_funs (List.concat (map f l))
end
end;
val mesg = with_flag(MESG_to_string, Lib.I) HOL_MESG
local
val chatting = ref true
val _ = Feedback.register_btrace("Define.storage_message", chatting)
in
fun been_stored (s,thm) =
(add_persistent_funs [(s,thm)];
if !chatting then
mesg ((if !Globals.interactive then
"Definition has been stored under "
else
"Saved definition __ ") ^Lib.quote s^"\n")
else ()
)
fun store(stem,eqs,ind) =
let val eqs_bind = defSuffix stem
val ind_bind = indSuffix stem
fun save x = Feedback.trace ("Theory.save_thm_reporting", 0) save_thm x
val _ = save (ind_bind, ind)
val eqns = save (eqs_bind, eqs)
val _ = add_persistent_funs [(eqs_bind,eqs)]
handle e => HOL_MESG ("Unable to add "^eqs_bind^" to global compset")
in
if !chatting then
mesg (String.concat
(if !Globals.interactive then
[ "Equations stored under ", Lib.quote eqs_bind,
".\nInduction stored under ", Lib.quote ind_bind, ".\n"]
else
[ "Saved definition __ ", Lib.quote eqs_bind,
"\nSaved induction ___ ", Lib.quote ind_bind, "\n"]))
else ()
end
end
local
val LIST_CONJ_GEN = LIST_CONJ o map GEN_ALL
in
fun save_defn (ABBREV {bind,eqn, ...}) = been_stored (bind,eqn)
| save_defn (PRIMREC{bind,eqs, ...}) = been_stored (bind,eqs)
| save_defn (NONREC {eqs, ind, stem, ...}) = store(stem,eqs,ind)
| save_defn (STDREC {eqs, ind, stem, ...}) = store(stem,LIST_CONJ_GEN eqs,ind)
| save_defn (TAILREC{eqs, ind, stem, ...}) = store(stem,LIST_CONJ_GEN eqs,ind)
| save_defn (MUTREC {eqs,ind,stem,...}) = store(stem,LIST_CONJ_GEN eqs,ind)
| save_defn (NESTREC{eqs,ind,stem, ...}) = store(stem,LIST_CONJ_GEN eqs,ind)
end
(*---------------------------------------------------------------------------
Termination condition extraction
---------------------------------------------------------------------------*)
fun extraction_thms constset thy =
let val {case_rewrites,case_congs} = extract_info constset thy
in (case_rewrites, case_congs@read_congs())
end;
(*---------------------------------------------------------------------------
Capturing termination conditions.
----------------------------------------------------------------------------*)
local fun !!v M = mk_forall(v, M)
val mem = Lib.op_mem aconv
fun set_diff a b = Lib.filter (fn x => not (mem x b)) a
in
fun solver (restrf,f,G,nref) _ context tm =
let val globals = f::G (* not to be generalized *)
fun genl tm = itlist !! (set_diff (rev(free_vars tm)) globals) tm
val rcontext = rev context
val antl = case rcontext of [] => []
| _ => [list_mk_conj(map concl rcontext)]
val TC = genl(list_mk_imp(antl, tm))
val (R,arg,pat) = wfrecUtils.dest_relation tm
in
if can(find_term (aconv restrf)) arg
then (nref := true; raise ERR "solver" "nested function")
else let val _ = if can(find_term (aconv f)) TC
then nref := true else ()
in case rcontext
of [] => SPEC_ALL(ASSUME TC)
| _ => MATCH_MP (SPEC_ALL (ASSUME TC)) (LIST_CONJ rcontext)
end
end
end;
fun extract FV congs f (proto_def,WFR) =
let val R = rand WFR
val CUT_LEM = ISPECL [f,R] relationTheory.RESTRICT_LEMMA
val restr_fR = rator(rator(lhs(snd(dest_imp (concl (SPEC_ALL CUT_LEM))))))
fun mk_restr p = mk_comb(restr_fR, p)
in fn (p,th) =>
let val nested_ref = ref false
val FV' = FV@free_vars(concl th)
val rwArgs = (RW.Pure [CUT_LEM],
RW.Context ([],RW.DONT_ADD),
RW.Congs congs,
RW.Solver (solver (mk_restr p, f, FV', nested_ref)))
val th' = CONV_RULE (RW.Rewrite RW.Fully rwArgs) th
in
(th', Lib.op_set_diff aconv (hyp th') [proto_def,WFR], !nested_ref)
end
end;
(*---------------------------------------------------------------------------*
* Perform TC extraction without making a definition. *
*---------------------------------------------------------------------------*)
type wfrec_eqns_result = {WFR : term,
SV : term list,
proto_def : term,
extracta : (thm * term list * bool) list,
pats : pattern list}
fun protect_rhs eqn = mk_eq(lhs eqn,combinSyntax.mk_I(rhs eqn))
fun protect eqns = list_mk_conj (map protect_rhs (strip_conj eqns));
val unprotect_term = rhs o concl o PURE_REWRITE_CONV [combinTheory.I_THM];
val unprotect_thm = PURE_REWRITE_RULE [combinTheory.I_THM];
(*---------------------------------------------------------------------------*)
(* Once patterns are instantiated and the clauses are simplified, there can *)
(* still remain right-hand sides with occurrences of fully concrete tests on *)
(* literals. Here we simplify those away. *)
(* *)
(* const_eq_ref is a reference cell that decides equality of literals such *)
(* as 23, "foo", #"G", 6w, 0b1000w. It gets updated in reduceLib, stringLib *)
(* and wordsLib. *)
(*---------------------------------------------------------------------------*)
fun elim_triv_literal_CONV tm =
let
val const_eq_conv = !const_eq_ref
val cnv = TRY_CONV (REWR_CONV literal_case_THM THENC BETA_CONV) THENC
RATOR_CONV (RATOR_CONV (RAND_CONV const_eq_conv)) THENC
PURE_ONCE_REWRITE_CONV [COND_CLAUSES]
in
cnv tm
end
fun checkSV pats SV =
let fun get_pat (GIVEN(p,_)) = p
| get_pat (OMITTED(p,_)) = p
fun strings_of vlist =
Lib.commafy (List.map (Lib.quote o #1 o dest_var)
(Listsort.sort Term.compare vlist))
in
if null SV then ()
else HOL_MESG (String.concat
["Definition is schematic in the following variables:\n ",
String.concat (strings_of SV)])
;
case intersect (free_varsl (map get_pat pats)) SV
of [] => ()
| probs =>
raise ERR "wfrec_eqns"
(String.concat
(["the following variables occur both free (schematic) ",
"and bound in the definition: \n "] @ strings_of probs))
end
(*---------------------------------------------------------------------------*)
(* Instantiate the recursion theorem and extract termination conditions, *)
(* but do not define the constant yet. *)
(*---------------------------------------------------------------------------*)
fun wfrec_eqns facts tup_eqs =
let val {functional,pats} =
mk_functional (TypeBasePure.toPmatchThry facts) (protect tup_eqs)
val SV = free_vars functional (* schematic variables *)
val _ = checkSV pats SV
val (f, Body) = dest_abs functional
val (x,_) = dest_abs Body
val (Name, fty) = dest_var f
val (f_dty, f_rty) = Type.dom_rng fty
val WFREC_THM0 = ISPEC functional relationTheory.WFREC_COROLLARY
val R = variant (free_vars tup_eqs) (fst(dest_forall(concl WFREC_THM0)))
val WFREC_THM = ISPECL [R, f] WFREC_THM0
val tmp = fst(wfrecUtils.strip_imp(concl WFREC_THM))
val proto_def = Lib.trye hd tmp
val WFR = Lib.trye (hd o tl) tmp
val R1 = rand WFR
val corollary' = funpow 2 UNDISCH WFREC_THM
val given_pats = givens pats
val corollaries = map (C SPEC corollary') given_pats
val eqns_consts = mk_set(find_terms is_const functional)
val (case_rewrites,congs) = extraction_thms eqns_consts facts
val RWcnv = REWRITES_CONV (add_rewrites empty_rewrites
(literal_case_THM::case_rewrites))
val rule = unprotect_thm o
RIGHT_CONV_RULE
(LIST_BETA_CONV
THENC REPEATC ((RWcnv THENC LIST_BETA_CONV) ORELSEC
elim_triv_literal_CONV))
val corollaries' = map rule corollaries
in
{proto_def=proto_def,
SV=Listsort.sort Term.compare SV,
WFR=WFR,
pats=pats,
extracta = map (extract [R1] congs f (proto_def,WFR))
(zip given_pats corollaries')}
end
(*---------------------------------------------------------------------------
* Pair patterns with termination conditions. The full list of patterns for
* a definition is merged with the TCs arising from the user-given clauses.
* There can be fewer clauses than the full list, if the user omitted some
* cases. This routine is used to prepare input for mk_induction.
*---------------------------------------------------------------------------*)
fun merge full_pats TCs =
let fun insert (p,TCs) =
let fun insrt ((x as (h,[]))::rst) =
if (aconv p h) then (p,TCs)::rst else x::insrt rst
| insrt (x::rst) = x::insrt rst
| insrt[] = raise ERR"merge.insert" "pat not found"
in insrt end
fun pass ([],ptcl_final) = ptcl_final
| pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
in
pass (TCs, map (fn p => (p,[])) full_pats)
end;
(*---------------------------------------------------------------------------*
* Define the constant after extracting the termination conditions. The *
* wellfounded relation used in the definition is computed by using the *
* choice operator on the extracted conditions (plus the condition that *
* such a relation must be wellfounded). *
* *
* There are three flavours of recursion: standard, nested, and mutual. *
* *
* A "standard" recursion is one that is not mutual or nested. *
*---------------------------------------------------------------------------*)
fun stdrec thy bindstem {proto_def,SV,WFR,pats,extracta} =
let val R1 = rand WFR
val f = lhs proto_def
val (extractants,TCl_0,_) = unzip3 extracta
fun gen_all away tm =
let val FV = free_vars tm
in itlist (fn v => fn tm =>
if mem v away then tm else mk_forall(v,tm)) FV tm
end
val TCs_0 = op_U aconv TCl_0
val TCl = map (map (gen_all (R1::SV))) TCl_0
val TCs = op_U aconv TCl
val full_rqt = WFR::TCs
val R2 = mk_select(R1, list_mk_conj full_rqt)
val R2abs = rand R2
val fvar = mk_var(fst(dest_var f),
itlist (curry op-->) (map type_of SV) (type_of f))
val fvar_app = list_mk_comb(fvar,SV)
val (def,theory) = make_definition thy (defPrim bindstem)
(subst [f |-> fvar_app, R1 |-> R2] proto_def)
val fconst = fst(strip_comb(lhs(snd(strip_forall(concl def)))))
val disch'd = itlist DISCH (proto_def::WFR::TCs_0) (LIST_CONJ extractants)
val inst'd = SPEC (list_mk_comb(fconst,SV))
(SPEC R2 (GENL [R1, f] disch'd))
val def' = MP inst'd (SPEC_ALL def)
val var_wits = LIST_CONJ (map ASSUME full_rqt)
val TC_choice_thm =
MP (CONV_RULE(BINOP_CONV BETA_CONV)(ISPECL[R2abs, R1] boolTheory.SELECT_AX)) var_wits
in
{theory = theory, R=R1, SV=SV,
rules = CONJUNCTS
(rev_itlist (C ModusPonens) (CONJUNCTS TC_choice_thm) def'),
full_pats_TCs = merge (map pat_of pats) (zip (givens pats) TCl),
patterns = pats}
end
(*---------------------------------------------------------------------------
Nested recursion.
---------------------------------------------------------------------------*)
fun nestrec thy bindstem {proto_def,SV,WFR,pats,extracta} =
let val R1 = rand WFR
val (f,rhs_proto_def) = dest_eq proto_def
(* make parameterized definition *)
val (Name,Ty) = Lib.trye dest_var f
val aux_name = Name^"_aux"
val faux = mk_var(aux_name,itlist(curry(op-->)) (map type_of (R1::SV)) Ty)
val aux_bindstem = auxStem bindstem
val (def,theory) =
make_definition thy (defSuffix aux_bindstem)
(mk_eq(list_mk_comb(faux,R1::SV), rhs_proto_def))
val def' = SPEC_ALL def
val faux_capp = lhs(concl def')
val faux_const = #1(strip_comb faux_capp)
val (extractants,TCl_0,_) = unzip3 extracta
val TCs_0 = op_U aconv TCl_0
val disch'd = itlist DISCH (proto_def::WFR::TCs_0) (LIST_CONJ extractants)
val inst'd = GEN R1 (MP (SPEC faux_capp (GEN f disch'd)) def')
fun kdisch keep th =
itlist (fn h => fn th => if op_mem aconv h keep then th else DISCH h th)
(hyp th) th
val disch'dl_0 = map (DISCH proto_def o
DISCH WFR o kdisch [proto_def,WFR])
extractants
val disch'dl_1 = map (fn d => MP (SPEC faux_capp (GEN f d)) def')
disch'dl_0
fun gen_all away tm =
let val FV = free_vars tm
in itlist (fn v => fn tm =>
if mem v away then tm else mk_forall(v,tm)) FV tm
end
val TCl = map (map (gen_all (R1::f::SV) o subst[f |-> faux_capp])) TCl_0
val TCs = op_U aconv TCl
val full_rqt = WFR::TCs
val R2 = mk_select(R1, list_mk_conj full_rqt)
val R2abs = rand R2
val R2inst'd = SPEC R2 inst'd
val fvar = mk_var(fst(dest_var f),
itlist (curry op-->) (map type_of SV) (type_of f))
val fvar_app = list_mk_comb(fvar,SV)
val (def1,theory1) = make_definition thy (defPrim bindstem)
(mk_eq(fvar_app, list_mk_comb(faux_const,R2::SV)))
val var_wits = LIST_CONJ (map ASSUME full_rqt)
val TC_choice_thm =
MP (CONV_RULE(BINOP_CONV BETA_CONV)(ISPECL[R2abs, R1] boolTheory.SELECT_AX)) var_wits
val elim_chosenTCs =
rev_itlist (C ModusPonens) (CONJUNCTS TC_choice_thm) R2inst'd
val rules = simplify [GSYM def1] elim_chosenTCs
val pat_TCs_list = merge (map pat_of pats) (zip (givens pats) TCl)
(* and now induction *)
val aux_ind = Induction.mk_induction theory1
{fconst=faux_const, R=R1, SV=SV,
pat_TCs_list=pat_TCs_list}
val ics = strip_conj(fst(dest_imp(snd(dest_forall(concl aux_ind)))))
fun dest_ic tm = if is_imp tm then strip_conj (fst(dest_imp tm)) else []
val ihs = Lib.flatten (map (dest_ic o snd o strip_forall) ics)
val nested_ihs = filter (can (find_term (aconv faux_const))) ihs
(* a nested ih is of the form
!(c1/\.../\ck ==> R a pat ==> P a)
where "aux R N" occurs in "c1/\.../\ck" or "a". In the latter case,
we have a nested recursion; in the former, there's just a call
to aux in the context. In both cases, we want to eliminate "R a pat"
by assuming "c1/\.../\ck ==> R a pat" and doing some work. Really,
what we prove is something of the form
!(c1/\.../\ck ==> R a pat) |-
(!(c1/\.../\ck ==> R a pat ==> P a))
=
(!(c1/\.../\ck ==> P a))
where the c1/\.../\ck might not be there (when there is no
context for the recursive call), and where !( ... ) denotes
a universal prefix.
*)
fun simp_nested_ih nih =
let val (lvs,tm) = strip_forall nih
val (ants,Pa) = strip_imp_only tm
val P = rator Pa (* keep R, P, and SV unquantified *)
val vs = op_set_diff aconv (free_varsl ants) (R1::P::SV)
val V = op_union aconv lvs vs
val has_context = (length ants = 2)
val ng = list_mk_forall(V,list_mk_imp (front_last ants))
val th1 = SPEC_ALL (ASSUME ng)
val th1a = if has_context then UNDISCH th1 else th1
val th2 = SPEC_ALL (ASSUME nih)
val th2a = if has_context then UNDISCH th2 else th2
val Rab = fst(dest_imp(concl th2a))
val th3 = MP th2a th1a
val th4 = if has_context
then DISCH (fst(dest_imp(snd(strip_forall ng)))) th3
else th3
val th5 = GENL lvs th4
val th6 = DISCH nih th5
val tha = SPEC_ALL(ASSUME (concl th5))
val thb = if has_context then UNDISCH tha else tha
val thc = DISCH Rab thb
val thd = if has_context
then DISCH (fst(dest_imp(snd(strip_forall ng)))) thc
else thc
val the = GENL lvs thd
val thf = DISCH_ALL the
in
MATCH_MP (MATCH_MP IMP_ANTISYM_AX th6) thf
end handle e => raise wrap_exn "nestrec.simp_nested_ih"
"failed while trying to generated nested ind. hyp." e
val nested_ih_simps = map simp_nested_ih nested_ihs
val ind0 = simplify nested_ih_simps aux_ind
val ind1 = UNDISCH_ALL (SPEC R2 (GEN R1 (DISCH_ALL ind0)))
val ind2 = simplify [GSYM def1] ind1
val ind3 = itlist ALPHA_PROVE_HYP (CONJUNCTS TC_choice_thm) ind2
in
{rules = CONJUNCTS rules,
ind = ind3,
SV = SV,
R = R1,
theory = theory1, aux_def = def, def = def1,
aux_rules = map UNDISCH_ALL disch'dl_1,
aux_ind = aux_ind
}
end;
(*---------------------------------------------------------------------------
Performs tupling and also eta-expansion.
---------------------------------------------------------------------------*)
fun tuple_args alist =
let
val find = Lib.C assoc1 alist
fun tupelo tm =
case dest_term tm of
LAMB (Bvar, Body) => mk_abs (Bvar, tupelo Body)
| _ =>
let
val (g, args) = strip_comb tm
val args' = map tupelo args
in
case find g of
NONE => list_mk_comb (g, args')
| SOME (_, (stem', argtys)) =>
if length args < length argtys (* partial application *)
then
let
val nvs = map (curry mk_var "a") (drop args argtys)
val nvs' = variants (free_varsl args') nvs
val comb' = mk_comb(stem', list_mk_pair(args' @nvs'))
in
list_mk_abs(nvs', comb')
end
else mk_comb(stem', list_mk_pair args')
end
in
tupelo
end;
(*---------------------------------------------------------------------------
Mutual recursion. This is reduced to an ordinary definition by
use of sum types. The n mutually recursive functions are mapped
to a single function "mut" having domain and range be sums of
the domains and ranges of the given functions. The domain sum
has n components. The range sum has k <= n components, built from
the set of range types. The arguments of the left hand side of
the function are uniformly injected into the domain sum. On the
right hand side, every occurrence of a function "f a" is translated
to "OUT(mut (IN a))", where IN is the compound injection function,
and OUT brings the result back to the original type of "f a".
Finally, each rhs is injected into the range sum.
After that translation, "mut" is defined. And then the individual
functions are defined. Rewriting then brings them out.
After that, induction is easy to recover from the induction theorem
for mut.
---------------------------------------------------------------------------*)
fun ndom_rng ty 0 = ([],ty)
| ndom_rng ty n =
let val (dom,rng) = dom_rng ty
val (L,last) = ndom_rng rng (n-1)
in (dom::L, last)
end;
fun mutrec thy bindstem eqns =
let val dom_rng = Type.dom_rng
val genvar = Term.genvar
val DEPTH_CONV = Conv.DEPTH_CONV
val BETA_CONV = Thm.BETA_CONV
val OUTL = sumTheory.OUTL
val OUTR = sumTheory.OUTR
val sum_case_def = sumTheory.sum_case_def
val CONJ = Thm.CONJ
fun dest_atom tm = (dest_var tm handle HOL_ERR _ => dest_const tm)
val eqnl = strip_conj eqns
val lhs_info = mk_set(map ((I##length) o strip_comb o lhs) eqnl)
val div_tys = map (fn (tm,i) => ndom_rng (type_of tm) i) lhs_info
val lhs_info1 = zip (map fst lhs_info) div_tys
val dom_tyl = map (list_mk_prod_type o fst) div_tys
val rng_tyl = mk_set (map snd div_tys)
val mut_dom = end_itlist mk_sum_type dom_tyl
val mut_rng = end_itlist mk_sum_type rng_tyl
val mut_name = unionStem bindstem
val mut = mk_var(mut_name, mut_dom --> mut_rng)
fun inform (f,(doml,rng)) =
let val s = fst(dest_atom f)
in if 1<length doml
then (f, (mk_var(s^"_TUPLED",list_mk_prod_type doml --> rng),doml))
else (f, (f,doml))
end
val eqns' = tuple_args (map inform lhs_info1) eqns
val eqnl' = strip_conj eqns'
val (L,R) = unzip (map dest_eq eqnl')
val fnl' = mk_set (map (fst o strip_comb o lhs) eqnl')
val fnvar_map = zip lhs_info1 fnl'
val gvl = map genvar dom_tyl
val gvr = map genvar rng_tyl
val injmap = zip fnl' (map2 (C (curry mk_abs)) (inject mut_dom gvl) gvl)
fun mk_lhs_mut_app (f,arg) =
mk_comb(mut,beta_conv (mk_comb(assoc f injmap,arg)))
val L1 = map (mk_lhs_mut_app o dest_comb) L
val gv_mut_rng = genvar mut_rng
val outfns = map (curry mk_abs gv_mut_rng) (project rng_tyl mut_rng gv_mut_rng)
val ty_outs = zip rng_tyl outfns
(* now replace each f by \x. outbar(mut(inbar x)) *)
fun fout f = (f,assoc (#2(dom_rng(type_of f))) ty_outs)
val RNG_OUTS = map fout fnl'
fun mk_rhs_mut f v =
(f |-> mk_abs(v,beta_conv (mk_comb(assoc f RNG_OUTS,
mk_lhs_mut_app (f,v)))))
val R1 = map (Term.subst (map2 mk_rhs_mut fnl' gvl)) R
val eqnl1 = zip L1 R1
val rng_injmap =
zip rng_tyl (map2 (C (curry mk_abs)) (inject mut_rng gvr) gvr)
fun f_rng_in f = (f,assoc (#2(dom_rng(type_of f))) rng_injmap)
val RNG_INS = map f_rng_in fnl'
val tmp = zip (map (#1 o dest_comb) L) R1
val R2 = map (fn (f,r) => beta_conv(mk_comb(assoc f RNG_INS, r))) tmp
val R3 = map (rhs o concl o QCONV (DEPTH_CONV BETA_CONV)) R2
val mut_eqns = list_mk_conj(map mk_eq (zip L1 R3))
val wfrec_res = wfrec_eqns thy mut_eqns
val defn =
if exists I (#3(unzip3 (#extracta wfrec_res))) (* nested *)
then let val {rules,ind,aux_rules, aux_ind, theory, def,aux_def,...}
= nestrec thy mut_name wfrec_res
in {rules=rules, ind=ind, theory=theory,
aux=SOME{rules=aux_rules, ind=aux_ind}}
end
else let val {rules,R,SV,theory,full_pats_TCs,...}
= stdrec thy mut_name wfrec_res
val f = #1(dest_comb(lhs (concl(Lib.trye hd rules))))
val ind = Induction.mk_induction theory
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
in {rules=rules, ind=ind, theory=theory, aux=NONE}
end
val theory1 = #theory defn
val mut_rules = #rules defn
val mut_constSV = #1(dest_comb(lhs(concl (hd mut_rules))))
val (mut_const,params) = strip_comb mut_constSV
fun define_subfn (n,((fvar,(argtys,rng)),ftupvar)) thy =
let val inbar = assoc ftupvar injmap
val outbar = assoc ftupvar RNG_OUTS
val (fvarname,_) = dest_atom fvar
val defvars = rev
(Lib.with_flag (Globals.priming, SOME"") (variants [fvar])
(map (curry mk_var "x") argtys))
val tup_defvars = list_mk_pair defvars
val newty = itlist (curry (op-->)) (map type_of params@argtys) rng
val fvar' = mk_var(fvarname,newty)
val dlhs = list_mk_comb(fvar',params@defvars)
val Uapp = mk_comb(mut_constSV,
beta_conv(mk_comb(inbar,list_mk_pair defvars)))
val drhs = beta_conv (mk_comb(outbar,Uapp))
val thybind = defExtract(mut_name,n)
in
(make_definition thy thybind (mk_eq(dlhs,drhs)) , (Uapp,outbar))
end
fun mk_def triple (defl,thy,Uout_map) =
let val ((d,thy'),Uout) = define_subfn triple thy
in (d::defl, thy', Uout::Uout_map)
end
val (defns,theory2,Uout_map) =
itlist mk_def (Lib.enumerate 0 fnvar_map) ([],theory1,[])
fun apply_outmap th =
let fun matches (pat,_) = Lib.can (Term.match_term pat)
(lhs (concl th))
val (_,outf) = Lib.first matches Uout_map
in AP_TERM outf th
end
val mut_rules1 = map apply_outmap mut_rules
val simp = Rules.simplify (OUTL::OUTR::map GSYM defns)
(* finally *)