1017 quotient_definition |
1017 quotient_definition |
1018 "bv6 :: trm6 \<Rightarrow> atom set" |
1018 "bv6 :: trm6 \<Rightarrow> atom set" |
1019 as |
1019 as |
1020 "rbv6" |
1020 "rbv6" |
1021 |
1021 |
|
1022 lemma [quot_respect]: |
|
1023 "(op = ===> alpha1 ===> alpha1) permute permute" |
|
1024 apply auto (* eqvt *) |
|
1025 sorry |
|
1026 |
1022 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
1027 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
1023 apply simp apply clarify |
1028 apply simp apply clarify |
1024 apply (erule alpha6.induct) |
1029 apply (erule alpha6.induct) |
1025 apply simp |
1030 apply simp |
1026 apply simp |
1031 apply simp |
1027 apply (erule exE) |
1032 apply (erule exE) |
1028 apply (simp add: alpha_gen) |
1033 apply (simp add: alpha_gen) |
1029 sorry |
1034 oops |
1030 |
1035 |
1031 lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6" |
1036 lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6" |
1032 sorry |
1037 apply simp apply clarify |
|
1038 apply (induct_tac x y rule: alpha6.induct) |
|
1039 apply simp_all |
|
1040 apply (erule exE) |
|
1041 apply (simp add: alpha_gen) |
|
1042 apply (erule conjE)+ |
|
1043 oops |
1033 |
1044 |
1034 lemma [quot_respect]: |
1045 lemma [quot_respect]: |
1035 "(op = ===> alpha6) rVr6 rVr6" |
1046 "(op = ===> alpha6) rVr6 rVr6" |
1036 "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6" |
1047 "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6" |
1037 "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6" |
1048 "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6" |
1039 apply clarify |
1050 apply clarify |
1040 apply (rule a3) |
1051 apply (rule a3) |
1041 apply (rule_tac x="0::perm" in exI) |
1052 apply (rule_tac x="0::perm" in exI) |
1042 apply (simp add: alpha_gen) |
1053 apply (simp add: alpha_gen) |
1043 (* needs rbv6_rsp *) |
1054 (* needs rbv6_rsp *) |
1044 sorry |
1055 oops |
1045 |
1056 |
1046 instantiation trm6 :: pt begin |
1057 instantiation trm6 :: pt begin |
1047 |
1058 |
1048 quotient_definition |
1059 quotient_definition |
1049 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
1060 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
1050 as |
1061 as |
1051 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
1062 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
1052 |
1063 |
1053 instance |
1064 instance |
|
1065 apply default |
1054 sorry |
1066 sorry |
1055 end |
1067 end |
|
1068 |
|
1069 lemma |
|
1070 "\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b); |
|
1071 \<And>t1 t2 s1 s2. \<lbrakk>t1 = t2; P t1 t2; s1 = s2; P s1 s2\<rbrakk> \<Longrightarrow> P (Ap6 t1 s1) (Ap6 t2 s2); |
|
1072 \<And>l1 r1 l2 r2. |
|
1073 \<exists>pi. (bv6 l1, r1) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P x1 x2) fv_trm6 pi (bv6 l2, r2) \<Longrightarrow> |
|
1074 P (Fo6 l1 r1) (Fo6 l2 r2)\<rbrakk> |
|
1075 \<Longrightarrow> P x1 x2" |
|
1076 unfolding alpha_gen |
|
1077 apply (lifting alpha6.induct[unfolded alpha_gen]) |
|
1078 apply(injection) |
|
1079 sorry |
1056 |
1080 |
1057 lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk> |
1081 lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk> |
1058 \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2" |
1082 \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2" |
1059 apply (unfold alpha_gen) |
1083 apply (unfold alpha_gen) |
1060 apply (lifting a3[unfolded alpha_gen]) |
1084 apply (lifting a3[unfolded alpha_gen]) |