Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Paper/Paper.thy
changeset 2471 894599a50af3
parent 2465 07ffa4e41659
child 2488 1c18f2cf3923
equal deleted inserted replaced
2470:bdb1eab47161 2471:894599a50af3 
    19   fresh ("_ # _" [51, 51] 50) and
 
    19   fresh ("_ # _" [51, 51] 50) and
 
    20   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
 
    20   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
 
    21   supp ("supp _" [78] 73) and
 
    21   supp ("supp _" [78] 73) and
 
    22   uminus ("-_" [78] 73) and
 
    22   uminus ("-_" [78] 73) and
 
    23   If  ("if _ then _ else _" 10) and
 
    23   If  ("if _ then _ else _" 10) and
 
    24   alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
 
    24   alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
 
    25   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
 
    26   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
 
    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 ("fa'(_')" [100] 100) and
 
    29   fv ("fa'(_')" [100] 100) and
 
    30   equal ("=") and
 
    30   equal ("=") and
 
    31   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
    31   alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
    32   Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
 
    32   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
 
    33   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
 
    33   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
 
    34   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
 
    34   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
 
    35   Abs_res ("[_]\<^bsub>res\<^esub>._") and
 
    35   Abs_res ("[_]\<^bsub>res\<^esub>._") and
 
    36   Abs_print ("_\<^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_set ("aux _" [1000] 10) and
 
    39   alpha_bn ("_ \<approx>bn _")
 
    39   alpha_bn ("_ \<approx>bn _")
 
    40 
    40 
    41 consts alpha_trm ::'a
 
    41 consts alpha_trm ::'a
 
    42 consts fa_trm :: 'a
 
    42 consts fa_trm :: 'a
 
    43 consts alpha_trm2 ::'a
 
    43 consts alpha_trm2 ::'a
 
   645   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
 
   645   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
 
   646   requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
 
   646   requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
 
   647   %
 
   647   %
 
   648   \begin{equation}\label{alphaset}
 
   648   \begin{equation}\label{alphaset}
 
   649   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
 
   649   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
 
   650   \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
 
   650   \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
 
   651               & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
 
   651               & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
 
   652   @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
 
   652   @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
 
   653   @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
 
   653   @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
 
   654   @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
   654   @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
   655   \end{array}
 
   655   \end{array}
 
   728 
   728 
   729   In the rest of this section we are going to introduce three abstraction 
   729   In the rest of this section we are going to introduce three abstraction 
   730   types. For this we define 
   730   types. For this we define 
   731   %
 
   731   %
 
   732   \begin{equation}
 
   732   \begin{equation}
 
   733   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
 
   733   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
 
   734   \end{equation}
 
   734   \end{equation}
 
   735   
   735   
   736   \noindent
 
   736   \noindent
 
   737   (similarly for $\approx_{\,\textit{abs\_res}}$ 
   737   (similarly for $\approx_{\,\textit{abs\_res}}$ 
   738   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
   738   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
   760   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
 
   760   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
 
   761   (in the third case). 
   761   (in the third case). 
   762   The elements in these types will be, respectively, written as:
 
   762   The elements in these types will be, respectively, written as:
 
   763 
   763 
   764   \begin{center}
 
   764   \begin{center}
 
   765   @{term "Abs as x"} \hspace{5mm} 
   765   @{term "Abs_set as x"} \hspace{5mm} 
   766   @{term "Abs_res as x"} \hspace{5mm}
 
   766   @{term "Abs_res as x"} \hspace{5mm}
 
   767   @{term "Abs_lst as x"} 
   767   @{term "Abs_lst as x"} 
   768   \end{center}
 
   768   \end{center}
 
   769 
   769 
   770   \noindent
 
   770   \noindent
 
   830   Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
   830   Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
   831   it, we use a trick from \cite{Pitts04} and first define an auxiliary 
   831   it, we use a trick from \cite{Pitts04} and first define an auxiliary 
   832   function @{text aux}, taking an abstraction as argument:
 
   832   function @{text aux}, taking an abstraction as argument:
 
   833   %
 
   833   %
 
   834   \begin{center}
 
   834   \begin{center}
 
   835   @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
 
   835   @{thm supp_set.simps[THEN eq_reflection, no_vars]}
 
   836   \end{center}
 
   836   \end{center}
 
   837   
   837   
   838   \noindent
 
   838   \noindent
 
   839   Using the second equation in \eqref{equivariance}, we can show that 
   839   Using the second equation in \eqref{equivariance}, we can show that 
   840   @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
 
   840   @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
 
   841   (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. 
   841   (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. 
   842   This in turn means
 
   842   This in turn means
 
   843   %
 
   843   %
 
   844   \begin{center}
 
   844   \begin{center}
 
   845   @{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
 
   845   @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
 
   846   \end{center}
 
   846   \end{center}
 
   847 
   847 
   848   \noindent
 
   848   \noindent
 
   849   using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
 
   849   using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
 
   850   we further obtain
 
   850   we further obtain
 
   858   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 
   858   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 
   859   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
   859   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
   860   Theorem~\ref{suppabs}. 
   860   Theorem~\ref{suppabs}. 
   861 
   861 
   862   The method of first considering abstractions of the
 
   862   The method of first considering abstractions of the
 
   863   form @{term "Abs as x"} etc is motivated by the fact that 
   863   form @{term "Abs_set as x"} etc is motivated by the fact that 
   864   we can conveniently establish  at the Isabelle/HOL level
 
   864   we can conveniently establish  at the Isabelle/HOL level
 
   865   properties about them.  It would be
 
   865   properties about them.  It would be
 
   866   laborious to write custom ML-code that derives automatically such properties 
   866   laborious to write custom ML-code that derives automatically such properties 
   867   for every term-constructor that binds some atoms. Also the generality of
 
   867   for every term-constructor that binds some atoms. Also the generality of
 
   868   the definitions for $\alpha$-equivalence will help us in the next section.
 
   868   the definitions for $\alpha$-equivalence will help us in the next section.
 
  1487   \noindent
 
  1487   \noindent
 
  1488   Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This 
  1488   Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This 
  1489   lets us formally define the premise @{text P} for a non-empty binding clause as:
 
  1489   lets us formally define the premise @{text P} for a non-empty binding clause as:
 
  1490   %
 
  1490   %
 
  1491   \begin{center}
 
  1491   \begin{center}
 
  1492   \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
 
  1492   \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
 
  1493   \end{center}
 
  1493   \end{center}
 
  1494 
  1494 
  1495   \noindent
 
  1495   \noindent
 
  1496   This premise accounts for $\alpha$-equivalence of the bodies of the binding
 
  1496   This premise accounts for $\alpha$-equivalence of the bodies of the binding
 
  1497   clause. 
  1497   clause.
nominal2