nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:8035515bbbc6
+:ad725de6e39b
 text {*
 The first step in a quotient constructions is to take a name for the new
 type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
 raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
 construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
-bool"}. Given this data, we can automatically declare the quotient type as
+bool"}. The user-visible part of the declaration is therefore
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
+\end{isabelle}
+\noindent
+and a proof that @{text "R"} is indeed an equivalence relation.
+Given this data, we can internally declare the quotient type as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
 \end{isabelle}
 \noindent
-being the set of equivalence classes of @{text "R"}. The restriction in this declaration
+being the (non-empty) set of equivalence classes of @{text "R"}. The
-is that the type variables in the raw type @{text "\<sigma>"} must be included in the
+restriction in this declaration is that the type variables in the raw type
-type variables @{text "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us
+@{text "\<sigma>"} must be included in the type variables @{text "\<alpha>s"} declared for
-with abstraction and representation functions having the type
+@{text "\<kappa>\<^isub>q"}. HOL will provide us with abstraction and
+representation functions having the type
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
 \end{isabelle}
 \noindent
-relating the new quotient type and raw type. However, as Homeier noted, it is easier
+and relating the new quotient type and equivalence classes of the raw
-to work with the following derived definitions
+type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
+to work with the following derived abstraction and representation functions
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
 \end{isabelle}
 \noindent
-on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"}. With these
+on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
-definitions the abstraction and representation functions relate directly the
+definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the quotient type
-quotient and raw types (their type is  @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+and the raw type directly, as can be seen from their type, namely @{text "\<sigma>
-respectively). We can show that the property
+\<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"}, respectively.  Given that
+@{text "R"} is an equivalence relation, the following property
 @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
 \noindent
 holds (for the proof see \cite{Homeier05}).
+The next step is to lift definitions over the raw type to definitions over the
+quotient type. For this we providing the declaration
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}
+\end{isabelle}
 To define a constant on the lifted type, an aggregate abstraction
 function is applied to the raw constant. Below we describe the operation
 that generates
 an aggregate @{term "Abs"} or @{term "Rep"} function given the
 \noindent
 where we already performed some @{text "\<beta>"}-simplifications. In our implementation
 we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"},
 namely @{term "map id = id"} and
-@{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstarction function
+@{text "f \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
 @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 \noindent
 which we can use for defining @{term "fconcat"} as follows
 obtaining a list and applies @{term abs_fset} obtaining the composed
 finite set.
 For every type map function we require the property that @{term "map id = id"}.
 With this we can compactify the term, removing the identity mappings,
-obtaining a definition that is the same as the one privided by Homeier
+obtaining a definition that is the same as the one provided by Homeier
 in the cases where the internal type does not change.
 {\it we should be able to prove}
 \begin{lemma}

changeset 2235	ad725de6e39b
parent 2234	8035515bbbc6
child 2236	b8dda31890ff