equal
deleted
inserted
replaced
1170 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1170 $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ |
1171 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1171 $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ |
1172 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1172 $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ |
1173 $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes |
1173 $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes |
1174 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
1174 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
1175 $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype |
1175 % $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype |
1176 with a free variable function @{text "fv\<^isup>\<alpha>"}\\\\ |
1176 % with a free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1177 $\bullet$ & @{term "{}"} otherwise |
1177 $\bullet$ & @{term "{}"} otherwise |
1178 \end{tabular} |
1178 \end{tabular} |
1179 \end{center} |
1179 \end{center} |
1180 |
1180 |
1181 \noindent Next, for each binding function @{text "bn"} we define a |
1181 \noindent Next, for each binding function @{text "bn"} we define a |
1198 $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\ |
1198 $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\ |
1199 $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\ |
1199 $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\ |
1200 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is |
1200 $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is |
1201 one of the datatypes |
1201 one of the datatypes |
1202 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
1202 we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\ |
1203 $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} |
1203 % $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} |
1204 and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1204 % and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\ |
1205 $\bullet$ & @{term "{}"} otherwise |
1205 $\bullet$ & @{term "{}"} otherwise |
1206 \end{tabular} |
1206 \end{tabular} |
1207 \end{center} |
1207 \end{center} |
1208 |
1208 |
1209 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1209 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1243 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1243 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1244 $\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"} |
1244 $\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"} |
1245 has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1245 has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1246 alpha-equivalence for @{term "x\<^isub>j"} |
1246 alpha-equivalence for @{term "x\<^isub>j"} |
1247 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1247 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1248 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
1248 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being |
1249 the types being defined, raw)\\ |
1249 defined\\ |
1250 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1250 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1251 \end{tabular} |
1251 \end{tabular} |
1252 \end{center} |
1252 \end{center} |
1253 |
1253 |
1254 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences |
1254 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences |
1257 is defined so, there are no permutations involved. For a binding function clause |
1257 is defined so, there are no permutations involved. For a binding function clause |
1258 @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent |
1258 @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent |
1259 @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if: |
1259 @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if: |
1260 \begin{center} |
1260 \begin{center} |
1261 \begin{tabular}{cp{7cm}} |
1261 \begin{tabular}{cp{7cm}} |
1262 $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\ |
1262 $\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\ |
1263 $\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"}\\ |
1263 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not of a type being defined |
1264 $\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"} |
1264 and does not occur in @{text "rhs"}\\ |
1265 under the binding function @{text "bn\<^isub>m"}\\ |
1265 $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is of a type being defined |
|
1266 occuring in @{text "rhs"} under the binding function @{text "bn\<^isub>m"}\\ |
1266 $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\ |
1267 $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\ |
1267 \end{tabular} |
1268 \end{tabular} |
1268 \end{center} |
1269 \end{center} |
1269 |
1270 |
1270 *} |
1271 *} |