36 | "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}" |
36 | "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}" |
37 | "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)" |
37 | "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)" |
38 | "rfv_bp (BUnit) = {}" |
38 | "rfv_bp (BUnit) = {}" |
39 | "rfv_bp (BVr x) = {atom x}" |
39 | "rfv_bp (BVr x) = {atom x}" |
40 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)" |
40 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)" |
|
41 print_theorems |
41 |
42 |
42 (* needs to be stated by the package *) |
43 (* needs to be stated by the package *) |
43 instantiation |
44 instantiation |
44 rtrm1 and bp :: pt |
45 rtrm1 and bp :: pt |
45 begin |
46 begin |
653 and rlts = |
654 and rlts = |
654 rLnil |
655 rLnil |
655 | rLcons "name" "rtrm5" "rlts" |
656 | rLcons "name" "rtrm5" "rlts" |
656 |
657 |
657 primrec |
658 primrec |
658 bv5 |
659 rbv5 |
659 where |
660 where |
660 "bv5 rLnil = {}" |
661 "rbv5 rLnil = {}" |
661 | "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
662 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
662 |
663 |
663 primrec |
664 primrec |
664 rfv_trm5 and rfv_lts |
665 rfv_trm5 and rfv_lts |
665 where |
666 where |
666 "rfv_trm5 (rVr5 n) = {atom n}" |
667 "rfv_trm5 (rVr5 n) = {atom n}" |
667 | "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)" |
668 | "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)" |
668 | "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)" |
669 | "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)" |
669 | "rfv_lts (rLnil) = {}" |
670 | "rfv_lts (rLnil) = {}" |
670 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)" |
671 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)" |
671 |
672 |
672 instantiation |
673 instantiation |
673 rtrm5 and rlts :: pt |
674 rtrm5 and rlts :: pt |
676 primrec |
677 primrec |
677 permute_rtrm5 and permute_rlts |
678 permute_rtrm5 and permute_rlts |
678 where |
679 where |
679 "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)" |
680 "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)" |
680 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)" |
681 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)" |
681 | "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)" |
682 | "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)" |
682 | "permute_rlts pi (rLnil) = rLnil" |
683 | "permute_rlts pi (rLnil) = rLnil" |
683 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)" |
684 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)" |
684 |
685 |
685 lemma pt_rtrm5_zero: |
686 lemma pt_rtrm5_zero: |
686 fixes t::rtrm5 |
687 fixes t::rtrm5 |
712 and |
713 and |
713 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100) |
714 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100) |
714 where |
715 where |
715 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)" |
716 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)" |
716 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2" |
717 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2" |
717 | a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
718 | a3: "\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and> |
718 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
719 (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and> |
719 (pi \<bullet> (bv5 l1) = bv5 l2)) |
720 (pi \<bullet> (rbv5 l1) = rbv5 l2)) |
720 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
721 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
721 | a4: "rLnil \<approx>l rLnil" |
722 | a4: "rLnil \<approx>l rLnil" |
722 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
723 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
723 |
724 |
724 print_theorems |
725 print_theorems |
725 |
726 |
726 lemma alpha5_inj: |
727 lemma alpha5_inj: |
727 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
728 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
728 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
729 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
729 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
730 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and> |
730 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
731 (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and> |
731 (pi \<bullet> (bv5 l1) = bv5 l2)))" |
732 (pi \<bullet> (rbv5 l1) = rbv5 l2)))" |
732 "rLnil \<approx>l rLnil" |
733 "rLnil \<approx>l rLnil" |
733 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)" |
734 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)" |
734 apply - |
735 apply - |
735 apply (simp_all add: alpha5_alphalts.intros) |
736 apply (simp_all add: alpha5_alphalts.intros) |
736 apply rule |
737 apply rule |
787 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
788 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
788 as |
789 as |
789 "rfv_trm5" |
790 "rfv_trm5" |
790 |
791 |
791 quotient_definition |
792 quotient_definition |
792 "fv_ltr :: lts \<Rightarrow> atom set" |
793 "fv_lts :: lts \<Rightarrow> atom set" |
793 as |
794 as |
794 "rfv_lts" |
795 "rfv_lts" |
795 |
796 |
|
797 quotient_definition |
|
798 "bv5 :: lts \<Rightarrow> atom set" |
|
799 as |
|
800 "rbv5" |
|
801 |
|
802 lemma alpha5_rfv: |
|
803 "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)" |
|
804 "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)" |
|
805 apply(induct rule: alpha5_alphalts.inducts) |
|
806 apply(simp_all add: alpha_gen) |
|
807 apply(erule conjE)+ |
|
808 apply(erule exE) |
|
809 apply(erule conjE)+ |
|
810 apply simp |
|
811 done |
|
812 |
|
813 lemma [quot_respect]: |
|
814 "(op = ===> alpha5 ===> alpha5) permute permute" |
|
815 "(op = ===> alphalts ===> alphalts) permute permute" |
|
816 "(op = ===> alpha5) rVr5 rVr5" |
|
817 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5" |
|
818 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
819 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
820 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
|
821 "(alpha5 ===> op =) rfv_trm5 rfv_trm5" |
|
822 "(alphalts ===> op =) rfv_lts rfv_lts" |
|
823 "(alphalts ===> op =) rbv5 rbv5" |
|
824 sorry |
|
825 |
|
826 instantiation trm5 and lts :: pt |
|
827 begin |
|
828 |
|
829 quotient_definition |
|
830 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
831 as |
|
832 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
|
833 |
|
834 quotient_definition |
|
835 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
836 as |
|
837 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
|
838 |
|
839 lemma permute_trm5_lts: |
|
840 "pi \<bullet> (Vr5 a) = Vr5 (pi \<bullet> a)" |
|
841 "pi \<bullet> (Ap5 t1 t2) = Ap5 (pi \<bullet> t1) (pi \<bullet> t2)" |
|
842 "pi \<bullet> (Lt5 ls t) = Lt5 (pi \<bullet> ls) (pi \<bullet> t)" |
|
843 "pi \<bullet> Lnil = Lnil" |
|
844 "pi \<bullet> (Lcons n t ls) = Lcons (pi \<bullet> n) (pi \<bullet> t) (pi \<bullet> ls)" |
|
845 by (lifting permute_rtrm5_permute_rlts.simps) |
|
846 |
|
847 lemma trm5_lts_zero: |
|
848 "0 \<bullet> (x\<Colon>trm5) = x" |
|
849 "0 \<bullet> (y\<Colon>lts) = y" |
|
850 sorry |
|
851 |
|
852 lemma trm5_lts_plus: |
|
853 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x" |
|
854 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y" |
|
855 sorry |
|
856 |
|
857 instance |
|
858 apply default |
|
859 apply (simp_all add: trm5_lts_zero trm5_lts_plus) |
|
860 done |
796 |
861 |
797 end |
862 end |
|
863 |
|
864 lemma alpha5_INJ: |
|
865 "((Vr5 a) = (Vr5 b)) = (a = b)" |
|
866 "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)" |
|
867 "(Lt5 l1 t1 = Lt5 l2 t2) = |
|
868 (\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2) \<and> |
|
869 (bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2) \<and> |
|
870 (pi \<bullet> (bv5 l1) = bv5 l2)))" |
|
871 "Lnil = Lnil" |
|
872 "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (ls1 = ls2 \<and> t1 = t2 \<and> n1 = n2)" |
|
873 unfolding alpha_gen |
|
874 apply(lifting alpha5_inj[unfolded alpha_gen]) |
|
875 done |
|
876 |
|
877 lemma bv5[simp]: |
|
878 "bv5 Lnil = {}" |
|
879 "bv5 (Lcons n t ltl) = {atom n} \<union> bv5 ltl" |
|
880 by (lifting rbv5.simps) |
|
881 |
|
882 lemma fv_trm5_lts[simp]: |
|
883 "fv_trm5 (Vr5 n) = {atom n}" |
|
884 "fv_trm5 (Ap5 t s) = fv_trm5 t \<union> fv_trm5 s" |
|
885 "fv_trm5 (Lt5 lts t) = fv_trm5 t - bv5 lts \<union> (fv_lts lts - bv5 lts)" |
|
886 "fv_lts Lnil = {}" |
|
887 "fv_lts (Lcons n t ltl) = fv_trm5 t \<union> fv_lts ltl" |
|
888 by (lifting rfv_trm5_rfv_lts.simps) |
|
889 |
|
890 lemma lets_ok: |
|
891 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
892 apply (subst alpha5_INJ) |
|
893 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
894 apply (simp only: alpha_gen) |
|
895 apply (simp add: permute_trm5_lts) |
|
896 sorry |
|
897 |
|
898 |
|
899 end |