21 (* to be given by the user *) |
21 (* to be given by the user *) |
22 primrec |
22 primrec |
23 bv1 |
23 bv1 |
24 where |
24 where |
25 "bv1 (BUnit) = {}" |
25 "bv1 (BUnit) = {}" |
26 | "bv1 (BVr x) = {x}" |
26 | "bv1 (BVr x) = {atom x}" |
27 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
27 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
28 |
28 |
29 (* needs to be calculated by the package *) |
29 (* needs to be calculated by the package *) |
30 primrec |
30 primrec |
31 fv_trm1 and fv_bp |
31 fv_trm1 and fv_bp |
32 where |
32 where |
33 "fv_trm1 (Vr1 x) = {x}" |
33 "fv_trm1 (Vr1 x) = {atom x}" |
34 | "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)" |
35 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}" |
35 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {atom x}" |
36 | "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)" |
37 | "fv_bp (BUnit) = {}" |
37 | "fv_bp (BUnit) = {}" |
38 | "fv_bp (BVr x) = {x}" |
38 | "fv_bp (BVr x) = {atom x}" |
39 | "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)" |
40 |
40 |
41 (* needs to be stated by the package *) |
41 (* needs to be stated by the package *) |
42 instantiation |
42 instantiation |
43 trm1 :: pt |
43 trm1 and bp :: pt |
44 bp :: pt |
44 begin |
45 begin |
45 |
46 |
46 primrec |
47 primrec |
47 permute_trm1 and permute_bp |
48 perm_trm1 and perm_bp |
48 where |
49 where |
49 "permute_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)" |
50 "perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)" |
50 | "permute_trm1 pi (Ap1 t1 t2) = Ap1 (permute_trm1 pi t1) (permute_trm1 pi t2)" |
51 | "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)" |
51 | "permute_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (permute_trm1 pi t)" |
52 | "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)" |
52 | "permute_trm1 pi (Lt1 bp t1 t2) = Lt1 (permute_bp pi bp) (permute_trm1 pi t1) (permute_trm1 pi t2)" |
53 | "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)" |
53 | "permute_bp pi (BUnit) = BUnit" |
54 | "perm_bp pi (BUnit) = BUnit" |
54 | "permute_bp pi (BVr a) = BVr (pi \<bullet> a)" |
55 | "perm_bp pi (BVr a) = BVr (pi \<bullet> a)" |
55 | "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)" |
56 | "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)" |
56 |
|
57 lemma pt_trm1_bp_zero: |
|
58 fixes t::trm1 |
|
59 and b::bp |
|
60 shows "0 \<bullet> t = t" |
|
61 and "0 \<bullet> b = b" |
|
62 apply(induct t and b rule: trm1_bp.inducts) |
|
63 apply(simp_all) |
|
64 done |
|
65 |
|
66 lemma pt_trm1_bp_plus: |
|
67 fixes t::trm1 |
|
68 and b::bp |
|
69 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
|
70 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)" |
|
71 apply(induct t and b rule: trm1_bp.inducts) |
|
72 apply(simp_all) |
|
73 done |
|
74 |
|
75 instance |
|
76 apply default |
|
77 apply(simp_all add: pt_trm1_bp_zero pt_trm1_bp_plus) |
|
78 done |
57 |
79 |
58 end |
80 end |
59 |
81 |
60 inductive |
82 inductive |
61 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
83 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
62 where |
84 where |
63 a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)" |
85 a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)" |
64 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2" |
86 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2" |
65 | a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> |
87 | a3: "\<exists>pi. (fv_trm1 t - {atom a} = fv_trm1 s - {atom b} \<and> |
66 (fv_trm1 t - {a})\<sharp>* pi \<and> |
88 (fv_trm1 t - {atom a})\<sharp>* pi \<and> |
67 (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b) |
89 (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b) |
68 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
90 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
69 | a4: "\<exists>pi::name prm.( |
91 | a4: "\<exists>pi.(t1 \<approx>1 t2 \<and> |
70 t1 \<approx>1 t2 \<and> |
92 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
71 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
93 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
72 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
94 (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *)) |
73 (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *) |
95 \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2" |
74 ) \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2" |
96 |
75 |
97 lemma alpha1_equivp: "equivp alpha1" |
76 lemma alpha1_equivp: "equivp alpha1" sorry |
98 sorry |
77 |
99 |
78 quotient_type qtrm1 = trm1 / alpha1 |
100 quotient_type qtrm1 = trm1 / alpha1 |
79 by (rule alpha1_equivp) |
101 by (rule alpha1_equivp) |
80 |
102 |
81 |
103 |
91 |
113 |
92 (* to be given by the user *) |
114 (* to be given by the user *) |
93 primrec |
115 primrec |
94 bv2 |
116 bv2 |
95 where |
117 where |
96 "bv2 (As x t) = {x}" |
118 "bv2 (As x t) = {atom x}" |
97 |
119 |
98 (* needs to be calculated by the package *) |
120 (* needs to be calculated by the package *) |
99 primrec |
121 primrec |
100 fv_trm2 and fv_assign |
122 fv_trm2 and fv_assign |
101 where |
123 where |
102 "fv_trm2 (Vr2 x) = {x}" |
124 "fv_trm2 (Vr2 x) = {atom x}" |
103 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
125 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
104 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}" |
126 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}" |
105 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
127 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
106 | "fv_assign (As x t) = (fv_trm2 t)" |
128 | "fv_assign (As x t) = (fv_trm2 t)" |
107 |
129 |
108 (* needs to be stated by the package *) |
130 (* needs to be stated by the package *) |
109 overloading |
131 instantiation |
110 perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2" (unchecked) |
132 trm2 and assign :: pt |
111 perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked) |
133 begin |
112 begin |
134 |
113 |
135 primrec |
114 primrec |
136 permute_trm2 and permute_assign |
115 perm_trm2 and perm_assign |
137 where |
116 where |
138 "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)" |
117 "perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)" |
139 | "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)" |
118 | "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)" |
140 | "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)" |
119 | "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)" |
141 | "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)" |
120 | "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)" |
142 | "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)" |
121 | "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)" |
143 |
|
144 lemma pt_trm2_assign_zero: |
|
145 fixes t::trm2 |
|
146 and b::assign |
|
147 shows "0 \<bullet> t = t" |
|
148 and "0 \<bullet> b = b" |
|
149 apply(induct t and b rule: trm2_assign.inducts) |
|
150 apply(simp_all) |
|
151 done |
|
152 |
|
153 lemma pt_trm2_assign_plus: |
|
154 fixes t::trm2 |
|
155 and b::assign |
|
156 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
|
157 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)" |
|
158 apply(induct t and b rule: trm2_assign.inducts) |
|
159 apply(simp_all) |
|
160 done |
|
161 |
|
162 instance |
|
163 apply default |
|
164 apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus) |
|
165 done |
|
166 |
122 |
167 |
123 end |
168 end |
124 |
169 |
125 inductive |
170 inductive |
126 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
171 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
127 where |
172 where |
128 a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)" |
173 a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)" |
129 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2" |
174 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2" |
130 | a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> |
175 | a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and> |
131 (fv_trm2 t - {a})\<sharp>* pi \<and> |
176 (fv_trm2 t - {atom a})\<sharp>* pi \<and> |
132 (pi \<bullet> t) \<approx>2 s \<and> |
177 (pi \<bullet> t) \<approx>2 s \<and> |
133 (pi \<bullet> a) = b) |
178 (pi \<bullet> a) = b) |
134 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s" |
179 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s" |
135 | a4: "\<exists>pi::name prm. ( |
180 | a4: "\<exists>pi. ( |
136 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and> |
181 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and> |
137 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and> |
182 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and> |
138 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
183 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
139 ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2" |
184 ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2" |
140 |
185 |
141 lemma alpha2_equivp: "equivp alpha2" sorry |
186 lemma alpha2_equivp: "equivp alpha2" |
|
187 sorry |
142 |
188 |
143 quotient_type qtrm2 = trm2 / alpha2 |
189 quotient_type qtrm2 = trm2 / alpha2 |
144 by (rule alpha2_equivp) |
190 by (rule alpha2_equivp) |
145 |
191 |
146 section {*** lets with many assignments ***} |
192 section {*** lets with many assignments ***} |
157 (* to be given by the user *) |
203 (* to be given by the user *) |
158 primrec |
204 primrec |
159 bv3 |
205 bv3 |
160 where |
206 where |
161 "bv3 ANil = {}" |
207 "bv3 ANil = {}" |
162 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
208 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
163 |
209 |
164 primrec |
210 primrec |
165 fv_trm3 and fv_assigns |
211 fv_trm3 and fv_assigns |
166 where |
212 where |
167 "fv_trm3 (Vr3 x) = {x}" |
213 "fv_trm3 (Vr3 x) = {atom x}" |
168 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
214 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
169 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}" |
215 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {atom x}" |
170 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
216 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
171 | "fv_assigns (ANil) = {}" |
217 | "fv_assigns (ANil) = {}" |
172 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
218 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
173 |
219 |
174 (* needs to be stated by the package *) |
220 (* needs to be stated by the package *) |
175 overloading |
221 instantiation |
176 perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3" (unchecked) |
222 trm3 and assigns :: pt |
177 perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked) |
223 begin |
178 begin |
224 |
179 |
225 primrec |
180 primrec |
226 permute_trm3 and permute_assigns |
181 perm_trm3 and perm_assigns |
227 where |
182 where |
228 "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)" |
183 "perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)" |
229 | "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)" |
184 | "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)" |
230 | "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)" |
185 | "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)" |
231 | "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)" |
186 | "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)" |
232 | "permute_assigns pi (ANil) = ANil" |
187 | "perm_assigns pi (ANil) = ANil" |
233 | "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)" |
188 | "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)" |
234 |
|
235 lemma pt_trm3_assigns_zero: |
|
236 fixes t::trm3 |
|
237 and b::assigns |
|
238 shows "0 \<bullet> t = t" |
|
239 and "0 \<bullet> b = b" |
|
240 apply(induct t and b rule: trm3_assigns.inducts) |
|
241 apply(simp_all) |
|
242 done |
|
243 |
|
244 lemma pt_trm3_assigns_plus: |
|
245 fixes t::trm3 |
|
246 and b::assigns |
|
247 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
|
248 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)" |
|
249 apply(induct t and b rule: trm3_assigns.inducts) |
|
250 apply(simp_all) |
|
251 done |
|
252 |
|
253 instance |
|
254 apply default |
|
255 apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus) |
|
256 done |
|
257 |
189 |
258 |
190 end |
259 end |
191 |
260 |
192 inductive |
261 inductive |
193 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
262 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
194 where |
263 where |
195 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
264 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
196 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
265 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
197 | a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> |
266 | a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and> |
198 (fv_trm3 t - {a})\<sharp>* pi \<and> |
267 (fv_trm3 t - {atom a})\<sharp>* pi \<and> |
199 (pi \<bullet> t) \<approx>3 s \<and> |
268 (pi \<bullet> t) \<approx>3 s \<and> |
200 (pi \<bullet> a) = b) |
269 (pi \<bullet> a) = b) |
201 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
270 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
202 | a4: "\<exists>pi::name prm. ( |
271 | a4: "\<exists>pi. ( |
203 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
272 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
204 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
273 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
205 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
274 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
206 ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2" |
275 ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2" |
207 |
276 |
208 lemma alpha3_equivp: "equivp alpha3" sorry |
277 lemma alpha3_equivp: "equivp alpha3" |
|
278 sorry |
209 |
279 |
210 quotient_type qtrm3 = trm3 / alpha3 |
280 quotient_type qtrm3 = trm3 / alpha3 |
211 by (rule alpha3_equivp) |
281 by (rule alpha3_equivp) |
212 |
282 |
213 |
283 |
221 thm trm4.recs |
291 thm trm4.recs |
222 |
292 |
223 primrec |
293 primrec |
224 fv_trm4 and fv_trm4_list |
294 fv_trm4 and fv_trm4_list |
225 where |
295 where |
226 "fv_trm4 (Vr4 x) = {x}" |
296 "fv_trm4 (Vr4 x) = {atom x}" |
227 | "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
297 | "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
228 | "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {x}" |
298 | "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {atom x}" |
229 | "fv_trm4_list ([]) = {}" |
299 | "fv_trm4_list ([]) = {}" |
230 | "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
300 | "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
231 |
301 |
232 |
302 |
233 (* needs to be stated by the package *) |
303 (* needs to be stated by the package *) |
234 (* there cannot be a clause for lists, as *) |
304 (* there cannot be a clause for lists, as *) |
235 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
305 (* permuteutations are already defined in Nominal (also functions, options, and so on) *) |
236 overloading |
306 instantiation |
237 perm_trm4 \<equiv> "perm :: 'x prm \<Rightarrow> trm4 \<Rightarrow> trm4" (unchecked) |
307 trm4 :: pt |
238 begin |
308 begin |
239 |
309 |
240 primrec |
310 (* does not work yet *) |
241 perm_trm4 |
311 primrec |
242 where |
312 permute_trm4 |
243 "perm_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)" |
313 where |
244 | "perm_trm4 pi (Ap4 t ts) = Ap4 (perm_trm4 pi t) (pi \<bullet> ts)" |
314 "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)" |
245 | "perm_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (perm_trm4 pi t)" |
315 | "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute pi ts)" |
|
316 | "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)" |
246 |
317 |
247 end |
318 end |
248 |
319 |
249 inductive |
320 inductive |
250 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
321 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |