-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathLSS.thy
More file actions
6113 lines (5832 loc) · 233 KB
/
LSS.thy
File metadata and controls
6113 lines (5832 loc) · 233 KB
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
theory LSS
imports Main
begin
type_synonym Var = nat
type_synonym Def = nat
type_synonym MuVar = nat
(* Source language type *)
datatype ST =
STFun ST ST |
STProd "ST list" |
STSum "ST list" |
STMu MuVar ST |
STVar MuVar
(* Source language expression *)
datatype SE =
SETup "SE list" |
SEProj nat SE |
SEInj "ST list" nat SE |
SEFold MuVar ST SE |
SEUnfold SE |
SELet Var SE SE |
SEMatch ST SE "(Var * SE) list" |
SELam Var ST SE Var ST SE ST |
SEApp SE SE |
SEVar Var |
SEDef Def |
(* In a small departure from the formalism presented in the paper, we forbid polymorphic recursion
by construction by requiring that definitions always refer to themselves via the "SESelf"
construct, which stands in for an "SEDef" referring to the current definition. Distinguishing
references to the current definition from references to other definitions slightly simplifies
proofs of the correctness of type inference. *)
SESelf Def ST
(* Source language program *)
datatype SP =
SPEntry Def |
SPDef Def ST SE SP
(* Source language typing context for variables *)
type_synonym STCV = "Var \<Rightarrow> ST option"
(* Source language typing context for definitions *)
type_synonym STCD = "Def \<Rightarrow> ST option"
(* Source language "self" context -- contains typing information about the current definition *)
datatype STCS = STCS (stcs_defs: STCD) (stcs_self_d: Def) (stcs_self_t: ST)
(* Substitution for source type level mu variables *)
fun st_subst :: "(MuVar \<Rightarrow> ST) \<Rightarrow> ST \<Rightarrow> ST" where
"st_subst m (STFun t1 t2) = STFun (st_subst m t1) (st_subst m t2)" |
"st_subst m (STProd ts) = STProd (map (st_subst m) ts)" |
"st_subst m (STSum ts) = STSum (map (st_subst m) ts)" |
"st_subst m (STMu u t) = STMu u (st_subst (m(u := STVar u)) t)" |
"st_subst m (STVar u) = m u"
(* Typing judgement for source expressions *)
function tj_se :: "STCS \<Rightarrow> STCV \<Rightarrow> SE \<Rightarrow> ST \<Rightarrow> bool" where
tj_se_tup: "tj_se sc gc (SETup es) t0 = (\<exists> ts.
length es = length ts \<and>
(\<forall> (e_el, t_el) \<in> set (zip es ts). tj_se sc gc e_el t_el) \<and>
t0 = STProd ts
)" |
tj_se_proj: "tj_se sc gc (SEProj i e) t0 = (\<exists> ts.
i < length ts \<and>
tj_se sc gc e (STProd ts) \<and>
t0 = ts ! i
)" |
tj_se_inj: "tj_se sc gc (SEInj ts i e) t0 = (
i < length ts \<and>
tj_se sc gc e (ts ! i) \<and>
t0 = STSum ts
)" |
tj_se_fold: "tj_se sc gc (SEFold u t e) t0 = (
tj_se sc gc e (st_subst (STVar(u := STMu u t)) t) \<and>
t0 = STMu u t
)" |
tj_se_unfold: "tj_se sc gc (SEUnfold e) t0 = (\<exists> u t.
tj_se sc gc e (STMu u t) \<and>
t0 = (st_subst (STVar(u := STMu u t)) t)
)" |
tj_se_let: "tj_se sc gc (SELet x e1 e2) t0 = (\<exists> t.
gc x = None \<and>
tj_se sc gc e1 t \<and>
tj_se sc (gc(x := Some t)) e2 t0
)" |
tj_se_match: "tj_se sc gc (SEMatch t_ret e_dis cases) t0 = (\<exists> ts.
length ts = length cases \<and>
tj_se sc gc e_dis (STSum ts) \<and>
(\<forall> (t_case, (x_case, e_case)) \<in> set (zip ts cases).
gc x_case = None \<and>
tj_se sc (gc(x_case := Some t_case)) e_case t_ret
) \<and>
t0 = t_ret
)" |
tj_se_lam: "tj_se sc gc (SELam x t1 e1 y t2 e2 t3) t0 = (
tj_se sc gc e1 t1 \<and>
tj_se sc (Map.empty(x := Some t1, y := Some t2)) e2 t3 \<and>
t0 = STFun t2 t3
)" |
tj_se_app: "tj_se sc gc (SEApp e1 e2) t0 = (\<exists> t_arg.
tj_se sc gc e1 (STFun t_arg t0) \<and>
tj_se sc gc e2 t_arg
)" |
tj_se_var: "tj_se sc gc (SEVar x) t0 = (gc x = Some t0)" |
tj_se_def: "tj_se sc gc (SEDef d) t0 = (stcs_defs sc d = Some t0)" |
tj_se_self: "tj_se sc gc (SESelf d t) t0 = (stcs_self_d sc = d \<and> stcs_self_t sc = t \<and> t0 = t)"
by(pat_completeness) auto
termination apply(relation "measure (\<lambda> (_, _, e, _). SE.size_SE e)", auto)
apply (meson le_imp_less_Suc order_refl set_zip_leftD size_list_estimation')
proof -
fix e_dis cases ts t_case x_case e_case
assume in_list: "(t_case :: ST, x_case :: Var, e_case :: SE) \<in> set (zip ts cases)"
then have "(x_case, e_case) \<in> set cases"
by (meson in_set_zipE)
then have "size_list (size_prod (\<lambda>_. 0) size_SE) cases \<ge> size_SE e_case"
proof(induct cases arbitrary: x_case e_case)
case Nil
then show ?case by auto
next
case (Cons case_hd case_tl)
then show ?case apply(case_tac "e_case = snd case_hd")
apply (simp add: size_prod_simp)
by fastforce
qed
then show "size_SE e_case
< Suc (size_list (size_prod (\<lambda>x. 0) size_SE) cases +
size_SE e_dis)"
by auto
qed
(* Lambda set variable *)
type_synonym LSVar = nat
(* Annotated language lambda set *)
datatype ALS =
ALSVar LSVar |
ALSSet "(Var * AT * Var * AT * AE * AT) list" |
ALSMuVar MuVar |
ALSMu MuVar ALS
(* Annotated language type *)
and AT =
ATFun ALS AT AT |
ATProd "AT list" |
ATSum "AT list" |
ATMu MuVar AT |
ATVar MuVar
(* Annotated language expression *)
and AE =
AETup "AE list" |
AEProj nat AE |
AEInj "AT list" nat AE |
AEFold MuVar AT AE |
AEUnfold AE |
AELet Var AE AE |
AEMatch AT AE "(Var * AE) list" |
AELam ALS Var AT AE Var AT AE AT |
AEApp ALS AE AE |
AEVar Var |
AEDef Def "ALS list" |
AESelf Def AT
(* Annotated language lambda *)
type_synonym AL = "Var * AT * Var * AT * AE * AT"
(* Annotated language lambda set constraint -- these are of the form 'lambda \<in> set' *)
type_synonym ALSC = "AL * ALS"
(* Annotated language program *)
datatype AP =
APEntry Def |
APDef Def "LSVar list" "ALSC list" AT AE AP
(* Substitution for lambda set level mu variables *)
fun
als_mu_subst :: "(MuVar \<Rightarrow> ALS) \<Rightarrow> ALS \<Rightarrow> ALS" and
at_mu_subst :: "(MuVar \<Rightarrow> ALS) \<Rightarrow> AT \<Rightarrow> AT" and
ae_mu_subst :: "(MuVar \<Rightarrow> ALS) \<Rightarrow> AE \<Rightarrow> AE"
where
"als_mu_subst m (ALSVar v) = ALSVar v" |
"als_mu_subst m (ALSSet s) = ALSSet (map (\<lambda> (x, t1, y, t2, e, t3). (x, at_mu_subst m t1, y, at_mu_subst m t2, ae_mu_subst m e, at_mu_subst m t3)) s)" |
"als_mu_subst m (ALSMuVar u) = m u" |
"als_mu_subst m (ALSMu u a) = ALSMu u (als_mu_subst (m(u := ALSMuVar u)) a)" |
"at_mu_subst m (ATFun a t1 t2) = ATFun (als_mu_subst m a) (at_mu_subst m t1) (at_mu_subst m t2)" |
"at_mu_subst m (ATProd ts) = ATProd (map (at_mu_subst m) ts)" |
"at_mu_subst m (ATSum ts) = ATSum (map (at_mu_subst m) ts)" |
"at_mu_subst m (ATMu u t) = ATMu u (at_mu_subst m t)" |
"at_mu_subst m (ATVar u) = ATVar u" |
"ae_mu_subst m (AETup es) = AETup (map (ae_mu_subst m) es)" |
"ae_mu_subst m (AEProj i e) = AEProj i (ae_mu_subst m e)" |
"ae_mu_subst m (AEInj ts i e) = AEInj (map (at_mu_subst m) ts) i (ae_mu_subst m e)" |
"ae_mu_subst m (AEFold u t e) = AEFold u (at_mu_subst m t) (ae_mu_subst m e)" |
"ae_mu_subst m (AEUnfold e) = AEUnfold (ae_mu_subst m e)" |
"ae_mu_subst m (AELet x e1 e2) = AELet x (ae_mu_subst m e1) (ae_mu_subst m e2)" |
"ae_mu_subst m (AEMatch t e cases) = AEMatch (at_mu_subst m t) (ae_mu_subst m e) (map (\<lambda>(case_x, case_e). (case_x, ae_mu_subst m case_e)) cases)" |
"ae_mu_subst m (AELam a x t1 e1 y t2 e2 t3) = AELam (als_mu_subst m a) x (at_mu_subst m t1) (ae_mu_subst m e1) y (at_mu_subst m t2) (ae_mu_subst m e2) (at_mu_subst m t3)" |
"ae_mu_subst m (AEApp a e1 e2) = AEApp (als_mu_subst m a) (ae_mu_subst m e1) (ae_mu_subst m e2)" |
"ae_mu_subst m (AEVar v) = AEVar v" |
"ae_mu_subst m (AEDef d as) = AEDef d (map (als_mu_subst m) as)" |
"ae_mu_subst m (AESelf d_self t_self) = (AESelf d_self (at_mu_subst m t_self))"
fun al_mu_subst :: "(MuVar \<Rightarrow> ALS) \<Rightarrow> AL \<Rightarrow> AL" where
"al_mu_subst m (x, t1, y, t2, e, t3) = (x, at_mu_subst m t1, y, at_mu_subst m t2, ae_mu_subst m e, at_mu_subst m t3)"
(* Substitution for lambda set variables *)
fun
als_lsv_subst :: "(LSVar \<Rightarrow> ALS) \<Rightarrow> ALS \<Rightarrow> ALS" and
at_lsv_subst :: "(LSVar \<Rightarrow> ALS) \<Rightarrow> AT \<Rightarrow> AT" and
ae_lsv_subst :: "(LSVar \<Rightarrow> ALS) \<Rightarrow> AE \<Rightarrow> AE"
where
"als_lsv_subst m (ALSVar v) = m v" |
"als_lsv_subst m (ALSSet s) = ALSSet (map (\<lambda> (x, t1, y, t2, e, t3). (x, at_lsv_subst m t1, y, at_lsv_subst m t2, ae_lsv_subst m e, at_lsv_subst m t3)) s)" |
"als_lsv_subst m (ALSMuVar u) = ALSMuVar u" |
"als_lsv_subst m (ALSMu u a) = ALSMu u (als_lsv_subst m a)" |
"at_lsv_subst m (ATFun a t1 t2) = ATFun (als_lsv_subst m a) (at_lsv_subst m t1) (at_lsv_subst m t2)" |
"at_lsv_subst m (ATProd ts) = ATProd (map (at_lsv_subst m) ts)" |
"at_lsv_subst m (ATSum ts) = ATSum (map (at_lsv_subst m) ts)" |
"at_lsv_subst m (ATMu u t) = ATMu u (at_lsv_subst m t)" |
"at_lsv_subst m (ATVar u) = ATVar u" |
"ae_lsv_subst m (AETup es) = AETup (map (ae_lsv_subst m) es)" |
"ae_lsv_subst m (AEProj i e) = AEProj i (ae_lsv_subst m e)" |
"ae_lsv_subst m (AEInj ts i e) = AEInj (map (at_lsv_subst m) ts) i (ae_lsv_subst m e)" |
"ae_lsv_subst m (AEFold u t e) = AEFold u (at_lsv_subst m t) (ae_lsv_subst m e)" |
"ae_lsv_subst m (AEUnfold e) = AEUnfold (ae_lsv_subst m e)" |
"ae_lsv_subst m (AELet x e1 e2) = AELet x (ae_lsv_subst m e1) (ae_lsv_subst m e2)" |
"ae_lsv_subst m (AEMatch t e cases) = AEMatch (at_lsv_subst m t) (ae_lsv_subst m e) (map (\<lambda>(case_x, case_e). (case_x, ae_lsv_subst m case_e)) cases)" |
"ae_lsv_subst m (AELam a x t1 e1 y t2 e2 t3) = AELam (als_lsv_subst m a) x (at_lsv_subst m t1) (ae_lsv_subst m e1) y (at_lsv_subst m t2) (ae_lsv_subst m e2) (at_lsv_subst m t3)" |
"ae_lsv_subst m (AEApp a e1 e2) = AEApp (als_lsv_subst m a) (ae_lsv_subst m e1) (ae_lsv_subst m e2)" |
"ae_lsv_subst m (AEVar v) = AEVar v" |
"ae_lsv_subst m (AEDef d as) = AEDef d (map (als_lsv_subst m) as)" |
"ae_lsv_subst m (AESelf d_self t_self) = (AESelf d_self (at_lsv_subst m t_self))"
(* Merging this case into the above definition blows the termination checker *)
fun al_lsv_subst :: "(LSVar \<Rightarrow> ALS) \<Rightarrow> AL \<Rightarrow> AL" where
"al_lsv_subst m (x, t1, y, t2, e, t3) = (x, at_lsv_subst m t1, y, at_lsv_subst m t2, ae_lsv_subst m e, at_lsv_subst m t3)"
(* Substitution for annotated type level mu variables *)
fun at_subst :: "(MuVar \<Rightarrow> AT) \<Rightarrow> AT \<Rightarrow> AT" where
"at_subst m (ATFun a t1 t2) = ATFun a (at_subst m t1) (at_subst m t2)" |
"at_subst m (ATProd ts) = ATProd (map (at_subst m) ts)" |
"at_subst m (ATSum ts) = ATSum (map (at_subst m) ts)" |
"at_subst m (ATMu u t) = ATMu u (at_subst (m(u := ATVar u)) t)" |
"at_subst m (ATVar u) = m u"
(* Annotated language typing context for values *)
type_synonym ATCV = "Var \<Rightarrow> AT option"
(* Annotated language typing context for definitions *)
type_synonym ATCD = "Def \<Rightarrow> ((LSVar list) * AT * (ALSC list)) option"
(* Annotated language "self" context -- contains typing information about the current definition *)
datatype ATCS = ATCS (atcs_defs: ATCD) (atcs_self_d: Def) (atcs_self_t: AT)
fun upd_w_list :: "('a * 'b) list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
"upd_w_list xs f = foldr (\<lambda> (x, y) new_f. (new_f(x := y))) xs f"
fun lsv_inst :: "LSVar list \<Rightarrow> ALS list \<Rightarrow> (LSVar \<Rightarrow> ALS)" where
"lsv_inst xs ys = upd_w_list (zip xs ys) ALSVar"
(* Typing judgement for annotated expressions *)
function tj_ae :: "ATCS \<Rightarrow> ATCV \<Rightarrow> AE \<Rightarrow> AT \<Rightarrow> bool" where
tj_ae_tup: "tj_ae sc gc (AETup es) t0 = (\<exists> ts.
length es = length ts \<and>
(\<forall> (e_el, t_el) \<in> set (zip es ts). tj_ae sc gc e_el t_el) \<and>
t0 = ATProd ts
)" |
tj_ae_proj: "tj_ae sc gc (AEProj i e) t0 = (\<exists> ts.
i < length ts \<and>
tj_ae sc gc e (ATProd ts) \<and>
t0 = ts ! i
)" |
tj_ae_inj: "tj_ae sc gc (AEInj ts i e) t0 = (
i < length ts \<and>
tj_ae sc gc e (ts ! i) \<and>
t0 = ATSum ts
)" |
tj_ae_fold: "tj_ae sc gc (AEFold u t e) t0 = (
tj_ae sc gc e (at_subst (ATVar(u := ATMu u t)) t) \<and>
t0 = ATMu u t
)" |
tj_ae_unfold: "tj_ae sc gc (AEUnfold e) t0 = (\<exists> u t.
tj_ae sc gc e (ATMu u t) \<and>
t0 = (at_subst (ATVar(u := ATMu u t)) t)
)" |
tj_ae_let: "tj_ae sc gc (AELet x e1 e2) t0 = (\<exists> t.
gc x = None \<and>
tj_ae sc gc e1 t \<and>
tj_ae sc (gc(x := Some t)) e2 t0
)" |
tj_ae_match: "tj_ae sc gc (AEMatch t_ret e_dis cases) t0 = (\<exists> ts.
length ts = length cases \<and>
tj_ae sc gc e_dis (ATSum ts) \<and>
(\<forall> (t_case, (x_case, e_case)) \<in> set (zip ts cases).
gc x_case = None \<and>
tj_ae sc (gc(x_case := Some t_case)) e_case t_ret
) \<and>
t0 = t_ret
)" |
tj_ae_lam: "tj_ae sc gc (AELam a x t1 e1 y t2 e2 t3) t0 = (
tj_ae sc gc e1 t1 \<and>
tj_ae sc (Map.empty(x := Some t1, y := Some t2)) e2 t3 \<and>
t0 = ATFun a t2 t3
)" |
tj_ae_app: "tj_ae sc gc (AEApp a e1 e2) t0 = (\<exists> t_arg.
tj_ae sc gc e1 (ATFun a t_arg t0) \<and>
tj_ae sc gc e2 t_arg
)" |
tj_ae_var: "tj_ae sc gc (AEVar x) t0 = (gc x = Some t0)" |
tj_ae_def: "tj_ae sc gc (AEDef d as) t0 = (\<exists> vs t cs.
atcs_defs sc d = Some (vs, t, cs) \<and>
length vs = length as \<and>
t0 = at_lsv_subst (lsv_inst vs as) t
)" |
tj_ae_self: "tj_ae sc gc (AESelf d t) t0 = (atcs_self_d sc = d \<and> atcs_self_t sc = t \<and> t0 = t)"
by(pat_completeness) auto
termination apply(relation "measure (\<lambda> (_, _, e, _). AE.size_AE e)", auto)
apply (meson le_imp_less_Suc order_refl set_zip_leftD size_list_estimation')
proof -
fix t_ret e_dis cases ts t_case x_case e_case
assume in_list: "(t_case :: AT, x_case :: Var, e_case :: AE) \<in> set (zip ts cases)"
then have "(x_case, e_case) \<in> set cases"
by (meson in_set_zipE)
then have "size_list (size_prod (\<lambda>_. 0) size_AE) cases \<ge> size_AE e_case"
proof(induct cases arbitrary: x_case e_case)
case Nil
then show ?case by auto
next
case (Cons case_hd case_tl)
then show ?case apply(case_tac "e_case = snd case_hd")
apply (simp add: size_prod_simp)
by fastforce
qed
then show "size_AE e_case
< Suc (size_list (size_prod (\<lambda>x. 0) size_AE) cases +
size_AT t_ret +
size_AE e_dis)"
by auto
qed
(* Annotated constraints context: constraints *)
type_synonym ACC = "ALSC list"
(* Constraint judgement for lambda set constraints *)
inductive cj_alsc :: "ALSC list \<Rightarrow> ALSC \<Rightarrow> bool" where
cj_alsc_assumption: "c \<in> set q \<Longrightarrow> cj_alsc q c" |
cj_alsc_set: "s \<in> set a \<Longrightarrow> cj_alsc q (s, ALSSet a)" |
cj_alsc_mu: "
cj_alsc q (l, als_mu_subst (ALSMuVar(u := ALSMu u a)) a) \<Longrightarrow>
cj_alsc q (l, ALSMu u a)
"
fun cj_alsc_all :: "ALSC list \<Rightarrow> ALSC list \<Rightarrow> bool" where
"cj_alsc_all q1 q2 = (\<forall> c \<in> set q2. cj_alsc q1 c)"
fun alsc_lsv_subst :: "(LSVar \<Rightarrow> ALS) \<Rightarrow> ALSC \<Rightarrow> ALSC" where
"alsc_lsv_subst m ((x, t1, y, t2, e, t3), a) = ((x, at_lsv_subst m t1, y, at_lsv_subst m t2, ae_lsv_subst m e, at_lsv_subst m t3), als_lsv_subst m a)"
fun alsc_lsv_subst_all :: "(LSVar \<Rightarrow> ALS) \<Rightarrow> ALSC list \<Rightarrow> ALSC list" where
"alsc_lsv_subst_all m q = map (alsc_lsv_subst m) q"
fun alsc_mu_subst :: "(MuVar \<Rightarrow> ALS) \<Rightarrow> ALSC \<Rightarrow> ALSC" where
"alsc_mu_subst m (l, a) = (al_mu_subst m l, als_mu_subst m a)"
fun alsc_mu_subst_all :: "(MuVar \<Rightarrow> ALS) \<Rightarrow> ACC \<Rightarrow> ACC" where
"alsc_mu_subst_all m cc = map (alsc_mu_subst m) cc"
(* Constraint judgement for annotated expressions *)
fun cj_ae :: "ATCD \<Rightarrow> ACC \<Rightarrow> AE \<Rightarrow> bool" where
"cj_ae dc cc (AETup es) = (\<forall> e \<in> set es. cj_ae dc cc e)" |
"cj_ae dc cc (AEProj _ e) = cj_ae dc cc e" |
"cj_ae dc cc (AEInj _ _ e) = cj_ae dc cc e" |
"cj_ae dc cc (AEFold _ _ e) = cj_ae dc cc e" |
"cj_ae dc cc (AEUnfold e) = cj_ae dc cc e" |
"cj_ae dc cc (AELet _ e1 e2) = (cj_ae dc cc e1 \<and> cj_ae dc cc e2)" |
"cj_ae dc cc (AEMatch _ e_dis cases) = (cj_ae dc cc e_dis \<and> (\<forall> (_, e_case) \<in> set cases. cj_ae dc cc e_case))" |
"cj_ae dc cc (AELam a x t1 e1 y t2 e2 t3) = (cj_alsc cc ((x, t1, y, t2, e2, t3), a) \<and> cj_ae dc cc e1 \<and> cj_ae dc cc e2)" |
"cj_ae dc cc (AEApp _ e1 e2) = (cj_ae dc cc e1 \<and> cj_ae dc cc e2)" |
"cj_ae dc cc (AEVar _) = True" |
"cj_ae dc cc (AEDef d as) = (
case dc d of
Some (vs, _, cs) \<Rightarrow> length vs = length as \<and> cj_alsc_all cc (alsc_lsv_subst_all (lsv_inst vs as) cs) |
None \<Rightarrow> False
)" |
"cj_ae dc cc (AESelf _ _) = True"
fun connected_components_step :: "(nat * nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat)" where
"connected_components_step (x, y) f = (\<lambda> z. if f z = min (f x) (f y) then max (f x) (f y) else f z)"
fun connected_components :: "(nat * nat) list \<Rightarrow> (nat \<Rightarrow> nat)" where
"connected_components edges = foldr connected_components_step edges id"
lemma connected_components_equiv: "(x, y) \<in> set edges \<Longrightarrow> connected_components edges x = connected_components edges y"
apply(induct edges)
by(auto)
fun
ti_fresh_t_list :: "nat \<Rightarrow> ST list \<Rightarrow> nat * (AT list)" and
ti_fresh_t :: "nat \<Rightarrow> ST \<Rightarrow> nat * AT" where
"ti_fresh_t_list count0 ts = (
foldr
(\<lambda> t (count_step, ts').
let (count_step', t') = ti_fresh_t count_step t in (count_step', t' # ts'))
ts
(count0, [])
)" |
"ti_fresh_t count0 (STFun t1 t2) = (
let
(count1, t1') = ti_fresh_t count0 t1;
(count2, t2') = ti_fresh_t count1 t2
in (count2 + 1, (ATFun (ALSVar count2) t1' t2'))
)" |
"ti_fresh_t count0 (STProd ts) = (
let (count_final, ts'_all) = ti_fresh_t_list count0 ts
in (count_final, ATProd ts'_all)
)" |
"ti_fresh_t count0 (STSum ts) = (
let (count_final, ts'_all) = ti_fresh_t_list count0 ts
in (count_final, ATSum ts'_all)
)" |
"ti_fresh_t count0 (STMu u t) = (
let (count, t') = ti_fresh_t count0 t in
(count, ATMu u t')
)" |
"ti_fresh_t count0 (STVar u) = (count0, ATVar u)
"
fun ti_fresh_e :: "ATCD \<Rightarrow> nat \<Rightarrow> SE \<Rightarrow> nat * AE" where
"ti_fresh_e dc count0 (SETup es) = (
let (count_final, es'_all) = (
foldr (\<lambda> t (count_step, es').
let (count_step', e') = ti_fresh_e dc count_step t in (count_step', e' # es')
) es (count0, []))
in (count_final, AETup es'_all)
)" |
"ti_fresh_e dc count0 (SEProj i e) = (
let (count1, e') = ti_fresh_e dc count0 e in
(count1, AEProj i e')
)" |
"ti_fresh_e dc count0 (SEInj ts i e) = (
let (count_ts, ts'_all) = (
foldr (\<lambda> t (count_step, ts').
let (count_step', t') = ti_fresh_t count_step t in (count_step', t' # ts')
) ts (count0, []));
(count_final, e') = ti_fresh_e dc count_ts e
in (count_final, AEInj ts'_all i e')
)" |
"ti_fresh_e dc count0 (SEFold u t e) = (
let
(count1, t') = ti_fresh_t count0 t;
(count2, e') = ti_fresh_e dc count1 e
in (count2, AEFold u t' e')
)" |
"ti_fresh_e dc count0 (SEUnfold e) = (
let (count1, e') = ti_fresh_e dc count0 e
in (count1, AEUnfold e')
)" |
"ti_fresh_e dc count0 (SELet x e1 e2) = (
let
(count1, e1') = ti_fresh_e dc count0 e1;
(count2, e2') = ti_fresh_e dc count1 e2
in (count2, AELet x e1' e2')
)" |
"ti_fresh_e dc count0 (SEMatch t e cases) = (
let
(count1, t') = ti_fresh_t count0 t;
(count2, e') = ti_fresh_e dc count0 e;
(count_final, cases'_final) = (
foldr (\<lambda> (x, e_case) (count_step, cases').
let (count_step', e_case') = ti_fresh_e dc count_step e_case in (count_step', (x, e_case') # cases')
) cases (count2, []))
in (count_final, AEMatch t' e' cases'_final)
)" |
"ti_fresh_e dc count0 (SELam x t1 e1 y t2 e2 t3) = (
let
(count1, t1') = ti_fresh_t count0 t1;
(count2, e1') = ti_fresh_e dc count1 e1;
(count3, t2') = ti_fresh_t count2 t2;
(count4, e2') = ti_fresh_e dc count3 e2;
(count5, t3') = ti_fresh_t count4 t3
in (count5 + 1, AELam (ALSVar count5) x t1' e1' y t2' e2' t3')
)" |
"ti_fresh_e dc count0 (SEApp e1 e2) = (
let
(count1, e1') = ti_fresh_e dc count0 e1;
(count2, e2') = ti_fresh_e dc count1 e2
in (count2 + 1, AEApp (ALSVar count2) e1' e2')
)" |
"ti_fresh_e dc count0 (SEVar x) = (count0, AEVar x)" |
(* The "None" case here is unnecessary, but it allows us to prove that the annotated expression
refines the source expression unconditionally *)
"ti_fresh_e dc count0 (SEDef d) = (
case dc d of
Some (vs, _) \<Rightarrow> let (count'_all, as_all) = foldr (\<lambda> _ (count', as_all).
(count' + 1, (ALSVar count') # as_all)
) vs (count0, []) in
(count'_all, AEDef d as_all) |
None \<Rightarrow> (count0, AEDef d [])
)" |
"ti_fresh_e dc count0 (SESelf d t) = (
let (count1, t') = ti_fresh_t count0 t in
(count1, AESelf d t')
)"
fun strip_at :: "AT \<Rightarrow> ST" where
"strip_at (ATFun a t1 t2) = STFun (strip_at t1) (strip_at t2)" |
"strip_at (ATProd ts) = STProd (map strip_at ts)" |
"strip_at (ATSum ts) = STSum (map strip_at ts)" |
"strip_at (ATMu u t) = STMu u (strip_at t)" |
"strip_at (ATVar u) = STVar u"
fun strip_ae :: "AE \<Rightarrow> SE" where
"strip_ae (AETup es) = SETup (map strip_ae es)" |
"strip_ae (AEProj i e) = SEProj i (strip_ae e)" |
"strip_ae (AEInj ts i e) = SEInj (map strip_at ts) i (strip_ae e)" |
"strip_ae (AEFold u t e) = SEFold u (strip_at t) (strip_ae e)" |
"strip_ae (AEUnfold e) = SEUnfold (strip_ae e)" |
"strip_ae (AELet x e1 e2) = SELet x (strip_ae e1) (strip_ae e2)" |
"strip_ae (AEMatch t e cases) = SEMatch (strip_at t) (strip_ae e) (map (\<lambda>(case_x, case_e). (case_x, strip_ae case_e)) cases)" |
"strip_ae (AELam a x t1 e1 y t2 e2 t3) = SELam x (strip_at t1) (strip_ae e1) y (strip_at t2) (strip_ae e2) (strip_at t3)" |
"strip_ae (AEApp a e1 e2) = SEApp (strip_ae e1) (strip_ae e2)" |
"strip_ae (AEVar x) = SEVar x" |
"strip_ae (AEDef d as) = SEDef d" |
"strip_ae (AESelf d t) = SESelf d (strip_at t)"
fun strip_ap :: "AP \<Rightarrow> SP" where
"strip_ap (APEntry d) = SPEntry d" |
"strip_ap (APDef d _ _ t e p) = SPDef d (strip_at t) (strip_ae e) (strip_ap p)"
fun strip_atcv :: "ATCV \<Rightarrow> STCV" where
"strip_atcv gc = (map_option strip_at) \<circ> gc"
fun strip_atcd :: "ATCD \<Rightarrow> STCD" where
"strip_atcd dc = (map_option (\<lambda> (_, t, _). strip_at t)) \<circ> dc"
fun strip_atcs :: "ATCS \<Rightarrow> STCS" where
"strip_atcs sc = (STCS (strip_atcd (atcs_defs sc)) (atcs_self_d sc) (strip_at (atcs_self_t sc)))"
(* ST/AT refinement *)
fun rj_st_at :: "ST \<Rightarrow> AT \<Rightarrow> bool" where
"rj_st_at t t' = (t = strip_at t')"
(* SE/AE refinement *)
fun rj_se_ae :: "SE \<Rightarrow> AE \<Rightarrow> bool" where
"rj_se_ae e e' = (e = strip_ae e')"
(* SP/AP refinement *)
fun rj_sp_ap :: "SP \<Rightarrow> AP \<Rightarrow> bool" where
"rj_sp_ap p p' = (p = strip_ap p')"
(* STCV/ATCV refinement *)
fun rj_stcv_atcv :: "STCV \<Rightarrow> ATCV \<Rightarrow> bool" where
"rj_stcv_atcv gc gc' = (gc = strip_atcv gc')"
(* STCD/ATCD refinement *)
fun rj_stcd_atcd :: "STCD \<Rightarrow> ATCD \<Rightarrow> bool" where
"rj_stcd_atcd dc dc' = (dc = strip_atcd dc')"
(* STCS/ATCS refinement *)
fun rj_stcs_atcs :: "STCS \<Rightarrow> ATCS \<Rightarrow> bool" where
"rj_stcs_atcs sc sc' = (sc = strip_atcs sc')"
lemma at_lsv_subst_preserve_strip: "strip_at (at_lsv_subst m t) = strip_at t"
by(induct_tac t, auto)
lemma ae_lsv_subst_preserve_strip: "strip_ae (ae_lsv_subst m e) = strip_ae e"
proof -
have "True \<and> True \<and> ?thesis"
apply(induct e rule: ALS_AT_AE.induct)
using at_lsv_subst_preserve_strip by auto
then show ?thesis by auto
qed
lemma at_mu_subst_preserve_strip: "strip_at (at_subst m t) = st_subst (strip_at \<circ> m) (strip_at t)"
by(induct t arbitrary: m, auto, simp add: fun_upd_comp)
lemma ti_fresh_refine_t: "rj_st_at t (snd (ti_fresh_t count t))"
proof(induct t arbitrary: count)
case (STFun t1 t2)
then show ?case
apply(simp)
by(simp add: split_def)
next
case (STProd ts)
then show ?case
apply(simp)
apply(simp add: split_def)
apply(induct ts)
by(auto)
next
case (STSum ts)
then show ?case
apply(simp)
apply(simp add: split_def)
apply(induct ts)
by(auto)
next
case (STMu x1 t)
then show ?case
apply(simp)
by(simp add: split_def)
next
case (STVar x)
then show ?case
by(auto)
qed
lemma ti_fresh_refine_e: "rj_se_ae e (snd (ti_fresh_e dc count e))"
proof(induct e arbitrary: count)
case (SETup es)
then show ?case
apply(simp)
apply(simp add: split_def)
apply(induct es)
by(auto)
next
case (SEProj i e)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SEInj ts i e)
then show ?case
apply(simp)
apply(simp add: split_def)
apply(induct ts)
using ti_fresh_refine_t apply(auto)
done
next
case (SEFold u t e)
then show ?case
apply(simp)
apply(simp add: split_def)
using ti_fresh_refine_t apply(auto)
done
next
case (SEUnfold e)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SELet x e1 e2)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SEMatch x e cases)
then show ?case
apply(simp)
apply(simp add: split_def)
using ti_fresh_refine_t apply(auto)
proof(induct cases)
case Nil
then show ?case
apply(auto)
done
next
case (Cons a cases)
then show ?case
apply(auto)
apply (metis (no_types, lifting) fst_conv prod_eqI snd_conv)
by blast
qed
next
case (SELam x t1 e1 y t2 e2 t3)
then show ?case
apply(simp)
apply(simp add: split_def)
using ti_fresh_refine_t apply(auto)
done
next
case (SEApp e1 e2)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SEVar x)
then show ?case
apply(simp)
done
next
case (SEDef x)
then show ?case
apply(simp)
apply(split option.split)
apply(simp add: split_def)
apply(auto)
by (metis sndI strip_ae.simps(11))
next
case (SESelf d t)
then show ?case
apply(simp)
apply(simp add: split_def)
using ti_fresh_refine_t apply(auto)
done
qed
lemma tj_se_ae_refine: "
tj_se sc gc e0 t0 \<Longrightarrow>
tj_ae sc' gc' e0' t0' \<Longrightarrow>
rj_stcs_atcs sc sc' \<Longrightarrow>
rj_stcv_atcv gc gc' \<Longrightarrow>
rj_se_ae e0 e0' \<Longrightarrow>
rj_st_at t0 t0'
"
proof(induct e0 arbitrary: e0' sc sc' gc gc' t0 t0')
case (SETup es)
obtain ts where ts_obtain: "t0 = STProd ts"
using SETup.prems by auto
obtain es' where es'_obtain: "e0' = AETup es' \<and> es = map strip_ae es'"
using SETup.prems by(case_tac e0', auto)
obtain ts' where ts'_obtain: "t0' = ATProd ts'"
using SETup.prems es'_obtain by auto
have each_refines: "\<And>i. i < length es \<Longrightarrow> rj_st_at (ts ! i) (ts' ! i)"
proof -
fix i
assume i_range: "i < length es"
show "rj_st_at (ts ! i) (ts' ! i)"
proof(rule SETup.hyps)
show "(es ! i) \<in> set es"
using SETup.prems i_range by auto
have "(es ! i, ts ! i) \<in> set (zip es ts)"
using i_range SETup.prems(1) ts_obtain apply auto
by (metis fst_conv in_set_zip snd_conv)
then show "tj_se sc gc (es ! i) (ts ! i)"
using SETup.prems(1) ts_obtain by auto
have "(es' ! i, ts' ! i) \<in> set (zip es' ts')"
using i_range SETup.prems(2) es'_obtain ts'_obtain in_set_zip by force
then show "tj_ae sc' gc' (es' ! i) (ts' ! i)"
using SETup.prems(2) es'_obtain ts'_obtain by auto
show "rj_stcs_atcs sc sc'"
using SETup.prems by auto
show "rj_stcv_atcv gc gc'"
using SETup.prems by auto
show "rj_se_ae (es ! i) (es' ! i)"
using SETup.prems i_range es'_obtain by auto
qed
qed
then show ?case
using ts_obtain ts'_obtain SETup.prems es'_obtain apply auto
by (simp add: nth_equalityI)
next
case (SEProj i e)
obtain ts where ts_obtain: "tj_se sc gc e (STProd ts)"
using SEProj.prems by auto
obtain e' where e'_obtain: "e0' = AEProj i e' \<and> e = strip_ae e'"
using SEProj.prems by(case_tac e0', auto)
obtain ts' where ts'_obtain: "tj_ae sc' gc' e' (ATProd ts')"
using SEProj.prems e'_obtain by auto
have ts_refine: "rj_st_at (STProd ts) (ATProd ts')"
proof(rule SEProj.hyps)
show "tj_se sc gc e (STProd ts)"
using ts_obtain .
show "tj_ae sc' gc' e' (ATProd ts')"
using ts'_obtain .
show "rj_stcs_atcs sc sc'"
using SEProj.prems by auto
show "rj_stcv_atcv gc gc'"
using SEProj.prems by auto
show "rj_se_ae e e'"
using e'_obtain by auto
qed
then have "rj_st_at (ts ! i) (ts' ! i)"
using SEProj.prems ts_obtain e'_obtain ts'_obtain apply auto
by (metis SEProj.hyps SEProj.prems(3) SEProj.prems(4) ST.inject(2) length_map nth_map rj_se_ae.elims(3) rj_st_at.simps)
then show ?case
using SEProj.prems apply auto
using SEProj.hyps e'_obtain by fastforce
next
case (SEInj ts i e)
have t0_decomp: "t0 = STSum ts"
using SEInj.prems by auto
obtain ts' e' where ts'_e'_obtain: "e0' = AEInj ts' i e'"
using SEInj.prems by(case_tac e0', auto)
then show ?case
using SEInj.prems t0_decomp ts'_e'_obtain by auto
next
case (SEFold u t e)
obtain t' e' where t'_e'_obtain: "e0' = AEFold u t' e' \<and> rj_st_at t t' \<and> rj_se_ae e e'"
using SEFold.prems by(case_tac e0', auto)
then show ?case
using SEFold.prems by auto
next
case (SEUnfold e)
obtain u t where u_t_obtain: "tj_se sc gc e (STMu u t) \<and> t0 = st_subst (STVar(u := STMu u t)) t"
using SEUnfold.prems by auto
obtain e' where e'_obtain: "e0' = AEUnfold e' \<and> rj_se_ae e e'"
using SEUnfold.prems by(case_tac e0', auto)
obtain t' where t'_obtain: "tj_ae sc' gc' e' (ATMu u t') \<and> t0' = at_subst (ATVar(u := ATMu u t')) t' \<and> rj_st_at t t'"
using SEUnfold.prems(2) e'_obtain apply(auto)
using SEUnfold.hyps SEUnfold.prems(3) SEUnfold.prems(4) u_t_obtain
by (metis (mono_tags, lifting) ST.inject(4) e'_obtain rj_st_at.elims(2) strip_at.simps(4))
have "(STVar(u := STMu u t)) = strip_at \<circ> (ATVar(u := ATMu u t'))"
using t'_obtain by auto
then have "strip_at (at_subst (ATVar(u := ATMu u t')) t') = st_subst (STVar(u := STMu u t)) t"
using t'_obtain at_mu_subst_preserve_strip by auto
then show ?case
using u_t_obtain e'_obtain t'_obtain by simp
next
case (SELet x e1 e2)
obtain t_var where t_var_obtain: "tj_se sc gc e1 t_var"
using SELet.prems by auto
obtain e1' e2' where e1'_e2'_obtain: "e0' = AELet x e1' e2' \<and> rj_se_ae e1 e1' \<and> rj_se_ae e2 e2'"
using SELet.prems by(case_tac e0', auto)
obtain t_var' where t_var'_obtain: "tj_ae sc' gc' e1' t_var' \<and> tj_ae sc' (gc'(x := Some t_var')) e2' t0'"
using SELet.prems e1'_e2'_obtain by(auto)
have t_var_refine: "rj_st_at t_var t_var'"
proof(rule SELet.hyps(1))
show "tj_se sc gc e1 t_var"
using t_var_obtain by auto
show "tj_ae sc' gc' e1' t_var'"
using t_var'_obtain by auto
show "rj_stcs_atcs sc sc'"
using SELet.prems by auto
show "rj_stcv_atcv gc gc'"
using SELet.prems by auto
show "rj_se_ae e1 e1'"
using e1'_e2'_obtain by auto
qed
show ?case
proof(rule SELet.hyps(2))
show "tj_se sc (gc(x := Some t_var)) e2 t0"
using SELet.prems t_var_obtain apply(auto)
by (metis SELet.hyps(1) SELet.prems(3) SELet.prems(4) e1'_e2'_obtain rj_st_at.elims(2) t_var'_obtain)
show "tj_ae sc' (gc'(x := Some t_var')) e2' t0'"
using t_var'_obtain by auto
show "rj_stcs_atcs sc sc'"
using SELet.prems by auto
show "rj_stcv_atcv (gc(x := Some t_var)) (gc'(x := Some t_var'))"
using SELet.prems t_var_refine by auto
show "rj_se_ae e2 e2'"
using e1'_e2'_obtain by auto
qed
next
case (SEMatch t_ret e_dis cases)
obtain t_ret' e_dis' cases' where t_ret'_obtain: "e0' = AEMatch t_ret' e_dis' cases' \<and> rj_st_at t_ret t_ret'"
using SEMatch.prems by(case_tac e0', auto)
then show ?case
using SEMatch.prems by auto
next
case (SELam x t1 e1 y t2 e2 t3)
obtain a t1' e1' t2' e2' t3' where e0'_decomp: "e0' = AELam a x t1' e1' y t2' e2' t3' \<and> rj_st_at t2 t2' \<and> rj_st_at t3 t3'"
using SELam.prems by(case_tac e0', auto)
then show ?case
using SELam.prems by auto
next
case (SEApp e1 e2)
obtain a e1' e2' where a_e1'_e2'_obtain: "e0' = AEApp a e1' e2' \<and> rj_se_ae e1 e1' \<and> rj_se_ae e2 e2'"
using SEApp.prems by(case_tac e0', auto)
obtain t_arg where t_arg_obtain: "tj_se sc gc e1 (STFun t_arg t0) \<and> tj_se sc gc e2 t_arg"
using SEApp.prems by auto
obtain t_arg' where t_arg'_obtain: "tj_ae sc' gc' e1' (ATFun a t_arg' t0') \<and> tj_ae sc' gc' e2' t_arg'"
using SEApp.prems a_e1'_e2'_obtain by auto
have "rj_st_at (STFun t_arg t0) (ATFun a t_arg' t0')"
proof(rule SEApp.hyps(1))
show "tj_se sc gc e1 (STFun t_arg t0)"
using t_arg_obtain by auto
show "tj_ae sc' gc' e1' (ATFun a t_arg' t0')"
using t_arg'_obtain by auto
show "rj_stcs_atcs sc sc'"
using SEApp.prems by auto
show "rj_stcv_atcv gc gc'"
using SEApp.prems by auto
show "rj_se_ae e1 e1'"
using a_e1'_e2'_obtain by auto
qed
then show ?case by auto
next
case (SEVar x)
have "e0' = AEVar x"
using SEVar.prems by(case_tac e0', auto)
then show ?case
using SEVar.prems by auto
next
case (SEDef d)
obtain as where e0'_decomp: "e0' = AEDef d as"
using SEDef.prems by(case_tac e0', auto)
then show ?case
using SEDef.prems at_lsv_subst_preserve_strip by auto
next
case (SESelf d t)
obtain t' where e0'_decomp: "e0' = AESelf d t' \<and> rj_st_at t t'"
using SESelf.prems by(case_tac e0', auto)
then show ?case
using SESelf.prems by auto
qed
(* Definition well-formed: source expression *)
fun dwf_se :: "STCD \<Rightarrow> SE \<Rightarrow> bool" where
"dwf_se dc (SETup es) = (\<forall> e \<in> set es. dwf_se dc e)" |
"dwf_se dc (SEProj i e) = dwf_se dc e" |
"dwf_se dc (SEInj ts i e) = dwf_se dc e" |
"dwf_se dc (SEFold u t e) = dwf_se dc e" |
"dwf_se dc (SEUnfold e) = dwf_se dc e" |
"dwf_se dc (SELet x e1 e2) = (dwf_se dc e1 \<and> dwf_se dc e2)" |
"dwf_se dc (SEMatch t e cases) = (dwf_se dc e \<and> (\<forall> (_, e_case) \<in> set cases. dwf_se dc e_case))" |
"dwf_se dc (SELam x t1 e1 y t2 e2 t3) = (dwf_se dc e1 \<and> dwf_se dc e2)" |
"dwf_se dc (SEApp e1 e2) = (dwf_se dc e1 \<and> dwf_se dc e2)" |
"dwf_se dc (SEVar x) = True" |
"dwf_se dc (SEDef d) = (dc d \<noteq> None)" |
"dwf_se dc (SESelf _ _) = True"
(* Definition well-formed: annotated expression *)
fun dwf_ae :: "ATCD \<Rightarrow> AE \<Rightarrow> bool" where
"dwf_ae dc (AETup es) = (\<forall> e \<in> set es. dwf_ae dc e)" |
"dwf_ae dc (AEProj i e) = dwf_ae dc e" |
"dwf_ae dc (AEInj ts i e) = dwf_ae dc e" |
"dwf_ae dc (AEFold u t e) = dwf_ae dc e" |
"dwf_ae dc (AEUnfold e) = dwf_ae dc e" |
"dwf_ae dc (AELet x e1 e2) = (dwf_ae dc e1 \<and> dwf_ae dc e2)" |
"dwf_ae dc (AEMatch t e cases) = (dwf_ae dc e \<and> (\<forall> (_, e_case) \<in> set cases. dwf_ae dc e_case))" |
"dwf_ae dc (AELam a x t1 e1 y t2 e2 t3) = (dwf_ae dc e1 \<and> dwf_ae dc e2)" |
"dwf_ae dc (AEApp a e1 e2) = (dwf_ae dc e1 \<and> dwf_ae dc e2)" |
"dwf_ae dc (AEVar x) = True" |
"dwf_ae dc (AEDef d as) = (case dc d of Some (vs, _) \<Rightarrow> (length vs = length as) | None \<Rightarrow> False)" |
"dwf_ae dc (AESelf _ _) = True"
lemma ti_fresh_dwf_e:
assumes dc_refine: "rj_stcd_atcd dc dc'"
shows "
dwf_se dc e \<Longrightarrow>
dwf_ae dc' (snd (ti_fresh_e dc' count e))
"
proof(induct e arbitrary: count)
case (SETup es)
then show ?case
apply(simp)
apply(simp add : split_def)
apply(induct es)
apply(auto)
done
next
case (SEProj i e)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SEInj ts i e)
then show ?case
apply(simp)
apply(simp add : split_def)
done
next
case (SEFold u t e)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SEUnfold e)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SELet x e1 e2)
then show ?case
apply(simp)
apply(simp add: split_def)
done
next
case (SEMatch t e cases)
then show ?case
apply(simp)
apply(simp add: split_def)
proof(induct cases)
case Nil
then show ?case
apply(simp)
done