equal
deleted
inserted
replaced
1088 @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"} |
1088 @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"} |
1089 \end{center} |
1089 \end{center} |
1090 |
1090 |
1091 \noindent |
1091 \noindent |
1092 We define them together with the auxiliary free variable functions for |
1092 We define them together with the auxiliary free variable functions for |
1093 binding functions |
1093 binding functions. Given binding functions of types |
|
1094 @{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 |
1094 |
1095 |
1095 \begin{center} |
1096 \begin{center} |
1096 @{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"} |
1097 @{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"} |
1097 \end{center} |
1098 \end{center} |
1098 |
1099 |
1164 with a free variable function @{text "fv_ty"}. This includes the currently defined |
1165 with a free variable function @{text "fv_ty"}. This includes the currently defined |
1165 types, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1166 types, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\ |
1166 $\bullet$ & @{term "{}"} otherwise |
1167 $\bullet$ & @{term "{}"} otherwise |
1167 \end{tabular} |
1168 \end{tabular} |
1168 \end{center} |
1169 \end{center} |
|
1170 |
|
1171 We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} |
|
1172 we need to define |
|
1173 |
|
1174 \begin{center} |
|
1175 @{text "\<approx>\<^isub>1 :: ty\<^isub>1 \<Rightarrow> ty\<^isub>1 \<Rightarrow> bool \<dots> \<approx>\<^isub>n :: ty\<^isub>n \<Rightarrow> ty\<^isub>n \<Rightarrow> bool"} |
|
1176 \end{center} |
|
1177 |
|
1178 \noindent |
|
1179 together with the auxiliary equivalences for binding functions. Given binding |
|
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 \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 \end{center} |
|
1184 |
|
1185 |
|
1186 |
1169 |
1187 |
1170 *} |
1188 *} |
1171 |
1189 |
1172 section {* The Lifting of Definitions and Properties *} |
1190 section {* The Lifting of Definitions and Properties *} |
1173 |
1191 |