1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal-General/Nominal2_Base" |
3 imports "../Nominal-General/Nominal2_Base" |
4 "../Nominal-General/Nominal2_Atoms" |
4 "../Nominal-General/Nominal2_Atoms" |
5 "../Nominal-General/Nominal2_Eqvt" |
5 "../Nominal-General/Nominal2_Eqvt" |
|
6 "../Nominal-General/Nominal2_Supp" |
6 "../Nominal-General/Atoms" |
7 "../Nominal-General/Atoms" |
7 "LaTeXsugar" |
8 "LaTeXsugar" |
8 begin |
9 begin |
9 |
10 |
10 notation (latex output) |
11 notation (latex output) |
41 (*>*) |
42 (*>*) |
42 |
43 |
43 section {* Introduction *} |
44 section {* Introduction *} |
44 |
45 |
45 text {* |
46 text {* |
|
47 The purpose of Nominal Isabelle is to provide a proving infratructure |
|
48 for conveninet reasoning about programming languages. At its core |
|
49 Nominal Isabelle is based on nominal logic by Pitts at al |
|
50 \cite{GabbayPitts02,Pitts03}. |
|
51 |
46 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
52 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
47 prover providing a proving infrastructure for convenient reasoning about |
53 prover providing a proving infrastructure for convenient reasoning about |
48 programming languages. It has been used to formalise an equivalence checking |
54 programming languages. At its core Nominal Isabelle is based on the nominal |
49 algorithm for LF \cite{UrbanCheneyBerghofer08}, |
55 logic work of Pitts et al \cite{GabbayPitts02,Pitts03}. The most basic |
50 Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
56 notion in this work is a sort-respecting permutation operation defined over |
51 \cite{BengtsonParrow07} and a strong normalisation result for |
57 a countably infinite collection of sorted atoms. The atoms are used for |
52 cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used |
58 representing variables that might be bound. Multiple sorts are necessary for |
53 by Pollack for formalisations in the locally-nameless approach to binding |
59 being able to represent different kinds of variables. For example, in the |
54 \cite{SatoPollack10}. |
60 language Mini-ML there are bound term variables and bound type variables; |
55 |
61 each kind needs to be represented by a different sort of atoms. |
56 At its core Nominal Isabelle is based on the nominal logic work of Pitts et |
62 |
57 al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a |
|
58 sort-respecting permutation operation defined over a countably infinite |
|
59 collection of sorted atoms. The atoms are used for representing variables |
|
60 that might be bound. Multiple sorts are necessary for being |
|
61 able to represent different kinds of variables. For example, in the language |
|
62 Mini-ML there are bound term variables and bound type variables; each kind |
|
63 needs to be represented by a different sort of atoms. |
|
64 |
63 |
65 Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
64 Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
66 atoms and sorts are used in the original formulation of the nominal logic work. |
65 atoms and sorts are used in the original formulation of the nominal logic work. |
67 Therefore it was decided in earlier versions of Nominal Isabelle to use a |
66 Therefore it was decided in earlier versions of Nominal Isabelle to use a |
68 separate type for each sort of atoms and let the type system enforce the |
67 separate type for each sort of atoms and let the type system enforce the |
856 This implies that atoms @{term a} and @{term c} must be equal, which clashes with our |
855 This implies that atoms @{term a} and @{term c} must be equal, which clashes with our |
857 assumption @{term "c \<noteq> a"} about how we chose @{text c}. |
856 assumption @{term "c \<noteq> a"} about how we chose @{text c}. |
858 Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support. |
857 Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support. |
859 *} |
858 *} |
860 |
859 |
|
860 section {* Support of Finite Sets *} |
|
861 |
|
862 text {* |
|
863 Sets is one instance of a type that is not generally finitely supported. |
|
864 However, it can be easily derived that finite sets of atoms are finitely |
|
865 supported, because their support can be characterised as: |
|
866 |
|
867 \begin{lemma}\label{finatomsets} |
|
868 If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}. |
|
869 \end{lemma} |
|
870 |
|
871 \begin{proof} |
|
872 finite-supp-unique |
|
873 \end{proof} |
|
874 |
|
875 More difficult is it to establish that finite sets of finitely |
|
876 supported objects are finitely supported. |
|
877 *} |
|
878 |
|
879 |
861 section {* Induction Principles *} |
880 section {* Induction Principles *} |
862 |
881 |
863 |
882 text {* |
|
883 While the use of functions as permutation provides us with a unique |
|
884 representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and |
|
885 @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has |
|
886 one draw back: it does not come readily with an induction principle. |
|
887 Such an induction principle is handy for deriving properties like |
|
888 |
|
889 @{thm [display, indent=10] supp_perm_eq} |
|
890 |
|
891 \noindent |
|
892 However, it is not too difficult to derive an induction principle, |
|
893 given the fact that we allow only permutations with a finite domain. |
|
894 *} |
864 |
895 |
865 |
896 |
866 section {* Concrete Atom Types *} |
897 section {* Concrete Atom Types *} |
867 |
898 |
868 text {* |
899 text {* |
1163 headway with formalising their results |
1194 headway with formalising their results |
1164 about simple type theory \cite{PaulsonBenzmueller}. |
1195 about simple type theory \cite{PaulsonBenzmueller}. |
1165 Because of its limitations, they did not attempt this with the old version |
1196 Because of its limitations, they did not attempt this with the old version |
1166 of Nominal Isabelle. We also hope we can make progress with formalisations of |
1197 of Nominal Isabelle. We also hope we can make progress with formalisations of |
1167 HOL-based languages. |
1198 HOL-based languages. |
|
1199 *} |
|
1200 |
|
1201 section {* Related Work *} |
|
1202 |
|
1203 text {* |
|
1204 Add here comparison with old work. |
1168 *} |
1205 *} |
1169 |
1206 |
1170 |
1207 |
1171 section {* Conclusion *} |
1208 section {* Conclusion *} |
1172 |
1209 |