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

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

   164   for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11}

   164   for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11}

   165   makes the formal

   165   makes the formal

   166   proof of the substitution lemma almost trivial.

   166   proof of the substitution lemma almost trivial.

   167 

   167 

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

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

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

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

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

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

   171   from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}

   174   from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}

   172   (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting

   175   (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting

   329   definitions that specify the input and output data of our three-step

   332   definitions that specify the input and output data of our three-step

   330   lifting procedure. Appendix A gives an example how our quotient

   333   lifting procedure. Appendix A gives an example how our quotient

   331   package works in practise.

   334   package works in practise.

   332 *}

   335 *}

   333 

   336 

   335 

   338 

   336 text {*

   339 text {*

   337   \noindent

   340   \noindent

   338   We will give in this section a crude overview of HOL and describe the main

   341   We will give in this section a crude overview of HOL and describe the main

   339   definitions given by Homeier for quotients \cite{Homeier05}.

   342   definitions given by Homeier for quotients \cite{Homeier05}.

   496                   & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\

   499                   & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\

   497   \end{tabular}

   500   \end{tabular}

   498   \end{isabelle}

   501   \end{isabelle}

   499 *}

   502 *}

   500 

   503 

   502 

   505 

   503 text {*

   506 text {*

   504   \noindent

   507   \noindent

   505   The first step in a quotient construction is to take a name for the new

   508   The first step in a quotient construction is to take a name for the new

   506   type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},

   509   type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},

   756   equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with

   759   equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with

   757   @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed

   760   @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed

   758   \end{proof}

   761   \end{proof}

   759 *}

   762 *}

   760 

   763 

   762 

   765 

   763 text {*

   766 text {*

   764   \noindent

   767   \noindent

   765   The main point of the quotient package is to automatically ``lift'' theorems

   768   The main point of the quotient package is to automatically ``lift'' theorems

   766   involving constants over the raw type to theorems involving constants over

   769   involving constants over the raw type to theorems involving constants over