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 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 |
1182 \begin{center} |
1182 \begin{center} |
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 @{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"} |
1184 \end{center} |
1184 \end{center} |
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 |
1186 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 |
1187 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 |
|
1188 exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that |
1190 the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. |
1189 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: |
1190 For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: |
1192 |
1191 |
1193 \begin{center} |
1192 \begin{center} |
1194 \begin{tabular}{cp{7cm}} |
1193 \begin{tabular}{cp{7cm}} |
1195 $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\ |
1194 $\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 |
1195 $\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"}\\ |
1196 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)"} |
1197 $\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 provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1198 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1200 function @{text "bn\<^isub>m"}, ...\\ |
1199 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
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"} |
1200 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1202 is bound in @{text "x\<^isub>j"} \\ |
1201 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>n"}\\ |
1203 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1202 $\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"} |
1203 $\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 is bound non-recursively in @{text "x\<^isub>j"} \\ |
1204 is bound in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the |
|
1205 alpha-equivalence for @{term "x\<^isub>j"} |
|
1206 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
|
1207 $\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"} |
|
1208 is bound non-recursively in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the |
|
1209 alpha-equivalence for @{term "x\<^isub>j"} |
|
1210 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1206 $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes |
1211 $\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)\\ |
1212 the types being defined, raw)\\ |
1208 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1213 $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\ |
1209 \end{tabular} |
1214 \end{tabular} |
1210 \end{center} |
1215 \end{center} |
1211 |
|
1212 |
1216 |
1213 *} |
1217 *} |
1214 |
1218 |
1215 section {* The Lifting of Definitions and Properties *} |
1219 section {* The Lifting of Definitions and Properties *} |
1216 |
1220 |