17 fresh ("_ # _" [51, 51] 50) and |
15 fresh ("_ # _" [51, 51] 50) and |
18 fresh_star ("_ #* _" [51, 51] 50) and |
16 fresh_star ("_ #* _" [51, 51] 50) and |
19 supp ("supp _" [78] 73) and |
17 supp ("supp _" [78] 73) and |
20 uminus ("-_" [78] 73) and |
18 uminus ("-_" [78] 73) and |
21 If ("if _ then _ else _" 10) and |
19 If ("if _ then _ else _" 10) and |
22 alpha_gen ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and |
20 alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and |
23 alpha_lst ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and |
21 alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and |
24 alpha_res ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and |
22 alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and |
25 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
23 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
26 fv ("fv'(_')" [100] 100) and |
24 fv ("fv'(_')" [100] 100) and |
27 equal ("=") and |
25 equal ("=") and |
28 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
26 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
29 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and |
27 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and |
442 given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom |
440 given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom |
443 set"}}, then @{text x} and @{text y} need to have the same set of free |
441 set"}}, then @{text x} and @{text y} need to have the same set of free |
444 variables; moreover there must be a permutation @{text p} such that {\it |
442 variables; moreover there must be a permutation @{text p} such that {\it |
445 ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but |
443 ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but |
446 {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, |
444 {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, |
447 say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that |
445 say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that |
448 @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The |
446 @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The |
449 requirements {\it i)} to {\it iv)} can be stated formally as follows: |
447 requirements {\it i)} to {\it iv)} can be stated formally as follows: |
450 % |
448 % |
451 \begin{equation}\label{alphaset} |
449 \begin{equation}\label{alphaset} |
452 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} |
450 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} |
453 \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\ |
451 \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\ |
554 %All properties are by unfolding the definitions and simple calculations. |
553 %All properties are by unfolding the definitions and simple calculations. |
555 %\end{proof} |
554 %\end{proof} |
556 |
555 |
557 |
556 |
558 In the rest of this section we are going to introduce a type- and term-constructor |
557 In the rest of this section we are going to introduce a type- and term-constructor |
559 for abstractions. For this we define |
558 for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$ |
|
559 and $\approx_{\textit{abs\_res}}$) |
560 % |
560 % |
561 \begin{equation} |
561 \begin{equation} |
562 @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"} |
562 @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"} |
563 \end{equation} |
563 \end{equation} |
564 |
564 |
565 \noindent |
565 \noindent |
566 Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these |
566 We can show that these relations are equivalence relations and equivariant |
567 relations are equivalence relations and equivariant |
|
568 (we only show the $\approx_{\textit{abs\_set}}$-case). |
567 (we only show the $\approx_{\textit{abs\_set}}$-case). |
569 |
568 |
570 \begin{lemma} |
569 \begin{lemma}\label{alphaeq} |
571 $\approx_{\textit{abs\_set}}$ is an equivalence |
570 $\approx_{\textit{abs\_set}}$ is an equivalence |
572 relations, and if @{term "abs_set (as, x) (bs, x)"} then also |
571 relations, and if @{term "abs_set (as, x) (bs, y)"} then also |
573 @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> x)"}. |
572 @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"}. |
574 \end{lemma} |
573 \end{lemma} |
575 |
574 |
576 \begin{proof} |
575 \begin{proof} |
577 Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have |
576 Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have |
578 a permutation @{text p} and for the proof obligation take @{term "-p"}. In case |
577 a permutation @{text p} and for the proof obligation take @{term "-p"}. In case |
579 of transitivity we have two permutations @{text p} and @{text q}, and for the |
578 of transitivity, we have two permutations @{text p} and @{text q}, and for the |
580 proof obligation use @{text "q + p"}. All the conditions are then by simple |
579 proof obligation use @{text "q + p"}. All conditions are then by simple |
581 calculations. |
580 calculations. |
582 \end{proof} |
581 \end{proof} |
583 |
582 |
|
583 \noindent |
|
584 We are also define the following two auxiliary functions taking a pair |
|
585 as argument. |
|
586 % |
|
587 \begin{equation}\label{aux} |
|
588 \begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
589 @{text "aux (as, x)"} & @{text "\<equiv>"} & @{text "supp x - as"}\\ |
|
590 @{text "aux_list (bs, x)"} & @{text "\<equiv>"} & @{text "supp x - set bs"} |
|
591 \end{array} |
|
592 \end{equation} |
|
593 |
|
594 \noindent |
|
595 The point of these two functions is that they are preserved under |
|
596 alpha-equivalence, that means for instance |
|
597 % |
|
598 \begin{equation}\label{auxpreserved} |
|
599 @{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\; |
|
600 @{term "aux (as, x) = aux (bs, y)"} |
|
601 \end{equation} |
|
602 |
|
603 Lemma \ref{alphaeq} allows us to use our quotient package and introduce |
|
604 new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"} |
|
605 representing the alpha-equivalence classes. Elements in these types |
|
606 we will, respectively, write as: |
|
607 |
|
608 \begin{center} |
|
609 @{term "Abs as x"} \hspace{5mm} |
|
610 @{term "Abs_lst as x"} \hspace{5mm} |
|
611 @{term "Abs_res as x"} |
|
612 \end{center} |
|
613 |
|
614 \noindent |
|
615 By definition we have |
|
616 |
|
617 \begin{center} |
|
618 @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\; |
|
619 @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} |
|
620 \end{center} |
|
621 |
|
622 |
584 \noindent |
623 \noindent |
585 The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and |
624 The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and |
586 $\approx_{\textit{abs\_res}}$) will be crucial below: |
625 $\approx_{\textit{abs\_res}}$) will be crucial below: |
587 |
626 |
588 \begin{lemma} |
627 \begin{lemma} |
589 @{thm[mode=IfThen] alpha_abs_swap[no_vars]} |
628 @{thm[mode=IfThen] abs_swap1(1)[no_vars]} |
590 \end{lemma} |
629 \end{lemma} |
591 |
630 |
592 \begin{proof} |
631 \begin{proof} |
593 This lemma is straightforward by observing that the assumptions give us |
632 This lemma is straightforward by observing that the assumptions give us |
594 @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp} |
633 @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp} |
595 is equivariant. |
634 is equivariant. |
596 \end{proof} |
635 \end{proof} |
597 |
|
598 \noindent |
|
599 We are also define the following |
|
600 |
|
601 @{text "aux (as, x) \<equiv> supp x - as"} |
|
602 |
|
603 |
|
604 |
|
605 \noindent |
|
606 This allows us to use our quotient package and introduce new types |
|
607 @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"} |
|
608 representing the alpha-equivalence classes. Elements in these types |
|
609 we will, respectively, write as: |
|
610 |
|
611 \begin{center} |
|
612 @{term "Abs as x"} \hspace{5mm} |
|
613 @{term "Abs_lst as x"} \hspace{5mm} |
|
614 @{term "Abs_res as x"} |
|
615 \end{center} |
|
616 |
|
617 |
636 |
618 \begin{lemma} |
637 \begin{lemma} |
619 $supp ([as]set. x) = supp x - as$ |
638 $supp ([as]set. x) = supp x - as$ |
620 \end{lemma} |
639 \end{lemma} |
621 *} |
640 *} |