738 \begin{lemma}\label{optimised} Let @{text x} be of permutation type. |
738 \begin{lemma}\label{optimised} Let @{text x} be of permutation type. |
739 We have that @{thm (concl) finite_supp_unique[no_vars]} |
739 We have that @{thm (concl) finite_supp_unique[no_vars]} |
740 provided @{thm (prem 1) finite_supp_unique[no_vars]}, |
740 provided @{thm (prem 1) finite_supp_unique[no_vars]}, |
741 @{thm (prem 2) finite_supp_unique[no_vars]}, and for |
741 @{thm (prem 2) finite_supp_unique[no_vars]}, and for |
742 all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a} |
742 all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a} |
743 and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}} |
743 and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}} |
744 \end{lemma} |
744 \end{lemma} |
745 |
745 |
746 \begin{proof} |
746 \begin{proof} |
747 By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite |
747 By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite |
748 set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will |
748 set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will |
1145 involving ``Church-style'' terms and bindings as shown in \eqref{church}. We |
1145 involving ``Church-style'' terms and bindings as shown in \eqref{church}. We |
1146 expect that the creation of such atoms can be easily automated so that the |
1146 expect that the creation of such atoms can be easily automated so that the |
1147 user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} |
1147 user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} |
1148 where the argument, or arguments, are datatypes for which we can automatically |
1148 where the argument, or arguments, are datatypes for which we can automatically |
1149 define an injective function like @{text "sort_ty"} (see \eqref{sortty}). |
1149 define an injective function like @{text "sort_ty"} (see \eqref{sortty}). |
1150 Our hope is that with this approach Benzmueller and Paulson, the authors of |
1150 Our hope is that with this approach Benzmueller and Paulson can make |
1151 \cite{PaulsonBenzmueller}, can make headway with formalising their results |
1151 headway with formalising their results |
1152 about simple type theory. |
1152 about simple type theory \cite{PaulsonBenzmueller}. |
1153 Because of its limitations, they did not attempt this with the old version |
1153 Because of its limitations, they did not attempt this with the old version |
1154 of Nominal Isabelle. We also hope we can make progress with formalisations of |
1154 of Nominal Isabelle. We also hope we can make progress with formalisations of |
1155 HOL-based languages. |
1155 HOL-based languages. |
1156 *} |
1156 *} |
1157 |
1157 |
1192 in order to make the approach based on a single type of sorted atoms to work. |
1192 in order to make the approach based on a single type of sorted atoms to work. |
1193 But of course it is analogous to the well-known trick of defining division by |
1193 But of course it is analogous to the well-known trick of defining division by |
1194 zero to return zero. |
1194 zero to return zero. |
1195 |
1195 |
1196 We noticed only one disadvantage of the permutations-as-functions: Over |
1196 We noticed only one disadvantage of the permutations-as-functions: Over |
1197 lists we can easily perform inductions. For permutation made up from |
1197 lists we can easily perform inductions. For permutations made up from |
1198 functions, we have to manually derive an appropriate induction principle. We |
1198 functions, we have to manually derive an appropriate induction principle. We |
1199 can establish such a principle, but we have no real experience yet whether ours |
1199 can establish such a principle, but we have no real experience yet whether ours |
1200 is the most useful principle: such an induction principle was not needed in |
1200 is the most useful principle: such an induction principle was not needed in |
1201 any of the reasoning we ported from the old Nominal Isabelle, except |
1201 any of the reasoning we ported from the old Nominal Isabelle, except |
1202 when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}. |
1202 when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}. |