equal
deleted
inserted
replaced
1021 quotient_definition |
1021 quotient_definition |
1022 "bv6 :: trm6 \<Rightarrow> atom set" |
1022 "bv6 :: trm6 \<Rightarrow> atom set" |
1023 as |
1023 as |
1024 "rbv6" |
1024 "rbv6" |
1025 |
1025 |
1026 |
1026 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
|
1027 apply simp apply clarify |
|
1028 apply (erule alpha6.induct) |
|
1029 apply simp |
|
1030 apply simp |
|
1031 apply (erule exE) |
|
1032 apply (simp add: alpha_gen) |
|
1033 sorry |
|
1034 |
|
1035 lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6" |
|
1036 sorry |
1027 |
1037 |
1028 lemma [quot_respect]: |
1038 lemma [quot_respect]: |
1029 "(op = ===> alpha6) rVr6 rVr6" |
1039 "(op = ===> alpha6) rVr6 rVr6" |
1030 "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6" |
1040 "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6" |
1031 "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6" |
1041 "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6" |
1037 (* needs rbv6_rsp *) |
1047 (* needs rbv6_rsp *) |
1038 sorry |
1048 sorry |
1039 |
1049 |
1040 instantiation trm6 :: pt begin |
1050 instantiation trm6 :: pt begin |
1041 |
1051 |
|
1052 quotient_definition |
|
1053 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
1054 as |
|
1055 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
|
1056 |
1042 instance |
1057 instance |
1043 sorry |
1058 sorry |
1044 end |
1059 end |
1045 |
1060 |
1046 lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk> |
1061 lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk> |
1047 \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2" |
1062 \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2" |
1048 apply (unfold alpha_gen) |
1063 apply (unfold alpha_gen) |
1049 apply (lifting a3[unfolded alpha_gen]) |
1064 apply (lifting a3[unfolded alpha_gen]) |
1050 apply injection |
1065 apply injection |
1051 |
|
1052 |
|
1053 |
|
1054 sorry |
1066 sorry |
1055 |
1067 |
1056 |
1068 |
1057 |
1069 |
1058 |
1070 |