475 by (rule itfun_Lam_aux2[OF f, OF c]) |
475 by (rule itfun_Lam_aux2[OF f, OF c]) |
476 also have "\<dots> = f3 b (itfun f1 f2 f3 t)" by (simp add: pt_swap_bij'[OF pt_name_inst, OF at_name_inst]) |
476 also have "\<dots> = f3 b (itfun f1 f2 f3 t)" by (simp add: pt_swap_bij'[OF pt_name_inst, OF at_name_inst]) |
477 finally show ?thesis by simp |
477 finally show ?thesis by simp |
478 qed |
478 qed |
479 |
479 |
480 constdefs |
|
481 depth_Var :: "name \<Rightarrow> nat" |
|
482 "depth_Var \<equiv> \<lambda>(a::name). 1" |
|
483 |
|
484 depth_App :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
485 "depth_App \<equiv> \<lambda>n1 n2. (max n1 n2)+1" |
|
486 |
|
487 depth_Lam :: "name \<Rightarrow> nat \<Rightarrow> nat" |
|
488 "depth_Lam \<equiv> \<lambda>(a::name) n. n+1" |
|
489 |
|
490 depth_lam :: "lam \<Rightarrow> nat" |
|
491 "depth_lam \<equiv> itfun depth_Var depth_App depth_Lam" |
|
492 |
|
493 lemma supp_depth_Var: |
|
494 shows "((supp depth_Var)::name set)={}" |
|
495 apply(simp add: depth_Var_def) |
|
496 apply(simp add: supp_def) |
|
497 apply(simp add: perm_fun_def) |
|
498 apply(simp add: perm_nat_def) |
|
499 done |
|
500 |
|
501 lemma supp_depth_App: |
|
502 shows "((supp depth_App)::name set)={}" |
|
503 apply(simp add: depth_App_def) |
|
504 apply(simp add: supp_def) |
|
505 apply(simp add: perm_fun_def) |
|
506 apply(simp add: perm_nat_def) |
|
507 done |
|
508 |
|
509 lemma supp_depth_Lam: |
|
510 shows "((supp depth_Lam)::name set)={}" |
|
511 apply(simp add: depth_Lam_def) |
|
512 apply(simp add: supp_def) |
|
513 apply(simp add: perm_fun_def) |
|
514 apply(simp add: perm_nat_def) |
|
515 done |
|
516 |
|
517 |
|
518 lemma fin_supp_depth: |
|
519 shows "finite ((supp (depth_Var,depth_App,depth_Lam))::name set)" |
|
520 (* FIXME: apply(finite_guess_debug add: perm_nat_def) doe note work -- something |
|
521 funny with the finite_guess tactic *) |
|
522 using supp_depth_Var supp_depth_Lam supp_depth_App |
|
523 by (simp add: supp_prod) |
|
524 |
|
525 lemma fresh_depth_Lam: |
|
526 shows "\<exists>(a::name). a\<sharp>depth_Lam \<and> (\<forall>n. a\<sharp>depth_Lam a n)" |
|
527 apply(rule exI) |
|
528 apply(rule conjI) |
|
529 apply(simp add: fresh_def) |
|
530 apply(force simp add: supp_depth_Lam) |
|
531 apply(unfold fresh_def) |
|
532 apply(simp add: supp_def) |
|
533 apply(simp add: perm_nat_def) |
|
534 done |
|
535 |
|
536 lemma depth_Var: |
|
537 shows "depth_lam (Var c) = 1" |
|
538 apply(simp add: depth_lam_def) |
|
539 apply(simp add: itfun_Var[OF fin_supp_depth, OF fresh_depth_Lam]) |
|
540 apply(simp add: depth_Var_def) |
|
541 done |
|
542 |
|
543 lemma depth_App: |
|
544 shows "depth_lam (App t1 t2) = (max (depth_lam t1) (depth_lam t2))+1" |
|
545 apply(simp add: depth_lam_def) |
|
546 apply(simp add: itfun_App[OF fin_supp_depth, OF fresh_depth_Lam]) |
|
547 apply(simp add: depth_App_def) |
|
548 done |
|
549 |
|
550 lemma depth_Lam: |
|
551 shows "depth_lam (Lam [a].t) = (depth_lam t)+1" |
|
552 apply(simp add: depth_lam_def) |
|
553 apply(rule trans) |
|
554 apply(rule itfun_Lam[OF fin_supp_depth, OF fresh_depth_Lam]) |
|
555 apply(simp add: fresh_def supp_prod supp_depth_Var supp_depth_App supp_depth_Lam) |
|
556 apply(simp add: depth_Lam_def) |
|
557 done |
|
558 |
|
559 text {* substitution *} |
|
560 constdefs |
|
561 subst_Var :: "name \<Rightarrow>lam \<Rightarrow> name \<Rightarrow> lam" |
|
562 "subst_Var b t \<equiv> \<lambda>a. (if a=b then t else (Var a))" |
|
563 |
|
564 subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
565 "subst_App b t \<equiv> \<lambda>r1 r2. App r1 r2" |
|
566 |
|
567 subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" |
|
568 "subst_Lam b t \<equiv> \<lambda>a r. Lam [a].r" |
|
569 |
|
570 subst_lam :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
571 "subst_lam b t \<equiv> itfun (subst_Var b t) (subst_App b t) (subst_Lam b t)" |
|
572 |
|
573 lemma supports_subst_Var: |
|
574 shows "((supp (b,t))::name set) supports (subst_Var b t)" |
|
575 apply(supports_simp add: subst_Var_def) |
|
576 apply(rule impI) |
|
577 apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) |
|
578 apply(simp add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]) |
|
579 done |
|
580 |
|
581 lemma supports_subst_App: |
|
582 shows "((supp (b,t))::name set) supports subst_App b t" |
|
583 by (supports_simp add: subst_App_def) |
|
584 |
|
585 lemma supports_subst_Lam: |
|
586 shows "((supp (b,t))::name set) supports subst_Lam b t" |
|
587 by (supports_simp add: subst_Lam_def) |
|
588 |
|
589 lemma fin_supp_subst: |
|
590 shows "finite ((supp (subst_Var b t,subst_App b t,subst_Lam b t))::name set)" |
|
591 apply(auto simp add: supp_prod) |
|
592 apply(rule supports_finite) |
|
593 apply(rule supports_subst_Var) |
|
594 apply(simp add: fs_name1) |
|
595 apply(rule supports_finite) |
|
596 apply(rule supports_subst_App) |
|
597 apply(simp add: fs_name1) |
|
598 apply(rule supports_finite) |
|
599 apply(rule supports_subst_Lam) |
|
600 apply(simp add: fs_name1) |
|
601 done |
|
602 |
|
603 lemma fresh_subst_Lam: |
|
604 shows "\<exists>(a::name). a\<sharp>(subst_Lam b t)\<and> (\<forall>y. a\<sharp>(subst_Lam b t) a y)" |
|
605 apply(subgoal_tac "\<exists>(c::name). c\<sharp>(b,t)") |
|
606 apply(auto) |
|
607 apply(rule_tac x="c" in exI) |
|
608 apply(auto) |
|
609 apply(rule supports_fresh) |
|
610 apply(rule supports_subst_Lam) |
|
611 apply(simp_all add: fresh_def[symmetric] fs_name1) |
|
612 apply(simp add: subst_Lam_def) |
|
613 apply(simp add: abs_fresh) |
|
614 apply(rule at_exists_fresh[OF at_name_inst]) |
|
615 apply(simp add: fs_name1) |
|
616 done |
|
617 |
|
618 lemma subst_Var: |
|
619 shows "subst_lam b t (Var a) = (if a=b then t else (Var a))" |
|
620 apply(simp add: subst_lam_def) |
|
621 apply(auto simp add: itfun_Var[OF fin_supp_subst, OF fresh_subst_Lam]) |
|
622 apply(auto simp add: subst_Var_def) |
|
623 done |
|
624 |
|
625 lemma subst_App: |
|
626 shows "subst_lam b t (App t1 t2) = App (subst_lam b t t1) (subst_lam b t t2)" |
|
627 apply(simp add: subst_lam_def) |
|
628 apply(auto simp add: itfun_App[OF fin_supp_subst, OF fresh_subst_Lam]) |
|
629 apply(auto simp add: subst_App_def) |
|
630 done |
|
631 |
|
632 lemma subst_Lam: |
|
633 assumes a: "a\<sharp>(b,t)" |
|
634 shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)" |
|
635 using a |
|
636 apply(simp add: subst_lam_def) |
|
637 apply(subgoal_tac "a\<sharp>(subst_Var b t,subst_App b t,subst_Lam b t)") |
|
638 apply(auto simp add: itfun_Lam[OF fin_supp_subst, OF fresh_subst_Lam]) |
|
639 apply(simp (no_asm) add: subst_Lam_def) |
|
640 apply(auto simp add: fresh_prod) |
|
641 apply(rule supports_fresh) |
|
642 apply(rule supports_subst_Var) |
|
643 apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod) |
|
644 apply(rule supports_fresh) |
|
645 apply(rule supports_subst_App) |
|
646 apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod) |
|
647 apply(rule supports_fresh) |
|
648 apply(rule supports_subst_Lam) |
|
649 apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod) |
|
650 done |
|
651 |
|
652 lemma subst_Lam': |
|
653 assumes a: "a\<noteq>b" |
|
654 and b: "a\<sharp>t" |
|
655 shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)" |
|
656 by (simp add: subst_Lam fresh_prod a b fresh_atm) |
|
657 |
|
658 lemma subst_Lam'': |
|
659 assumes a: "a\<sharp>b" |
|
660 and b: "a\<sharp>t" |
|
661 shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)" |
|
662 by (simp add: subst_Lam fresh_prod a b) |
|
663 |
|
664 consts |
|
665 subst_syn :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900) |
|
666 translations |
|
667 "t1[a::=t2]" \<rightleftharpoons> "subst_lam a t2 t1" |
|
668 |
|
669 declare subst_Var[simp] |
|
670 declare subst_App[simp] |
|
671 declare subst_Lam[simp] |
|
672 declare subst_Lam'[simp] |
|
673 declare subst_Lam''[simp] |
|
674 |
|
675 lemma subst_eqvt[simp]: |
|
676 fixes pi:: "name prm" |
|
677 and t1:: "lam" |
|
678 and t2:: "lam" |
|
679 and a :: "name" |
|
680 shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]" |
|
681 apply(nominal_induct t1 avoiding: b t2 rule: lam.induct) |
|
682 apply(auto simp add: perm_bij fresh_prod fresh_atm) |
|
683 apply(subgoal_tac "(pi\<bullet>name)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*) |
|
684 apply(simp) |
|
685 (*A*) |
|
686 apply(simp add: pt_fresh_right[OF pt_name_inst, OF at_name_inst], perm_simp add: fresh_prod fresh_atm) |
|
687 done |
|
688 |
|
689 lemma subst_supp: |
|
690 shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)" |
|
691 apply(nominal_induct t1 avoiding: a t2 rule: lam.induct) |
|
692 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp) |
|
693 apply(blast)+ |
|
694 done |
|
695 |
|
696 end |
480 end |