--- 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}
*}
--- 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%
--- 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"
*)