1146 involving ``Church-style'' terms and bindings as shown in \eqref{church}. We |
1146 involving ``Church-style'' terms and bindings as shown in \eqref{church}. We |
1147 expect that the creation of such atoms can be easily automated so that the |
1147 expect that the creation of such atoms can be easily automated so that the |
1148 user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} |
1148 user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} |
1149 where the argument, or arguments, are datatypes for which we can automatically |
1149 where the argument, or arguments, are datatypes for which we can automatically |
1150 define an injective function like @{text "sort_ty"} (see \eqref{sortty}). |
1150 define an injective function like @{text "sort_ty"} (see \eqref{sortty}). |
1151 Our hope is that with this approach Benzmueller and Paulson, the authors of |
1151 Our hope is that with this approach Benzmueller and Paulson can make |
1152 \cite{PaulsonBenzmueller}, can make headway with formalising their results |
1152 headway with formalising their results |
1153 about simple type theory. |
1153 about simple type theory \cite{PaulsonBenzmueller}. |
1154 Because of its limitations, they did not attempt this with the old version |
1154 Because of its limitations, they did not attempt this with the old version |
1155 of Nominal Isabelle. We also hope we can make progress with formalisations of |
1155 of Nominal Isabelle. We also hope we can make progress with formalisations of |
1156 HOL-based languages. |
1156 HOL-based languages. |
1157 *} |
1157 *} |
1158 |
1158 |
1193 in order to make the approach based on a single type of sorted atoms to work. |
1193 in order to make the approach based on a single type of sorted atoms to work. |
1194 But of course it is analogous to the well-known trick of defining division by |
1194 But of course it is analogous to the well-known trick of defining division by |
1195 zero to return zero. |
1195 zero to return zero. |
1196 |
1196 |
1197 We noticed only one disadvantage of the permutations-as-functions: Over |
1197 We noticed only one disadvantage of the permutations-as-functions: Over |
1198 lists we can easily perform inductions. For permutation made up from |
1198 lists we can easily perform inductions. For permutations made up from |
1199 functions, we have to manually derive an appropriate induction principle. We |
1199 functions, we have to manually derive an appropriate induction principle. We |
1200 can establish such a principle, but we have no real experience yet whether ours |
1200 can establish such a principle, but we have no real experience yet whether ours |
1201 is the most useful principle: such an induction principle was not needed in |
1201 is the most useful principle: such an induction principle was not needed in |
1202 any of the reasoning we ported from the old Nominal Isabelle, except |
1202 any of the reasoning we ported from the old Nominal Isabelle, except |
1203 when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}. |
1203 when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}. |