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
|
open HolKernel boolLib bossLib IndDefLib IndDefRules listTheory optionTheory relationTheory pairTheory
open rich_listTheory combinTheory;
open ottTheory ottLib caml_typedefTheory;
open utilTheory shiftTheory;
val _ = new_theory "basic";
val OPTION_MAP_I = Q.prove (
`!x. OPTION_MAP (\y . y) x = x`,
Cases THEN SRW_TAC [] []);
val domEB_def = Define
`(domEB EB_tv = name_tv) /\
(domEB (EB_vn value_name typescheme) = name_vn value_name) /\
(domEB (EB_cc constr_name typeconstr) = name_cn constr_name) /\
(domEB (EB_pc constr_name type_params_opt t_list typeconstr) = name_cn constr_name) /\
(domEB (EB_td typeconstr_name kind) = name_tcn typeconstr_name) /\
(domEB (EB_ta type_params_opt typeconstr_name t) = name_tcn typeconstr_name) /\
(domEB (EB_tr typeconstr_name kind field_name_list) = name_tcn typeconstr_name) /\
(domEB (EB_fn field_name type_params_opt typeconstr_name typexpr) = name_fn field_name) /\
(domEB (EB_l location t) = name_l location)`;
val domEB_thm = Q.prove (
`!EB name. JdomEB EB name = (domEB EB = name)`,
Cases THEN SRW_TAC [] [JdomEB_cases, domEB_def, clause_name_def] THEN METIS_TAC [typexprs_nchotomy]);
val domE_thm = Q.prove (
`!E names. JdomE E names = (MAP domEB E = names)`,
Induct THENL
[SRW_TAC [] [Once JdomE_cases, clause_name_def] THEN METIS_TAC [],
SRW_TAC [] [Once JdomE_cases, domEB_thm, clause_name_def] THEN METIS_TAC []]);
val lookup_def = Define
`(lookup [] name = NONE) /\
(lookup (EB::E) name =
if domEB EB = name then
SOME EB
else OPTION_MAP (\EB2. shiftEB 0 (if domEB EB = name_tv then 1 else 0) EB2) (lookup E name))`;
val lookup_append_thm = Q.store_thm ("lookup_append_thm",
`!E1 E2 name. lookup (E1++E2) name =
case lookup E1 name of
NONE => OPTION_MAP (\EB. shiftEB 0 (num_tv E1) EB) (lookup E2 name)
| SOME EB => SOME EB`,
Induct THEN SRW_TAC [] [lookup_def, num_tv_def, OPTION_MAP_I, shiftEB_add_thm] THEN
Cases_on `lookup E1 name` THEN FULL_SIMP_TAC list_ss [] THEN Cases_on `lookup E2 name` THEN
SRW_TAC [] [] THEN Cases_on `h` THEN SRW_TAC [] [num_tv_def, shiftEB_add_thm] THEN
FULL_SIMP_TAC list_ss [domEB_def] THEN SRW_TAC [] []);
val lookup_dom_thm = Q.store_thm ("lookup_dom_thm",
`!E name. (MEM name (MAP domEB E) = ?EB. lookup E name = SOME EB) /\
(~MEM name (MAP domEB E) = (lookup E name = NONE))`,
Induct THEN SRW_TAC [] [lookup_def] THEN METIS_TAC [NOT_SOME_NONE]);
val lookup_thm = Q.prove (
`!E name EB. Jlookup_EB E name EB = (lookup E name = SOME EB)`,
Induct THENL [
SRW_TAC [] [Once Jlookup_cases, lookup_def, clause_name_def],
SIMP_TAC list_ss [Once Jlookup_cases] THEN Cases THEN
SRW_TAC [] [lookup_def, domE_thm, domEB_thm, clause_name_def] THEN EQ_TAC THEN
SRW_TAC [] [domEB_def] THEN
FULL_SIMP_TAC list_ss [domEB_def, name_distinct, name_11, shiftEB_add_thm]]);
val idx_bound_def = Define
`(idx_bound [] idx = F) /\
(idx_bound (EB_tv::E) 0 = T) /\
(idx_bound (EB_tv::E) (SUC n2) = idx_bound E n2) /\
(idx_bound (_::E) n = idx_bound E n)`;
val idx_bound_thm = Q.prove (
`!E idx num. Jidx_bound E idx = idx_bound E idx`,
Induct THENL [
SRW_TAC [] [Once Jidx_cases, idx_bound_def],
SRW_TAC [] [Once Jidx_cases, idx_bound_def, clause_name_def] THEN
Cases_on `h` THEN SRW_TAC [] [idx_bound_def, domEB_thm, domEB_def] THEN
Cases_on `idx` THEN SRW_TAC [] [idx_bound_def] THEN FULL_SIMP_TAC list_ss [arithmeticTheory.ADD1]]);
val Slookup_thm = Q.prove (
`!st l v. JSlookup st l v = (list_assoc l st = SOME v)`,
Induct THEN ONCE_REWRITE_TAC [JSlookup_cases] THEN SRW_TAC [] [list_assoc_def, clause_name_def] THEN
Cases_on `h` THEN SRW_TAC [] [list_assoc_def]);
val recfun_def = Define
`recfun (LRBs_inj letrec_bindings) pattern_matching =
(substs_value_name_expr
(MAP (\letrec_binding. case letrec_binding of
LRB_simple x pattern_matching =>
(x , Expr_letrec (LRBs_inj letrec_bindings)
(Expr_ident x)))
letrec_bindings)
(Expr_function pattern_matching))`;
val recfun_thm = Q.prove (
`!letrec_bindings pattern_matching expr. Jrecfun letrec_bindings pattern_matching expr =
(recfun letrec_bindings pattern_matching = expr)`,
Cases THEN SRW_TAC [] [Jrecfun_cases, recfun_def, clause_name_def] THEN EQ_TAC THEN SRW_TAC [] [] THENL
[SRW_TAC [] [MAP_MAP,
Q.prove (`!x. (case (\(a, b). LRB_simple a b) x of LRB_simple a b => P a b) =
(case x of (a, b) => P a b)`,
Cases THEN SRW_TAC [] []),
LAMBDA_PROD],
Q.EXISTS_TAC `MAP (\x. case x of LRB_simple a b => (a, b)) l` THEN
SRW_TAC [] [MAP_MAP,
Q.prove (`!x f. ((\(x_ ,pattern_matching_). f x_)
case x of LRB_simple a b => (a,b)) =
case x of LRB_simple a b => f a`,
Cases THEN SRW_TAC [] [])] THEN
Induct_on `l` THEN SRW_TAC [] [] THEN Cases_on `h` THEN SRW_TAC [] []
]);
val funval_def = Define
`(funval (Expr_uprim unary_prim) = T) /\
(funval (Expr_bprim binary_prim) = T) /\
(funval (Expr_apply (Expr_bprim binary_prim) v) = is_value_of_expr v) /\
(funval (Expr_function pattern_matching) = T) /\
(funval _ = F)`;
val funval_thm = Q.prove (
`!v. Jfunval v = funval v`,
Cases THEN SRW_TAC [] [funval_def, Jfunval_cases, clause_name_def] THEN
Cases_on `e` THEN SRW_TAC [] [funval_def, Jfunval_cases]);
val tp_to_tv_def = Define
`tp_to_tv (TP_var tv) = tv`;
val tp_to_tv_thm = Q.store_thm ("tp_to_tv_thm",
`TP_var (tp_to_tv v) = v`,
Cases_on `v` THEN SRW_TAC [] [tp_to_tv_def]);
val lrbs_to_lrblist_def = Define
`lrbs_to_lrblist (LRBs_inj x) = x`;
val lrbs_to_lrblist_thm = Q.store_thm ("lrbs_to_lrblist_thm",
`!x. LRBs_inj (lrbs_to_lrblist x) = x`,
Cases THEN SRW_TAC [] [lrbs_to_lrblist_def]);
val patexp_to_pelist_def = Define
`patexp_to_pelist (PE_inj x y) = (x, y)`;
val patexp_to_pelist_thm = Q.store_thm ("patexp_to_pelist_thm",
`!x. PE_inj (FST (patexp_to_pelist x)) (SND (patexp_to_pelist x)) = x`,
Cases THEN SRW_TAC [] [patexp_to_pelist_def]);
val tpo_to_tps_def = Define
`tpo_to_tps (TPS_nary tps) = tps`;
val tpo_to_tps_thm = Q.store_thm ("tpo_to_tps_thm",
`!tpo. TPS_nary (tpo_to_tps tpo) = tpo`,
Cases THEN SRW_TAC [] [tpo_to_tps_def]);
val field_to_fn_def = Define
`field_to_fn (F_name f) = f`;
val field_to_fn_thm = Q.store_thm ("field_to_fn_thm",
`!f. F_name (field_to_fn f) = f`,
Cases THEN SRW_TAC [] [field_to_fn_def]);
val t_size_def = Define
`(t_size (TE_var v) = 2:num) /\
(t_size (TE_idxvar a b) = 1) /\
(t_size TE_any = 1) /\
(t_size (TE_arrow t1 t2) = 1 + t_size t1 + t_size t2) /\
(t_size (TE_tuple tlist) = 1 + t1_size tlist) /\
(t_size (TE_constr tlist tc) = 1 + t1_size tlist) /\
(t1_size [] = 1) /\
(t1_size (t1::tlist) = t_size t1 + t1_size tlist)`;
val ts_size_def = Define
`(ts_size (TS_forall t) = 1 + (t_size t))`;
val EB_size_def = Define
`(EB_size EB_tv = 1) /\
(EB_size (EB_vn x ts) = 2 + ts_size ts) /\
(EB_size (EB_cc cn tc) = 3) /\
(EB_size (EB_pc cn (TPS_nary tplist) (typexprs_inj tlist) tc) = 4 + LENGTH tplist + t1_size tlist) /\
(EB_size (EB_fn fn (TPS_nary tplist) tcn t) = 4 + LENGTH tplist + t_size t) /\
(EB_size (EB_td tcn k) = 3) /\
(EB_size (EB_tr tcn k fnlist) = 4 + LENGTH fnlist) /\
(EB_size (EB_ta (TPS_nary tplist) tcn t) = 2 + LENGTH tplist + t_size t) /\
(EB_size (EB_l l t) = 2 + t_size t)`;
val E_size_def = Define
`(E_size [] = 0) /\
(E_size (EB::E) = EB_size EB + E_size E)`;
local
val lem1 = Q.prove (
`!t. 0 < t1_size t`,
Induct THEN SRW_TAC [ARITH_ss] [t_size_def]);
val lem2 = Q.prove (
`!t l. MEM t l ==> t_size t < t1_size l`,
Induct_on `l` THEN SRW_TAC [] [t_size_def] THEN RES_TAC THEN ASSUME_TAC (Q.SPEC `l` lem1) THEN
DECIDE_TAC);
val lem3 = Q.prove (
`!t. 0 < t_size t`,
Induct THEN SRW_TAC [ARITH_ss] [t_size_def]);
in
val Eok_def = tDefine "Eok"
`(Eok [] <=> T) /\
(Eok (EB_tv::E) <=> Eok E) /\
(Eok (EB_vn value_name ts::E) <=> tsok E ts) /\
(Eok (EB_cc constr_name TC_exn::E) <=>
Eok E /\ ~MEM (name_cn constr_name) (MAP domEB E)) /\
(Eok (EB_cc constr_name (TC_name typeconstr_name)::E) <=>
Eok E /\ (?kind. lookup E (name_tcn typeconstr_name) = SOME (EB_td typeconstr_name kind)) /\
~MEM (name_cn constr_name) (MAP domEB E)) /\
(Eok (EB_cc constr_name tc::E) <=> F) /\
(Eok (EB_pc constr_name (TPS_nary []) (typexprs_inj t_list) TC_exn::E) <=>
EVERY (tkind E) t_list /\
~MEM (name_cn constr_name) (MAP domEB E) /\
LENGTH t_list >= 1) /\
(Eok (EB_pc constr_name (TPS_nary vars) (typexprs_inj t_list) (TC_name typeconstr_name)::E) <=>
EVERY (\t. ntsok E vars t) t_list /\
(lookup E (name_tcn typeconstr_name) = SOME (EB_td typeconstr_name (LENGTH vars))) /\
~MEM (name_cn constr_name) (MAP domEB E) /\
LENGTH t_list >= 1) /\
(Eok (EB_pc constr_name params (typexprs_inj t_list) tc::E) <=> F) /\
(Eok (EB_fn field_name (TPS_nary vars) typeconstr_name t::E) <=>
ntsok E vars t /\
~MEM (name_fn field_name) (MAP domEB E) /\
?field_name_list. (lookup E (name_tcn typeconstr_name) =
SOME (EB_tr typeconstr_name (LENGTH vars) field_name_list)) /\
MEM field_name field_name_list) /\
(Eok (EB_td typeconstr_name kind::E) <=>
Eok E /\
~MEM (name_tcn typeconstr_name) (MAP domEB E)) /\
(Eok (EB_ta (TPS_nary vars) typeconstr_name t::E) <=>
~MEM (name_tcn typeconstr_name) (MAP domEB E) /\ ntsok E vars t) /\
(Eok (EB_tr typeconstr_name kind field_name_list::E) <=>
Eok E /\
~MEM (name_tcn typeconstr_name) (MAP domEB E) /\
ALL_DISTINCT (MAP name_fn field_name_list)) /\
(Eok (EB_l location t::E) <=>
tkind E t /\
~MEM (name_l location) (MAP domEB E)) /\
(typeconstr_kind E (TC_name typeconstr_name) =
if Eok E then
case lookup E (name_tcn typeconstr_name) of
NONE => NONE
| SOME (EB_td tcn kind) => SOME kind
| SOME (EB_ta (TPS_nary type_params_opt) tcn t) =>
if ALL_DISTINCT type_params_opt then
SOME (LENGTH type_params_opt)
else
NONE
| SOME (EB_tr tcn kind field_name_list) =>
SOME kind
else
NONE) /\
(typeconstr_kind E TC_int = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_char = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_string = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_float = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_bool = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_unit = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_exn = if Eok E then SOME 0 else NONE) /\
(typeconstr_kind E TC_list = if Eok E then SOME 1 else NONE) /\
(typeconstr_kind E TC_option = if Eok E then SOME 1 else NONE) /\
(typeconstr_kind E TC_ref = if Eok E then SOME 1 else NONE) /\
(tsok E (TS_forall t) = tkind (EB_tv::E) t) /\
(ntsok E vars t <=>
ALL_DISTINCT vars /\
tkind E (substs_typevar_typexpr (MAP (\tp. (tp_to_tv tp, TE_constr [] TC_unit)) vars) t)) /\
(tkind E (TE_var typevar) <=> F) /\
(tkind E (TE_idxvar idx n) <=>
Eok E /\ idx_bound E idx) /\
(tkind E TE_any <=> F) /\
(tkind E (TE_arrow t1 t2) <=>
tkind E t1 /\ tkind E t2) /\
(tkind E (TE_tuple t_list) <=>
EVERY (tkind E) t_list /\ LENGTH t_list >= 2) /\
(tkind E (TE_constr t_list typeconstr) <=>
(typeconstr_kind E typeconstr = SOME (LENGTH t_list)) /\ EVERY (tkind E) t_list)`
(WF_REL_TAC `inv_image ($< LEX $<)
(\a. (sum_size (E_size)
(sum_size (\(x,y). E_size x)
(sum_size (\(x,y). E_size x + ts_size y)
(sum_size (\(x,y,z). E_size x + t_size z)
(\(x,y). E_size x))))) a,
(sum_size (\x. 0)
(sum_size (\(x,y). 1)
(sum_size (\x. 0)
(sum_size (\(x,y,z). 0)
(\(x,y). t_size y))))) a)` THEN
SRW_TAC [ARITH_ss] [LENGTH_REVERSE, E_size_def, EB_size_def, t_size_def, ts_size_def, lem1, lem3] THEN
IMP_RES_TAC lem2 THEN SRW_TAC [ARITH_ss] [EB_size_def, ts_size_def]);
val Eok_ind = fetch "-" "Eok_ind";
end;
val lookup_name_thm = Q.store_thm ("lookup_name_thm",
`!E.
(!tv EB. (lookup E name_tv = SOME EB) ==> (EB = EB_tv)) /\
(!vn EB. (lookup E (name_vn vn) = SOME EB) ==> ?ts. EB = EB_vn vn ts) /\
(!cn EB. (lookup E (name_cn cn) = SOME EB) ==> (?typeconstr. EB = EB_cc cn typeconstr) \/
?typ tlist typeconstr. EB = EB_pc cn typ tlist typeconstr) /\
(!tcn EB. (lookup E (name_tcn tcn) = SOME EB) ==> (?kind. EB = EB_td tcn kind) \/
(?tpo t. EB = EB_ta tpo tcn t) \/
?k fnl. EB = EB_tr tcn k fnl) /\
(!fn EB. (lookup E (name_fn fn) = SOME EB) ==> ?tpo tcn t. EB = EB_fn fn tpo tcn t) /\
(!l EB. (lookup E (name_l l) = SOME EB) ==> ?t. EB = EB_l l t)`,
Induct THEN SRW_TAC [] [lookup_def, domEB_def, shiftEB_add_thm] THEN RES_TAC THEN SRW_TAC [] [shiftEB_def] THEN
Cases_on `EB` THEN
FULL_SIMP_TAC list_ss [domEB_def, name_11, name_distinct] THEN METIS_TAC []);
local
val SIMP = SIMP_RULE bool_ss [clause_name_def, EVERY_MAP, EVERY_CONJ, ETA_THM, LAMBDA_PROD2, lookup_thm,
domE_thm, idx_bound_thm];
val JTEok_rules2 = SIMP JTEok_rules;
val JTEok_cases2 = SIMP JTEok_cases;
in
val Eok_thm = Q.prove (
`(!E. JTEok E <=> Eok E) /\
(!E tc k. JTtypeconstr E tc k <=> (typeconstr_kind E tc = SOME k)) /\
(!E ts k. JTts E ts k <=> tsok E ts /\ (k = 0)) /\
(!E tps t k. JTtsnamed E (TPS_nary tps) t k <=> ntsok E tps t /\ (k = 0)) /\
(!E t k. JTt E t k <=> tkind E t /\ (k = 0))`,
HO_MATCH_MP_TAC Eok_ind THEN
SRW_TAC [ARITH_ss] [Eok_def, domE_thm, lookup_thm, JTEok_rules2] THEN
ONCE_REWRITE_TAC [JTEok_cases2] THEN SRW_TAC [ARITH_ss] [EVERY_MEM] THENL [
EQ_TAC THEN SRW_TAC [] [] THEN1 METIS_TAC [] THEN
Cases_on `ts` THEN SRW_TAC [] [] THEN Cases_on `t` THEN SRW_TAC [] [],
METIS_TAC [],
EQ_TAC THEN SRW_TAC [] [] THEN
FULL_SIMP_TAC list_ss [MAP_MAP, MAP_REVERSE] THEN
SRW_TAC [] [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN
Q.EXISTS_TAC `MAP tp_to_tv tps` THEN
SRW_TAC [] [MAP_MAP, MAP_I, tp_to_tv_thm] THEN METIS_TAC [],
EQ_TAC THEN SRW_TAC [] [] THEN
FULL_SIMP_TAC list_ss [MAP_MAP, MAP_REVERSE] THEN
SRW_TAC [] [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN
Q.EXISTS_TAC `MAP tp_to_tv tps` THEN
SRW_TAC [] [MAP_MAP, MAP_I, tp_to_tv_thm] THEN METIS_TAC [],
EQ_TAC THEN SRW_TAC [] [] THEN
FULL_SIMP_TAC list_ss [MAP_MAP, MAP_REVERSE] THEN
SRW_TAC [] [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN
Q.EXISTS_TAC `MAP tp_to_tv tps` THEN
SRW_TAC [] [MAP_MAP, MAP_I, tp_to_tv_thm] THEN METIS_TAC [],
Cases_on `lookup E (name_tcn typeconstr_name)` THEN SRW_TAC [] []
THEN IMP_RES_TAC lookup_name_thm THEN SRW_TAC [] [] THEN
FULL_SIMP_TAC list_ss [name_11, name_distinct] THEN
Cases_on `tpo` THEN SRW_TAC [ARITH_ss] [clause_name_def, JTtps_kind_cases] THEN METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
EQ_TAC THEN SRW_TAC [] [] THEN FULL_SIMP_TAC list_ss [MAP_MAP, tp_to_tv_def] THEN1 METIS_TAC [] THEN
Q.EXISTS_TAC `MAP tp_to_tv tps` THEN SRW_TAC [] [tp_to_tv_def, MAP_MAP, tp_to_tv_thm, MAP_I],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC []]);
end;
val idxsub_def = ottDefine "idxsub"
`(idxsub tl (TE_var v) = TE_var v) /\
(idxsub tl (TE_idxvar 0 n) = if n < LENGTH tl then EL n tl else TE_constr [] TC_unit) /\
(idxsub tl (TE_idxvar (SUC n) n') = TE_idxvar n n') /\
(idxsub tl TE_any = TE_any) /\
(idxsub tl (TE_arrow t1 t2) = TE_arrow (idxsub tl t1) (idxsub tl t2)) /\
(idxsub tl (TE_tuple tl') = TE_tuple (MAP (idxsub tl) tl')) /\
(idxsub tl (TE_constr tl' tcn) = TE_constr (MAP (idxsub tl) tl') tcn)`;
val idxsubn0_thm = Q.store_thm ("idxsubn0_thm",
`(!t tl. idxsubn 0 tl t = idxsub tl t) /\
(!tl' tl. MAP (idxsubn 0 tl) tl' = MAP (idxsub tl) tl')`,
Induct THEN SRW_TAC [] [idxsubn_def, idxsub_def, GSYM ETA_THM] THEN1
(Cases_on `n` THEN SRW_TAC [] [idxsub_def]) THEN METIS_TAC []);
local
val JTidxsub_fun = structural_cases [typexpr_11, typexpr_distinct]
1
[get_terms ftv_typexpr_def]
JTidxsub_cases;
val lem1 = Q.prove (
`!tl t t'. JTidxsub tl t t' ==> (t' = idxsub tl t)`,
RULE_INDUCT_TAC JTidxsub_ind [idxsub_def, LAMBDA_PROD2, EVERY_MAP, MAP_MAP, GSYM arithmeticTheory.ADD1]
[([``"JTinxsub_idx0"``, ``"JTinxsub_idx1"``],
SRW_TAC [] [] THEN FULL_SIMP_TAC list_ss [EL_APPEND1, EL_APPEND2]),
([``"JTinxsub_tuple"``, ``"JTinxsub_tc"``],
Induct THEN SRW_TAC [] [])]);
val lem2 = Q.prove (
`!tl t t'. (t' = idxsub tl t) ==> JTidxsub tl t t'`,
HO_MATCH_MP_TAC (fetch "-" "idxsub_ind") THEN
SRW_TAC [] [JTidxsub_fun, idxsub_def, clause_name_def, EVERY_MAP, LAMBDA_PROD2] THENL
[DISJ1_TAC THEN MAP_EVERY Q.EXISTS_TAC [`LASTN (LENGTH tl - n - 1) tl`, `FIRSTN n tl`] THEN
SRW_TAC [ARITH_ss] [LENGTH_FIRSTN] THEN METIS_TAC [FIRSTN_EL_LASTN],
DISJ2_TAC THEN DECIDE_TAC,
DECIDE_TAC,
Q.EXISTS_TAC `MAP (\t. (t, idxsub tl t)) tl'` THEN SRW_TAC [] [MAP_MAP, MAP_I, EVERY_MAP, EVERY_MEM],
Q.EXISTS_TAC `MAP (\t. (t, idxsub tl t)) tl'` THEN
SRW_TAC [] [MAP_MAP, MAP_I, EVERY_MAP, EVERY_MEM]]);
in
val idxsub_thm = Q.prove (
`!tl t t'. JTidxsub tl t t' = (t' = idxsub tl t)`,
METIS_TAC [lem1, lem2]);
end;
val SIMP1 = SIMP_RULE bool_ss [EVERY_MAP, EVERY_CONJ, ETA_THM, LAMBDA_PROD2, lookup_thm, Slookup_thm,
idx_bound_thm, domE_thm, recfun_thm, funval_thm, Eok_thm, idxsub_thm];
val SIMP2 = SIMP_RULE bool_ss [EVERY_MAP, EVERY_CONJ, ETA_THM, LAMBDA_PROD2, lookup_thm, Slookup_thm,
idx_bound_thm, domE_thm, recfun_thm, funval_thm, Eok_thm, clause_name_def,
idxsub_thm];
val JM_matchP_cases = save_thm ("JM_matchP_cases", SIMP2 JmatchP_cases);
val _ = save_thm ("JM_matchP_sind", SIMP1 (derive_strong_induction (JmatchP_rules, JmatchP_ind)));
val _ = save_thm ("JM_matchP_ind", SIMP1 JmatchP_ind);
val _ = save_thm ("JM_matchP_rules", SIMP2 JmatchP_rules);
val JM_match_cases = save_thm ("JM_match_cases", SIMP2 Jmatch_cases);
val _ = save_thm ("JM_match_sind", SIMP1 (derive_strong_induction (Jmatch_rules, Jmatch_ind)));
val _ = save_thm ("JM_match_ind", SIMP1 Jmatch_ind);
val _ = save_thm ("JM_match_rules", SIMP2 Jmatch_rules);
val JRB_dbehaviour_cases = save_thm ("JRB_dbehaviour_cases", SIMP2 Jdbehaviour_cases);
val _ = save_thm ("JRB_dbehaviour_ind", SIMP1 Jdbehaviour_ind);
val _ = save_thm ("JRB_dbehaviour_rules", SIMP2 Jdbehaviour_rules);
val JRB_ebehaviour_cases = save_thm ("JRB_ebehaviour_cases", SIMP2 Jebehaviour_cases);
val _ = save_thm ("JRB_ebehaviour_ind", SIMP1 Jebehaviour_ind);
val _ = save_thm ("JRB_ebehaviour_rules", SIMP2 Jebehaviour_rules);
val JR_expr_cases = save_thm ("JR_expr_cases", SIMP2 Jred_cases);
val _ = save_thm ("JR_expr_sind", SIMP1 (derive_strong_induction (Jred_rules, Jred_ind)));
val _ = save_thm ("JR_expr_ind", SIMP1 Jred_ind);
val _ = save_thm ("JR_expr_rules", SIMP2 Jred_rules);
val JRbprim_cases = save_thm ("JRbprim_cases", SIMP2 JRbprim_cases);
val _ = save_thm ("JRbprim_ind", SIMP1 JRbprim_ind);
val _ = save_thm ("JRbprim_rules", SIMP2 JRbprim_rules);
val JRdefn_cases = save_thm ("JRdefn_cases", SIMP2 JRdefn_cases);
val _ = save_thm ("JRdefn_sind", SIMP1 (derive_strong_induction (JRdefn_rules, JRdefn_ind)));
val _ = save_thm ("JRdefn_ind", SIMP1 JRdefn_ind);
val _ = save_thm ("JRdefn_rules", SIMP2 JRdefn_rules);
val JRmatching_step_cases = save_thm ("JRmatching_step_cases", SIMP2 JRmatching_step_cases);
val _ = save_thm ("JRmatching_step_ind", SIMP1 JRmatching_step_ind);
val _ = save_thm ("JRmatching_step_rules", SIMP2 JRmatching_step_rules);
val JRmatching_success_cases = save_thm ("JRmatching_success_cases", SIMP2 JRmatching_success_cases);
val _ = save_thm ("JRmatching_success_ind", SIMP1 JRmatching_success_ind);
val _ = save_thm ("JRmatching_success_rules", SIMP2 JRmatching_success_rules);
val JRstore_cases = save_thm ("JRstore_cases", SIMP2 JRstore_cases);
val _ = save_thm ("JRstore_ind", SIMP1 JRstore_ind);
val _ = save_thm ("JRstore_rules", SIMP2 JRstore_rules);
val JRtop_cases = save_thm ("JRtop_cases", SIMP2 JRtop_cases);
val _ = save_thm ("JRtop_ind", SIMP1 JRtop_ind);
val _ = save_thm ("JRtop_rules", SIMP2 JRtop_rules);
val JRuprim_cases = save_thm ("JRuprim_cases", SIMP2 JRuprim_cases);
val _ = save_thm ("JRuprim_ind", SIMP1 JRuprim_ind);
val _ = save_thm ("JRuprim_rules", SIMP2 JRuprim_rules);
val JTbprim_cases = save_thm ("JTbprim_cases", SIMP2 JTbprim_cases);
val _ = save_thm ("JTbprim_ind", SIMP1 JTbprim_ind);
val _ = save_thm ("JTbprim_rules", SIMP2 JTbprim_rules);
val JTconst_cases = save_thm ("JTconst_cases", SIMP2 JTconst_cases);
val _ = save_thm ("JTconst_ind", SIMP1 JTconst_ind);
val _ = save_thm ("JTconst_rules", SIMP2 JTconst_rules);
val JTconstr_c_cases = save_thm ("JTconstr_c_cases", SIMP2 JTconstr_c_cases);
val _ = save_thm ("JTconstr_c_ind", SIMP1 JTconstr_c_ind);
val _ = save_thm ("JTconstr_c_rules", SIMP2 JTconstr_c_rules);
val JTconstr_decl_cases = save_thm ("JTconstr_decl_cases", SIMP2 JTconstr_decl_cases);
val _ = save_thm ("JTconstr_decl_ind", SIMP1 JTconstr_decl_ind);
val _ = save_thm ("JTconstr_decl_rules", SIMP2 JTconstr_decl_rules);
val JTconstr_p_cases = save_thm ("JTconstr_p_cases", SIMP2 JTconstr_p_cases);
val _ = save_thm ("JTconstr_p_ind", SIMP1 JTconstr_p_ind);
val _ = save_thm ("JTconstr_p_rules", SIMP2 JTconstr_p_rules);
val JTdefinition_cases = save_thm ("JTdefinition_cases", SIMP2 JTdefinition_cases);
val _ = save_thm ("JTdefinition_ind", SIMP1 JTdefinition_ind);
val _ = save_thm ("JTdefinition_rules", SIMP2 JTdefinition_rules);
val JTdefinitions_cases = save_thm ("JTdefinitions_cases", SIMP2 JTdefinitions_cases);
val _ = save_thm ("JTdefinitions_sind",
SIMP1 (derive_strong_induction (JTdefinitions_rules, JTdefinitions_ind)));
val _ = save_thm ("JTdefinitions_ind", SIMP1 JTdefinitions_ind);
val _ = save_thm ("JTdefinitions_rules", SIMP2 JTdefinitions_rules);
val JTe_cases = save_thm ("JTe_cases", SIMP2 JTe_cases);
val _ = save_thm ("JTe_sind", SIMP1 (derive_strong_induction (JTe_rules, JTe_ind)));
val _ = save_thm ("JTe_ind", SIMP1 JTe_ind);
val _ = save_thm ("JTe_rules", SIMP2 JTe_rules);
val JTeq_cases = save_thm ("JTeq_cases", SIMP2 JTeq_cases);
val _ = save_thm ("JTeq_ind", SIMP1 JTeq_ind);
val _ = save_thm ("JTeq_rules", SIMP2 JTeq_rules);
val JTfield_decl_cases = save_thm ("JTfield_decl_cases", SIMP2 JTfield_decl_cases);
val _ = save_thm ("JTfield_decl_ind", SIMP1 JTfield_decl_ind);
val _ = save_thm ("JTfield_decl_rules", SIMP2 JTfield_decl_rules);
val JTfield_cases = save_thm ("JTfield_cases", SIMP2 JTfield_cases);
val _ = save_thm ("JTfield_ind", SIMP1 JTfield_ind);
val _ = save_thm ("JTfield_rules", SIMP2 JTfield_rules);
val JTinst_cases = save_thm ("JTinst_cases", SIMP2 JTinst_cases);
val _ = save_thm ("JTinst_ind", SIMP1 JTinst_ind);
val _ = save_thm ("JTinst_rules", SIMP2 JTinst_rules);
val JTinst_named_cases = save_thm ("JTinst_named_cases", SIMP2 JTinst_named_cases);
val _ = save_thm ("JTinst_named_ind", SIMP1 JTinst_named_ind);
val _ = save_thm ("JTinst_named_rules", SIMP2 JTinst_named_rules);
val JTinst_any_cases = save_thm ("JTinst_any_cases", SIMP2 JTinst_any_cases);
val _ = save_thm ("JTinst_any_ind", SIMP1 JTinst_any_ind);
val _ = save_thm ("JTinst_any_rules", SIMP2 JTinst_any_rules);
val JTLin_cases = save_thm ("JTLin_cases", SIMP2 JTLin_cases);
val _ = save_thm ("JTLin_ind", SIMP1 JTLin_ind);
val _ = save_thm ("JTLin_rules", SIMP2 JTLin_rules);
val JTLout_cases = save_thm ("JTLout_cases", SIMP2 JTLout_cases);
val _ = save_thm ("JTLout_ind", SIMP1 JTLout_ind);
val _ = save_thm ("JTLout_rules", SIMP2 JTLout_rules);
val JTpat_cases = save_thm ("JTpat_cases", SIMP2 JTpat_cases);
val _ = save_thm ("JTpat_sind", SIMP1 (derive_strong_induction (JTpat_rules, JTpat_ind)));
val _ = save_thm ("JTpat_ind", SIMP1 JTpat_ind);
val _ = save_thm ("JTpat_rules", SIMP2 JTpat_rules);
val JTstore_cases = save_thm ("JTstore_cases", SIMP2 JTstore_cases);
val _ = save_thm ("JTstore_sind", SIMP1 (derive_strong_induction (JTstore_rules, JTstore_ind)));
val _ = save_thm ("JTstore_ind", SIMP1 JTstore_ind);
val _ = save_thm ("JTstore_rules", SIMP2 JTstore_rules);
val JTtype_definition_cases = save_thm ("JTtype_definition_cases", SIMP2 JTtype_definition_cases);
val _ = save_thm ("JTtype_definition_ind", SIMP1 JTtype_definition_ind);
val _ = save_thm ("JTtype_definition_rules", SIMP2 JTtype_definition_rules);
val JTtypedef_cases = save_thm ("JTtypedef_cases", SIMP2 JTtypedef_cases);
val _ = save_thm ("JTtypedef_ind", SIMP1 JTtypedef_ind);
val _ = save_thm ("JTtypedef_rules", SIMP2 JTtypedef_rules);
val JTuprim_cases = save_thm ("JTuprim_cases", SIMP2 JTuprim_cases);
val _ = save_thm ("JTuprim_ind", SIMP1 JTuprim_ind);
val _ = save_thm ("JTuprim_rules", SIMP2 JTuprim_rules);
val JTvalue_name_cases = save_thm ("JTvalue_name_cases", SIMP2 JTval_cases);
val _ = save_thm ("JTvalue_name_ind", SIMP1 JTval_ind);
val _ = save_thm ("JTvalue_name_rules", SIMP2 JTval_rules);
val JTtop_cases = save_thm ("JTtop_cases", SIMP2 JTtop_cases);
val _ = save_thm ("JTtop_ind", SIMP1 JTtop_ind);
val _ = save_thm ("JTtop_rules", SIMP2 JTtop_rules);
val JTprog_cases = save_thm ("JTprog_cases", SIMP2 JTprog_cases);
val _ = save_thm ("JTprog_ind", SIMP1 JTprog_ind);
val _ = save_thm ("JTprog_rules", SIMP2 JTprog_rules);
val is_binary_prim_app_value_of_expr_thm = Q.prove (
`!e. is_binary_prim_app_value_of_expr e = (?bp. e = Expr_bprim bp)`,
Cases THEN SRW_TAC [] [is_binary_prim_app_value_of_expr_def]);
val _ = save_thm ("is_value_of_expr_def",
PURE_REWRITE_RULE [is_binary_prim_app_value_of_expr_thm] is_value_of_expr_def);
val expr_terms = get_terms is_value_of_expr_def;
val pattern_matching_terms = [``PM_pm pat_exp_list``];
val let_binding_terms = [``LB_simple pattern expr``];
val letrec_binding_terms = [``LRBs_inj letrec_binding_list``];
val _ = save_thm ("JTe_fun",
structural_cases [expr_11, expr_distinct, pattern_matching_11,
let_binding_11, letrec_bindings_11]
2
[expr_terms, pattern_matching_terms, let_binding_terms, letrec_binding_terms]
JTe_cases);
val _ = save_thm ("JR_expr_fun",
structural_cases [expr_11, expr_distinct]
0
[expr_terms]
JR_expr_cases);
val _ = save_thm ("JTpat_fun",
structural_cases [pattern_11, pattern_distinct]
2
[get_terms ftv_pattern_def]
JTpat_cases);
val _ = save_thm ("JTconst_fun",
structural_cases [constant_11, constant_distinct]
1
[[``CONST_int n``, ``CONST_float f``, ``CONST_char c``, ``CONST_string s``,
``CONST_constr constr``, ``CONST_true``, ``CONST_false``, ``CONST_unit``,
``CONST_nil``]]
JTconst_cases);
val JM_matchP_fun = save_thm ("JM_matchP_fun",
structural_cases [pattern_11, pattern_distinct]
1
[get_terms ftv_pattern_def]
JM_matchP_cases);
val JM_match_fun = save_thm ("JM_match_fun",
structural_cases [pattern_11, pattern_distinct]
1
[get_terms ftv_pattern_def]
JM_match_cases);
val JTdefinition_fun = save_thm ("JTdefinition_fun",
structural_cases [definition_11, definition_distinct]
1
[[``D_let lb``,
``D_letrec lrbs``,
``D_type td``,
``D_exception ed``]]
JTdefinition_cases);
val JTdefinitions_fun = save_thm ("JTdefinitions_fun",
structural_cases [definitions_11, definitions_distinct]
1 [[``Ds_nil``, ``Ds_cons d ds``]]
JTdefinitions_cases);
val JTprog_fun = save_thm ("JTprog_fun",
structural_cases [program_11, program_distinct]
1 [[``Prog_defs ds``,
``Prog_raise v``]]
JTprog_cases);
val JRdefn_fun = save_thm ("JRdefn_fun",
structural_cases [definitions_11, definitions_distinct, definition_11, definition_distinct,
program_11, program_distinct]
1
[[``Prog_defs Ds_nil``,
``Prog_defs (Ds_cons (D_let lb) ds)``,
``Prog_defs (Ds_cons (D_letrec lrbs) ds)``,
``Prog_defs (Ds_cons (D_type td) ds)``,
``Prog_defs (Ds_cons (D_exception ed) ds)``,
``Prog_raise v``]]
JRdefn_cases);
val JTstore_fun = save_thm ("JTstore_fun", SIMP_RULE list_ss []
(structural_cases [list_11, list_distinct]
1
[[``[]:store``,
``(l, v)::(store:store)``]]
JTstore_cases));
val JTinst_any_fun = save_thm ("JTinst_any_fun",
structural_cases [typexpr_11, typexpr_distinct]
2
[get_terms ftv_typexpr_def]
JTinst_any_cases);
val JTeq_fun = save_thm ("JTeq_fun",
structural_cases [typexpr_11, typexpr_distinct]
1
[get_terms ftv_typexpr_def]
JTeq_cases);
(* This otherwise useless definition is accompanied by a nice induction principle. *)
val Eok2_def = Define
`(Eok2 [] = T) /\
(Eok2 (EB_tv::E) = Eok2 E) /\
(Eok2 (EB_vn value_name (TS_forall t)::E) = Eok2 E) /\
(Eok2 (EB_cc constr_name TC_exn::E) = Eok2 E) /\
(Eok2 (EB_cc constr_name (TC_name typeconstr_name)::E) = Eok2 E) /\
(Eok2 (EB_cc constr_name tc::E) = F) /\
(Eok2 (EB_pc constr_name (TPS_nary []) (typexprs_inj t_list) TC_exn::E) = Eok2 E) /\
(Eok2 (EB_pc constr_name (TPS_nary vars) (typexprs_inj t_list) (TC_name typeconstr_name)::E) = Eok2 E) /\
(Eok2 (EB_pc constr_name params (typexprs_inj t_list) tc::E) = F) /\
(Eok2 (EB_fn field_name (TPS_nary vars) typeconstr_name t::E) = Eok2 E) /\
(Eok2 (EB_td typeconstr_name kind::E) = Eok2 E) /\
(Eok2 (EB_ta tps typeconstr_name t::E) = Eok2 E) /\
(Eok2 (EB_tr typeconstr_name kind field_name_list::E) = Eok2 E) /\
(Eok2 (EB_l location t::E) = Eok2 E)`;
val is_abbrev_tc_def = Define `
(is_abbrev_tc E (TE_constr _ (TC_name tcn)) =
case lookup E (name_tcn tcn) of
SOME (EB_ta x y z) => T
| _ => F) /\
(is_abbrev_tc E _ = F)`;
val is_abbrev_tc_cases = Q.store_thm ("is_abbrev_tc_cases",
`!E t. is_abbrev_tc E t <=> ?ts tcn tps t'. (t = TE_constr ts (TC_name tcn)) /\
(lookup E (name_tcn tcn) = SOME (EB_ta (TPS_nary tps) tcn t'))`,
Cases_on `t` THEN SRW_TAC [] [is_abbrev_tc_def] THEN
Cases_on `t'` THEN SRW_TAC [] [is_abbrev_tc_def] THEN
Cases_on `lookup E (name_tcn t)` THEN SRW_TAC [] [is_abbrev_tc_def] THEN
Cases_on `x` THEN SRW_TAC [] [is_abbrev_tc_def] THEN
IMP_RES_TAC lookup_name_thm THEN
FULL_SIMP_TAC list_ss [environment_binding_11, environment_binding_distinct, type_params_opt_nchotomy]);
val is_record_tc_def = Define `
(is_record_tc E (TE_constr _ (TC_name tcn)) =
case lookup E (name_tcn tcn) of
SOME (EB_tr x y z) => T
| _ => F) /\
(is_record_tc E _ = F)`;
val is_record_tc_cases = Q.store_thm ("is_record_tc_cases",
`!E t. is_record_tc E t <=> (?ts tcn k fns. (t = TE_constr ts (TC_name tcn)) /\
(lookup E (name_tcn tcn) = SOME (EB_tr tcn k fns)))`,
Cases_on `t` THEN SRW_TAC [] [is_record_tc_def] THEN
Cases_on `t'` THEN SRW_TAC [] [is_record_tc_def] THEN
Cases_on `lookup E (name_tcn t)` THEN SRW_TAC [] [is_record_tc_def] THEN
Cases_on `x` THEN SRW_TAC [] [is_abbrev_tc_def] THEN
IMP_RES_TAC lookup_name_thm THEN
FULL_SIMP_TAC list_ss [environment_binding_11, environment_binding_distinct]);
val is_constr_tc_def = Define `
(is_constr_tc E (TE_constr _ (TC_name tcn)) =
case lookup E (name_tcn tcn) of
SOME (EB_td x y) => T
| _ => F) /\
(is_constr_tc E (TE_constr [] TC_exn) = T) /\
(is_constr_tc E (TE_constr [t] TC_option) = T) /\
(is_constr_tc E _ = F)`;
val is_constr_tc_cases = Q.store_thm ("is_constr_tc_cases",
`!E t. is_constr_tc E t <=> (?ts tcn k. (t = TE_constr ts (TC_name tcn)) /\
(lookup E (name_tcn tcn) = SOME (EB_td tcn k))) \/
(?t'. t = TE_constr [t'] TC_option) \/
(t = TE_constr [] TC_exn)`,
Cases_on `t` THEN SRW_TAC [] [is_constr_tc_def] THEN
Cases_on `t'` THEN SRW_TAC [] [is_constr_tc_def] THEN
TRY (Cases_on `l` THEN SRW_TAC [] [is_constr_tc_def]) THEN
TRY (Cases_on `lookup E (name_tcn t)` THEN SRW_TAC [] [is_constr_tc_def]) THEN
TRY (Cases_on `t` THEN SRW_TAC [] [is_constr_tc_def]) THEN
TRY (Cases_on `t'` THEN SRW_TAC [] [is_constr_tc_def]) THEN
Cases_on `x` THEN SRW_TAC [] [is_abbrev_tc_def] THEN
IMP_RES_TAC lookup_name_thm THEN
FULL_SIMP_TAC list_ss [environment_binding_11, environment_binding_distinct]);
val JM_match_lem = Q.prove (
`!e p s. JM_match e p s ==> JM_matchP e p`,
RULE_INDUCT_TAC Jmatch_ind [JM_matchP_fun, ELIM_UNCURRY, EVERY_MAP, EVERY_MEM]
[([``"JM_match_construct"``, ``"JM_match_tuple"``],
SRW_TAC [] [] THEN Q.EXISTS_TAC `MAP (\x. (FST x, FST (SND x))) v_pat_substs_x_list` THEN
SRW_TAC [] [MAP_MAP, ETA_THM] THEN FULL_SIMP_TAC list_ss [MEM_MAP]),
([``"JM_match_record"``],
SRW_TAC [] [] THEN
MAP_EVERY Q.EXISTS_TAC [`fn_v''_list`,
`MAP (\(a, b, c, d). (a, b, d)) field_name'_pat_substs_x_v'_list`,
`field_name_v_list`] THEN
SRW_TAC [] [LAMBDA_PROD2, MAP_MAP] THEN FULL_SIMP_TAC list_ss [MEM_MAP])]);
local
val lem1 = Q.prove (
`!l1 l2 P.
(LENGTH l1 = LENGTH l2) /\
EVERY (\x. P (FST x) (FST (SND x)) (substs_x_xs (SND (SND x)))) (ZIP (MAP FST l1,ZIP (MAP SND l1,l2))) ==>
EVERY (\x. P (FST (FST x)) (SND (FST x)) (SND x)) (ZIP (l1,MAP substs_x_xs l2))`,
Induct THEN SRW_TAC [] [] THEN Cases_on `l2` THEN FULL_SIMP_TAC list_ss []);
val lem2 = Q.prove (
`!l1 l2 f g. (LENGTH l1 = LENGTH l2) ==>
(MAP (\x. (f (FST x),g (FST x))) (ZIP (l1,l2)) =
MAP (\z. (f z, g z)) l1)`,
Induct THEN SRW_TAC [] [] THEN Cases_on `l2` THEN FULL_SIMP_TAC list_ss []);
val lem3 = Q.prove (
`!l1 l2 P.
(LENGTH l1 = LENGTH l2) /\
EVERY (\x. P (SND (FST x)) (SND (FST (SND x))) (substs_x_xs (SND (SND x))))
(ZIP (MAP (\z. (F_name (FST z),SND (SND z))) l1,
ZIP (MAP (\z. (F_name (FST z),FST (SND z))) l1,l2))) ==>
EVERY (\x. P (SND (SND (FST x))) (FST (SND (FST x))) (substs_x_xs (SND x))) (ZIP (l1,l2))`,
Induct THEN SRW_TAC [] [] THEN Cases_on `l2` THEN FULL_SIMP_TAC list_ss []);
in
val JM_matchP_lem = Q.prove (
`(!p e. JM_matchP e p ==> ?s. JM_match e p (substs_x_xs s) /\ EVERY is_value_of_expr (MAP SND s)) /\
(!plist elist. (LENGTH plist = LENGTH elist) /\ EVERY (UNCURRY JM_matchP) (ZIP (elist, plist)) ==>
?slist. (LENGTH plist = LENGTH slist) /\ EVERY is_value_of_expr (MAP SND (FLAT slist)) /\
EVERY (\(e, p, s). JM_match e p (substs_x_xs s))
(ZIP (elist, (ZIP (plist, slist))))) /\
(!fplist felist. (LENGTH felist = LENGTH fplist) /\
EVERY (\((f:field,e),(f':field,p)). JM_matchP e p) (ZIP (felist, fplist)) ==>
?slist. (LENGTH fplist = LENGTH slist) /\ EVERY is_value_of_expr (MAP SND (FLAT slist)) /\
EVERY (\((f,e), (f,p), s). JM_match e p (substs_x_xs s))
(ZIP (felist, (ZIP (fplist, slist))))) /\
(!(fp:field#pattern) (fe:field#expr). JM_matchP (SND fe) (SND fp) ==>
?s. JM_match (SND fe) (SND fp) (substs_x_xs s) /\ EVERY is_value_of_expr (MAP SND s))`,
Induct THEN SRW_TAC [] [JM_match_fun, JM_matchP_fun, EVERY_MAP] THEN
FULL_SIMP_TAC list_ss [EVERY_MAP, ELIM_UNCURRY] THENL [
RES_TAC THEN Q.EXISTS_TAC `s++[(v,e)]` THEN SRW_TAC [] [],
METIS_TAC [],
METIS_TAC [],
METIS_TAC [],
Q.PAT_X_ASSUM `!elist. P elist ==> Q elist` (MP_TAC o Q.SPEC `MAP FST (v_pat_list:(expr#pattern) list)`) THEN
SRW_TAC [] [ZIP_MAP_ID] THEN Q.EXISTS_TAC `FLAT slist` THEN SRW_TAC [] [] THEN
Q.EXISTS_TAC `MAP (\((v, p), s). (v, p, s)) (ZIP (v_pat_list, MAP substs_x_xs slist))` THEN
SRW_TAC [] [MAP_MAP, LAMBDA_PROD2, EVERY_MAP] THEN
SRW_TAC [] [GSYM MAP_MAP, MAP_FST_ZIP, MAP_SND_ZIP, GSYM EVERY_MAP] THEN
SRW_TAC [] [MAP_MAP, MAP_I, EVERY_MAP, lem1] THEN
SRW_TAC [] [ZIP_MAP,MAP_MAP] THEN METIS_TAC [MAP_ZIP],
Q.PAT_X_ASSUM `!elist. P elist ==> Q elist` (MP_TAC o Q.SPEC `MAP FST (v_pat_list:(expr#pattern) list)`) THEN
SRW_TAC [] [ZIP_MAP_ID] THEN Q.EXISTS_TAC `FLAT slist` THEN SRW_TAC [] [] THEN
Q.EXISTS_TAC `MAP (\((v, p), s). (v, p, s)) (ZIP (v_pat_list, MAP substs_x_xs slist))` THEN
SRW_TAC [] [MAP_MAP, LAMBDA_PROD2, EVERY_MAP] THEN
SRW_TAC [] [GSYM MAP_MAP, MAP_FST_ZIP, MAP_SND_ZIP, GSYM EVERY_MAP] THEN
SRW_TAC [] [MAP_MAP, MAP_I, EVERY_MAP, lem1] THEN
SRW_TAC [] [ZIP_MAP,MAP_MAP] THEN METIS_TAC [MAP_ZIP],
Q.PAT_X_ASSUM `!felist. P felist ==> Q felist`
(MP_TAC o Q.SPEC `MAP (\(fn, p:pattern, v:expr). (F_name fn, v)) field_name'_pat_v'_list`) THEN
SRW_TAC [] [MAP_MAP, MAP_ZIP_SAME, ZIP_MAP, EVERY_MAP, LAMBDA_PROD2] THEN
Q.EXISTS_TAC `FLAT slist` THEN SRW_TAC [] [] THEN
MAP_EVERY Q.EXISTS_TAC [`fn_v''_list`,
`MAP (\((f, p, v), s). (f, p, substs_x_xs s, v))
(ZIP (field_name'_pat_v'_list, slist))`,
`field_name_v_list`] THEN
SRW_TAC [] [ETA_THM, MAP_MAP, LAMBDA_PROD2, EVERY_MAP, MAP_SND_ZIP, lem2] THEN
SRW_TAC [] [GSYM EVERY_MAP, GSYM MAP_MAP, MAP_FST_ZIP] THEN
SRW_TAC [] [EVERY_MAP, lem3],
RES_TAC THEN Q.EXISTS_TAC `s'++s` THEN SRW_TAC [] [] THEN
MAP_EVERY Q.EXISTS_TAC [`substs_x_xs s'`, `substs_x_xs s`] THEN SRW_TAC [] [],
Cases_on `felist` THEN FULL_SIMP_TAC list_ss [] THEN
Q.PAT_ASSUM `!felist'. P felist' ==> ?slist. (LENGTH fplist = LENGTH slist) /\ Q felist' slist`
(MP_TAC o Q.SPEC `t`) THEN
SRW_TAC [] [] THEN RES_TAC THEN Q.EXISTS_TAC `s::slist` THEN SRW_TAC [] [] THEN METIS_TAC [],
Cases_on `elist` THEN FULL_SIMP_TAC list_ss [] THEN
Q.PAT_X_ASSUM `!elist. P elist ==> ?slist. (LENGTH elist = LENGTH slist) /\ Q elist slist`
(MP_TAC o Q.SPEC `t`) THEN
SRW_TAC [] [] THEN RES_TAC THEN Q.EXISTS_TAC `s::slist` THEN SRW_TAC [] []
]);
end;
val JM_match_is_val_thm = Q.store_thm ("JM_match_is_val_thm",
`!e p s. JM_match e p s ==> !s'. (s = substs_x_xs s') ==> EVERY is_value_of_expr (MAP SND s')`,
RULE_INDUCT_TAC Jmatch_ind [EVERY_MAP, ELIM_UNCURRY, MAP_MAP]
[([``"JM_match_tuple"``, ``"JM_match_construct"``],
SRW_TAC [] [EVERY_MEM, MEM_FLAT, EXISTS_MAP, EXISTS_MEM] THEN
Cases_on `x'` THEN FULL_SIMP_TAC list_ss [] THEN
Cases_on `r` THEN FULL_SIMP_TAC list_ss [] THEN
Cases_on `r'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [SND]),
([``"JM_match_record"``],
SRW_TAC [] [EVERY_MEM, MEM_FLAT, EXISTS_MAP, EXISTS_MEM] THEN
Cases_on `x'` THEN FULL_SIMP_TAC list_ss [] THEN
Cases_on `r` THEN FULL_SIMP_TAC list_ss [] THEN
Cases_on `r'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
Cases_on `q''` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
METIS_TAC [FST, SND]),
([``"JM_match_cons"``],
SRW_TAC [] [EVERY_MEM] THEN
Cases_on `s` THEN Cases_on `s'` THEN FULL_SIMP_TAC (srw_ss()) [])]);
val JM_matchP_thm = Q.store_thm ("JM_matchP_thm",
`!p e. JM_matchP e p = ?s. JM_match e p (substs_x_xs s)`,
METIS_TAC [JM_matchP_lem, JM_match_lem, JM_match_is_val_thm]);
val _ = export_theory();
|
