# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1328863679 -3600
# Node ID f1201fac73980db5aec5fdff478fd721744c85a6
# Parent  f37da60a8cc63c883eaa01d2e66698e6214f45e8
more specification of the quotient package in IsarRef

diff -r f37da60a8cc6 -r f1201fac7398 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 10 09:02:51 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 10 09:47:59 2012 +0100
@@ -1272,6 +1272,7 @@
     @{method_def (HOL) "regularize"} & : & @{text method} \\
     @{method_def (HOL) "injection"} & : & @{text method} \\
     @{method_def (HOL) "cleaning"} & : & @{text method} \\
+    @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\
     @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
     @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
     @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
@@ -1366,6 +1367,17 @@
     local theory store and used by the @{method (HOL) "injection"}
     and @{method (HOL) "cleaning"} methods respectively.
 
+  \item @{attribute (HOL) quot_thm} declares that a certain theorem
+    is a quotient extension theorem. Quotient extension theorems
+    allow for quotienting inside container types. Given a polymorphic
+    type that serves as a container, a map function defined for this
+    container  using @{command (HOL) "enriched_type"} and a relation
+    map defined for for the container type, the quotient extension
+    theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
+    (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
+    are stored in a database and are used all the steps of lifting
+    theorems.
+
   \end{description}
 
 *}
diff -r f37da60a8cc6 -r f1201fac7398 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 10 09:02:51 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 10 09:47:59 2012 +0100
@@ -1789,6 +1789,7 @@
     \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\
     \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\
     \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\
+    \indexdef{HOL}{attribute}{quot\_thm}\hypertarget{attribute.HOL.quot-thm}{\hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}}} & : & \isa{attribute} \\
     \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\
     \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\
     \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\
@@ -1941,6 +1942,16 @@
     local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}
     and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively.
 
+  \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem
+    is a quotient extension theorem. Quotient extension theorems
+    allow for quotienting inside container types. Given a polymorphic
+    type that serves as a container, a map function defined for this
+    container  using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
+    map defined for for the container type, the quotient extension
+    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
+    are stored in a database and are used all the steps of lifting
+    theorems.
+
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r f37da60a8cc6 -r f1201fac7398 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 10 09:02:51 2012 +0100
+++ b/src/HOL/List.thy	Fri Feb 10 09:47:59 2012 +0100
@@ -3372,7 +3372,7 @@
 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
 by (induct xs) auto
 
-(* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
+(* Needs count:: 'a \<Rightarrow> 'a list \<Rightarrow> nat
 lemma length_removeAll:
   "length(removeAll x xs) = length xs - count x xs"
 *)