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