equal
deleted
inserted
replaced
148 quotient_type trm1 = rtrm1 / alpha1 |
148 quotient_type trm1 = rtrm1 / alpha1 |
149 by (rule alpha1_equivp) |
149 by (rule alpha1_equivp) |
150 |
150 |
151 quotient_definition |
151 quotient_definition |
152 "Vr1 :: name \<Rightarrow> trm1" |
152 "Vr1 :: name \<Rightarrow> trm1" |
153 as |
153 is |
154 "rVr1" |
154 "rVr1" |
155 |
155 |
156 quotient_definition |
156 quotient_definition |
157 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
157 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
158 as |
158 is |
159 "rAp1" |
159 "rAp1" |
160 |
160 |
161 quotient_definition |
161 quotient_definition |
162 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1" |
162 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1" |
163 as |
163 is |
164 "rLm1" |
164 "rLm1" |
165 |
165 |
166 quotient_definition |
166 quotient_definition |
167 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
167 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
168 as |
168 is |
169 "rLt1" |
169 "rLt1" |
170 |
170 |
171 quotient_definition |
171 quotient_definition |
172 "fv_trm1 :: trm1 \<Rightarrow> atom set" |
172 "fv_trm1 :: trm1 \<Rightarrow> atom set" |
173 as |
173 is |
174 "rfv_trm1" |
174 "rfv_trm1" |
175 |
175 |
176 lemma alpha_rfv1: |
176 lemma alpha_rfv1: |
177 shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s" |
177 shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s" |
178 apply(induct rule: alpha1.induct) |
178 apply(induct rule: alpha1.induct) |
209 instantiation trm1 and bp :: pt |
209 instantiation trm1 and bp :: pt |
210 begin |
210 begin |
211 |
211 |
212 quotient_definition |
212 quotient_definition |
213 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
213 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
214 as |
214 is |
215 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
215 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
216 |
216 |
217 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
217 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
218 |
218 |
219 instance |
219 instance |
703 lts = rlts / alphalts |
703 lts = rlts / alphalts |
704 by (auto intro: alpha5_equivps) |
704 by (auto intro: alpha5_equivps) |
705 |
705 |
706 quotient_definition |
706 quotient_definition |
707 "Vr5 :: name \<Rightarrow> trm5" |
707 "Vr5 :: name \<Rightarrow> trm5" |
708 as |
708 is |
709 "rVr5" |
709 "rVr5" |
710 |
710 |
711 quotient_definition |
711 quotient_definition |
712 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5" |
712 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5" |
713 as |
713 is |
714 "rAp5" |
714 "rAp5" |
715 |
715 |
716 quotient_definition |
716 quotient_definition |
717 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5" |
717 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5" |
718 as |
718 is |
719 "rLt5" |
719 "rLt5" |
720 |
720 |
721 quotient_definition |
721 quotient_definition |
722 "Lnil :: lts" |
722 "Lnil :: lts" |
723 as |
723 is |
724 "rLnil" |
724 "rLnil" |
725 |
725 |
726 quotient_definition |
726 quotient_definition |
727 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts" |
727 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts" |
728 as |
728 is |
729 "rLcons" |
729 "rLcons" |
730 |
730 |
731 quotient_definition |
731 quotient_definition |
732 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
732 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
733 as |
733 is |
734 "rfv_trm5" |
734 "rfv_trm5" |
735 |
735 |
736 quotient_definition |
736 quotient_definition |
737 "fv_lts :: lts \<Rightarrow> atom set" |
737 "fv_lts :: lts \<Rightarrow> atom set" |
738 as |
738 is |
739 "rfv_lts" |
739 "rfv_lts" |
740 |
740 |
741 quotient_definition |
741 quotient_definition |
742 "bv5 :: lts \<Rightarrow> atom set" |
742 "bv5 :: lts \<Rightarrow> atom set" |
743 as |
743 is |
744 "rbv5" |
744 "rbv5" |
745 |
745 |
746 lemma rbv5_eqvt: |
746 lemma rbv5_eqvt: |
747 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
747 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
748 sorry |
748 sorry |
825 instantiation trm5 and lts :: pt |
825 instantiation trm5 and lts :: pt |
826 begin |
826 begin |
827 |
827 |
828 quotient_definition |
828 quotient_definition |
829 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
829 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
830 as |
830 is |
831 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
831 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
832 |
832 |
833 quotient_definition |
833 quotient_definition |
834 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
834 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
835 as |
835 is |
836 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
836 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
837 |
837 |
838 lemma trm5_lts_zero: |
838 lemma trm5_lts_zero: |
839 "0 \<bullet> (x\<Colon>trm5) = x" |
839 "0 \<bullet> (x\<Colon>trm5) = x" |
840 "0 \<bullet> (y\<Colon>lts) = y" |
840 "0 \<bullet> (y\<Colon>lts) = y" |
993 trm6 = rtrm6 / alpha6 |
993 trm6 = rtrm6 / alpha6 |
994 by (auto intro: alpha6_equivps) |
994 by (auto intro: alpha6_equivps) |
995 |
995 |
996 quotient_definition |
996 quotient_definition |
997 "Vr6 :: name \<Rightarrow> trm6" |
997 "Vr6 :: name \<Rightarrow> trm6" |
998 as |
998 is |
999 "rVr6" |
999 "rVr6" |
1000 |
1000 |
1001 quotient_definition |
1001 quotient_definition |
1002 "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6" |
1002 "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6" |
1003 as |
1003 is |
1004 "rLm6" |
1004 "rLm6" |
1005 |
1005 |
1006 quotient_definition |
1006 quotient_definition |
1007 "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6" |
1007 "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6" |
1008 as |
1008 is |
1009 "rLt6" |
1009 "rLt6" |
1010 |
1010 |
1011 quotient_definition |
1011 quotient_definition |
1012 "fv_trm6 :: trm6 \<Rightarrow> atom set" |
1012 "fv_trm6 :: trm6 \<Rightarrow> atom set" |
1013 as |
1013 is |
1014 "rfv_trm6" |
1014 "rfv_trm6" |
1015 |
1015 |
1016 quotient_definition |
1016 quotient_definition |
1017 "bv6 :: trm6 \<Rightarrow> atom set" |
1017 "bv6 :: trm6 \<Rightarrow> atom set" |
1018 as |
1018 is |
1019 "rbv6" |
1019 "rbv6" |
1020 |
1020 |
1021 lemma [quot_respect]: |
1021 lemma [quot_respect]: |
1022 "(op = ===> alpha6 ===> alpha6) permute permute" |
1022 "(op = ===> alpha6 ===> alpha6) permute permute" |
1023 apply auto (* will work with eqvt *) |
1023 apply auto (* will work with eqvt *) |
1075 |
1075 |
1076 instantiation trm6 :: pt begin |
1076 instantiation trm6 :: pt begin |
1077 |
1077 |
1078 quotient_definition |
1078 quotient_definition |
1079 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
1079 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
1080 as |
1080 is |
1081 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
1081 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
1082 |
1082 |
1083 instance |
1083 instance |
1084 apply default |
1084 apply default |
1085 sorry |
1085 sorry |
1314 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
1314 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
1315 sorry |
1315 sorry |
1316 |
1316 |
1317 quotient_definition |
1317 quotient_definition |
1318 "qVar9 :: name \<Rightarrow> lam9" |
1318 "qVar9 :: name \<Rightarrow> lam9" |
1319 as |
1319 is |
1320 "Var9" |
1320 "Var9" |
1321 |
1321 |
1322 quotient_definition |
1322 quotient_definition |
1323 "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9" |
1323 "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9" |
1324 as |
1324 is |
1325 "Lam9" |
1325 "Lam9" |
1326 |
1326 |
1327 quotient_definition |
1327 quotient_definition |
1328 "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9" |
1328 "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9" |
1329 as |
1329 is |
1330 "Bla9" |
1330 "Bla9" |
1331 |
1331 |
1332 quotient_definition |
1332 quotient_definition |
1333 "fv_lam9 :: lam9 \<Rightarrow> atom set" |
1333 "fv_lam9 :: lam9 \<Rightarrow> atom set" |
1334 as |
1334 is |
1335 "rfv_lam9" |
1335 "rfv_lam9" |
1336 |
1336 |
1337 quotient_definition |
1337 quotient_definition |
1338 "fv_bla9 :: bla9 \<Rightarrow> atom set" |
1338 "fv_bla9 :: bla9 \<Rightarrow> atom set" |
1339 as |
1339 is |
1340 "rfv_bla9" |
1340 "rfv_bla9" |
1341 |
1341 |
1342 quotient_definition |
1342 quotient_definition |
1343 "bv9 :: lam9 \<Rightarrow> atom set" |
1343 "bv9 :: lam9 \<Rightarrow> atom set" |
1344 as |
1344 is |
1345 "rbv9" |
1345 "rbv9" |
1346 |
1346 |
1347 instantiation lam9 and bla9 :: pt |
1347 instantiation lam9 and bla9 :: pt |
1348 begin |
1348 begin |
1349 |
1349 |
1350 quotient_definition |
1350 quotient_definition |
1351 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
1351 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
1352 as |
1352 is |
1353 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
1353 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
1354 |
1354 |
1355 quotient_definition |
1355 quotient_definition |
1356 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
1356 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
1357 as |
1357 is |
1358 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
1358 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
1359 |
1359 |
1360 instance |
1360 instance |
1361 sorry |
1361 sorry |
1362 |
1362 |