more specification of the quotient package in IsarRef
authorCezary Kaliszyk <cezarykaliszyk@gmail.com>
Fri Feb 10 09:47:59 2012 +0100 (2012-02-10)
changeset 46448f1201fac7398
parent 46447 f37da60a8cc6
child 46449 312b49fba357
more specification of the quotient package in IsarRef
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
src/HOL/List.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 10 09:02:51 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 10 09:47:59 2012 +0100
     1.3 @@ -1272,6 +1272,7 @@
     1.4      @{method_def (HOL) "regularize"} & : & @{text method} \\
     1.5      @{method_def (HOL) "injection"} & : & @{text method} \\
     1.6      @{method_def (HOL) "cleaning"} & : & @{text method} \\
     1.7 +    @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\
     1.8      @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
     1.9      @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
    1.10      @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
    1.11 @@ -1366,6 +1367,17 @@
    1.12      local theory store and used by the @{method (HOL) "injection"}
    1.13      and @{method (HOL) "cleaning"} methods respectively.
    1.14  
    1.15 +  \item @{attribute (HOL) quot_thm} declares that a certain theorem
    1.16 +    is a quotient extension theorem. Quotient extension theorems
    1.17 +    allow for quotienting inside container types. Given a polymorphic
    1.18 +    type that serves as a container, a map function defined for this
    1.19 +    container  using @{command (HOL) "enriched_type"} and a relation
    1.20 +    map defined for for the container type, the quotient extension
    1.21 +    theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
    1.22 +    (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
    1.23 +    are stored in a database and are used all the steps of lifting
    1.24 +    theorems.
    1.25 +
    1.26    \end{description}
    1.27  
    1.28  *}
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 10 09:02:51 2012 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 10 09:47:59 2012 +0100
     2.3 @@ -1789,6 +1789,7 @@
     2.4      \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\
     2.5      \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\
     2.6      \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\
     2.7 +    \indexdef{HOL}{attribute}{quot\_thm}\hypertarget{attribute.HOL.quot-thm}{\hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}}} & : & \isa{attribute} \\
     2.8      \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\
     2.9      \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\
    2.10      \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\
    2.11 @@ -1941,6 +1942,16 @@
    2.12      local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}
    2.13      and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively.
    2.14  
    2.15 +  \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem
    2.16 +    is a quotient extension theorem. Quotient extension theorems
    2.17 +    allow for quotienting inside container types. Given a polymorphic
    2.18 +    type that serves as a container, a map function defined for this
    2.19 +    container  using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
    2.20 +    map defined for for the container type, the quotient extension
    2.21 +    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
    2.22 +    are stored in a database and are used all the steps of lifting
    2.23 +    theorems.
    2.24 +
    2.25    \end{description}%
    2.26  \end{isamarkuptext}%
    2.27  \isamarkuptrue%
     3.1 --- a/src/HOL/List.thy	Fri Feb 10 09:02:51 2012 +0100
     3.2 +++ b/src/HOL/List.thy	Fri Feb 10 09:47:59 2012 +0100
     3.3 @@ -3372,7 +3372,7 @@
     3.4  lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
     3.5  by (induct xs) auto
     3.6  
     3.7 -(* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
     3.8 +(* Needs count:: 'a \<Rightarrow> 'a list \<Rightarrow> nat
     3.9  lemma length_removeAll:
    3.10    "length(removeAll x xs) = length xs - count x xs"
    3.11  *)