# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276394766 -7200
# Node ID 42d576c547047c62e983c5e1a4bf7b7be4269e63
# Parent  36c9d9e658c756dc0c9a2f5658b8acd9f85e9c05
polishing of ABS/REP

diff -r 36c9d9e658c7 -r 42d576c54704 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sat Jun 12 11:32:36 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 04:06:06 2010 +0200
@@ -11,8 +11,8 @@
   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_rel ("_ \<^raw:\mbox{\tt{===\textgreater}}> _" 51) and
+  fun_map ("_ \<^raw:\mbox{\singlearr}> _" 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
@@ -41,6 +41,7 @@
 *}
 (*>*)
 
+
 section {* Introduction *}
 
 text {* 
@@ -294,7 +295,7 @@
 
 *}
 
-section {* Lifting of Definitions *}
+section {* Quotient Types and Lifting of Definitions *}
 
 (* Say more about containers? *)
 
@@ -314,18 +315,40 @@
   is the function that returns a map for a given type. Then REP/ABS is defined
   as follows:
 
-  \begin{itemize}
-  \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"}
-  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
-  \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)"}
-  \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))"}
-  \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"}
-  \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"}
-  \end{itemize}
+  {\it the first argument is the raw type and the second argument the quotient type}
+
+
+  \begin{center}
+  \begin{tabular}{rcl}
+
+  % type variable case says that variables must be equal...therefore subsumed by the equal case below
+  %
+  %\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\ 
+  %@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\
+  %@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\
+
+  \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
@@ -339,6 +362,17 @@
   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 *}
@@ -450,7 +484,7 @@
 *}
 
 
-section {* Lifting Theorems *}
+section {* Lifting of Theorems *}
 
 text {*
   The core of the quotient package takes an original theorem that
@@ -763,6 +797,7 @@
 *}
 
 
+
 (*<*)
 end
 (*>*)
diff -r 36c9d9e658c7 -r 42d576c54704 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Sat Jun 12 11:32:36 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Sun Jun 13 04:06:06 2010 +0200
@@ -8,16 +8,24 @@
 \usepackage{pdfsetup}
 \usepackage{tikz}
 \usepackage{pgf}
+\usepackage{verbdef}
 
 \urlstyle{rm}
 \isabellestyle{it}
 \renewcommand{\isastyle}{\isastyleminor}
 
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\verbdef\singlearr|--->|
+\verbdef\doublearr|===>|
+
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
+
+\newcommand{\isasymsinglearr}{\singlearr}
+\newcommand{\isasymdoublearr}{\doublearr}
+
 \begin{document}
 
 \title{Quotients Revisited for Isabelle/HOL}