nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:36c9d9e658c7
+:42d576c54704
 notation (latex output)
 rel_conj ("_ OOO _" [53, 53] 52) and
 "op -->" (infix "\<rightarrow>" 100) and
 "==>" (infix "\<Rightarrow>" 100) and
-fun_map ("_ \<^raw:\mbox{\tt{---\textgreater}}> _" 51) and
+fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
-fun_rel ("_ \<^raw:\mbox{\tt{===\textgreater}}> _" 51) and
+fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
 fempty ("\<emptyset>") and
 funion ("_ \<union> _") and
 finsert ("{_} \<union> _") and
 Cons ("_::_") and
 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
 (*>*)
 section {* Introduction *}
 text {*
 \begin{flushright}
 @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
 \end{eqnarray}
 *}
-section {* Lifting of Definitions *}
+section {* Quotient Types and Lifting of Definitions *}
 (* Say more about containers? *)
 text {*
 maps are known. Such maps for most common types (list, pair, sum,
 option, \ldots) are described in Homeier, and we assume that @{text "map"}
 is the function that returns a map for a given type. Then REP/ABS is defined
 as follows:
-\begin{itemize}
+{\it the first argument is the raw type and the second argument the quotient type}
-\item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
-\item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
-\item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
+\begin{center}
-\item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
+\begin{tabular}{rcl}
-\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
-\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+% type variable case says that variables must be equal...therefore subsumed by the equal case below
-\item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+%
-\item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+%\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\
-\item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+%@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\
-\item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+%@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\
-\end{itemize}
+\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
+@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
+@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
+\multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
+@{text "ABS (\<sigma>\<^isub>1 \<rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+@{text "REP (\<sigma>\<^isub>1 \<rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
+@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "\<kappa>_map (ABS (\<sigma>s, \<tau>s))"}\\
+@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "\<kappa>_map (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
+@{text "ABS (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>2_Abs \<circ> \<kappa>\<^isub>1_map (ABS (\<sigma>s', \<tau>s'))"}\\
+@{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "\<kappa>\<^isub>1_map (REP (\<sigma>s', \<tau>s')) \<circ> \<kappa>\<^isub>2_Rep"}\\
+\end{tabular}
+\end{center}
+\begin{center}
+\begin{tabular}{rcl}
+@{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"}\\
+@{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n) \<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m) \<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"}\\
+provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+\end{tabular}
+\end{center}
 Apart from the last 2 points the definition is same as the one implemented in
 in Homeier's HOL package. Adding composition in last two cases is necessary
 for compositional quotients. We ilustrate the different behaviour of the
 definition by showing the derived definition of @{term fconcat}:
 The aggregate @{term Abs} function takes a finite set of finite sets
 and applies @{term "map rep_fset"} composed with @{term rep_fset} to
 its input, obtaining a list of lists, passes the result to @{term concat}
 obtaining a list and applies @{term abs_fset} obtaining the composed
 finite set.
+{\it we can compactify the term by noticing that map id\ldots id = id}
+{\it we should be able to prove}
+\begin{lemma}
+If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
+and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
+then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
+@{text "\<tau> \<Rightarrow> \<sigma>"}.
+\end{lemma}
 *}
 subsection {* Respectfulness *}
 text {*
 @{thm [display] quotient_compose_list[no_vars]}
 *}
-section {* Lifting Theorems *}
+section {* Lifting of Theorems *}
 text {*
 The core of the quotient package takes an original theorem that
 talks about the raw types, and the statement of the theorem that
 it is supposed to produce. This is different from other existing
 \end{itemize}
 *}
 (*<*)
 end
 (*>*)

changeset 2227	42d576c54704
parent 2226	36c9d9e658c7
child 2228	a827d36fa467