519 |
519 |
520 quotient_definition |
520 quotient_definition |
521 "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option" |
521 "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option" |
522 is match_Lam_raw |
522 is match_Lam_raw |
523 |
523 |
|
524 lemma swap_fresh: |
|
525 assumes a: "fv_lam_raw t \<sharp>* p" |
|
526 shows "alpha_lam_raw (p \<bullet> t) t" |
|
527 using a apply (induct t) |
|
528 apply (simp add: supp_at_base fresh_star_def) |
|
529 apply (rule alpha_lam_raw.intros) |
|
530 apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm) |
|
531 apply (simp) |
|
532 apply (simp only: fresh_star_union) |
|
533 apply clarify |
|
534 apply (rule alpha_lam_raw.intros) |
|
535 apply simp |
|
536 apply simp |
|
537 apply simp |
|
538 apply (rule alpha_lam_raw.intros) |
|
539 sorry |
|
540 |
524 lemma [quot_respect]: |
541 lemma [quot_respect]: |
525 "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw" |
542 "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw" |
526 proof (intro fun_relI, clarify) |
543 proof (intro fun_relI, clarify) |
527 fix S t s |
544 fix S t s |
528 assume a: "alpha_lam_raw t s" |
545 assume a: "alpha_lam_raw t s" |
549 proof |
566 proof |
550 show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h) |
567 show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h) |
551 next |
568 next |
552 have "atom y \<sharp> p" sorry |
569 have "atom y \<sharp> p" sorry |
553 have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry |
570 have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry |
554 then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" sorry |
571 then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto |
555 have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry |
572 then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry |
556 have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry |
573 have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry |
557 then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry |
574 then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry |
558 then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t) |
575 then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t) |
559 ((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h . |
576 ((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h . |
560 qed |
577 qed |
583 prefer 3 |
600 prefer 3 |
584 apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s") |
601 apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s") |
585 apply (simp only: new_def) |
602 apply (simp only: new_def) |
586 apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a") |
603 apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a") |
587 apply (simp only: fresh_def) |
604 apply (simp only: fresh_def) |
588 |
605 (*thm supp_finite_atom_fset*) |
589 thm new_def |
606 sorry |
590 apply simp |
|
591 |
|
592 |
607 |
593 function subst where |
608 function subst where |
594 "subst v s t = ( |
609 "subst v s t = ( |
595 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
610 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
596 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
611 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
597 case match_Lam (supp (v,s)) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
612 case match_Lam (supp (v,s)) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
598 by pat_completeness auto |
613 by pat_completeness auto |
599 |
614 |
600 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
615 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
601 apply auto[1] |
616 apply auto[1] |
602 defer |
617 apply (case_tac a) apply simp |
603 apply (case_tac a) apply simp |
618 apply (frule lam_some) apply simp |
604 apply (frule app_some) apply simp |
619 apply (case_tac a) apply simp |
605 apply (case_tac a) apply simp |
620 apply (frule app_some) apply simp |
606 apply (frule app_some) apply simp |
621 apply (case_tac a) apply simp |
607 apply (case_tac a) apply simp |
622 apply (frule app_some) apply simp |
608 apply (frule lam_some) |
|
609 apply simp |
|
610 done |
623 done |
611 |
624 |
612 lemmas lam_exhaust = lam_raw.exhaust[quot_lifted] |
625 lemmas lam_exhaust = lam_raw.exhaust[quot_lifted] |
613 |
626 |
614 lemma subst_eqvt: |
627 lemma subst_eqvt: |
675 apply (simp only: lam.eq_iff) |
688 apply (simp only: lam.eq_iff) |
676 sorry |
689 sorry |
677 qed |
690 qed |
678 qed |
691 qed |
679 |
692 |
680 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
693 |
681 by (induct t) simp_all |
694 lemma subst_proper_eqs: |
682 |
695 "subst y s (Var x) = (if x = y then s else (Var x))" |
683 function |
696 "subst y s (App l r) = App (subst y s l) (subst y s r)" |
684 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
697 "atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" |
685 where |
698 apply (subst subst.simps) |
686 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
699 apply (simp only: match_Var_simps) |
687 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
700 apply (simp only: option.simps) |
688 | "subst_raw (Lam_raw x t) y s = |
701 apply (subst subst.simps) |
689 Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x})) |
702 apply (simp only: match_App_simps) |
690 (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))) \<bullet> t) y s)" |
703 apply (simp only: option.simps) |
691 by (pat_completeness, auto) |
704 apply (simp only: prod.simps) |
692 termination |
705 apply (simp only: match_Var_simps) |
693 apply (relation "measure (\<lambda>(t, y, s). (size t))") |
706 apply (simp only: option.simps) |
694 apply (auto simp add: size_no_change) |
707 apply (subst subst.simps) |
695 done |
708 apply (simp only: match_Lam_simps) |
696 |
709 apply (simp only: match_Var_simps) |
697 lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) = |
710 apply (simp only: match_App_simps) |
698 (if (atom y \<in> fv_lam_raw t) then fv_lam_raw s \<union> (fv_lam_raw t - {atom y}) else fv_lam_raw t)" |
711 apply (simp only: option.simps) |
699 apply (induct t arbitrary: s) |
712 apply (simp only: Let_def) |
700 apply (auto simp add: supp_at_base)[1] |
713 apply (simp only: option.simps) |
701 apply (auto simp add: supp_at_base)[1] |
714 apply (simp only: prod.simps) |
702 apply (simp only: fv_lam_raw.simps) |
|
703 apply simp |
|
704 apply (rule conjI) |
|
705 apply clarify |
|
706 oops |
|
707 |
|
708 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
|
709 oops |
|
710 |
|
711 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)" |
|
712 apply (induct t arbitrary: p y s) |
|
713 apply simp_all |
|
714 apply(perm_simp) |
|
715 oops |
|
716 |
|
717 lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x" |
|
718 apply (induct x arbitrary: d) |
|
719 apply (simp_all add: alpha_lam_raw.intros) |
|
720 apply (rule alpha_lam_raw.intros) |
|
721 apply (rule_tac x="(name \<leftrightarrow> new (insert (atom d) (supp d)))" in exI) |
|
722 apply (simp add: alphas) |
|
723 oops |
|
724 |
|
725 quotient_definition |
|
726 subst2 ("_ [ _ ::= _ ]" [100,100,100] 100) |
|
727 where |
|
728 "subst2 :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw" |
|
729 |
|
730 lemmas fv_rsp = quot_respect(10)[simplified] |
|
731 |
|
732 lemma subst_rsp_pre1: |
|
733 assumes a: "alpha_lam_raw a b" |
|
734 shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" |
|
735 using a |
|
736 apply (induct a b arbitrary: c y rule: alpha_lam_raw.induct) |
|
737 apply (simp add: equivp_reflp[OF lam_equivp]) |
|
738 apply (simp add: alpha_lam_raw.intros) |
|
739 apply (simp only: alphas) |
|
740 apply clarify |
|
741 apply (simp only: subst_raw.simps) |
|
742 apply (rule alpha_lam_raw.intros) |
|
743 apply (simp only: alphas) |
|
744 sorry |
715 sorry |
745 |
716 |
746 lemma subst_rsp_pre2: |
|
747 assumes a: "alpha_lam_raw a b" |
|
748 shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)" |
|
749 using a |
|
750 apply (induct c arbitrary: a b y) |
|
751 apply (simp add: equivp_reflp[OF lam_equivp]) |
|
752 apply (simp add: alpha_lam_raw.intros) |
|
753 apply simp |
|
754 apply (rule alpha_lam_raw.intros) |
|
755 apply (rule_tac x="((new (insert (atom y) (fv_lam_raw a \<union> fv_lam_raw c) - |
|
756 {atom name}))\<leftrightarrow>(new (insert (atom y) (fv_lam_raw b \<union> fv_lam_raw c) - |
|
757 {atom name})))" in exI) |
|
758 apply (simp only: alphas) |
|
759 apply (tactic {* split_conj_tac 1 *}) |
|
760 prefer 3 |
|
761 sorry |
|
762 |
|
763 lemma [quot_respect]: |
|
764 "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" |
|
765 proof (intro fun_relI, simp) |
|
766 fix a b c d :: lam_raw |
|
767 fix y :: name |
|
768 assume a: "alpha_lam_raw a b" |
|
769 assume b: "alpha_lam_raw c d" |
|
770 have c: "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" using subst_rsp_pre1 a by simp |
|
771 then have d: "alpha_lam_raw (subst_raw b y c) (subst_raw b y d)" using subst_rsp_pre2 b by simp |
|
772 show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)" |
|
773 using c d equivp_transp[OF lam_equivp] by blast |
|
774 qed |
|
775 |
|
776 lemma simp3: |
|
777 "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> alpha_lam_raw (subst_raw (Lam_raw x t) y s) (Lam_raw x (subst_raw t y s))" |
|
778 apply simp |
|
779 apply (rule alpha_lam_raw.intros) |
|
780 apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) - |
|
781 {atom x})))" in exI) |
|
782 apply (simp only: alphas) |
|
783 sorry |
|
784 |
|
785 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] |
|
786 simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars] |
|
787 |
|
788 |
|
789 thm subst_raw.simps(3)[quot_lifted,no_vars] |
|
790 |
|
791 end |
717 end |
792 |
718 |
793 |
719 |
794 |
720 |