23 apply(drule_tac x="- p \<bullet> xa" in bspec) |
23 apply(drule_tac x="- p \<bullet> xa" in bspec) |
24 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
24 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
25 apply(simp) |
25 apply(simp) |
26 apply(simp) |
26 apply(simp) |
27 done |
27 done |
|
28 |
|
29 lemma fresh_minus_perm: |
|
30 fixes p::perm |
|
31 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
|
32 apply(simp add: fresh_def) |
|
33 apply(simp only: supp_minus_perm) |
|
34 done |
28 |
35 |
29 lemma fresh_plus: |
36 lemma fresh_plus: |
30 fixes p q::perm |
37 fixes p q::perm |
31 shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)" |
38 shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)" |
32 unfolding fresh_def |
39 unfolding fresh_def |
144 inductive |
151 inductive |
145 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
152 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
146 where |
153 where |
147 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
154 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
148 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
155 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
149 | a3: "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s)) \<Longrightarrow> rLam a t \<approx> rLam b s" |
156 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s) |
150 |
157 \<Longrightarrow> rLam a t \<approx> rLam b s" |
151 thm alpha.induct |
|
152 |
158 |
153 lemma a3_inverse: |
159 lemma a3_inverse: |
154 assumes "rLam a t \<approx> rLam b s" |
160 assumes "rLam a t \<approx> rLam b s" |
155 shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))" |
161 shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)" |
156 using assms |
162 using assms |
157 apply(erule_tac alpha.cases) |
163 apply(erule_tac alpha.cases) |
158 apply(auto) |
164 apply(auto) |
159 done |
165 done |
160 |
166 |
164 apply(induct rule: alpha.induct) |
170 apply(induct rule: alpha.induct) |
165 apply(simp add: a1) |
171 apply(simp add: a1) |
166 apply(simp add: a2) |
172 apply(simp add: a2) |
167 apply(simp) |
173 apply(simp) |
168 apply(rule a3) |
174 apply(rule a3) |
|
175 apply(erule conjE) |
169 apply(erule exE) |
176 apply(erule exE) |
|
177 apply(erule conjE) |
170 apply(rule_tac x="pi \<bullet> pia" in exI) |
178 apply(rule_tac x="pi \<bullet> pia" in exI) |
171 apply(simp add: alpha_gen.simps) |
179 apply(rule conjI) |
172 apply(erule conjE)+ |
|
173 apply(rule conjI)+ |
|
174 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
180 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
175 apply(simp add: eqvts atom_eqvt) |
181 apply(simp add: eqvts atom_eqvt) |
176 apply(rule conjI) |
182 apply(rule conjI) |
177 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
183 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
178 apply(simp add: eqvts atom_eqvt) |
184 apply(simp add: eqvts atom_eqvt) |
185 apply(induct t rule: rlam.induct) |
191 apply(induct t rule: rlam.induct) |
186 apply(simp add: a1) |
192 apply(simp add: a1) |
187 apply(simp add: a2) |
193 apply(simp add: a2) |
188 apply(rule a3) |
194 apply(rule a3) |
189 apply(rule_tac x="0" in exI) |
195 apply(rule_tac x="0" in exI) |
190 apply(rule alpha_gen_refl) |
196 apply(simp_all add: fresh_star_def fresh_zero_perm) |
191 apply(assumption) |
197 done |
192 done |
|
193 |
|
194 lemma fresh_minus_perm: |
|
195 fixes p::perm |
|
196 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
|
197 apply(simp add: fresh_def) |
|
198 apply(simp only: supp_minus_perm) |
|
199 done |
|
200 |
|
201 lemma alpha_gen_atom_sym: |
|
202 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
203 shows "\<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R x2 x1 f pi ({atom b}, s) \<Longrightarrow> |
|
204 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
|
205 apply(erule exE) |
|
206 apply(rule_tac x="- pi" in exI) |
|
207 apply(simp add: alpha_gen.simps) |
|
208 apply(erule conjE)+ |
|
209 apply(rule conjI) |
|
210 apply(simp add: fresh_star_def fresh_minus_perm) |
|
211 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
212 apply simp |
|
213 apply(rule a) |
|
214 apply assumption |
|
215 done |
|
216 |
198 |
217 lemma alpha_sym: |
199 lemma alpha_sym: |
218 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
200 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
219 apply(induct rule: alpha.induct) |
201 apply(induct rule: alpha.induct) |
220 apply(simp add: a1) |
202 apply(simp add: a1) |
221 apply(simp add: a2) |
203 apply(simp add: a2) |
222 apply(rule a3) |
204 apply(rule a3) |
223 apply(rule alpha_gen_atom_sym) |
205 apply(erule exE) |
224 apply(rule alpha_eqvt) |
206 apply(rule_tac x="- pi" in exI) |
225 apply(assumption)+ |
207 apply(simp) |
226 done |
208 apply(simp add: fresh_star_def fresh_minus_perm) |
|
209 apply(erule conjE)+ |
|
210 apply(rotate_tac 3) |
|
211 apply(drule_tac pi="- pi" in alpha_eqvt) |
|
212 apply(simp) |
|
213 done |
227 |
214 |
228 lemma alpha_trans: |
215 lemma alpha_trans: |
229 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
216 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
230 apply(induct arbitrary: t3 rule: alpha.induct) |
217 apply(induct arbitrary: t3 rule: alpha.induct) |
231 apply(erule alpha.cases) |
218 apply(erule alpha.cases) |
236 apply(simp_all) |
223 apply(simp_all) |
237 apply(simp add: a2) |
224 apply(simp add: a2) |
238 apply(rotate_tac 1) |
225 apply(rotate_tac 1) |
239 apply(erule alpha.cases) |
226 apply(erule alpha.cases) |
240 apply(simp_all) |
227 apply(simp_all) |
241 apply(simp add: alpha_gen.simps) |
|
242 apply(erule conjE)+ |
228 apply(erule conjE)+ |
243 apply(erule exE)+ |
229 apply(erule exE)+ |
244 apply(erule conjE)+ |
230 apply(erule conjE)+ |
245 apply(rule a3) |
231 apply(rule a3) |
246 apply(rule_tac x="pia + pi" in exI) |
232 apply(rule_tac x="pia + pi" in exI) |
247 apply(simp add: alpha_gen.simps) |
|
248 apply(simp add: fresh_star_plus) |
233 apply(simp add: fresh_star_plus) |
249 apply(drule_tac x="- pia \<bullet> sa" in spec) |
234 apply(drule_tac x="- pia \<bullet> sa" in spec) |
250 apply(drule mp) |
235 apply(drule mp) |
251 apply(rotate_tac 7) |
236 apply(rotate_tac 7) |
252 apply(drule_tac pi="- pia" in alpha_eqvt) |
237 apply(drule_tac pi="- pia" in alpha_eqvt) |
264 done |
249 done |
265 |
250 |
266 lemma alpha_rfv: |
251 lemma alpha_rfv: |
267 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
252 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
268 apply(induct rule: alpha.induct) |
253 apply(induct rule: alpha.induct) |
269 apply(simp_all add: alpha_gen.simps) |
254 apply(simp_all) |
270 done |
255 done |
|
256 |
|
257 inductive |
|
258 alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
|
259 where |
|
260 a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)" |
|
261 | a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2" |
|
262 | a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s" |
|
263 |
|
264 lemma fv_vars: |
|
265 fixes a::name |
|
266 assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x" |
|
267 shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)" |
|
268 using a1 |
|
269 apply(induct t) |
|
270 apply(auto) |
|
271 apply(rule a21) |
|
272 apply(case_tac "name = a") |
|
273 apply(simp) |
|
274 apply(simp) |
|
275 defer |
|
276 apply(rule a22) |
|
277 apply(simp) |
|
278 apply(simp) |
|
279 apply(rule a23) |
|
280 apply(case_tac "a = name") |
|
281 apply(simp) |
|
282 oops |
|
283 |
|
284 |
|
285 lemma |
|
286 assumes a1: "t \<approx>2 s" |
|
287 shows "t \<approx> s" |
|
288 using a1 |
|
289 apply(induct) |
|
290 apply(rule alpha.intros) |
|
291 apply(simp) |
|
292 apply(rule alpha.intros) |
|
293 apply(simp) |
|
294 apply(simp) |
|
295 apply(rule alpha.intros) |
|
296 apply(erule disjE) |
|
297 apply(rule_tac x="0" in exI) |
|
298 apply(simp add: fresh_star_def fresh_zero_perm) |
|
299 apply(erule conjE)+ |
|
300 apply(drule alpha_rfv) |
|
301 apply(simp) |
|
302 apply(rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
303 apply(simp) |
|
304 apply(erule conjE)+ |
|
305 apply(rule conjI) |
|
306 apply(drule alpha_rfv) |
|
307 apply(drule sym) |
|
308 apply(simp) |
|
309 apply(simp add: rfv_eqvt[symmetric]) |
|
310 defer |
|
311 apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})") |
|
312 apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})") |
|
313 |
|
314 defer |
|
315 sorry |
|
316 |
|
317 lemma |
|
318 assumes a1: "t \<approx> s" |
|
319 shows "t \<approx>2 s" |
|
320 using a1 |
|
321 apply(induct) |
|
322 apply(rule alpha2.intros) |
|
323 apply(simp) |
|
324 apply(rule alpha2.intros) |
|
325 apply(simp) |
|
326 apply(simp) |
|
327 apply(clarify) |
|
328 apply(rule alpha2.intros) |
|
329 apply(frule alpha_rfv) |
|
330 apply(rotate_tac 4) |
|
331 apply(drule sym) |
|
332 apply(simp) |
|
333 apply(drule sym) |
|
334 apply(simp) |
|
335 oops |
271 |
336 |
272 quotient_type lam = rlam / alpha |
337 quotient_type lam = rlam / alpha |
273 by (rule alpha_equivp) |
338 by (rule alpha_equivp) |
274 |
339 |
275 quotient_definition |
340 quotient_definition |
311 "(op = ===> alpha ===> alpha) rLam rLam" |
376 "(op = ===> alpha ===> alpha) rLam rLam" |
312 apply(auto) |
377 apply(auto) |
313 apply(rule a3) |
378 apply(rule a3) |
314 apply(rule_tac x="0" in exI) |
379 apply(rule_tac x="0" in exI) |
315 unfolding fresh_star_def |
380 unfolding fresh_star_def |
316 apply(simp add: fresh_star_def fresh_zero_perm alpha_gen.simps) |
381 apply(simp add: fresh_star_def fresh_zero_perm) |
317 apply(simp add: alpha_rfv) |
382 apply(simp add: alpha_rfv) |
318 done |
383 done |
319 |
384 |
320 lemma rfv_rsp[quot_respect]: |
385 lemma rfv_rsp[quot_respect]: |
321 "(alpha ===> op =) rfv rfv" |
386 "(alpha ===> op =) rfv rfv" |
374 |
439 |
375 lemma a2: |
440 lemma a2: |
376 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
441 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
377 by (lifting a2) |
442 by (lifting a2) |
378 |
443 |
379 lemma alpha_gen_rsp_pre: |
444 lemma a3: |
380 assumes a5: "\<And>t s. R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s)" |
445 "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)\<rbrakk> |
381 and a1: "R s1 t1" |
446 \<Longrightarrow> Lam a t = Lam b s" |
382 and a2: "R s2 t2" |
447 apply (lifting a3) |
383 and a3: "\<And>a b c d. R a b \<Longrightarrow> R c d \<Longrightarrow> R1 a c = R2 b d" |
|
384 and a4: "\<And>x y. R x y \<Longrightarrow> fv1 x = fv2 y" |
|
385 shows "(a, s1) \<approx>gen R1 fv1 pi (b, s2) = (a, t1) \<approx>gen R2 fv2 pi (b, t2)" |
|
386 apply (simp add: alpha_gen.simps) |
|
387 apply (simp only: a4[symmetric, OF a1] a4[symmetric, OF a2]) |
|
388 apply auto |
|
389 apply (subst a3[symmetric]) |
|
390 apply (rule a5) |
|
391 apply (rule a1) |
|
392 apply (rule a2) |
|
393 apply (assumption) |
|
394 apply (subst a3) |
|
395 apply (rule a5) |
|
396 apply (rule a1) |
|
397 apply (rule a2) |
|
398 apply (assumption) |
|
399 done |
|
400 |
|
401 lemma [quot_respect]: "(prod_rel op = alpha ===> |
|
402 (alpha ===> alpha ===> op =) ===> (alpha ===> op =) ===> op = ===> prod_rel op = alpha ===> op =) |
|
403 alpha_gen alpha_gen" |
|
404 apply simp |
|
405 apply clarify |
|
406 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt]) |
|
407 apply auto |
|
408 done |
|
409 |
|
410 lemma pi_rep: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)" |
|
411 apply (unfold rep_lam_def) |
|
412 sorry |
|
413 |
|
414 lemma [quot_preserve]: "(prod_fun id rep_lam ---> |
|
415 (abs_lam ---> abs_lam ---> id) ---> (abs_lam ---> id) ---> id ---> (prod_fun id rep_lam) ---> id) |
|
416 alpha_gen = alpha_gen" |
|
417 apply (simp add: expand_fun_eq) |
|
418 apply (simp add: alpha_gen.simps) |
|
419 apply (simp add: pi_rep) |
|
420 apply (simp only: Quotient_abs_rep[OF Quotient_lam]) |
|
421 apply auto |
|
422 done |
|
423 |
|
424 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)" |
|
425 apply (simp add: expand_fun_eq) |
|
426 sledgehammer |
|
427 sorry |
|
428 |
|
429 |
|
430 lemma a3: |
|
431 "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s" |
|
432 apply (lifting a3) |
|
433 done |
448 done |
434 |
449 |
435 lemma a3_inv: |
450 lemma a3_inv: |
436 assumes "Lam a t = Lam b s" |
451 assumes "Lam a t = Lam b s" |
437 shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)" |
452 shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)" |