1140 \end{tabular} |
1140 \end{tabular} |
1141 \end{center} |
1141 \end{center} |
1142 |
1142 |
1143 \marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?} |
1143 \marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?} |
1144 |
1144 |
1145 |
|
1146 \noindent Next, for each binding function @{text "bn"} we define a |
1145 \noindent Next, for each binding function @{text "bn"} we define a |
1147 free variable function @{text "fv_bn"}. The basic idea behind this |
1146 free variable function @{text "fv_bn"}. The basic idea behind this |
1148 function is to compute all the free atoms under this binding |
1147 function is to compute all the free atoms under this binding |
1149 function. So given that @{text "bn"} is a binding function for type |
1148 function. So given that @{text "bn"} is a binding function for type |
1150 @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the |
1149 @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the |
1151 omission of the arguments present in @{text "bn"}. |
1150 omission of the arguments present in @{text "bn"}. |
1152 |
1151 |
1153 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1152 For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, |
1154 we define @{text "fv_bn"} to be the union of the values calculated |
1153 we define @{text "fv_bn"} to be the union of the values calculated |
1155 for @{text "x\<^isub>j"} as follows: |
1154 for @{text "x\<^isub>j"} as follows: |
|
1155 |
|
1156 \marginpar{raw for being defined} |
1156 |
1157 |
1157 \begin{center} |
1158 \begin{center} |
1158 \begin{tabular}{cp{7cm}} |
1159 \begin{tabular}{cp{7cm}} |
1159 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ |
1160 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ |
1160 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1161 $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} |
1161 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1162 with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\ |
1162 $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\ |
1163 $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\ |
1163 $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\ |
1164 $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\ |
1164 $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype |
1165 $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype |
1165 with a free variable function @{text "fv_ty"}. This includes the currently defined |
1166 with a free variable function @{text "fv_ty"}. This includes the types being |
1166 types, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1167 defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1167 $\bullet$ & @{term "{}"} otherwise |
1168 $\bullet$ & @{term "{}"} otherwise |
1168 \end{tabular} |
1169 \end{tabular} |
1169 \end{center} |
1170 \end{center} |
1170 |
1171 |
1171 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1172 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
1172 we need to define |
1173 we need to define |
1180 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 |
1181 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 |
1181 \begin{center} |
1182 \begin{center} |
1182 @{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"} |
1183 @{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"} |
1183 \end{center} |
1184 \end{center} |
1184 |
1185 |
1185 |
1186 TODO existance of permutations. |
|
1187 |
|
1188 Given a term-constructor @{text "C 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 |
|
1190 the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. |
|
1191 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: |
|
1192 |
|
1193 \begin{center} |
|
1194 \begin{tabular}{cp{7cm}} |
|
1195 $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\ |
|
1196 $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a deep non-recursive binder |
|
1197 with the auxiliary binding function @{text "bn\<^isub>m"}\\ |
|
1198 $\bullet$ & @{text "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x)) \<approx>gen \<approx>s fvs pi (bn\<^isub>m y\<^isub>j, (y\<^isub>j, s)"} |
|
1199 provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
|
1200 function @{text "bn\<^isub>m"}, ...\\ |
|
1201 $\bullet$ & @{text "(x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"} |
|
1202 is bound in @{text "x\<^isub>j"} \\ |
|
1203 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
|
1204 $\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "bn\<^isub>m x\<^isub>n"} |
|
1205 is bound non-recursively in @{text "x\<^isub>j"} \\ |
|
1206 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
|
1207 the types being defined, raw)\\ |
|
1208 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
|
1209 \end{tabular} |
|
1210 \end{center} |
1186 |
1211 |
1187 |
1212 |
1188 *} |
1213 *} |
1189 |
1214 |
1190 section {* The Lifting of Definitions and Properties *} |
1215 section {* The Lifting of Definitions and Properties *} |