510 apply simp_all |
507 apply simp_all |
511 done |
508 done |
512 |
509 |
513 lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
510 lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
514 |
511 |
515 primrec match_Lam_raw where |
512 definition new where |
|
513 "new (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)" |
|
514 |
|
515 definition |
|
516 "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then |
|
517 (let z = new (S, t) in Some (z, THE s. t = Lam z s)) else None)" |
|
518 |
|
519 lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)" |
|
520 apply auto |
|
521 apply (simp only: lam.eq_iff alphas) |
|
522 apply clarify |
|
523 apply (simp add: eqvts) |
|
524 sorry |
|
525 |
|
526 lemma match_Lam_simps: |
|
527 "match_Lam S (Var n) = None" |
|
528 "match_Lam S (App l r) = None" |
|
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 |
|
533 done |
|
534 |
|
535 (* |
|
536 lemma match_Lam_simps2: |
|
537 "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)" |
|
538 apply (rule_tac t="Lam n s" |
|
539 and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst) |
|
540 defer |
|
541 apply (subst match_Lam_simps(3)) |
|
542 defer |
|
543 apply simp |
|
544 *) |
|
545 |
|
546 (*primrec match_Lam_raw where |
516 "match_Lam_raw (S :: atom set) (Var_raw x) = None" |
547 "match_Lam_raw (S :: atom set) (Var_raw x) = None" |
517 | "match_Lam_raw S (App_raw x y) = None" |
548 | "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))" |
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))" |
519 |
550 |
520 quotient_definition |
551 quotient_definition |
577 qed |
608 qed |
578 qed |
609 qed |
579 qed |
610 qed |
580 |
611 |
581 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
612 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
|
613 *) |
582 |
614 |
583 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
615 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
584 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
616 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
585 |
617 |
586 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
618 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
587 apply (induct x rule: lam.induct) |
619 apply (induct x rule: lam.induct) |
588 apply (simp_all add: match_Lam_simps) |
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] |
589 apply (simp add: Let_def) |
626 apply (simp add: Let_def) |
590 apply (erule conjE) |
627 apply (thin_tac "\<exists>n s. Lam name lam = Lam n s") |
591 apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S") |
628 apply clarify |
592 apply (rule conjI) |
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 |
593 apply (simp add: lam.eq_iff) |
633 apply (simp add: lam.eq_iff) |
594 apply (rule_tac x="(name \<leftrightarrow> z)" in exI) |
634 apply (rule_tac x="(name \<leftrightarrow> (new (S, Lam name lam)))" in exI) |
595 apply (simp add: alphas) |
635 apply (simp add: alphas) |
596 apply (simp add: eqvts) |
636 apply (simp add: eqvts) |
597 apply (simp only: lam.fv(3)[symmetric]) |
637 apply (rule conjI) |
598 apply (subgoal_tac "Lam name lam = Lam z s") |
|
599 apply (simp del: lam.fv) |
|
600 prefer 3 |
|
601 apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s") |
|
602 apply (simp only: new_def) |
|
603 apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a") |
|
604 apply (simp only: fresh_def) |
|
605 (*thm supp_finite_atom_fset*) |
|
606 sorry |
638 sorry |
607 |
639 |
608 function subst where |
640 function subst where |
609 "subst v s t = ( |
641 "subst v s t = ( |
610 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
642 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
611 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
643 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
612 case match_Lam (supp (v,s)) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
644 case match_Lam (v,s) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
613 by pat_completeness auto |
645 by pat_completeness auto |
614 |
646 |
615 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
647 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
616 apply auto[1] |
648 apply auto[1] |
617 apply (case_tac a) apply simp |
649 apply (case_tac a) apply simp |
644 apply (simp only: option.cases) |
676 apply (simp only: option.cases) |
645 apply (simp only: prod.cases) |
677 apply (simp only: prod.cases) |
646 apply (simp only: lam.perm) |
678 apply (simp only: lam.perm) |
647 apply (subst (3) subst.simps) |
679 apply (subst (3) subst.simps) |
648 apply (subst match_Var_simps) |
680 apply (subst match_Var_simps) |
649 apply (simp only: option.cases) |
681 apply (simp only: option.cases) |
650 apply (subst match_App_simps) |
682 apply (subst match_App_simps) |
651 apply (simp only: option.cases) |
683 apply (simp only: option.cases) |
652 apply (simp only: prod.cases) |
684 apply (simp only: prod.cases) |
653 apply (subst 1(2)[of "(l, r)" "l" "r"]) |
685 apply (subst 1(2)[of "(l, r)" "l" "r"]) |
654 apply (simp add: match_Var_simps) |
686 apply (simp add: match_Var_simps) |
669 apply (subst subst.simps) |
701 apply (subst subst.simps) |
670 apply (subst match_Var_simps) |
702 apply (subst match_Var_simps) |
671 apply (simp only: option.cases) |
703 apply (simp only: option.cases) |
672 apply (subst match_App_simps) |
704 apply (subst match_App_simps) |
673 apply (simp only: option.cases) |
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 |
674 apply (subst match_Lam_simps) |
708 apply (subst match_Lam_simps) |
675 apply (simp only: Let_def) |
709 defer |
676 apply (simp only: option.cases) |
710 apply (simp only: option.cases) |
677 apply (simp only: prod.cases) |
711 apply (simp only: prod.cases) |
678 apply (subst (2) subst.simps) |
712 apply (subst (2) subst.simps) |
679 apply (subst match_Var_simps) |
713 apply (subst match_Var_simps) |
680 apply (simp only: option.cases) |
714 apply (simp only: option.cases) |
681 apply (subst match_App_simps) |
715 apply (subst match_App_simps) |
682 apply (simp only: option.cases) |
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 |
683 apply (subst match_Lam_simps) |
719 apply (subst match_Lam_simps) |
684 apply (simp only: Let_def) |
720 defer |
685 apply (simp only: option.cases) |
721 apply (simp only: option.cases) |
686 apply (simp only: prod.cases) |
722 apply (simp only: prod.cases) |
687 apply (simp only: lam.perm) |
723 apply (simp only: lam.perm) |
688 apply (simp only: lam.eq_iff) |
724 thm 1(1) |
689 sorry |
725 sorry |
690 qed |
726 qed |
691 qed |
727 qed |
692 |
|
693 |
728 |
694 lemma subst_proper_eqs: |
729 lemma subst_proper_eqs: |
695 "subst y s (Var x) = (if x = y then s else (Var x))" |
730 "subst y s (Var x) = (if x = y then s else (Var x))" |
696 "subst y s (App l r) = App (subst y s l) (subst y s r)" |
731 "subst y s (App l r) = App (subst y s l) (subst y s r)" |
697 "atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" |
732 "atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" |
703 apply (simp only: option.simps) |
738 apply (simp only: option.simps) |
704 apply (simp only: prod.simps) |
739 apply (simp only: prod.simps) |
705 apply (simp only: match_Var_simps) |
740 apply (simp only: match_Var_simps) |
706 apply (simp only: option.simps) |
741 apply (simp only: option.simps) |
707 apply (subst subst.simps) |
742 apply (subst subst.simps) |
708 apply (simp only: match_Lam_simps) |
|
709 apply (simp only: match_Var_simps) |
743 apply (simp only: match_Var_simps) |
|
744 apply (simp only: option.simps) |
710 apply (simp only: match_App_simps) |
745 apply (simp only: match_App_simps) |
711 apply (simp only: option.simps) |
746 apply (simp only: option.simps) |
712 apply (simp only: Let_def) |
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 |
713 apply (simp only: option.simps) |
751 apply (simp only: option.simps) |
714 apply (simp only: prod.simps) |
752 apply (simp only: prod.simps) |
715 sorry |
753 sorry |
716 |
754 |
717 end |
755 end |