14 BUnit |
17 BUnit |
15 | BVr "name" |
18 | BVr "name" |
16 | BPr "bp" "bp" |
19 | BPr "bp" "bp" |
17 |
20 |
18 (* to be given by the user *) |
21 (* to be given by the user *) |
19 fun |
22 primrec |
20 bv1 |
23 bv1 |
21 where |
24 where |
22 "bv1 (BUnit) = {}" |
25 "bv1 (BUnit) = {}" |
23 | "bv1 (BVr x) = {x}" |
26 | "bv1 (BVr x) = {x}" |
24 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
27 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
25 |
28 |
26 (* needs to be calculated by the package *) |
29 (* needs to be calculated by the package *) |
27 fun |
30 primrec |
28 fv_trm1 and fv_bp |
31 fv_trm1 and fv_bp |
29 where |
32 where |
30 "fv_trm1 (Vr1 x) = {x}" |
33 "fv_trm1 (Vr1 x) = {x}" |
31 | "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)" |
34 | "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)" |
32 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}" |
35 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}" |
33 | "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)" |
36 | "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)" |
34 | "fv_bp (BUnit) = {}" |
37 | "fv_bp (BUnit) = {}" |
35 | "fv_bp (BVr x) = {x}" |
38 | "fv_bp (BVr x) = {x}" |
36 | "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)" |
39 | "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)" |
37 |
40 |
38 text {*** lets with single assignments ***} |
41 (* needs to be stated by the package *) |
|
42 overloading |
|
43 perm_trm1 \<equiv> "perm :: 'x prm \<Rightarrow> trm1 \<Rightarrow> trm1" (unchecked) |
|
44 perm_bp \<equiv> "perm :: 'x prm \<Rightarrow> bp \<Rightarrow> bp" (unchecked) |
|
45 begin |
|
46 |
|
47 primrec |
|
48 perm_trm1 and perm_bp |
|
49 where |
|
50 "perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)" |
|
51 | "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)" |
|
52 | "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)" |
|
53 | "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)" |
|
54 | "perm_bp pi (BUnit) = BUnit" |
|
55 | "perm_bp pi (BVr a) = BVr (pi \<bullet> a)" |
|
56 | "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)" |
|
57 |
|
58 end |
|
59 |
|
60 |
|
61 section {*** lets with single assignments ***} |
|
62 |
39 datatype trm2 = |
63 datatype trm2 = |
40 Vr2 "name" |
64 Vr2 "name" |
41 | Ap2 "trm2" "trm2" |
65 | Ap2 "trm2" "trm2" |
42 | Lm2 "name" "trm2" |
66 | Lm2 "name" "trm2" |
43 | Lt2 "assign" "trm2" |
67 | Lt2 "assign" "trm2" |
44 and assign = |
68 and assign = |
45 As "name" "trm2" |
69 As "name" "trm2" |
46 |
70 |
47 (* to be given by the user *) |
71 (* to be given by the user *) |
48 fun |
72 primrec |
49 bv2 |
73 bv2 |
50 where |
74 where |
51 "bv2 (As x t) = {x}" |
75 "bv2 (As x t) = {x}" |
52 |
76 |
53 (* needs to be calculated by the package *) |
77 (* needs to be calculated by the package *) |
54 fun |
78 primrec |
55 fv_trm2 and fv_assign |
79 fv_trm2 and fv_assign |
56 where |
80 where |
57 "fv_trm2 (Vr2 x) = {x}" |
81 "fv_trm2 (Vr2 x) = {x}" |
58 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
82 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
59 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}" |
83 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}" |
60 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
84 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
61 | "fv_assign (As x t) = (fv_trm2 t)" |
85 | "fv_assign (As x t) = (fv_trm2 t)" |
62 |
86 |
|
87 (* needs to be stated by the package *) |
|
88 overloading |
|
89 perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2" (unchecked) |
|
90 perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked) |
|
91 begin |
63 |
92 |
64 text {*** lets with many assignments ***} |
93 primrec |
|
94 perm_trm2 and perm_assign |
|
95 where |
|
96 "perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)" |
|
97 | "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)" |
|
98 | "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)" |
|
99 | "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)" |
|
100 | "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)" |
|
101 |
|
102 end |
|
103 |
|
104 |
|
105 section {*** lets with many assignments ***} |
|
106 |
65 datatype trm3 = |
107 datatype trm3 = |
66 Vr3 "name" |
108 Vr3 "name" |
67 | Ap3 "trm3" "trm3" |
109 | Ap3 "trm3" "trm3" |
68 | Lm3 "name" "trm3" |
110 | Lm3 "name" "trm3" |
69 | Lt3 "assigns" "trm3" |
111 | Lt3 "assigns" "trm3" |
70 and assigns = |
112 and assigns = |
71 ANil |
113 ANil |
72 | ACons "name" "trm3" "assigns" |
114 | ACons "name" "trm3" "assigns" |
73 |
115 |
74 (* to be given by the user *) |
116 (* to be given by the user *) |
75 fun |
117 primrec |
76 bv3 |
118 bv3 |
77 where |
119 where |
78 "bv3 ANil = {}" |
120 "bv3 ANil = {}" |
79 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
121 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
80 |
122 |
81 fun |
123 primrec |
82 fv_trm3 and fv_assigns |
124 fv_trm3 and fv_assigns |
83 where |
125 where |
84 "fv_trm3 (Vr3 x) = {x}" |
126 "fv_trm3 (Vr3 x) = {x}" |
85 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
127 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
86 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}" |
128 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}" |
87 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
129 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
88 | "fv_assigns (ANil) = {}" |
130 | "fv_assigns (ANil) = {}" |
89 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
131 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
90 |
132 |
|
133 (* needs to be stated by the package *) |
|
134 overloading |
|
135 perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3" (unchecked) |
|
136 perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked) |
|
137 begin |
|
138 |
|
139 primrec |
|
140 perm_trm3 and perm_assigns |
|
141 where |
|
142 "perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)" |
|
143 | "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)" |
|
144 | "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)" |
|
145 | "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)" |
|
146 | "perm_assigns pi (ANil) = ANil" |
|
147 | "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)" |
|
148 |
91 end |
149 end |
|
150 |
|
151 |
|
152 end |