121   over the structure of terms. This can be fiendishly complicated (see

   121   over the structure of terms. This can be fiendishly complicated (see

   122   \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof

   122   \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof

   123   about raw lambda-terms). In contrast, if we reason about

   123   about raw lambda-terms). In contrast, if we reason about

   124   $\alpha$-equated lambda-terms, that means terms quotient according to

   124   $\alpha$-equated lambda-terms, that means terms quotient according to

   125   $\alpha$-equivalence, then the reasoning infrastructure provided, 

   125   $\alpha$-equivalence, then the reasoning infrastructure provided, 

   127   proof of the substitution lemma almost trivial. 

   128   proof of the substitution lemma almost trivial. 

   128 

   129 

   129   The difficulty is that in order to be able to reason about integers, finite

   130   The difficulty is that in order to be able to reason about integers, finite

   130   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning

   131   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning

   131   infrastructure by transferring, or \emph{lifting}, definitions and theorems

   132   infrastructure by transferring, or \emph{lifting}, definitions and theorems

   643   example about @{term "concat"} and @{term "fconcat"}, where we have the raw type

   644   example about @{term "concat"} and @{term "fconcat"}, where we have the raw type

   644   @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>

   645   @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>

   645   fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)

   646   fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)

   646   the abstraction function

   647   the abstraction function

   647 

   648 

   649   \begin{tabular}{l}

   650   \begin{tabular}{l}

   650   @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\

   651   @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\

   651   \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}

   652   \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}

   652   \end{tabular}

   653   \end{tabular}

   653   \end{isabelle}

   654   \end{isabelle}

   845 

   846 

   846 %%% Cezary: I think this would be a nice thing to do but we have not

   847 %%% Cezary: I think this would be a nice thing to do but we have not

   847 %%% done it, the theorems need to be 'guessed' from the remaining obligations

   848 %%% done it, the theorems need to be 'guessed' from the remaining obligations

   848 

   849 

   849   \begin{isabelle}\ \ \ \ \ %%%

   850   \begin{isabelle}\ \ \ \ \ %%%

   851   \end{isabelle}

   852   \end{isabelle}

   852 

   853 

   853   \noindent

   854   \noindent

   854   where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.

   855   where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.

   855   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 

   856   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 

   857   \begin{isabelle}\ \ \ \ \ %%%

   858   \begin{isabelle}\ \ \ \ \ %%%

   858   @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}

   859   @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}

   859   \end{isabelle}

   860   \end{isabelle}

   860 

   861 

   861   \noindent

   862   \noindent

   863   an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated

   864   an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated

   864   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,

   865   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,

   865   then we need to show this preservation property.

   866   then we need to show this preservation property.

   866 

   867 

   867   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}

   868   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}

  1243 

  1244 

  1244 text {*

  1245 text {*

  1245 

  1246 

  1246   \noindent

  1247   \noindent

  1247   The code of the quotient package and the examples described here are already

  1248   The code of the quotient package and the examples described here are already

  1250   heavily used in the new version of Nominal Isabelle, which provides a

  1252   heavily used in the new version of Nominal Isabelle, which provides a

  1251   convenient reasoning infrastructure for programming language calculi

  1253   convenient reasoning infrastructure for programming language calculi

  1252   involving general binders.  To achieve this, it builds types representing

  1254   involving general binders.  To achieve this, it builds types representing

  1253   @{text \<alpha>}-equivalent terms.  Earlier versions of Nominal Isabelle have been

  1255   @{text \<alpha>}-equivalent terms.  Earlier versions of Nominal Isabelle have been

  1254   used successfully in formalisations of an equivalence checking algorithm for

  1256   used successfully in formalisations of an equivalence checking algorithm for

  1295 %%

  1297 %%

  1296 %% give an example for this

  1298 %% give an example for this

  1297 %%

  1299 %%

  1298   \medskip

  1300   \medskip

  1299 

  1301 

  1305 

  1307 

  1306 *}

  1308 *}

  1307 

  1309 

  1308 

  1310 

  1309 

  1311