1183 functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define |
1183 functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define |
1184 \begin{center} |
1184 \begin{center} |
1185 @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"} |
1185 @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"} |
1186 \end{center} |
1186 \end{center} |
1187 |
1187 |
1188 Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances |
1188 Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances |
1189 of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there |
1189 of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if there |
1190 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that |
1190 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that |
1191 the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. |
1191 the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. |
1192 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: |
1192 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: |
1193 |
1193 |
1194 \begin{center} |
1194 \begin{center} |
1195 \begin{tabular}{cp{7cm}} |
1195 \begin{tabular}{cp{7cm}} |
1196 $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\ |
1196 $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\ |
1198 with the auxiliary binding function @{text "bn\<^isub>m"}\\ |
1198 with the auxiliary binding function @{text "bn\<^isub>m"}\\ |
1199 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"} |
1199 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x\<^isub>n)) \<approx>gen R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"} |
1200 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1200 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1201 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
1201 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
1202 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1202 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1203 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>n"}\\ |
1203 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\ |
1204 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1204 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1205 $\bullet$ & @{term "(x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"} |
1205 $\bullet$ & @{term "({x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} has |
1206 is bound in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1206 a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1207 alpha-equivalence for @{term "x\<^isub>j"} |
1207 alpha-equivalence for @{term "x\<^isub>j"} |
1208 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1208 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1209 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "bn\<^isub>m x\<^isub>n"} |
1209 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} |
1210 is bound non-recursively in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1210 has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1211 alpha-equivalence for @{term "x\<^isub>j"} |
1211 alpha-equivalence for @{term "x\<^isub>j"} |
1212 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1212 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1213 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
1213 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
1214 the types being defined, raw)\\ |
1214 the types being defined, raw)\\ |
1215 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1215 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1218 |
1218 |
1219 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences |
1219 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences |
1220 for their respective types, the difference is that they ommit checking the arguments that |
1220 for their respective types, the difference is that they ommit checking the arguments that |
1221 are bound. We assumed that there are no bindings in the type on which the binding function |
1221 are bound. We assumed that there are no bindings in the type on which the binding function |
1222 is defined so, there are no permutations involved. For a binding function clause |
1222 is defined so, there are no permutations involved. For a binding function clause |
1223 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent |
1223 @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent |
1224 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if: |
1224 @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if: |
1225 \begin{center} |
1225 \begin{center} |
1226 \begin{tabular}{cp{7cm}} |
1226 \begin{tabular}{cp{7cm}} |
1227 $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\ |
1227 $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\ |
1228 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not a nominal datatype and does not occur in @{text "rhs"}\\ |
1228 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not a nominal datatype and does not occur in @{text "rhs"}\\ |
1229 $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a nominal datatype occuring in @{text "rhs"} |
1229 $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a nominal datatype occuring in @{text "rhs"} |