405 apply clarify |
405 apply clarify |
406 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt]) |
406 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt]) |
407 apply auto |
407 apply auto |
408 done |
408 done |
409 |
409 |
410 lemma pi_rep: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)" |
410 (* pi_abs would be also sufficient to prove the next lemma *) |
|
411 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)" |
411 apply (unfold rep_lam_def) |
412 apply (unfold rep_lam_def) |
412 sorry |
413 sorry |
413 |
414 |
414 lemma [quot_preserve]: "(prod_fun id rep_lam ---> |
415 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 (abs_lam ---> abs_lam ---> id) ---> (abs_lam ---> id) ---> id ---> (prod_fun id rep_lam) ---> id) |
416 alpha_gen = alpha_gen" |
417 alpha_gen = alpha_gen" |
417 apply (simp add: expand_fun_eq) |
418 apply (simp add: expand_fun_eq) |
418 apply (simp add: alpha_gen.simps) |
419 apply (simp add: alpha_gen.simps) |
419 apply (simp add: pi_rep) |
420 apply (simp add: replam_eqvt) |
420 apply (simp only: Quotient_abs_rep[OF Quotient_lam]) |
421 apply (simp only: Quotient_abs_rep[OF Quotient_lam]) |
421 apply auto |
422 apply auto |
422 done |
423 done |
423 |
424 |
424 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)" |
425 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)" |
425 apply (simp add: expand_fun_eq) |
426 apply (simp add: expand_fun_eq) |
426 sorry |
427 apply (simp add: Quotient_rel_rep[OF Quotient_lam]) |
427 |
428 done |
428 |
429 |
429 lemma a3: |
430 lemma a3: |
430 "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s" |
431 "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s" |
431 apply (lifting a3) |
432 apply (lifting a3) |
432 done |
433 done |
433 |
434 |
|
435 |
434 lemma a3_inv: |
436 lemma a3_inv: |
435 assumes "Lam a t = Lam b s" |
437 "Lam a t = Lam b s \<Longrightarrow> \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)" |
436 shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)" |
|
437 using assms |
|
438 apply(lifting a3_inverse) |
438 apply(lifting a3_inverse) |
439 done |
439 done |
440 |
440 |
441 lemma alpha_cases: |
441 lemma alpha_cases: |
442 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
442 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
443 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
443 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
444 \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
444 \<And>a t b s. \<lbrakk>a1 = Lam a t; a2 = Lam b s; \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)\<rbrakk> |
445 \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s\<rbrakk> |
|
446 \<Longrightarrow> P\<rbrakk> |
445 \<Longrightarrow> P\<rbrakk> |
447 \<Longrightarrow> P" |
446 \<Longrightarrow> P" |
448 by (lifting alpha.cases) |
447 by (lifting alpha.cases) |
|
448 |
|
449 thm alpha.induct |
449 |
450 |
450 (* not sure whether needed *) |
451 (* not sure whether needed *) |
451 lemma alpha_induct: |
452 lemma alpha_induct: |
452 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
453 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
453 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
454 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
454 \<And>t a s b. |
455 \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
455 \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> |
|
456 (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s)\<rbrakk> |
|
457 \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
|
458 \<Longrightarrow> qxb qx qxa" |
456 \<Longrightarrow> qxb qx qxa" |
459 by (lifting alpha.induct) |
457 by (lifting alpha.induct) |
460 |
458 |
461 (* should they lift automatically *) |
459 (* should they lift automatically *) |
462 lemma lam_inject [simp]: |
460 lemma lam_inject [simp]: |
566 lemma supp_fv: |
564 lemma supp_fv: |
567 shows "supp t = fv t" |
565 shows "supp t = fv t" |
568 apply(induct t rule: lam_induct) |
566 apply(induct t rule: lam_induct) |
569 apply(simp add: var_supp) |
567 apply(simp add: var_supp) |
570 apply(simp add: app_supp) |
568 apply(simp add: app_supp) |
571 apply(subgoal_tac "supp (Lam name lam) = supp (Abst {atom name} lam)") |
569 apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)") |
572 apply(simp add: supp_Abst) |
570 apply(simp add: supp_Abs) |
573 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
571 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
574 apply(simp add: Lam_pseudo_inject) |
572 apply(simp add: Lam_pseudo_inject) |
575 apply(simp add: abs_eq alpha_gen) |
573 apply(simp add: Abs_eq_iff) |
|
574 apply(simp add: alpha_gen.simps) |
576 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
575 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
577 done |
576 done |
578 |
577 |
579 lemma lam_supp2: |
578 lemma lam_supp2: |
580 shows "supp (Lam x t) = supp (Abst {atom x} t)" |
579 shows "supp (Lam x t) = supp (Abs {atom x} t)" |
581 apply(simp add: supp_def permute_set_eq atom_eqvt) |
580 apply(simp add: supp_def permute_set_eq atom_eqvt) |
582 apply(simp add: Lam_pseudo_inject) |
581 apply(simp add: Lam_pseudo_inject) |
583 apply(simp add: abs_eq supp_fv alpha_gen) |
582 apply(simp add: Abs_eq_iff) |
|
583 apply(simp add: alpha_gen supp_fv) |
584 done |
584 done |
585 |
585 |
586 lemma lam_supp: |
586 lemma lam_supp: |
587 shows "supp (Lam x t) = ((supp t) - {atom x})" |
587 shows "supp (Lam x t) = ((supp t) - {atom x})" |
588 apply(simp add: lam_supp2) |
588 apply(simp add: lam_supp2) |
589 apply(simp add: supp_Abst) |
589 apply(simp add: supp_Abs) |
590 done |
590 done |
591 |
591 |
592 lemma fresh_lam: |
592 lemma fresh_lam: |
593 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
593 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
594 apply(simp add: fresh_def) |
594 apply(simp add: fresh_def) |