470 |
470 |
471 (* |
471 (* |
472 nominal_inductive typing |
472 nominal_inductive typing |
473 *) |
473 *) |
474 |
474 |
|
475 (* Substitution *) |
|
476 |
|
477 definition new where |
|
478 "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)" |
|
479 |
|
480 primrec match_Var_raw where |
|
481 "match_Var_raw (Var_raw x) = Some x" |
|
482 | "match_Var_raw (App_raw x y) = None" |
|
483 | "match_Var_raw (Lam_raw n t) = None" |
|
484 |
|
485 quotient_definition |
|
486 "match_Var :: lam \<Rightarrow> name option" |
|
487 is match_Var_raw |
|
488 |
|
489 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
|
490 apply rule |
|
491 apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
492 apply simp_all |
|
493 done |
|
494 |
|
495 lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
|
496 |
|
497 primrec match_App_raw where |
|
498 "match_App_raw (Var_raw x) = None" |
|
499 | "match_App_raw (App_raw x y) = Some (x, y)" |
|
500 | "match_App_raw (Lam_raw n t) = None" |
|
501 |
|
502 quotient_definition |
|
503 "match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
|
504 is match_App_raw |
|
505 |
|
506 lemma [quot_respect]: |
|
507 "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw" |
|
508 apply (intro fun_relI) |
|
509 apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
510 apply simp_all |
|
511 done |
|
512 |
|
513 lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
|
514 |
|
515 primrec match_Lam_raw where |
|
516 "match_Lam_raw (S :: atom set) (Var_raw x) = None" |
|
517 | "match_Lam_raw S (App_raw x y) = None" |
|
518 | "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))" |
|
519 |
|
520 quotient_definition |
|
521 "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option" |
|
522 is match_Lam_raw |
|
523 |
|
524 lemma [quot_respect]: |
|
525 "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw" |
|
526 proof (intro fun_relI, clarify) |
|
527 fix S t s |
|
528 assume a: "alpha_lam_raw t s" |
|
529 show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)" |
|
530 using a proof (induct t s rule: alpha_lam_raw.induct) |
|
531 case goal1 show ?case by simp |
|
532 next |
|
533 case goal2 show ?case by simp |
|
534 next |
|
535 case (goal3 x t y s) |
|
536 then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and> |
|
537 option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1) |
|
538 (match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" .. |
|
539 then have |
|
540 c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and |
|
541 d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and |
|
542 e: "alpha_lam_raw (p \<bullet> t) s" and |
|
543 f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and |
|
544 g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+ |
|
545 let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))" |
|
546 have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp |
|
547 show ?case |
|
548 unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv |
|
549 proof |
|
550 show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h) |
|
551 next |
|
552 have "atom y \<sharp> p" sorry |
|
553 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 |
|
555 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 |
|
557 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) |
|
559 ((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h . |
|
560 qed |
|
561 qed |
|
562 qed |
|
563 |
|
564 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
|
565 |
|
566 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
|
567 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
|
568 |
|
569 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
|
570 apply (induct x rule: lam.induct) |
|
571 apply (simp_all add: match_Lam_simps) |
|
572 apply (simp add: Let_def) |
|
573 apply (erule conjE) |
|
574 apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S") |
|
575 apply (rule conjI) |
|
576 apply (simp add: lam.eq_iff) |
|
577 apply (rule_tac x="(name \<leftrightarrow> z)" in exI) |
|
578 apply (simp add: alphas) |
|
579 apply (simp add: eqvts) |
|
580 apply (simp only: lam.fv(3)[symmetric]) |
|
581 apply (subgoal_tac "Lam name lam = Lam z s") |
|
582 apply (simp del: lam.fv) |
|
583 prefer 3 |
|
584 apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s") |
|
585 apply (simp only: new_def) |
|
586 apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a") |
|
587 apply (simp only: fresh_def) |
|
588 |
|
589 thm new_def |
|
590 apply simp |
|
591 |
|
592 |
|
593 function subst where |
|
594 "subst v s t = ( |
|
595 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> |
|
597 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 |
|
599 |
|
600 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
|
601 apply auto[1] |
|
602 defer |
|
603 apply (case_tac a) apply simp |
|
604 apply (frule app_some) apply simp |
|
605 apply (case_tac a) apply simp |
|
606 apply (frule app_some) apply simp |
|
607 apply (case_tac a) apply simp |
|
608 apply (frule lam_some) |
|
609 apply simp |
|
610 done |
|
611 |
|
612 lemmas lam_exhaust = lam_raw.exhaust[quot_lifted] |
|
613 |
|
614 lemma subst_eqvt: |
|
615 "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" |
|
616 proof (induct v s t rule: subst.induct) |
|
617 case (1 v s t) |
|
618 show ?case proof (cases t rule: lam_exhaust) |
|
619 fix n |
|
620 assume "t = Var n" |
|
621 then show ?thesis by (simp add: match_Var_simps) |
|
622 next |
|
623 fix l r |
|
624 assume "t = App l r" |
|
625 then show ?thesis |
|
626 apply (simp only:) |
|
627 apply (subst subst.simps) |
|
628 apply (subst match_Var_simps) |
|
629 apply (simp only: option.cases) |
|
630 apply (subst match_App_simps) |
|
631 apply (simp only: option.cases) |
|
632 apply (simp only: prod.cases) |
|
633 apply (simp only: lam.perm) |
|
634 apply (subst (3) subst.simps) |
|
635 apply (subst match_Var_simps) |
|
636 apply (simp only: option.cases) |
|
637 apply (subst match_App_simps) |
|
638 apply (simp only: option.cases) |
|
639 apply (simp only: prod.cases) |
|
640 apply (subst 1(2)[of "(l, r)" "l" "r"]) |
|
641 apply (simp add: match_Var_simps) |
|
642 apply (simp add: match_App_simps) |
|
643 apply (rule refl) |
|
644 apply (subst 1(3)[of "(l, r)" "l" "r"]) |
|
645 apply (simp add: match_Var_simps) |
|
646 apply (simp add: match_App_simps) |
|
647 apply (rule refl) |
|
648 apply (rule refl) |
|
649 done |
|
650 next |
|
651 fix n t' |
|
652 assume "t = Lam n t'" |
|
653 then show ?thesis |
|
654 apply (simp only: ) |
|
655 apply (simp only: lam.perm) |
|
656 apply (subst subst.simps) |
|
657 apply (subst match_Var_simps) |
|
658 apply (simp only: option.cases) |
|
659 apply (subst match_App_simps) |
|
660 apply (simp only: option.cases) |
|
661 apply (subst match_Lam_simps) |
|
662 apply (simp only: Let_def) |
|
663 apply (simp only: option.cases) |
|
664 apply (simp only: prod.cases) |
|
665 apply (subst (2) subst.simps) |
|
666 apply (subst match_Var_simps) |
|
667 apply (simp only: option.cases) |
|
668 apply (subst match_App_simps) |
|
669 apply (simp only: option.cases) |
|
670 apply (subst match_Lam_simps) |
|
671 apply (simp only: Let_def) |
|
672 apply (simp only: option.cases) |
|
673 apply (simp only: prod.cases) |
|
674 apply (simp only: lam.perm) |
|
675 apply (simp only: lam.eq_iff) |
|
676 sorry |
|
677 qed |
|
678 qed |
|
679 |
|
680 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
|
681 by (induct t) simp_all |
|
682 |
|
683 function |
|
684 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
|
685 where |
|
686 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
|
687 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
|
688 | "subst_raw (Lam_raw x t) y s = |
|
689 Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x})) |
|
690 (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))) \<bullet> t) y s)" |
|
691 by (pat_completeness, auto) |
|
692 termination |
|
693 apply (relation "measure (\<lambda>(t, y, s). (size t))") |
|
694 apply (auto simp add: size_no_change) |
|
695 done |
|
696 |
|
697 lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) = |
|
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)" |
|
699 apply (induct t arbitrary: s) |
|
700 apply (auto simp add: supp_at_base)[1] |
|
701 apply (auto simp add: supp_at_base)[1] |
|
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 |
|
745 |
|
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] |
475 |
790 |
476 end |
791 end |
477 |
792 |
478 |
793 |
479 |
794 |