27 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
27 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
28 abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and |
28 abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and |
29 fv ("fv'(_')" [100] 100) and |
29 fv ("fv'(_')" [100] 100) and |
30 equal ("=") and |
30 equal ("=") and |
31 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
31 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
32 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and |
32 Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and |
33 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
33 Abs_lst ("[_]\<^bsub>list\<^esub>._") and |
34 Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and |
34 Abs_dist ("[_]\<^bsub>#list\<^esub>._") and |
35 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and |
35 Abs_res ("[_]\<^bsub>res\<^esub>._") and |
36 Abs_print ("_\<^raw:$\!$>\<^bsub>set\<^esub>._") and |
36 Abs_print ("_\<^bsub>set\<^esub>._") and |
37 Cons ("_::_" [78,77] 73) and |
37 Cons ("_::_" [78,77] 73) and |
38 supp_gen ("aux _" [1000] 10) and |
38 supp_gen ("aux _" [1000] 10) and |
39 alpha_bn ("_ \<approx>bn _") |
39 alpha_bn ("_ \<approx>bn _") |
40 (*>*) |
40 (*>*) |
41 |
41 |
113 where @{text z} does not occur freely in the type. In this paper we will |
113 where @{text z} does not occur freely in the type. In this paper we will |
114 give a general binding mechanism and associated notion of alpha-equivalence |
114 give a general binding mechanism and associated notion of alpha-equivalence |
115 that can be used to faithfully represent this kind of binding in Nominal |
115 that can be used to faithfully represent this kind of binding in Nominal |
116 Isabelle. The difficulty of finding the right notion for alpha-equivalence |
116 Isabelle. The difficulty of finding the right notion for alpha-equivalence |
117 can be appreciated in this case by considering that the definition given by |
117 can be appreciated in this case by considering that the definition given by |
118 Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). A related |
118 Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
119 notion of alpha-equivalence that allows vacuous binders, there called weakening |
|
120 of contexts, is defined in for the $\Pi\Sigma$-calculus \cite{Altenkirch10}. |
|
121 |
119 |
122 However, the notion of alpha-equivalence that is preserved by vacuous |
120 However, the notion of alpha-equivalence that is preserved by vacuous |
123 binders is not always wanted. For example in terms like |
121 binders is not always wanted. For example in terms like |
124 % |
122 % |
125 \begin{equation}\label{one} |
123 \begin{equation}\label{one} |