6 consts |
6 consts |
7 fv :: "'a \<Rightarrow> 'b" |
7 fv :: "'a \<Rightarrow> 'b" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
9 alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
10 abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c" |
10 abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c" |
11 alpha2 :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f" |
11 Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
|
12 |
12 |
13 |
13 definition |
14 definition |
14 "equal \<equiv> (op =)" |
15 "equal \<equiv> (op =)" |
15 |
16 |
16 notation (latex output) |
17 notation (latex output) |
23 alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and |
24 alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and |
24 alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and |
25 alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and |
25 alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and |
26 alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and |
26 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
27 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
27 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 |
28 alpha2 ("_ \<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 ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and |
33 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
33 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
|
34 Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and |
34 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and |
35 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and |
35 Cons ("_::_" [78,77] 73) and |
36 Cons ("_::_" [78,77] 73) and |
36 supp_gen ("aux _" [1000] 10) and |
37 supp_gen ("aux _" [1000] 10) and |
37 alpha_bn ("_ \<approx>bn _") |
38 alpha_bn ("_ \<approx>bn _") |
38 (*>*) |
39 (*>*) |
2070 properties like \eqref{bnprop} provide us with means to support more interesting |
2071 properties like \eqref{bnprop} provide us with means to support more interesting |
2071 binding functions. |
2072 binding functions. |
2072 |
2073 |
2073 |
2074 |
2074 We have also not yet played with other binding modes. For example we can |
2075 We have also not yet played with other binding modes. For example we can |
2075 imagine that there is need for a binding mode \isacommand{bind\_\#list} with an associated |
2076 imagine that there is need for a binding mode \isacommand{bind\_\#list} with |
2076 alpha-equivalence definition as follows: |
2077 an associated abstraction of the form |
2077 % |
2078 % |
2078 \begin{center} |
2079 \begin{center} |
2079 $\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} |
2080 @{term "Abs_dist as x"} |
2080 \multicolumn{2}{l}{@{term "alpha2 (as, x) R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm] |
2081 \end{center} |
2081 & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\ |
2082 |
2082 \wedge & @{term "(fv(x) - set as) \<sharp>* p"}\\ |
2083 \noindent |
2083 \wedge & @{text "(p \<bullet> x) R y"}\\ |
2084 where instead of lists, we abstract lists of distinct elements. |
2084 \wedge & @{term "(p \<bullet> as) = bs"}\\ |
2085 Once we feel confident about such binding modes, our implementation |
2085 \wedge & @{term "distinct as"} |
|
2086 \end{array}$ |
|
2087 \end{center} |
|
2088 |
|
2089 \noindent |
|
2090 In this definition we added the requirement that all bound variables in a |
|
2091 list are distinct. Once we feel confident about such binding modes, our implementation |
|
2092 can be easily extended to accommodate them. |
2086 can be easily extended to accommodate them. |
2093 |
2087 |
2094 \medskip |
2088 \medskip |
2095 \noindent |
2089 \noindent |
2096 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
2090 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |