472 nominal_inductive typing |
472 nominal_inductive typing |
473 *) |
473 *) |
474 |
474 |
475 (* Substitution *) |
475 (* Substitution *) |
476 |
476 |
|
477 primrec match_Var_raw where |
|
478 "match_Var_raw (Var_raw x) = Some x" |
|
479 | "match_Var_raw (App_raw x y) = None" |
|
480 | "match_Var_raw (Lam_raw n t) = None" |
|
481 |
|
482 quotient_definition |
|
483 "match_Var :: lam \<Rightarrow> name option" |
|
484 is match_Var_raw |
|
485 |
|
486 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
|
487 apply rule |
|
488 apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
489 apply simp_all |
|
490 done |
|
491 |
|
492 lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
|
493 |
|
494 primrec match_App_raw where |
|
495 "match_App_raw (Var_raw x) = None" |
|
496 | "match_App_raw (App_raw x y) = Some (x, y)" |
|
497 | "match_App_raw (Lam_raw n t) = None" |
|
498 |
|
499 quotient_definition |
|
500 "match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
|
501 is match_App_raw |
|
502 |
|
503 lemma [quot_respect]: |
|
504 "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw" |
|
505 apply (intro fun_relI) |
|
506 apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
507 apply simp_all |
|
508 done |
|
509 |
|
510 lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
|
511 |
477 definition new where |
512 definition new where |
478 "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)" |
513 "new (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)" |
479 |
514 |
480 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
515 definition |
481 by (induct t) simp_all |
516 "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then |
482 |
517 (let z = new (S, t) in Some (z, THE s. t = Lam z s)) else None)" |
483 function |
518 |
484 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
519 lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)" |
485 where |
520 apply auto |
486 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
521 apply (simp only: lam.eq_iff alphas) |
487 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
522 apply clarify |
488 | "subst_raw (Lam_raw x t) y s = |
523 apply (simp add: eqvts) |
489 Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x})) |
524 sorry |
490 (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))) \<bullet> t) y s)" |
525 |
491 by (pat_completeness, auto) |
526 lemma match_Lam_simps: |
492 termination |
527 "match_Lam S (Var n) = None" |
493 apply (relation "measure (\<lambda>(t, y, s). (size t))") |
528 "match_Lam S (App l r) = None" |
494 apply (auto simp add: size_no_change) |
529 "z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)" |
|
530 apply (simp_all add: match_Lam_def) |
|
531 apply (simp add: lam_half_inj) |
|
532 apply auto |
495 done |
533 done |
496 |
534 |
497 lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) = |
535 (* |
498 (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)" |
536 lemma match_Lam_simps2: |
499 apply (induct t arbitrary: s) |
537 "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)" |
500 apply (auto simp add: supp_at_base)[1] |
538 apply (rule_tac t="Lam n s" |
501 apply (auto simp add: supp_at_base)[1] |
539 and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst) |
502 apply (simp only: fv_lam_raw.simps) |
540 defer |
|
541 apply (subst match_Lam_simps(3)) |
|
542 defer |
503 apply simp |
543 apply simp |
504 apply (rule conjI) |
544 *) |
|
545 |
|
546 (*primrec match_Lam_raw where |
|
547 "match_Lam_raw (S :: atom set) (Var_raw x) = None" |
|
548 | "match_Lam_raw S (App_raw x y) = None" |
|
549 | "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))" |
|
550 |
|
551 quotient_definition |
|
552 "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option" |
|
553 is match_Lam_raw |
|
554 |
|
555 lemma swap_fresh: |
|
556 assumes a: "fv_lam_raw t \<sharp>* p" |
|
557 shows "alpha_lam_raw (p \<bullet> t) t" |
|
558 using a apply (induct t) |
|
559 apply (simp add: supp_at_base fresh_star_def) |
|
560 apply (rule alpha_lam_raw.intros) |
|
561 apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm) |
|
562 apply (simp) |
|
563 apply (simp only: fresh_star_union) |
505 apply clarify |
564 apply clarify |
506 sorry |
565 apply (rule alpha_lam_raw.intros) |
507 |
|
508 thm supp_at_base |
|
509 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
|
510 sorry |
|
511 |
|
512 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)" |
|
513 apply (induct t arbitrary: p y s) |
|
514 apply simp_all |
|
515 apply(perm_simp) |
|
516 apply simp |
566 apply simp |
517 sorry |
567 apply simp |
518 |
|
519 lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x" |
|
520 apply (induct x arbitrary: d) |
|
521 apply (simp_all add: alpha_lam_raw.intros) |
|
522 apply (rule alpha_lam_raw.intros) |
|
523 apply (rule_tac x="(name \<leftrightarrow> new (insert (atom d) (supp d)))" in exI) |
|
524 apply (simp add: alphas) |
|
525 oops |
|
526 |
|
527 quotient_definition |
|
528 subst ("_ [ _ ::= _ ]" [100,100,100] 100) |
|
529 where |
|
530 "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw" |
|
531 |
|
532 lemmas fv_rsp = quot_respect(10)[simplified] |
|
533 |
|
534 lemma subst_rsp_pre1: |
|
535 assumes a: "alpha_lam_raw a b" |
|
536 shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" |
|
537 using a |
|
538 apply (induct a b arbitrary: c y rule: alpha_lam_raw.induct) |
|
539 apply (simp add: equivp_reflp[OF lam_equivp]) |
|
540 apply (simp add: alpha_lam_raw.intros) |
|
541 apply (simp only: alphas) |
|
542 apply clarify |
|
543 apply (simp only: subst_raw.simps) |
|
544 apply (rule alpha_lam_raw.intros) |
|
545 apply (simp only: alphas) |
|
546 sorry |
|
547 |
|
548 lemma subst_rsp_pre2: |
|
549 assumes a: "alpha_lam_raw a b" |
|
550 shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)" |
|
551 using a |
|
552 apply (induct c arbitrary: a b y) |
|
553 apply (simp add: equivp_reflp[OF lam_equivp]) |
|
554 apply (simp add: alpha_lam_raw.intros) |
|
555 apply simp |
568 apply simp |
556 apply (rule alpha_lam_raw.intros) |
569 apply (rule alpha_lam_raw.intros) |
557 sorry |
570 sorry |
558 |
571 |
559 lemma [quot_respect]: |
572 lemma [quot_respect]: |
560 "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" |
573 "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw" |
561 proof (intro fun_relI, simp) |
574 proof (intro fun_relI, clarify) |
562 fix a b c d :: lam_raw |
575 fix S t s |
563 fix y :: name |
576 assume a: "alpha_lam_raw t s" |
564 assume a: "alpha_lam_raw a b" |
577 show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)" |
565 assume b: "alpha_lam_raw c d" |
578 using a proof (induct t s rule: alpha_lam_raw.induct) |
566 have c: "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" using subst_rsp_pre1 a by simp |
579 case goal1 show ?case by simp |
567 then have d: "alpha_lam_raw (subst_raw b y c) (subst_raw b y d)" using subst_rsp_pre2 b by simp |
580 next |
568 show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)" |
581 case goal2 show ?case by simp |
569 using c d equivp_transp[OF lam_equivp] by blast |
582 next |
|
583 case (goal3 x t y s) |
|
584 then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and> |
|
585 option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1) |
|
586 (match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" .. |
|
587 then have |
|
588 c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and |
|
589 d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and |
|
590 e: "alpha_lam_raw (p \<bullet> t) s" and |
|
591 f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and |
|
592 g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+ |
|
593 let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))" |
|
594 have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp |
|
595 show ?case |
|
596 unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv |
|
597 proof |
|
598 show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h) |
|
599 next |
|
600 have "atom y \<sharp> p" sorry |
|
601 have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry |
|
602 then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto |
|
603 then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry |
|
604 have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry |
|
605 then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry |
|
606 then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t) |
|
607 ((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h . |
|
608 qed |
|
609 qed |
570 qed |
610 qed |
571 |
611 |
572 lemma simp3: |
612 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
573 "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))" |
613 *) |
574 apply simp |
614 |
575 apply (rule alpha_lam_raw.intros) |
615 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
576 apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) - |
616 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
577 {atom x})))" in exI) |
617 |
578 apply (simp only: alphas) |
618 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
579 apply simp |
619 apply (induct x rule: lam.induct) |
|
620 apply (simp_all add: match_Lam_simps) |
|
621 apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S") |
|
622 apply (simp add: match_Lam_def) |
|
623 apply (subgoal_tac "\<exists>n s. Lam name lam = Lam n s") |
|
624 prefer 2 |
|
625 apply auto[1] |
|
626 apply (simp add: Let_def) |
|
627 apply (thin_tac "\<exists>n s. Lam name lam = Lam n s") |
|
628 apply clarify |
|
629 apply (rule conjI) |
|
630 apply (rule_tac t="THE s. Lam name lam = Lam (new (S, Lam name lam)) s" and |
|
631 s="(name \<leftrightarrow> (new (S, Lam name lam))) \<bullet> lam" in subst) |
|
632 defer |
|
633 apply (simp add: lam.eq_iff) |
|
634 apply (rule_tac x="(name \<leftrightarrow> (new (S, Lam name lam)))" in exI) |
|
635 apply (simp add: alphas) |
|
636 apply (simp add: eqvts) |
|
637 apply (rule conjI) |
580 sorry |
638 sorry |
581 |
639 |
582 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] |
640 function subst where |
583 simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars] |
641 "subst v s t = ( |
|
642 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
|
643 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
|
644 case match_Lam (v,s) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
|
645 by pat_completeness auto |
|
646 |
|
647 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
|
648 apply auto[1] |
|
649 apply (case_tac a) apply simp |
|
650 apply (frule lam_some) apply simp |
|
651 apply (case_tac a) apply simp |
|
652 apply (frule app_some) apply simp |
|
653 apply (case_tac a) apply simp |
|
654 apply (frule app_some) apply simp |
|
655 done |
|
656 |
|
657 lemmas lam_exhaust = lam_raw.exhaust[quot_lifted] |
|
658 |
|
659 lemma subst_eqvt: |
|
660 "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" |
|
661 proof (induct v s t rule: subst.induct) |
|
662 case (1 v s t) |
|
663 show ?case proof (cases t rule: lam_exhaust) |
|
664 fix n |
|
665 assume "t = Var n" |
|
666 then show ?thesis by (simp add: match_Var_simps) |
|
667 next |
|
668 fix l r |
|
669 assume "t = App l r" |
|
670 then show ?thesis |
|
671 apply (simp only:) |
|
672 apply (subst subst.simps) |
|
673 apply (subst match_Var_simps) |
|
674 apply (simp only: option.cases) |
|
675 apply (subst match_App_simps) |
|
676 apply (simp only: option.cases) |
|
677 apply (simp only: prod.cases) |
|
678 apply (simp only: lam.perm) |
|
679 apply (subst (3) subst.simps) |
|
680 apply (subst match_Var_simps) |
|
681 apply (simp only: option.cases) |
|
682 apply (subst match_App_simps) |
|
683 apply (simp only: option.cases) |
|
684 apply (simp only: prod.cases) |
|
685 apply (subst 1(2)[of "(l, r)" "l" "r"]) |
|
686 apply (simp add: match_Var_simps) |
|
687 apply (simp add: match_App_simps) |
|
688 apply (rule refl) |
|
689 apply (subst 1(3)[of "(l, r)" "l" "r"]) |
|
690 apply (simp add: match_Var_simps) |
|
691 apply (simp add: match_App_simps) |
|
692 apply (rule refl) |
|
693 apply (rule refl) |
|
694 done |
|
695 next |
|
696 fix n t' |
|
697 assume "t = Lam n t'" |
|
698 then show ?thesis |
|
699 apply (simp only: ) |
|
700 apply (simp only: lam.perm) |
|
701 apply (subst subst.simps) |
|
702 apply (subst match_Var_simps) |
|
703 apply (simp only: option.cases) |
|
704 apply (subst match_App_simps) |
|
705 apply (simp only: option.cases) |
|
706 apply (rule_tac t="Lam n t'" and s="Lam (new ((v, s), Lam n t')) ((n \<leftrightarrow> new ((v, s), Lam n t')) \<bullet> t')" in subst) |
|
707 defer |
|
708 apply (subst match_Lam_simps) |
|
709 defer |
|
710 apply (simp only: option.cases) |
|
711 apply (simp only: prod.cases) |
|
712 apply (subst (2) subst.simps) |
|
713 apply (subst match_Var_simps) |
|
714 apply (simp only: option.cases) |
|
715 apply (subst match_App_simps) |
|
716 apply (simp only: option.cases) |
|
717 apply (rule_tac t="Lam (p \<bullet> n) (p \<bullet> t')" and s="Lam (new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) (((p \<bullet> n) \<leftrightarrow> new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) \<bullet> t')" in subst) |
|
718 defer |
|
719 apply (subst match_Lam_simps) |
|
720 defer |
|
721 apply (simp only: option.cases) |
|
722 apply (simp only: prod.cases) |
|
723 apply (simp only: lam.perm) |
|
724 thm 1(1) |
|
725 sorry |
|
726 qed |
|
727 qed |
|
728 |
|
729 lemma subst_proper_eqs: |
|
730 "subst y s (Var x) = (if x = y then s else (Var x))" |
|
731 "subst y s (App l r) = App (subst y s l) (subst y s r)" |
|
732 "atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" |
|
733 apply (subst subst.simps) |
|
734 apply (simp only: match_Var_simps) |
|
735 apply (simp only: option.simps) |
|
736 apply (subst subst.simps) |
|
737 apply (simp only: match_App_simps) |
|
738 apply (simp only: option.simps) |
|
739 apply (simp only: prod.simps) |
|
740 apply (simp only: match_Var_simps) |
|
741 apply (simp only: option.simps) |
|
742 apply (subst subst.simps) |
|
743 apply (simp only: match_Var_simps) |
|
744 apply (simp only: option.simps) |
|
745 apply (simp only: match_App_simps) |
|
746 apply (simp only: option.simps) |
|
747 apply (rule_tac t="Lam x t" and s="Lam (new ((y, s), Lam x t)) ((x \<leftrightarrow> new ((y, s), Lam x t)) \<bullet> t)" in subst) |
|
748 defer |
|
749 apply (subst match_Lam_simps) |
|
750 defer |
|
751 apply (simp only: option.simps) |
|
752 apply (simp only: prod.simps) |
|
753 sorry |
584 |
754 |
585 end |
755 end |
586 |
756 |
587 |
757 |
588 |
758 |