1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Test" |
3 imports "../Nominal/Test" "LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 notation (latex output) |
6 notation (latex output) |
7 swap ("'(_ _')" [1000, 1000] 1000) and |
7 swap ("'(_ _')" [1000, 1000] 1000) and |
8 fresh ("_ # _" [51, 51] 50) and |
8 fresh ("_ # _" [51, 51] 50) and |
|
9 fresh_star ("_ #* _" [51, 51] 50) and |
9 supp ("supp _" [78] 73) and |
10 supp ("supp _" [78] 73) and |
10 uminus ("-_" [78] 73) and |
11 uminus ("-_" [78] 73) and |
11 If ("if _ then _ else _" 10) |
12 If ("if _ then _ else _" 10) |
12 (*>*) |
13 (*>*) |
13 |
14 |
18 It has not yet fared so well in the POPLmark challenge |
19 It has not yet fared so well in the POPLmark challenge |
19 as the second part contain a formalisation of records |
20 as the second part contain a formalisation of records |
20 where ... |
21 where ... |
21 |
22 |
22 The difficulty can be appreciated by considering that the |
23 The difficulty can be appreciated by considering that the |
23 definition given by Leroy in [] is incorrect (it omits a |
24 definition given by Leroy in \cite{Leroy92} is incorrect (it omits a |
24 side-condition). |
25 side-condition). |
25 |
26 |
26 Examples: type-schemes, Spi-calculus |
27 Examples: type-schemes, Spi-calculus |
27 |
28 |
28 Contributions: We provide definitions for when terms |
29 Contributions: We provide definitions for when terms |
29 involving general bindings are alpha-equivelent. |
30 involving general bindings are alpha-equivelent. |
|
31 |
|
32 %\begin{center} |
|
33 %\begin{pspicture}(0.5,0.0)(8,2.5) |
|
34 %%\showgrid |
|
35 %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) |
|
36 %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} |
|
37 %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9) |
|
38 |
|
39 %\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5) |
|
40 |
|
41 %\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1) |
|
42 %\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9) |
|
43 |
|
44 %\rput(7.3,2.2){$\mathtt{phi}$} |
|
45 %\rput(6,1.5){$\lama$} |
|
46 %\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}} |
|
47 %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}} |
|
48 %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}} |
|
49 %\rput[c](1.7,1.5){$\lama$} |
|
50 %\rput(3.7,1.75){isomorphism} |
|
51 %\end{pspicture} |
|
52 %\end{center} |
|
53 |
|
54 |
30 *} |
55 *} |
31 |
56 |
32 section {* A Short Review of the Nominal Logic Work *} |
57 section {* A Short Review of the Nominal Logic Work *} |
33 |
58 |
34 text {* |
59 text {* |
35 At its core, Nominal Isabelle is based on the nominal logic work by Pitts |
60 At its core, Nominal Isabelle is based on the nominal logic work by Pitts |
36 \cite{Pitts03}. The central notions in this work are sorted atoms and |
61 \cite{Pitts03}. Two central notions in this work are sorted atoms and |
37 permutations of atoms. The sorted atoms represent different |
62 permutations of atoms. The sorted atoms represent different |
38 kinds of variables, such as term- and type-variables in Core-Haskell, and it |
63 kinds of variables, such as term- and type-variables in Core-Haskell, and it |
39 is assumed that there is an infinite supply of atoms for each sort. |
64 is assumed that there is an infinite supply of atoms for each sort. |
40 However, in order to simplify the description of our work, we shall |
65 However, in order to simplify the description of our work, we shall |
41 assume in this paper that there is only a single sort of atoms. |
66 assume in this paper that there is only a single sort of atoms. |
42 |
67 |
43 Permutations are bijective functions from atoms to atoms that are |
68 Permutations are bijective functions from atoms to atoms that are |
44 the identity everywhere except on a finite number of atoms. There is a |
69 the identity everywhere except on a finite number of atoms. There is a |
45 two-place permutation operation written |
70 two-place permutation operation written |
46 |
71 |
47 @{text [display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
72 @{text[display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
48 |
73 |
49 \noindent |
74 \noindent |
50 with a generic type in which @{text "\<alpha>"} stands for the type of atoms |
75 with a generic type in which @{text "\<alpha>"} stands for the type of atoms |
51 and @{text "\<beta>"} for the type of the objects on which the permutation |
76 and @{text "\<beta>"} for the type of the objects on which the permutation |
52 acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"}, |
77 acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"}, |
60 definition is general in the sense that it applies not only to lambda-terms, |
85 definition is general in the sense that it applies not only to lambda-terms, |
61 but also to lists, products, sets and even functions. The definition depends |
86 but also to lists, products, sets and even functions. The definition depends |
62 only on the permutation operation and on the notion of equality defined for |
87 only on the permutation operation and on the notion of equality defined for |
63 the type of @{text x}, namely: |
88 the type of @{text x}, namely: |
64 |
89 |
65 @{thm [display,indent=5] supp_def[no_vars, THEN eq_reflection]} |
90 @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]} |
66 |
91 |
67 \noindent |
92 \noindent |
68 There is also the derived notion for when an atom @{text a} is \emph{fresh} |
93 There is also the derived notion for when an atom @{text a} is \emph{fresh} |
69 for an @{text x}, defined as |
94 for an @{text x}, defined as |
70 |
95 |
71 @{thm [display,indent=5] fresh_def[no_vars]} |
96 @{thm[display,indent=5] fresh_def[no_vars]} |
72 |
97 |
73 \noindent |
98 \noindent |
|
99 We also use for sets of atoms the abbreviation @{thm fresh_star_def[no_vars]}. |
74 A striking consequence of these definitions is that we can prove |
100 A striking consequence of these definitions is that we can prove |
75 without knowing anything about the structure of @{term x} that |
101 without knowing anything about the structure of @{term x} that |
76 swapping two fresh atoms, say @{text a} and @{text b}, leave |
102 swapping two fresh atoms, say @{text a} and @{text b}, leave |
77 @{text x} unchanged. For the proof we use the following lemma |
103 @{text x} unchanged. |
78 about swappings applied to an @{text x}: |
104 |
|
105 \begin{Property} |
|
106 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
|
107 \end{Property} |
|
108 |
|
109 \begin{Property} |
|
110 @{thm[mode=IfThen] at_set_avoiding[no_vars]} |
|
111 \end{Property} |
79 |
112 |
80 *} |
113 *} |
81 |
114 |
82 |
115 |
83 section {* Abstractions *} |
116 section {* Abstractions *} |