# HG changeset patch # User wenzelm # Date 1333468096 -7200 # Node ID 610d9c212376216d33df1355799155bf11bbe400 # Parent 9d02327ede5617319dbfd1b273461ade9f8294f7# Parent c82a0b2606a128980fb8fcea43bcd4c4dabc0d22 merged diff -r c82a0b2606a1 -r 610d9c212376 Admin/isatest/isatest-settings --- a/Admin/isatest/isatest-settings Tue Apr 03 17:21:33 2012 +0200 +++ b/Admin/isatest/isatest-settings Tue Apr 03 17:48:16 2012 +0200 @@ -25,7 +25,8 @@ hoelzl@in.tum.de \ krauss@in.tum.de \ noschinl@in.tum.de \ -kuncar@in.tum.de" +kuncar@in.tum.de \ +ns441@cam.ac.uk" LOGPREFIX=$HOME/log MASTERLOG=$LOGPREFIX/isatest.log diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Makefile --- a/doc-src/ProgProve/Makefile Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Makefile Tue Apr 03 17:48:16 2012 +0200 @@ -10,7 +10,7 @@ NAME = prog-prove FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \ - svmono.cls mathpartir.sty isabelle.sty isabellesym.sty + svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy dvi: $(NAME).dvi diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/Basics.thy --- a/doc-src/ProgProve/Thys/Basics.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/Basics.thy Tue Apr 03 17:48:16 2012 +0200 @@ -136,10 +136,13 @@ single identifier can be dropped. When Isabelle prints a syntax error message, it refers to the HOL syntax as the \concept{inner syntax} and the enclosing theory language as the \concept{outer syntax}. +\sem \begin{warn} For reasons of readability, we almost never show the quotation marks in this book. Consult the accompanying theory files to see where they need to go. \end{warn} +\endsem +% *} (*<*) end diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/Bool_nat_list.thy --- a/doc-src/ProgProve/Thys/Bool_nat_list.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy Tue Apr 03 17:48:16 2012 +0200 @@ -158,13 +158,19 @@ done declare [[names_short]] (*>*) -datatype 'a list = Nil | Cons "'a" "('a list)" +datatype 'a list = Nil | Cons 'a "'a list" -text{* This means that all lists are built up from @{const Nil}, the empty -list, and @{const Cons}, the operation of putting an element in front of a -list. Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"}, +text{* +\begin{itemize} +\item Type @{typ "'a list"} is the type of list over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type). +\item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}). +Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"}, or @{term"Cons x (Cons y Nil)"} etc. - +\item \isacom{datatype} requires no quotation marks on the +left-hand side, but on the right-hand side each of the argument +types of a constructor needs to be enclosed in quotation marks, unless +it is just an identifier (e.g.\ @{typ nat} or @{typ 'a}). +\end{itemize} We also define two standard functions, append and reverse: *} fun app :: "'a list \ 'a list \ 'a list" where @@ -189,11 +195,12 @@ text{* yields @{value "rev(Cons a (Cons b Nil))"}. \medskip -Figure~\ref{fig:MyList} shows the theory created so far. Notice where the -quotations marks are needed that we mostly sweep under the carpet. In -particular, notice that \isacom{datatype} requires no quotation marks on the -left-hand side, but that on the right-hand side each of the argument -types of a constructor needs to be enclosed in quotation marks. +Figure~\ref{fig:MyList} shows the theory created so far. +% Notice where the +%quotations marks are needed that we mostly sweep under the carpet. In +%particular, notice that \isacom{datatype} requires no quotation marks on the +%left-hand side, but that on the right-hand side each of the argument +%types of a constructor needs to be enclosed in quotation marks. \begin{figure}[htbp] \begin{alltt} @@ -380,10 +387,11 @@ @{text"length :: 'a list \ nat"} (with the obvious definition), and the map function that applies a function to all elements of a list: \begin{isabelle} -\isacom{fun} @{text "map :: ('a \ 'b) \ 'a list \ 'b list"}\\ -@{thm map.simps(1)} @{text"|"}\\ -@{thm map.simps(2)} +\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \ 'b) \ 'a list \ 'b list"}\\ +@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\ +@{text"\""}@{thm map.simps(2)}@{text"\""} \end{isabelle} +\sem Also useful are the \concept{head} of a list, its first element, and the \concept{tail}, the rest of the list: \begin{isabelle} @@ -398,6 +406,8 @@ Note that since HOL is a logic of total functions, @{term"hd []"} is defined, but we do now know what the result is. That is, @{term"hd []"} is not undefined but underdefined. +\endsem +% *} (*<*) end diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/Isar.thy --- a/doc-src/ProgProve/Thys/Isar.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/Isar.thy Tue Apr 03 17:48:16 2012 +0200 @@ -178,7 +178,7 @@ \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} Lemmas can also be stated in a more structured fashion. To demonstrate this -feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\ surj f"}} +feature with Cantor's theorem, we rephrase @{prop"\ surj f"} a little: *} @@ -190,7 +190,8 @@ txt{* The optional \isacom{fixes} part allows you to state the types of variables up front rather than by decorating one of their occurrences in the formula with a type constraint. The key advantage of the structured format is -the \isacom{assumes} part that allows you to name each assumption. The +the \isacom{assumes} part that allows you to name each assumption; multiple +assumptions can be separated by \isacom{and}. The \isacom{shows} part gives the goal. The actual theorem that will come out of the proof is @{prop"surj f \ False"}, but during the proof the assumption @{prop"surj f"} is available under the name @{text s} like any other fact. @@ -393,7 +394,8 @@ text_raw{* \begin{isamarkuptext}% -How to prove set equality and subset relationship: + +Finally, how to prove set equality and subset relationship: \end{isamarkuptext}% \begin{tabular}{@ {}ll@ {}} \begin{minipage}[t]{.4\textwidth} @@ -544,7 +546,7 @@ \subsection{Raw proof blocks} -Sometimes one would like to prove some lemma locally with in a proof. +Sometimes one would like to prove some lemma locally within a proof. A lemma that shares the current context of assumptions but that has its own assumptions and is generalised over its locally fixed variables at the end. This is what a \concept{raw proof block} does: @@ -745,7 +747,7 @@ \begin{quote} \isacom{fix} @{text n}\\ \isacom{assume} @{text"Suc:"} - \begin{tabular}[t]{l}@{text"A(n) \ P(n)"}\\@{text"A(Suc n)"}\end{tabular}\\ + \begin{tabular}[t]{l}@{text"\"A(n) \ P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\ \isacom{let} @{text"?case = \"P(Suc n)\""} \end{quote} The list of assumptions @{text Suc} is actually subdivided @@ -812,8 +814,8 @@ ~\\ \isacom{fix} @{text n}\\ \isacom{assume} @{text"evSS:"} - \begin{tabular}[t]{l} @{text"ev n"}\\@{text"even n"}\end{tabular}\\ -\isacom{let} @{text"?case = even(Suc(Suc n))"}\\ + \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\ +\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\ \end{minipage} \end{tabular} \medskip diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/Logic.thy --- a/doc-src/ProgProve/Thys/Logic.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/Logic.thy Tue Apr 03 17:48:16 2012 +0200 @@ -438,7 +438,7 @@ inductive ev :: "nat \ bool" where ev0: "ev 0" | evSS: (*<*)"ev n \ ev (Suc(Suc n))"(*>*) -text_raw{* @{prop"ev n \ ev (n + 2)"} *} +text_raw{* @{prop[source]"ev n \ ev (n + 2)"} *} text{* To get used to inductive definitions, we will first prove a few properties of @{const ev} informally before we descend to the Isabelle level. diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/MyList.thy --- a/doc-src/ProgProve/Thys/MyList.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/MyList.thy Tue Apr 03 17:48:16 2012 +0200 @@ -2,7 +2,7 @@ imports Main begin -datatype 'a list = Nil | Cons "'a" "('a list)" +datatype 'a list = Nil | Cons 'a "'a list" fun app :: "'a list => 'a list => 'a list" where "app Nil ys = ys" | diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/Types_and_funs.thy --- a/doc-src/ProgProve/Thys/Types_and_funs.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/Types_and_funs.thy Tue Apr 03 17:48:16 2012 +0200 @@ -55,7 +55,7 @@ As an example, consider binary trees: *} -datatype 'a tree = Tip | Node "('a tree)" 'a "('a tree)" +datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" text{* with a mirror function: *} @@ -86,8 +86,8 @@ done (*>*) fun lookup :: "('a * 'b) list \ 'a \ 'b option" where -"lookup [] x' = None" | -"lookup ((x,y) # ps) x' = (if x = x' then Some y else lookup ps x')" +"lookup [] x = None" | +"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)" text{* Note that @{text"\\<^isub>1 * \\<^isub>2"} is the type of pairs, also written @{text"\\<^isub>1 \ \\<^isub>2"}. diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/document/Basics.tex --- a/doc-src/ProgProve/Thys/document/Basics.tex Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Basics.tex Tue Apr 03 17:48:16 2012 +0200 @@ -147,10 +147,13 @@ single identifier can be dropped. When Isabelle prints a syntax error message, it refers to the HOL syntax as the \concept{inner syntax} and the enclosing theory language as the \concept{outer syntax}. +\sem \begin{warn} For reasons of readability, we almost never show the quotation marks in this book. Consult the accompanying theory files to see where they need to go. -\end{warn}% +\end{warn} +\endsem +%% \end{isamarkuptext}% \isamarkuptrue% % diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/document/Bool_nat_list.tex --- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Tue Apr 03 17:48:16 2012 +0200 @@ -216,13 +216,18 @@ % \endisadelimproof \isacommand{datatype}\isamarkupfalse% -\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}% \begin{isamarkuptext}% -This means that all lists are built up from \isa{Nil}, the empty -list, and \isa{Cons}, the operation of putting an element in front of a -list. Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil}, +\begin{itemize} +\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of list over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type). +\item Lists have two constructors: \isa{Nil}, the empty list, and \isa{Cons}, which puts an element (of type \isa{{\isaliteral{27}{\isacharprime}}a}) in front of a list (of type \isa{{\isaliteral{27}{\isacharprime}}a\ list}). +Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil}, or \isa{Cons\ x\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ Nil{\isaliteral{29}{\isacharparenright}}} etc. - +\item \isacom{datatype} requires no quotation marks on the +left-hand side, but on the right-hand side each of the argument +types of a constructor needs to be enclosed in quotation marks, unless +it is just an identifier (e.g.\ \isa{nat} or \isa{{\isaliteral{27}{\isacharprime}}a}). +\end{itemize} We also define two standard functions, append and reverse:% \end{isamarkuptext}% \isamarkuptrue% @@ -254,11 +259,12 @@ yields \isa{Cons\ b\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}}. \medskip -Figure~\ref{fig:MyList} shows the theory created so far. Notice where the -quotations marks are needed that we mostly sweep under the carpet. In -particular, notice that \isacom{datatype} requires no quotation marks on the -left-hand side, but that on the right-hand side each of the argument -types of a constructor needs to be enclosed in quotation marks. +Figure~\ref{fig:MyList} shows the theory created so far. +% Notice where the +%quotations marks are needed that we mostly sweep under the carpet. In +%particular, notice that \isacom{datatype} requires no quotation marks on the +%left-hand side, but that on the right-hand side each of the argument +%types of a constructor needs to be enclosed in quotation marks. \begin{figure}[htbp] \begin{alltt} @@ -551,10 +557,11 @@ \isa{length\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} (with the obvious definition), and the map function that applies a function to all elements of a list: \begin{isabelle} -\isacom{fun} \isa{map\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list}\\ -\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} \isa{{\isaliteral{7C}{\isacharbar}}}\\ -\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs} +\isacom{fun} \isa{map} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{22}{\isachardoublequote}}}\\ +\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{7C}{\isacharbar}}}\\ +\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}\isa{{\isaliteral{22}{\isachardoublequote}}} \end{isabelle} +\sem Also useful are the \concept{head} of a list, its first element, and the \concept{tail}, the rest of the list: \begin{isabelle} @@ -568,7 +575,9 @@ \end{isabelle} Note that since HOL is a logic of total functions, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is defined, but we do now know what the result is. That is, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is not undefined -but underdefined.% +but underdefined. +\endsem +%% \end{isamarkuptext}% \isamarkuptrue% % diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/document/Isar.tex --- a/doc-src/ProgProve/Thys/document/Isar.tex Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Isar.tex Tue Apr 03 17:48:16 2012 +0200 @@ -269,7 +269,7 @@ \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} Lemmas can also be stated in a more structured fashion. To demonstrate this -feature with Cantor's theorem, we rephrase \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f{\isaliteral{22}{\isachardoublequote}}}} +feature with Cantor's theorem, we rephrase \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f} a little:% \end{isamarkuptext}% \isamarkuptrue% @@ -288,7 +288,8 @@ The optional \isacom{fixes} part allows you to state the types of variables up front rather than by decorating one of their occurrences in the formula with a type constraint. The key advantage of the structured format is -the \isacom{assumes} part that allows you to name each assumption. The +the \isacom{assumes} part that allows you to name each assumption; multiple +assumptions can be separated by \isacom{and}. The \isacom{shows} part gives the goal. The actual theorem that will come out of the proof is \isa{surj\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False}, but during the proof the assumption \isa{surj\ f} is available under the name \isa{s} like any other fact.% @@ -672,7 +673,8 @@ \endisadelimproof % \begin{isamarkuptext}% -How to prove set equality and subset relationship: + +Finally, how to prove set equality and subset relationship: \end{isamarkuptext}% \begin{tabular}{@ {}ll@ {}} \begin{minipage}[t]{.4\textwidth} @@ -942,7 +944,7 @@ \subsection{Raw proof blocks} -Sometimes one would like to prove some lemma locally with in a proof. +Sometimes one would like to prove some lemma locally within a proof. A lemma that shares the current context of assumptions but that has its own assumptions and is generalised over its locally fixed variables at the end. This is what a \concept{raw proof block} does: @@ -1307,7 +1309,7 @@ \begin{quote} \isacom{fix} \isa{n}\\ \isacom{assume} \isa{Suc{\isaliteral{3A}{\isacharcolon}}} - \begin{tabular}[t]{l}\isa{A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}}\\\isa{A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}\end{tabular}\\ + \begin{tabular}[t]{l}\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\ \isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \end{quote} The list of assumptions \isa{Suc} is actually subdivided @@ -1399,8 +1401,8 @@ ~\\ \isacom{fix} \isa{n}\\ \isacom{assume} \isa{evSS{\isaliteral{3A}{\isacharcolon}}} - \begin{tabular}[t]{l} \isa{ev\ n}\\\isa{even\ n}\end{tabular}\\ -\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\\ + \begin{tabular}[t]{l} \isa{{\isaliteral{22}{\isachardoublequote}}ev\ n{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}even\ n{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\ +\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ \end{minipage} \end{tabular} \medskip diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/document/Logic.tex --- a/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 03 17:48:16 2012 +0200 @@ -570,7 +570,7 @@ \ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline evSS{\isaliteral{3A}{\isacharcolon}}\ \ % -\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} +\isa{{\isaliteral{22}{\isachardoublequote}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} % \begin{isamarkuptext}% To get used to inductive definitions, we will first prove a few diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/Thys/document/Types_and_funs.tex --- a/doc-src/ProgProve/Thys/document/Types_and_funs.tex Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Types_and_funs.tex Tue Apr 03 17:48:16 2012 +0200 @@ -68,7 +68,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% -\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}% \begin{isamarkuptext}% with a mirror function:% \end{isamarkuptext}% @@ -122,8 +122,8 @@ \endisadelimproof \isacommand{fun}\isamarkupfalse% \ lookup\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ then\ Some\ y\ else\ lookup\ ps\ x{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ a\ {\isaliteral{3D}{\isacharequal}}\ x\ then\ Some\ b\ else\ lookup\ ps\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% \begin{isamarkuptext}% Note that \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} is the type of pairs, also written \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. diff -r c82a0b2606a1 -r 610d9c212376 doc-src/ProgProve/prelude.tex --- a/doc-src/ProgProve/prelude.tex Tue Apr 03 17:21:33 2012 +0200 +++ b/doc-src/ProgProve/prelude.tex Tue Apr 03 17:48:16 2012 +0200 @@ -88,9 +88,9 @@ \hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces} {\par\end{trivlist}} -\renewcommand{\isachardoublequote}{} -\renewcommand{\isachardoublequoteopen}{} -\renewcommand{\isachardoublequoteclose}{} +\chardef\isachardoublequote=`\"% +\chardef\isachardoublequoteopen=`\"% +\chardef\isachardoublequoteclose=`\"% \renewcommand{\isacharbackquoteopen}{\isacharbackquote} \renewcommand{\isacharbackquoteclose}{\isacharbackquote} diff -r c82a0b2606a1 -r 610d9c212376 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Apr 03 17:21:33 2012 +0200 +++ b/etc/isar-keywords.el Tue Apr 03 17:48:16 2012 +0200 @@ -190,7 +190,9 @@ "print_orders" "print_quotconsts" "print_quotients" + "print_quotientsQ3" "print_quotmaps" + "print_quotmapsQ3" "print_rules" "print_simpset" "print_statement" @@ -403,7 +405,9 @@ "print_orders" "print_quotconsts" "print_quotients" + "print_quotientsQ3" "print_quotmaps" + "print_quotmapsQ3" "print_rules" "print_simpset" "print_statement" diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Archimedean_Field.thy Tue Apr 03 17:48:16 2012 +0200 @@ -194,6 +194,9 @@ lemma floor_of_nat [simp]: "floor (of_nat n) = int n" using floor_of_int [of "of_nat n"] by simp +lemma le_floor_add: "floor x + floor y \ floor (x + y)" + by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le) + text {* Floor with numerals *} lemma floor_zero [simp]: "floor 0 = 0" @@ -340,6 +343,9 @@ lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n" using ceiling_of_int [of "of_nat n"] by simp +lemma ceiling_add_le: "ceiling (x + y) \ ceiling x + ceiling y" + by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling) + text {* Ceiling with numerals *} lemma ceiling_zero [simp]: "ceiling 0 = 0" diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 03 17:48:16 2012 +0200 @@ -281,6 +281,7 @@ Hilbert_Choice.thy \ Int.thy \ Lazy_Sequence.thy \ + Lifting.thy \ List.thy \ Main.thy \ Map.thy \ @@ -315,6 +316,10 @@ Tools/code_evaluation.ML \ Tools/groebner.ML \ Tools/int_arith.ML \ + Tools/Lifting/lifting_def.ML \ + Tools/Lifting/lifting_info.ML \ + Tools/Lifting/lifting_term.ML \ + Tools/Lifting/lifting_setup.ML \ Tools/list_code.ML \ Tools/list_to_set_comprehension.ML \ Tools/nat_numeral_simprocs.ML \ @@ -1496,7 +1501,7 @@ Quotient_Examples/FSet.thy \ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \ - Quotient_Examples/Lift_Fun.thy + Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/DAList.thy --- a/src/HOL/Library/DAList.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/DAList.thy Tue Apr 03 17:48:16 2012 +0200 @@ -39,33 +39,29 @@ subsection {* Primitive operations *} -(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) - -quotient_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" -where "lookup" is "map_of :: ('key * 'value) list \ 'key \ 'value option" .. +lift_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" is map_of .. -quotient_definition empty :: "('key, 'value) alist" -where "empty" is "[] :: ('key * 'value) list" by simp +lift_definition empty :: "('key, 'value) alist" is "[]" by simp -quotient_definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" -where "update" is "AList.update :: 'key \ 'value \ ('key * 'value) list \ ('key * 'value) list" +lift_definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" + is AList.update by (simp add: distinct_update) (* FIXME: we use an unoptimised delete operation. *) -quotient_definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" -where "delete" is "AList.delete :: 'key \ ('key * 'value) list \ ('key * 'value) list" +lift_definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" + is AList.delete by (simp add: distinct_delete) -quotient_definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" -where "map_entry" is "AList.map_entry :: 'key \ ('value \ 'value) \ ('key * 'value) list \ ('key * 'value) list" +lift_definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" + is AList.map_entry by (simp add: distinct_map_entry) -quotient_definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" -where "filter" is "List.filter :: ('key \ 'value \ bool) \ ('key * 'value) list \ ('key * 'value) list" +lift_definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" + is List.filter by (simp add: distinct_map_fst_filter) -quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" -where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list" +lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" + is AList.map_default by (simp add: distinct_map_default) subsection {* Abstract operation properties *} diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1111,14 +1111,12 @@ text {* Operations on alists with distinct keys *} -quotient_definition join :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) alist \ ('a, 'b) alist \ ('a, 'b) alist" -where - "join" is "join_raw :: ('a \ 'b \ 'b \ 'b) \ ('a \ 'b) list \ ('a \ 'b) list \ ('a \ 'b) list" +lift_definition join :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) alist \ ('a, 'b) alist \ ('a, 'b) alist" +is join_raw by (simp add: distinct_join_raw) -quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \ ('a, 'b) alist \ ('a, 'b) alist" -where - "subtract_entries" is "subtract_entries_raw :: ('a \ 'b) list \ ('a \ 'b) list \ ('a \ 'b) list" +lift_definition subtract_entries :: "('a, ('b :: minus)) alist \ ('a, 'b) alist \ ('a, 'b) alist" +is subtract_entries_raw by (simp add: distinct_subtract_entries_raw) text {* Implementing multisets by means of association lists *} diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/Quotient_List.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_List.thy +(* Title: HOL/Library/Quotient3_List.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -56,63 +56,63 @@ "equivp R \ equivp (list_all2 R)" by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE) -lemma list_quotient [quot_thm]: - assumes "Quotient R Abs Rep" - shows "Quotient (list_all2 R) (map Abs) (map Rep)" -proof (rule QuotientI) - from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) +lemma list_quotient3 [quot_thm]: + assumes "Quotient3 R Abs Rep" + shows "Quotient3 (list_all2 R) (map Abs) (map Rep)" +proof (rule Quotient3I) + from assms have "\x. Abs (Rep x) = x" by (rule Quotient3_abs_rep) then show "\xs. map Abs (map Rep xs) = xs" by (simp add: comp_def) next - from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient_rel_rep) + from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient3_rel_rep) then show "\xs. list_all2 R (map Rep xs) (map Rep xs)" by (simp add: list_all2_map1 list_all2_map2 list_all2_eq) next fix xs ys - from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient_rel) + from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient3_rel) then show "list_all2 R xs ys \ list_all2 R xs xs \ list_all2 R ys ys \ map Abs xs = map Abs ys" by (induct xs ys rule: list_induct2') auto qed -declare [[map list = (list_all2, list_quotient)]] +declare [[mapQ3 list = (list_all2, list_quotient3)]] lemma cons_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" - by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) + by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) lemma cons_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)" by auto lemma nil_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "map Abs [] = []" by simp lemma nil_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "list_all2 R [] []" by simp lemma map_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" by (induct l) - (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma map_prs [quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" and "((abs1 ---> id) ---> map rep1 ---> id) map = map" by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def) - (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma map_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map" and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map" apply (simp_all add: fun_rel_def) @@ -124,35 +124,35 @@ done lemma foldr_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" - by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + by (induct l) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma foldr_prs [quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" apply (simp add: fun_eq_iff) by (simp only: fun_eq_iff foldr_prs_aux[OF a b]) (simp) lemma foldl_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" - by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + by (induct l arbitrary:e) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma foldl_prs [quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" by (simp add: fun_eq_iff foldl_prs_aux [OF a b]) (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) lemma foldl_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl" apply(auto simp add: fun_rel_def) apply (erule_tac P="R1 xa ya" in rev_mp) @@ -162,8 +162,8 @@ done lemma foldr_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr" apply (auto simp add: fun_rel_def) apply (erule list_all2_induct, simp_all) @@ -183,18 +183,18 @@ by (simp add: list_all2_rsp fun_rel_def) lemma [quot_preserve]: - assumes a: "Quotient R abs1 rep1" + assumes a: "Quotient3 R abs1 rep1" shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2" apply (simp add: fun_eq_iff) apply clarify apply (induct_tac xa xb rule: list_induct2') - apply (simp_all add: Quotient_abs_rep[OF a]) + apply (simp_all add: Quotient3_abs_rep[OF a]) done lemma [quot_preserve]: - assumes a: "Quotient R abs1 rep1" + assumes a: "Quotient3 R abs1 rep1" shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" - by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a]) + by (induct l m rule: list_induct2') (simp_all add: Quotient3_rel_rep[OF a]) lemma list_all2_find_element: assumes a: "x \ set a" @@ -207,4 +207,48 @@ shows "list_all2 R x x" by (induct x) (auto simp add: a) +lemma list_quotient: + assumes "Quotient R Abs Rep T" + shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)" +proof (rule QuotientI) + from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) + then show "\xs. List.map Abs (List.map Rep xs) = xs" by (simp add: comp_def) +next + from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient_rel_rep) + then show "\xs. list_all2 R (List.map Rep xs) (List.map Rep xs)" + by (simp add: list_all2_map1 list_all2_map2 list_all2_eq) +next + fix xs ys + from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient_rel) + then show "list_all2 R xs ys \ list_all2 R xs xs \ list_all2 R ys ys \ List.map Abs xs = List.map Abs ys" + by (induct xs ys rule: list_induct2') auto +next + { + fix l1 l2 + have "List.length l1 = List.length l2 \ + (\(x, y)\set (zip l1 l1). R x y) = (\(x, y)\set (zip l1 l2). R x x)" + by (induction rule: list_induct2) auto + } note x = this + { + fix f g + have "list_all2 (\x y. f x y \ g x y) = (\ x y. list_all2 f x y \ list_all2 g x y)" + by (intro ext) (auto simp add: list_all2_def) + } note list_all2_conj = this + from assms have t: "T = (\x y. R x x \ Abs x = y)" by (rule Quotient_cr_rel) + show "list_all2 T = (\x y. list_all2 R x x \ List.map Abs x = y)" + apply (simp add: t list_all2_conj[symmetric]) + apply (rule sym) + apply (simp add: list_all2_conj) + apply(intro ext) + apply (intro rev_conj_cong) + unfolding list_all2_def apply (metis List.list_all2_eq list_all2_def list_all2_map1) + apply (drule conjunct1) + apply (intro conj_cong) + apply simp + apply(simp add: x) + done +qed + +declare [[map list = (list_all2, list_quotient)]] + end diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Option.thy +(* Title: HOL/Library/Quotient3_Option.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -55,36 +55,36 @@ by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) lemma option_quotient [quot_thm]: - assumes "Quotient R Abs Rep" - shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" - apply (rule QuotientI) - apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms]) - using Quotient_rel [OF assms] + assumes "Quotient3 R Abs Rep" + shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" + apply (rule Quotient3I) + apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) + using Quotient3_rel [OF assms] apply (simp add: option_rel_unfold split: option.split) done -declare [[map option = (option_rel, option_quotient)]] +declare [[mapQ3 option = (option_rel, option_quotient)]] lemma option_None_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "option_rel R None None" by simp lemma option_Some_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(R ===> option_rel R) Some Some" by auto lemma option_None_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "Option.map Abs None = None" by simp lemma option_Some_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(Rep ---> Option.map Abs) Some = Some" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q]) + apply(simp add: Quotient3_abs_rep[OF q]) done end diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Product.thy +(* Title: HOL/Library/Quotient3_Product.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -32,66 +32,67 @@ using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) lemma prod_quotient [quot_thm]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" - shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" - apply (rule QuotientI) + assumes "Quotient3 R1 Abs1 Rep1" + assumes "Quotient3 R2 Abs2 Rep2" + shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" + apply (rule Quotient3I) apply (simp add: map_pair.compositionality comp_def map_pair.identity - Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)]) - apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)]) - using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)] + Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)]) + apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)]) + using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)] apply (auto simp add: split_paired_all) done -declare [[map prod = (prod_rel, prod_quotient)]] +declare [[mapQ3 prod = (prod_rel, prod_quotient)]] lemma Pair_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" by (auto simp add: prod_rel_def) lemma Pair_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) done lemma fst_rsp [quot_respect]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" + assumes "Quotient3 R1 Abs1 Rep1" + assumes "Quotient3 R2 Abs2 Rep2" shows "(prod_rel R1 R2 ===> R1) fst fst" by auto lemma fst_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1]) lemma snd_rsp [quot_respect]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" + assumes "Quotient3 R1 Abs1 Rep1" + assumes "Quotient3 R2 Abs2 Rep2" shows "(prod_rel R1 R2 ===> R2) snd snd" by auto lemma snd_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q2]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2]) lemma split_rsp [quot_respect]: shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" - by (auto intro!: fun_relI elim!: fun_relE) + unfolding prod_rel_def fun_rel_def + by auto lemma split_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_respect]: shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> @@ -99,11 +100,11 @@ by (auto simp add: fun_rel_def) lemma [quot_preserve]: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" + assumes q1: "Quotient3 R1 abs1 rep1" + and q2: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_preserve]: shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Set.thy +(* Title: HOL/Library/Quotient3_Set.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -9,77 +9,77 @@ begin lemma set_quotient [quot_thm]: - assumes "Quotient R Abs Rep" - shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)" -proof (rule QuotientI) - from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) + assumes "Quotient3 R Abs Rep" + shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)" +proof (rule Quotient3I) + from assms have "\x. Abs (Rep x) = x" by (rule Quotient3_abs_rep) then show "\xs. Rep -` (Abs -` xs) = xs" unfolding vimage_def by auto next show "\xs. set_rel R (Abs -` xs) (Abs -` xs)" unfolding set_rel_def vimage_def - by auto (metis Quotient_rel_abs[OF assms])+ + by auto (metis Quotient3_rel_abs[OF assms])+ next fix r s show "set_rel R r s = (set_rel R r r \ set_rel R s s \ Rep -` r = Rep -` s)" unfolding set_rel_def vimage_def set_eq_iff - by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ + by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+ qed -declare [[map set = (set_rel, set_quotient)]] +declare [[mapQ3 set = (set_rel, set_quotient)]] lemma empty_set_rsp[quot_respect]: "set_rel R {} {}" unfolding set_rel_def by simp lemma collect_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "((R ===> op =) ===> set_rel R) Collect Collect" by (intro fun_relI) (simp add: fun_rel_def set_rel_def) lemma collect_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "((Abs ---> id) ---> op -` Rep) Collect = Collect" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF assms]) + by (simp add: Quotient3_abs_rep[OF assms]) lemma union_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" by (intro fun_relI) (simp add: set_rel_def) lemma union_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \ = op \" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) + by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]]) lemma diff_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -" by (intro fun_relI) (simp add: set_rel_def) lemma diff_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff) + by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff) lemma inter_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" by (intro fun_relI) (auto simp add: set_rel_def) lemma inter_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \ = op \" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) + by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]]) lemma mem_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(Rep ---> op -` Abs ---> id) op \ = op \" - by (simp add: fun_eq_iff Quotient_abs_rep[OF assms]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms]) lemma mem_rsp[quot_respect]: shows "(R ===> set_rel R ===> op =) op \ op \" diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Sum.thy +(* Title: HOL/Library/Quotient3_Sum.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -55,44 +55,44 @@ by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) lemma sum_quotient [quot_thm]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" - apply (rule QuotientI) + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" + shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" + apply (rule Quotient3I) apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 - Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2]) - using Quotient_rel [OF q1] Quotient_rel [OF q2] + Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) + using Quotient3_rel [OF q1] Quotient3_rel [OF q2] apply (simp add: sum_rel_unfold comp_def split: sum.split) done -declare [[map sum = (sum_rel, sum_quotient)]] +declare [[mapQ3 sum = (sum_rel, sum_quotient)]] lemma sum_Inl_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R1 ===> sum_rel R1 R2) Inl Inl" by auto lemma sum_Inr_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R2 ===> sum_rel R1 R2) Inr Inr" by auto lemma sum_Inl_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q1]) + apply(simp add: Quotient3_abs_rep[OF q1]) done lemma sum_Inr_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q2]) + apply(simp add: Quotient3_abs_rep[OF q2]) done end diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Lifting.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lifting.thy Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,316 @@ +(* Title: HOL/Lifting.thy + Author: Brian Huffman and Ondrej Kuncar + Author: Cezary Kaliszyk and Christian Urban +*) + +header {* Lifting package *} + +theory Lifting +imports Plain Equiv_Relations +keywords + "print_quotmaps" "print_quotients" :: diag and + "lift_definition" :: thy_goal and + "setup_lifting" :: thy_decl +uses + ("Tools/Lifting/lifting_info.ML") + ("Tools/Lifting/lifting_term.ML") + ("Tools/Lifting/lifting_def.ML") + ("Tools/Lifting/lifting_setup.ML") +begin + +subsection {* Function map and function relation *} + +notation map_fun (infixr "--->" 55) + +lemma map_fun_id: + "(id ---> id) = id" + by (simp add: fun_eq_iff) + +definition + fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) +where + "fun_rel R1 R2 = (\f g. \x y. R1 x y \ R2 (f x) (g y))" + +lemma fun_relI [intro]: + assumes "\x y. R1 x y \ R2 (f x) (g y)" + shows "(R1 ===> R2) f g" + using assms by (simp add: fun_rel_def) + +lemma fun_relE: + assumes "(R1 ===> R2) f g" and "R1 x y" + obtains "R2 (f x) (g y)" + using assms by (simp add: fun_rel_def) + +lemma fun_rel_eq: + shows "((op =) ===> (op =)) = (op =)" + by (auto simp add: fun_eq_iff elim: fun_relE) + +lemma fun_rel_eq_rel: + shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" + by (simp add: fun_rel_def) + +subsection {* Quotient Predicate *} + +definition + "Quotient R Abs Rep T \ + (\a. Abs (Rep a) = a) \ + (\a. R (Rep a) (Rep a)) \ + (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ + T = (\x y. R x x \ Abs x = y)" + +lemma QuotientI: + assumes "\a. Abs (Rep a) = a" + and "\a. R (Rep a) (Rep a)" + and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" + and "T = (\x y. R x x \ Abs x = y)" + shows "Quotient R Abs Rep T" + using assms unfolding Quotient_def by blast + +lemma Quotient_abs_rep: + assumes a: "Quotient R Abs Rep T" + shows "Abs (Rep a) = a" + using a + unfolding Quotient_def + by simp + +lemma Quotient_rep_reflp: + assumes a: "Quotient R Abs Rep T" + shows "R (Rep a) (Rep a)" + using a + unfolding Quotient_def + by blast + +lemma Quotient_rel: + assumes a: "Quotient R Abs Rep T" + shows "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} + using a + unfolding Quotient_def + by blast + +lemma Quotient_cr_rel: + assumes a: "Quotient R Abs Rep T" + shows "T = (\x y. R x x \ Abs x = y)" + using a + unfolding Quotient_def + by blast + +lemma Quotient_refl1: + assumes a: "Quotient R Abs Rep T" + shows "R r s \ R r r" + using a unfolding Quotient_def + by fast + +lemma Quotient_refl2: + assumes a: "Quotient R Abs Rep T" + shows "R r s \ R s s" + using a unfolding Quotient_def + by fast + +lemma Quotient_rel_rep: + assumes a: "Quotient R Abs Rep T" + shows "R (Rep a) (Rep b) \ a = b" + using a + unfolding Quotient_def + by metis + +lemma Quotient_rep_abs: + assumes a: "Quotient R Abs Rep T" + shows "R r r \ R (Rep (Abs r)) r" + using a unfolding Quotient_def + by blast + +lemma Quotient_rel_abs: + assumes a: "Quotient R Abs Rep T" + shows "R r s \ Abs r = Abs s" + using a unfolding Quotient_def + by blast + +lemma Quotient_symp: + assumes a: "Quotient R Abs Rep T" + shows "symp R" + using a unfolding Quotient_def using sympI by (metis (full_types)) + +lemma Quotient_transp: + assumes a: "Quotient R Abs Rep T" + shows "transp R" + using a unfolding Quotient_def using transpI by (metis (full_types)) + +lemma Quotient_part_equivp: + assumes a: "Quotient R Abs Rep T" + shows "part_equivp R" +by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI) + +lemma identity_quotient: "Quotient (op =) id id (op =)" +unfolding Quotient_def by simp + +lemma Quotient_alt_def: + "Quotient R Abs Rep T \ + (\a b. T a b \ Abs a = b) \ + (\b. T (Rep b) b) \ + (\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y)" +apply safe +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (rule QuotientI) +apply simp +apply metis +apply simp +apply (rule ext, rule ext, metis) +done + +lemma Quotient_alt_def2: + "Quotient R Abs Rep T \ + (\a b. T a b \ Abs a = b) \ + (\b. T (Rep b) b) \ + (\x y. R x y \ T x (Abs y) \ T y (Abs x))" + unfolding Quotient_alt_def by (safe, metis+) + +lemma fun_quotient: + assumes 1: "Quotient R1 abs1 rep1 T1" + assumes 2: "Quotient R2 abs2 rep2 T2" + shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)" + using assms unfolding Quotient_alt_def2 + unfolding fun_rel_def fun_eq_iff map_fun_apply + by (safe, metis+) + +lemma apply_rsp: + fixes f g::"'a \ 'c" + assumes q: "Quotient R1 Abs1 Rep1 T1" + and a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by (auto elim: fun_relE) + +lemma apply_rsp': + assumes a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by (auto elim: fun_relE) + +lemma apply_rsp'': + assumes "Quotient R Abs Rep T" + and "(R ===> S) f f" + shows "S (f (Rep x)) (f (Rep x))" +proof - + from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) + then show ?thesis using assms(2) by (auto intro: apply_rsp') +qed + +subsection {* Quotient composition *} + +lemma Quotient_compose: + assumes 1: "Quotient R1 Abs1 Rep1 T1" + assumes 2: "Quotient R2 Abs2 Rep2 T2" + shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \ Abs1) (Rep1 \ Rep2) (T1 OO T2)" +proof - + from 1 have Abs1: "\a b. T1 a b \ Abs1 a = b" + unfolding Quotient_alt_def by simp + from 1 have Rep1: "\b. T1 (Rep1 b) b" + unfolding Quotient_alt_def by simp + from 2 have Abs2: "\a b. T2 a b \ Abs2 a = b" + unfolding Quotient_alt_def by simp + from 2 have Rep2: "\b. T2 (Rep2 b) b" + unfolding Quotient_alt_def by simp + from 2 have R2: + "\x y. R2 x y \ T2 x (Abs2 x) \ T2 y (Abs2 y) \ Abs2 x = Abs2 y" + unfolding Quotient_alt_def by simp + show ?thesis + unfolding Quotient_alt_def + apply simp + apply safe + apply (drule Abs1, simp) + apply (erule Abs2) + apply (rule pred_compI) + apply (rule Rep1) + apply (rule Rep2) + apply (rule pred_compI, assumption) + apply (drule Abs1, simp) + apply (clarsimp simp add: R2) + apply (rule pred_compI, assumption) + apply (drule Abs1, simp)+ + apply (clarsimp simp add: R2) + apply (drule Abs1, simp)+ + apply (clarsimp simp add: R2) + apply (rule pred_compI, assumption) + apply (rule pred_compI [rotated]) + apply (erule conversepI) + apply (drule Abs1, simp)+ + apply (simp add: R2) + done +qed + +subsection {* Invariant *} + +definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" + where "invariant R = (\x y. R x \ x = y)" + +lemma invariant_to_eq: + assumes "invariant P x y" + shows "x = y" +using assms by (simp add: invariant_def) + +lemma fun_rel_eq_invariant: + shows "((invariant R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" +by (auto simp add: invariant_def fun_rel_def) + +lemma invariant_same_args: + shows "invariant P x x \ P x" +using assms by (auto simp add: invariant_def) + +lemma copy_type_to_Quotient: + assumes "type_definition Rep Abs UNIV" + and T_def: "T \ (\x y. Abs x = y)" + shows "Quotient (op =) Abs Rep T" +proof - + interpret type_definition Rep Abs UNIV by fact + from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI) +qed + +lemma copy_type_to_equivp: + fixes Abs :: "'a \ 'b" + and Rep :: "'b \ 'a" + assumes "type_definition Rep Abs (UNIV::'a set)" + shows "equivp (op=::'a\'a\bool)" +by (rule identity_equivp) + +lemma invariant_type_to_Quotient: + assumes "type_definition Rep Abs {x. P x}" + and T_def: "T \ (\x y. (invariant P) x x \ Abs x = y)" + shows "Quotient (invariant P) Abs Rep T" +proof - + interpret type_definition Rep Abs "{x. P x}" by fact + from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def) +qed + +lemma invariant_type_to_part_equivp: + assumes "type_definition Rep Abs {x. P x}" + shows "part_equivp (invariant P)" +proof (intro part_equivpI) + interpret type_definition Rep Abs "{x. P x}" by fact + show "\x. invariant P x x" using Rep by (auto simp: invariant_def) +next + show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) +next + show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) +qed + +subsection {* ML setup *} + +text {* Auxiliary data for the lifting package *} + +use "Tools/Lifting/lifting_info.ML" +setup Lifting_Info.setup + +declare [[map "fun" = (fun_rel, fun_quotient)]] + +use "Tools/Lifting/lifting_term.ML" + +use "Tools/Lifting/lifting_def.ML" + +use "Tools/Lifting/lifting_setup.ML" + +hide_const (open) invariant + +end diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Metis_Examples/Clausification.thy --- a/src/HOL/Metis_Examples/Clausification.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Metis_Examples/Clausification.thy Tue Apr 03 17:48:16 2012 +0200 @@ -131,7 +131,7 @@ by (metis bounded_def subset_eq) lemma - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient R Abs Rep T" shows "symp R" using a unfolding Quotient_def using sympI by (metis (full_types)) diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Num.thy --- a/src/HOL/Num.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Num.thy Tue Apr 03 17:48:16 2012 +0200 @@ -193,7 +193,7 @@ text {* The @{const num_of_nat} conversion *} lemma num_of_nat_One: - "n \ 1 \ num_of_nat n = Num.One" + "n \ 1 \ num_of_nat n = One" by (cases n) simp_all lemma num_of_nat_plus_distrib: @@ -865,8 +865,11 @@ Natural numbers *} +lemma Suc_1 [simp]: "Suc 1 = 2" + unfolding Suc_eq_plus1 by (rule one_add_one) + lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)" - unfolding numeral_plus_one [symmetric] by simp + unfolding Suc_eq_plus1 by (rule numeral_plus_one) definition pred_numeral :: "num \ nat" where [code del]: "pred_numeral k = numeral k - 1" @@ -881,9 +884,9 @@ by (simp_all add: numeral.simps BitM_plus_one) lemma pred_numeral_simps [simp]: - "pred_numeral Num.One = 0" - "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)" - "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)" + "pred_numeral One = 0" + "pred_numeral (Bit0 k) = numeral (BitM k)" + "pred_numeral (Bit1 k) = numeral (Bit0 k)" unfolding pred_numeral_def eval_nat_numeral by (simp_all only: diff_Suc_Suc diff_0) @@ -897,7 +900,7 @@ by (simp only: numeral_One One_nat_def) lemma Suc_nat_number_of_add: - "Suc (numeral v + n) = numeral (v + Num.One) + n" + "Suc (numeral v + n) = numeral (v + One) + n" by simp (*Maps #n to n for n = 1, 2*) diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient.thy Tue Apr 03 17:48:16 2012 +0200 @@ -5,11 +5,10 @@ header {* Definition of Quotient Types *} theory Quotient -imports Plain Hilbert_Choice Equiv_Relations +imports Plain Hilbert_Choice Equiv_Relations Lifting keywords - "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and + "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and "quotient_type" :: thy_goal and "/" and - "setup_lifting" :: thy_decl and "quotient_definition" :: thy_goal uses ("Tools/Quotient/quotient_info.ML") @@ -53,37 +52,6 @@ shows "x \ Respects R \ R x x" unfolding Respects_def by simp -subsection {* Function map and function relation *} - -notation map_fun (infixr "--->" 55) - -lemma map_fun_id: - "(id ---> id) = id" - by (simp add: fun_eq_iff) - -definition - fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) -where - "fun_rel R1 R2 = (\f g. \x y. R1 x y \ R2 (f x) (g y))" - -lemma fun_relI [intro]: - assumes "\x y. R1 x y \ R2 (f x) (g y)" - shows "(R1 ===> R2) f g" - using assms by (simp add: fun_rel_def) - -lemma fun_relE: - assumes "(R1 ===> R2) f g" and "R1 x y" - obtains "R2 (f x) (g y)" - using assms by (simp add: fun_rel_def) - -lemma fun_rel_eq: - shows "((op =) ===> (op =)) = (op =)" - by (auto simp add: fun_eq_iff elim: fun_relE) - -lemma fun_rel_eq_rel: - shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" - by (simp add: fun_rel_def) - subsection {* set map (vimage) and set relation *} definition "set_rel R xs ys \ \x y. R x y \ x \ xs \ y \ ys" @@ -106,155 +74,169 @@ subsection {* Quotient Predicate *} definition - "Quotient R Abs Rep \ + "Quotient3 R Abs Rep \ (\a. Abs (Rep a) = a) \ (\a. R (Rep a) (Rep a)) \ (\r s. R r s \ R r r \ R s s \ Abs r = Abs s)" -lemma QuotientI: +lemma Quotient3I: assumes "\a. Abs (Rep a) = a" and "\a. R (Rep a) (Rep a)" and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" - shows "Quotient R Abs Rep" - using assms unfolding Quotient_def by blast + shows "Quotient3 R Abs Rep" + using assms unfolding Quotient3_def by blast -lemma Quotient_abs_rep: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_abs_rep: + assumes a: "Quotient3 R Abs Rep" shows "Abs (Rep a) = a" using a - unfolding Quotient_def + unfolding Quotient3_def by simp -lemma Quotient_rep_reflp: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rep_reflp: + assumes a: "Quotient3 R Abs Rep" shows "R (Rep a) (Rep a)" using a - unfolding Quotient_def + unfolding Quotient3_def by blast -lemma Quotient_rel: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rel: + assumes a: "Quotient3 R Abs Rep" shows "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} using a - unfolding Quotient_def + unfolding Quotient3_def by blast -lemma Quotient_refl1: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_refl1: + assumes a: "Quotient3 R Abs Rep" shows "R r s \ R r r" - using a unfolding Quotient_def + using a unfolding Quotient3_def by fast -lemma Quotient_refl2: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_refl2: + assumes a: "Quotient3 R Abs Rep" shows "R r s \ R s s" - using a unfolding Quotient_def + using a unfolding Quotient3_def by fast -lemma Quotient_rel_rep: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rel_rep: + assumes a: "Quotient3 R Abs Rep" shows "R (Rep a) (Rep b) \ a = b" using a - unfolding Quotient_def + unfolding Quotient3_def by metis -lemma Quotient_rep_abs: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rep_abs: + assumes a: "Quotient3 R Abs Rep" shows "R r r \ R (Rep (Abs r)) r" - using a unfolding Quotient_def + using a unfolding Quotient3_def + by blast + +lemma Quotient3_rel_abs: + assumes a: "Quotient3 R Abs Rep" + shows "R r s \ Abs r = Abs s" + using a unfolding Quotient3_def by blast -lemma Quotient_rel_abs: - assumes a: "Quotient R Abs Rep" - shows "R r s \ Abs r = Abs s" - using a unfolding Quotient_def - by blast - -lemma Quotient_symp: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_symp: + assumes a: "Quotient3 R Abs Rep" shows "symp R" - using a unfolding Quotient_def using sympI by metis + using a unfolding Quotient3_def using sympI by metis -lemma Quotient_transp: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_transp: + assumes a: "Quotient3 R Abs Rep" shows "transp R" - using a unfolding Quotient_def using transpI by metis + using a unfolding Quotient3_def using transpI by (metis (full_types)) -lemma identity_quotient: - shows "Quotient (op =) id id" - unfolding Quotient_def id_def +lemma Quotient3_part_equivp: + assumes a: "Quotient3 R Abs Rep" + shows "part_equivp R" +by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI) + +lemma identity_quotient3: + shows "Quotient3 (op =) id id" + unfolding Quotient3_def id_def by blast -lemma fun_quotient: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" - shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" +lemma fun_quotient3: + assumes q1: "Quotient3 R1 abs1 rep1" + and q2: "Quotient3 R2 abs2 rep2" + shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" proof - - have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" - using q1 q2 by (simp add: Quotient_def fun_eq_iff) + have "\a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + using q1 q2 by (simp add: Quotient3_def fun_eq_iff) moreover - have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + have "\a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" by (rule fun_relI) - (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2], - simp (no_asm) add: Quotient_def, simp) + (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], + simp (no_asm) add: Quotient3_def, simp) + moreover - have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + { + fix r s + have "(R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" - apply(auto simp add: fun_rel_def fun_eq_iff) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - done - ultimately - show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" - unfolding Quotient_def by blast + proof - + + have "(R1 ===> R2) r s \ (R1 ===> R2) r r" unfolding fun_rel_def + using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] + by (metis (full_types) part_equivp_def) + moreover have "(R1 ===> R2) r s \ (R1 ===> R2) s s" unfolding fun_rel_def + using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] + by (metis (full_types) part_equivp_def) + moreover have "(R1 ===> R2) r s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s" + apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis + moreover have "((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s) \ (R1 ===> R2) r s" + apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def + by (metis map_fun_apply) + + ultimately show ?thesis by blast + qed + } + ultimately show ?thesis by (intro Quotient3I) (assumption+) qed lemma abs_o_rep: - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient3 R Abs Rep" shows "Abs o Rep = id" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF a]) + by (simp add: Quotient3_abs_rep[OF a]) lemma equals_rsp: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and a: "R xa xb" "R ya yb" shows "R xa ya = R xb yb" - using a Quotient_symp[OF q] Quotient_transp[OF q] + using a Quotient3_symp[OF q] Quotient3_transp[OF q] by (blast elim: sympE transpE) lemma lambda_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" unfolding fun_eq_iff - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp lemma lambda_prs1: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" unfolding fun_eq_iff - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp lemma rep_abs_rsp: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and a: "R x1 x2" shows "R x1 (Rep (Abs x2))" - using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] + using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] by metis lemma rep_abs_rsp_left: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and a: "R x1 x2" shows "R (Rep (Abs x1)) x2" - using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] + using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] by metis text{* @@ -264,24 +246,19 @@ will be provable; which is why we need to use @{text apply_rsp} and not the primed version *} -lemma apply_rsp: +lemma apply_rspQ3: fixes f g::"'a \ 'c" - assumes q: "Quotient R1 Abs1 Rep1" + assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)" using a by (auto elim: fun_relE) -lemma apply_rsp': - assumes a: "(R1 ===> R2) f g" "R1 x y" - shows "R2 (f x) (g y)" - using a by (auto elim: fun_relE) - -lemma apply_rsp'': - assumes "Quotient R Abs Rep" +lemma apply_rspQ3'': + assumes "Quotient3 R Abs Rep" and "(R ===> S) f f" shows "S (f (Rep x)) (f (Rep x))" proof - - from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) + from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp) then show ?thesis using assms(2) by (auto intro: apply_rsp') qed @@ -393,29 +370,29 @@ "x \ p \ Babs p m x = m x" lemma babs_rsp: - assumes q: "Quotient R1 Abs1 Rep1" + assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" apply (auto simp add: Babs_def in_respects fun_rel_def) apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") using a apply (simp add: Babs_def fun_rel_def) apply (simp add: in_respects fun_rel_def) - using Quotient_rel[OF q] + using Quotient3_rel[OF q] by metis lemma babs_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" apply (rule ext) apply (simp add:) apply (subgoal_tac "Rep1 x \ Respects R1") - apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) - apply (simp add: in_respects Quotient_rel_rep[OF q1]) + apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) + apply (simp add: in_respects Quotient3_rel_rep[OF q1]) done lemma babs_simp: - assumes q: "Quotient R1 Abs Rep" + assumes q: "Quotient3 R1 Abs Rep" shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" apply(rule iffI) apply(simp_all only: babs_rsp[OF q]) @@ -423,7 +400,7 @@ apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") apply(metis Babs_def) apply (simp add: in_respects) - using Quotient_rel[OF q] + using Quotient3_rel[OF q] by metis (* If a user proves that a particular functional relation @@ -451,15 +428,15 @@ (* 2 lemmas needed for cleaning of quantifiers *) lemma all_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "Ball (Respects R) ((absf ---> id) f) = All f" - using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def + using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def by metis lemma ex_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "Bex (Respects R) ((absf ---> id) f) = Ex f" - using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def + using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def by metis subsection {* @{text Bex1_rel} quantifier *} @@ -508,7 +485,7 @@ done lemma bex1_rel_rsp: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" apply (simp add: fun_rel_def) apply clarify @@ -520,7 +497,7 @@ lemma ex1_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" apply (simp add:) apply (subst Bex1_rel_def) @@ -535,7 +512,7 @@ apply (rule_tac x="absf x" in exI) apply (simp) apply rule+ - using a unfolding Quotient_def + using a unfolding Quotient3_def apply metis apply rule+ apply (erule_tac x="x" in ballE) @@ -548,10 +525,10 @@ apply (rule_tac x="repf x" in exI) apply (simp only: in_respects) apply rule - apply (metis Quotient_rel_rep[OF a]) -using a unfolding Quotient_def apply (simp) + apply (metis Quotient3_rel_rep[OF a]) +using a unfolding Quotient3_def apply (simp) apply rule+ -using a unfolding Quotient_def in_respects +using a unfolding Quotient3_def in_respects apply metis done @@ -587,7 +564,7 @@ subsection {* Various respects and preserve lemmas *} lemma quot_rel_rsp: - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient3 R Abs Rep" shows "(R ===> R ===> op =) R R" apply(rule fun_relI)+ apply(rule equals_rsp[OF a]) @@ -595,12 +572,12 @@ done lemma o_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and q3: "Quotient R3 Abs3 Rep3" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" + and q3: "Quotient3 R3 Abs3 Rep3" shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \ = op \" and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \ = op \" - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] by (simp_all add: fun_eq_iff) lemma o_rsp: @@ -609,26 +586,26 @@ by (force elim: fun_relE)+ lemma cond_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "absf (if a then repf b else repf c) = (if a then b else c)" - using a unfolding Quotient_def by auto + using a unfolding Quotient3_def by auto lemma if_prs: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(id ---> Rep ---> Rep ---> Abs) If = If" - using Quotient_abs_rep[OF q] + using Quotient3_abs_rep[OF q] by (auto simp add: fun_eq_iff) lemma if_rsp: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(op = ===> R ===> R ===> R) If If" by force lemma let_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by (auto simp add: fun_eq_iff) lemma let_rsp: @@ -640,9 +617,9 @@ by auto lemma id_prs: - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient3 R Abs Rep" shows "(Rep ---> Abs) id = id" - by (simp add: fun_eq_iff Quotient_abs_rep [OF a]) + by (simp add: fun_eq_iff Quotient3_abs_rep [OF a]) locale quot_type = @@ -673,8 +650,8 @@ by (metis assms exE_some equivp[simplified part_equivp_def]) lemma Quotient: - shows "Quotient R abs rep" - unfolding Quotient_def abs_def rep_def + shows "Quotient3 R abs rep" + unfolding Quotient3_def abs_def rep_def proof (intro conjI allI) fix a r s show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - @@ -703,149 +680,114 @@ subsection {* Quotient composition *} -lemma OOO_quotient: +lemma OOO_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" fixes R2' :: "'a \ 'a \ bool" fixes R2 :: "'b \ 'b \ bool" - assumes R1: "Quotient R1 Abs1 Rep1" - assumes R2: "Quotient R2 Abs2 Rep2" + assumes R1: "Quotient3 R1 Abs1 Rep1" + assumes R2: "Quotient3 R2 Abs2 Rep2" assumes Abs1: "\x y. R2' x y \ R1 x x \ R1 y y \ R2 (Abs1 x) (Abs1 y)" assumes Rep1: "\x y. R2 x y \ R2' (Rep1 x) (Rep1 y)" - shows "Quotient (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" -apply (rule QuotientI) - apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1]) + shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" +apply (rule Quotient3I) + apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) apply simp apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI) - apply (rule Quotient_rep_reflp [OF R1]) + apply (rule Quotient3_rep_reflp [OF R1]) apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated]) - apply (rule Quotient_rep_reflp [OF R1]) + apply (rule Quotient3_rep_reflp [OF R1]) apply (rule Rep1) - apply (rule Quotient_rep_reflp [OF R2]) + apply (rule Quotient3_rep_reflp [OF R2]) apply safe apply (rename_tac x y) apply (drule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) - apply (drule Quotient_refl1 [OF R2], drule Rep1) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_refl1 [OF R2], drule Rep1) apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption) apply (erule pred_compI) - apply (erule Quotient_symp [OF R1, THEN sympD]) - apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) - apply (rule conjI, erule Quotient_refl1 [OF R1]) - apply (rule conjI, rule Quotient_rep_reflp [OF R1]) - apply (subst Quotient_abs_rep [OF R1]) - apply (erule Quotient_rel_abs [OF R1]) + apply (erule Quotient3_symp [OF R1, THEN sympD]) + apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient3_refl1 [OF R1]) + apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) + apply (subst Quotient3_abs_rep [OF R1]) + apply (erule Quotient3_rel_abs [OF R1]) apply (rename_tac x y) apply (drule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) - apply (drule Quotient_refl2 [OF R2], drule Rep1) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_refl2 [OF R2], drule Rep1) apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption) apply (erule pred_compI) - apply (erule Quotient_symp [OF R1, THEN sympD]) - apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) - apply (rule conjI, erule Quotient_refl2 [OF R1]) - apply (rule conjI, rule Quotient_rep_reflp [OF R1]) - apply (subst Quotient_abs_rep [OF R1]) - apply (erule Quotient_rel_abs [OF R1, THEN sym]) + apply (erule Quotient3_symp [OF R1, THEN sympD]) + apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient3_refl2 [OF R1]) + apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) + apply (subst Quotient3_abs_rep [OF R1]) + apply (erule Quotient3_rel_abs [OF R1, THEN sym]) apply simp - apply (rule Quotient_rel_abs [OF R2]) - apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption) - apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption) + apply (rule Quotient3_rel_abs [OF R2]) + apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption) + apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption) apply (erule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) apply (rename_tac a b c d) apply simp apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI) - apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) - apply (rule conjI, erule Quotient_refl1 [OF R1]) - apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1]) + apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient3_refl1 [OF R1]) + apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated]) - apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) - apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1]) - apply (erule Quotient_refl2 [OF R1]) + apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) apply (rule Rep1) apply (drule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) apply (drule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) - apply (drule Quotient_rel_abs [OF R1]) - apply (drule Quotient_rel_abs [OF R1]) - apply (drule Quotient_rel_abs [OF R1]) - apply (drule Quotient_rel_abs [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) apply simp - apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2]) + apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2]) apply simp done -lemma OOO_eq_quotient: +lemma OOO_eq_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" - assumes R1: "Quotient R1 Abs1 Rep1" - assumes R2: "Quotient op= Abs2 Rep2" - shows "Quotient (R1 OOO op=) (Abs2 \ Abs1) (Rep1 \ Rep2)" + assumes R1: "Quotient3 R1 Abs1 Rep1" + assumes R2: "Quotient3 op= Abs2 Rep2" + shows "Quotient3 (R1 OOO op=) (Abs2 \ Abs1) (Rep1 \ Rep2)" using assms -by (rule OOO_quotient) auto +by (rule OOO_quotient3) auto subsection {* Invariant *} -definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" - where "invariant R = (\x y. R x \ x = y)" - -lemma invariant_to_eq: - assumes "invariant P x y" - shows "x = y" -using assms by (simp add: invariant_def) - -lemma fun_rel_eq_invariant: - shows "((invariant R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" -by (auto simp add: invariant_def fun_rel_def) - -lemma invariant_same_args: - shows "invariant P x x \ P x" -using assms by (auto simp add: invariant_def) - -lemma copy_type_to_Quotient: +lemma copy_type_to_Quotient3: assumes "type_definition Rep Abs UNIV" - shows "Quotient (op =) Abs Rep" + shows "Quotient3 (op =) Abs Rep" proof - interpret type_definition Rep Abs UNIV by fact - from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI) + from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I) qed -lemma copy_type_to_equivp: - fixes Abs :: "'a \ 'b" - and Rep :: "'b \ 'a" - assumes "type_definition Rep Abs (UNIV::'a set)" - shows "equivp (op=::'a\'a\bool)" -by (rule identity_equivp) - -lemma invariant_type_to_Quotient: +lemma invariant_type_to_Quotient3: assumes "type_definition Rep Abs {x. P x}" - shows "Quotient (invariant P) Abs Rep" + shows "Quotient3 (Lifting.invariant P) Abs Rep" proof - interpret type_definition Rep Abs "{x. P x}" by fact - from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def) -qed - -lemma invariant_type_to_part_equivp: - assumes "type_definition Rep Abs {x. P x}" - shows "part_equivp (invariant P)" -proof (intro part_equivpI) - interpret type_definition Rep Abs "{x. P x}" by fact - show "\x. invariant P x x" using Rep by (auto simp: invariant_def) -next - show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) -next - show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) + from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def) qed subsection {* ML setup *} @@ -855,9 +797,9 @@ use "Tools/Quotient/quotient_info.ML" setup Quotient_Info.setup -declare [[map "fun" = (fun_rel, fun_quotient)]] +declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]] -lemmas [quot_thm] = fun_quotient +lemmas [quot_thm] = fun_quotient3 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp lemmas [quot_preserve] = if_prs o_prs let_prs id_prs lemmas [quot_equiv] = identity_equivp @@ -960,6 +902,4 @@ map_fun (infixr "--->" 55) and fun_rel (infixr "===>" 55) -hide_const (open) invariant - end diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/DList.thy --- a/src/HOL/Quotient_Examples/DList.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/DList.thy Tue Apr 03 17:48:16 2012 +0200 @@ -227,7 +227,7 @@ lemma list_of_dlist_dlist [simp]: "list_of_dlist (dlist xs) = remdups xs" unfolding list_of_dlist_def map_fun_apply id_def - by (metis Quotient_rep_abs[OF Quotient_dlist] dlist_eq_def) + by (metis Quotient3_rep_abs[OF Quotient3_dlist] dlist_eq_def) lemma remdups_list_of_dlist [simp]: "remdups (list_of_dlist dxs) = list_of_dlist dxs" @@ -236,7 +236,7 @@ lemma dlist_list_of_dlist [simp, code abstype]: "dlist (list_of_dlist dxs) = dxs" by (simp add: list_of_dlist_def) - (metis Quotient_def Quotient_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist) + (metis Quotient3_def Quotient3_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist) lemma dlist_filter_simps: "filter P empty = empty" diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Quotient_Examples/FSet.thy +(* Title: HOL/Quotient3_Examples/FSet.thy Author: Cezary Kaliszyk, TU Munich Author: Christian Urban, TU Munich @@ -117,15 +117,15 @@ by (simp only: list_eq_def set_map) lemma quotient_compose_list_g: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and e: "equivp R" - shows "Quotient ((list_all2 R) OOO (op \)) + shows "Quotient3 ((list_all2 R) OOO (op \)) (abs_fset \ (map Abs)) ((map Rep) \ rep_fset)" - unfolding Quotient_def comp_def + unfolding Quotient3_def comp_def proof (intro conjI allI) fix a r s show "abs_fset (map Abs (map Rep (rep_fset a))) = a" - by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id) + by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id) have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))" by (rule list_all2_refl'[OF e]) have c: "(op \ OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" @@ -146,37 +146,37 @@ assume d: "b \ ba" assume e: "list_all2 R ba s" have f: "map Abs r = map Abs b" - using Quotient_rel[OF list_quotient[OF q]] c by blast + using Quotient3_rel[OF list_quotient3[OF q]] c by blast have "map Abs ba = map Abs s" - using Quotient_rel[OF list_quotient[OF q]] e by blast + using Quotient3_rel[OF list_quotient3[OF q]] e by blast then have g: "map Abs s = map Abs ba" by simp then show "map Abs r \ map Abs s" using d f map_list_eq_cong by simp qed then show "abs_fset (map Abs r) = abs_fset (map Abs s)" - using Quotient_rel[OF Quotient_fset] by blast + using Quotient3_rel[OF Quotient3_fset] by blast next assume a: "(list_all2 R OOO op \) r r \ (list_all2 R OOO op \) s s \ abs_fset (map Abs r) = abs_fset (map Abs s)" then have s: "(list_all2 R OOO op \) s s" by simp have d: "map Abs r \ map Abs s" - by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a) + by (subst Quotient3_rel [OF Quotient3_fset, symmetric]) (simp add: a) have b: "map Rep (map Abs r) \ map Rep (map Abs s)" by (rule map_list_eq_cong[OF d]) have y: "list_all2 R (map Rep (map Abs s)) s" - by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]]) + by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]]) have c: "(op \ OO list_all2 R) (map Rep (map Abs r)) s" by (rule pred_compI) (rule b, rule y) have z: "list_all2 R r (map Rep (map Abs r))" - by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]]) + by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]]) then show "(list_all2 R OOO op \) r s" using a c pred_compI by simp qed qed lemma quotient_compose_list[quot_thm]: - shows "Quotient ((list_all2 op \) OOO (op \)) + shows "Quotient3 ((list_all2 op \) OOO (op \)) (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" - by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp) + by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_equivp) section {* Quotient definitions for fsets *} @@ -404,19 +404,19 @@ done lemma Nil_prs2 [quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(Abs \ map f) [] = Abs []" by simp lemma Cons_prs2 [quot_preserve]: - assumes q: "Quotient R1 Abs1 Rep1" - and r: "Quotient R2 Abs2 Rep2" + assumes q: "Quotient3 R1 Abs1 Rep1" + and r: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> (map Rep1 \ Rep2) ---> (Abs2 \ map Abs1)) (op #) = (id ---> Rep2 ---> Abs2) (op #)" - by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) + by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) lemma append_prs2 [quot_preserve]: - assumes q: "Quotient R1 Abs1 Rep1" - and r: "Quotient R2 Abs2 Rep2" + assumes q: "Quotient3 R1 Abs1 Rep1" + and r: "Quotient3 R2 Abs2 Rep2" shows "((map Rep1 \ Rep2) ---> (map Rep1 \ Rep2) ---> (Abs2 \ map Abs1)) op @ = (Rep2 ---> Rep2 ---> Abs2) op @" by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id) @@ -485,7 +485,7 @@ lemma map_prs2 [quot_preserve]: shows "((abs_fset ---> rep_fset) ---> (map rep_fset \ rep_fset) ---> abs_fset \ map abs_fset) map = (id ---> rep_fset ---> abs_fset) map" by (auto simp add: fun_eq_iff) - (simp only: map_map[symmetric] map_prs_aux[OF Quotient_fset Quotient_fset]) + (simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_fset]) section {* Lifted theorems *} diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/Lift_DList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,86 @@ +(* Title: HOL/Quotient_Examples/Lift_DList.thy + Author: Ondrej Kuncar +*) + +theory Lift_DList +imports Main "~~/src/HOL/Library/Quotient_List" +begin + +subsection {* The type of distinct lists *} + +typedef (open) 'a dlist = "{xs::'a list. distinct xs}" + morphisms list_of_dlist Abs_dlist +proof + show "[] \ {xs. distinct xs}" by simp +qed + +setup_lifting type_definition_dlist + +text {* Fundamental operations: *} + +lift_definition empty :: "'a dlist" is "[]" +by simp + +lift_definition insert :: "'a \ 'a dlist \ 'a dlist" is List.insert +by simp + +lift_definition remove :: "'a \ 'a dlist \ 'a dlist" is List.remove1 +by simp + +lift_definition map :: "('a \ 'b) \ 'a dlist \ 'b dlist" is "\f. remdups o List.map f" +by simp + +lift_definition filter :: "('a \ bool) \ 'a dlist \ 'a dlist" is List.filter +by simp + +text {* Derived operations: *} + +lift_definition null :: "'a dlist \ bool" is List.null +by simp + +lift_definition member :: "'a dlist \ 'a \ bool" is List.member +by simp + +lift_definition length :: "'a dlist \ nat" is List.length +by simp + +lift_definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.fold +by simp + +lift_definition foldr :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.foldr +by simp + +lift_definition concat :: "'a dlist dlist \ 'a dlist" is "remdups o List.concat" +proof - + { + fix x y + have "list_all2 cr_dlist x y \ + List.map Abs_dlist x = y \ list_all2 (Lifting.invariant distinct) x x" + unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto + } + note cr = this + + fix x :: "'a list list" and y :: "'a list list" + assume a: "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\\) x y" + from a have l_x: "list_all2 (Lifting.invariant distinct) x x" by (auto simp add: cr) + from a have l_y: "list_all2 (Lifting.invariant distinct) y y" by (auto simp add: cr) + from a have m: "(Lifting.invariant distinct) (List.map Abs_dlist x) (List.map Abs_dlist y)" + by (auto simp add: cr) + + have "x = y" + proof - + have m':"List.map Abs_dlist x = List.map Abs_dlist y" using m unfolding Lifting.invariant_def by simp + have dist: "\l. list_all2 (Lifting.invariant distinct) l l \ !x. x \ (set l) \ distinct x" + unfolding list_all2_def Lifting.invariant_def by (auto simp add: zip_same) + from dist[OF l_x] dist[OF l_y] have "inj_on Abs_dlist (set x \ set y)" by (intro inj_onI) + (metis CollectI UnE Abs_dlist_inverse) + with m' show ?thesis by (rule map_inj_on) + qed + then show "?thesis x y" unfolding Lifting.invariant_def by auto +qed + +text {* We can export code: *} + +export_code empty insert remove map filter null member length fold foldr concat in SML + +end diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/Lift_Fun.thy --- a/src/HOL/Quotient_Examples/Lift_Fun.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Quotient_Examples/Lift_Fun.thy +(* Title: HOL/Quotient3_Examples/Lift_Fun.thy Author: Ondrej Kuncar *) @@ -53,12 +53,12 @@ enriched_type map_endofun : map_endofun proof - - have "\ x. abs_endofun (rep_endofun x) = x" using Quotient_endofun by (auto simp: Quotient_def) + have "\ x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def) then show "map_endofun id id = id" by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) - have a:"\ x. rep_endofun (abs_endofun x) = x" using Quotient_endofun - Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast + have a:"\ x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun + Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast show "\f g h i. map_endofun f g \ map_endofun h i = map_endofun (f \ h) (i \ g)" by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) qed @@ -74,34 +74,34 @@ endofun_rel' done lemma endofun_quotient: -assumes a: "Quotient R Abs Rep" -shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)" -proof (intro QuotientI) +assumes a: "Quotient3 R Abs Rep" +shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)" +proof (intro Quotient3I) show "\a. map_endofun Abs Rep (map_endofun Rep Abs a) = a" by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs) next show "\a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)" - using fun_quotient[OF a a, THEN Quotient_rep_reflp] + using fun_quotient3[OF a a, THEN Quotient3_rep_reflp] unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def - by (metis (mono_tags) Quotient_endofun rep_abs_rsp) + by (metis (mono_tags) Quotient3_endofun rep_abs_rsp) next have abs_to_eq: "\ x y. abs_endofun x = abs_endofun y \ x = y" - by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun]) + by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun]) fix r s show "endofun_rel R r s = (endofun_rel R r r \ endofun_rel R s s \ map_endofun Abs Rep r = map_endofun Abs Rep s)" apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def) - using fun_quotient[OF a a,THEN Quotient_refl1] + using fun_quotient3[OF a a,THEN Quotient3_refl1] apply metis - using fun_quotient[OF a a,THEN Quotient_refl2] + using fun_quotient3[OF a a,THEN Quotient3_refl2] apply metis - using fun_quotient[OF a a, THEN Quotient_rel] + using fun_quotient3[OF a a, THEN Quotient3_rel] apply metis - by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq) + by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq) qed -declare [[map endofun = (endofun_rel, endofun_quotient)]] +declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]] quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \ 'a) \ ('a \ 'a)" done diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/Lift_RBT.thy --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Apr 03 17:48:16 2012 +0200 @@ -1,4 +1,6 @@ -(* Author: Lukas Bulwahn, TU Muenchen *) +(* Title: HOL/Quotient_Examples/Lift_RBT.thy + Author: Lukas Bulwahn and Ondrej Kuncar +*) header {* Lifting operations of RBT trees *} @@ -35,53 +37,35 @@ setup_lifting type_definition_rbt -quotient_definition lookup where "lookup :: ('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +by simp + +lift_definition empty :: "('a\linorder, 'b) rbt" is RBT_Impl.Empty +by (simp add: empty_def) + +lift_definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.insert" +by simp + +lift_definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.delete" +by simp + +lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries by simp -(* FIXME: quotient_definition at the moment requires that types variables match exactly, -i.e., sort constraints must be annotated to the constant being lifted. -But, it should be possible to infer the necessary sort constraints, making the explicit -sort constraints unnecessary. - -Hence this unannotated quotient_definition fails: - -quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" -is "RBT_Impl.Empty" - -Similar issue for quotient_definition for entries, keys, map, and fold. -*) - -quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" -is "(RBT_Impl.Empty :: ('a\linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def) - -quotient_definition insert where "insert :: 'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.insert" by simp +lift_definition keys :: "('a\linorder, 'b) rbt \ 'a list" is RBT_Impl.keys +by simp -quotient_definition delete where "delete :: 'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.delete" by simp - -(* FIXME: unnecessary type annotations *) -quotient_definition "entries :: ('a\linorder, 'b) rbt \ ('a \ 'b) list" -is "RBT_Impl.entries :: ('a\linorder, 'b) RBT_Impl.rbt \ ('a \ 'b) list" by simp - -(* FIXME: unnecessary type annotations *) -quotient_definition "keys :: ('a\linorder, 'b) rbt \ 'a list" -is "RBT_Impl.keys :: ('a\linorder, 'b) RBT_Impl.rbt \ 'a list" by simp - -quotient_definition "bulkload :: ('a\linorder \ 'b) list \ ('a, 'b) rbt" -is "RBT_Impl.bulkload" by simp - -quotient_definition "map_entry :: 'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.map_entry" by simp - -(* FIXME: unnecesary type annotations *) -quotient_definition map where "map :: ('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.map :: ('a \ 'b \ 'b) \ ('a\linorder, 'b) RBT_Impl.rbt \ ('a, 'b) RBT_Impl.rbt" +lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "RBT_Impl.bulkload" by simp -(* FIXME: unnecessary type annotations *) -quotient_definition fold where "fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" -is "RBT_Impl.fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) RBT_Impl.rbt \ 'c \ 'c" by simp +lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map_entry +by simp + +lift_definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map +by simp + +lift_definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" is RBT_Impl.fold +by simp export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Tue Apr 03 17:48:16 2012 +0200 @@ -2,7 +2,7 @@ Author: Lukas Bulwahn and Ondrej Kuncar *) -header {* Example of lifting definitions with the quotient infrastructure *} +header {* Example of lifting definitions with the lifting infrastructure *} theory Lift_Set imports Main @@ -16,19 +16,14 @@ setup_lifting type_definition_set[unfolded set_def] -text {* Now, we can employ quotient_definition to lift definitions. *} +text {* Now, we can employ lift_definition to lift definitions. *} -quotient_definition empty where "empty :: 'a set" -is "bot :: 'a \ bool" done +lift_definition empty :: "'a set" is "bot :: 'a \ bool" done term "Lift_Set.empty" thm Lift_Set.empty_def -definition insertp :: "'a \ ('a \ bool) \ 'a \ bool" where - "insertp x P y \ y = x \ P y" - -quotient_definition insert where "insert :: 'a => 'a set => 'a set" -is insertp done +lift_definition insert :: "'a => 'a set => 'a set" is "\ x P y. y = x \ P y" done term "Lift_Set.insert" thm Lift_Set.insert_def diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Apr 03 17:48:16 2012 +0200 @@ -145,9 +145,9 @@ (abs_int (x + u, y + v))" apply(simp add: plus_int_def id_simps) apply(fold plus_int_raw.simps) - apply(rule Quotient_rel_abs[OF Quotient_int]) + apply(rule Quotient3_rel_abs[OF Quotient3_int]) apply(rule plus_int_raw_rsp_aux) - apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) + apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int]) done definition int_of_nat_raw: @@ -255,31 +255,25 @@ minus_add_distrib[of z1 z2] for z1 z2 w :: int -lemma int_induct_raw: - assumes a: "P (0::nat, 0)" - and b: "\i. P i \ P (plus_int_raw i (1, 0))" - and c: "\i. P i \ P (plus_int_raw i (uminus_int_raw (1, 0)))" - shows "P x" -proof (cases x, clarify) - fix a b - show "P (a, b)" - proof (induct a arbitrary: b rule: nat.induct) - case zero - show "P (0, b)" using assms by (induct b) auto - next - case (Suc n) - then show ?case using assms by auto - qed -qed +lemma int_induct2: + assumes "P 0 0" + and "\n m. P n m \ P (Suc n) m" + and "\n m. P n m \ P n (Suc m)" + shows "P n m" +using assms +by (induction_schema) (pat_completeness, lexicographic_order) + lemma int_induct: - fixes x :: int + fixes j :: int assumes a: "P 0" - and b: "\i. P i \ P (i + 1)" - and c: "\i. P i \ P (i - 1)" - shows "P x" - using a b c unfolding minus_int_def - by (lifting int_induct_raw) + and b: "\i::int. P i \ P (i + 1)" + and c: "\i::int. P i \ P (i - 1)" + shows "P j" +using a b c +unfolding minus_int_def +by (descending) (auto intro: int_induct2) + text {* Magnitide of an Integer, as a Natural Number: @{term nat} *} @@ -289,7 +283,8 @@ quotient_definition "int_to_nat::int \ nat" is - "int_to_nat_raw" unfolding int_to_nat_raw_def by force + "int_to_nat_raw" +unfolding int_to_nat_raw_def by auto lemma nat_le_eq_zle: fixes w z::"int" diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/Quotient_Message.thy --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Apr 03 17:48:16 2012 +0200 @@ -307,20 +307,15 @@ thus "Decrypt K X = Decrypt K X'" by simp qed -lemma msg_induct_aux: - shows "\\N. P (Nonce N); - \X Y. \P X; P Y\ \ P (MPair X Y); - \K X. P X \ P (Crypt K X); - \K X. P X \ P (Decrypt K X)\ \ P msg" - by (lifting freemsg.induct) - lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: assumes N: "\N. P (Nonce N)" and M: "\X Y. \P X; P Y\ \ P (MPair X Y)" and C: "\K X. P X \ P (Crypt K X)" and D: "\K X. P X \ P (Decrypt K X)" shows "P msg" - using N M C D by (rule msg_induct_aux) + using N M C D + by (descending) (auto intro: freemsg.induct) + subsection{*The Abstract Discriminator*} diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Quotient_Examples/ROOT.ML Tue Apr 03 17:48:16 2012 +0200 @@ -5,5 +5,5 @@ *) use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", - "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"]; + "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"]; diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/SPARK/Tools/fdl_lexer.ML --- a/src/HOL/SPARK/Tools/fdl_lexer.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Tue Apr 03 17:48:16 2012 +0200 @@ -174,6 +174,7 @@ identifier @@@ (Scan.repeat1 ($$$ "." @@@ identifier) >> flat); val whitespace = Scan.many (is_whitespace o symbol); +val whitespace1 = Scan.many1 (is_whitespace o symbol); val whitespace' = Scan.many (is_whitespace' o symbol); val newline = Scan.one (is_newline o symbol); @@ -261,7 +262,7 @@ Scan.repeat (Scan.unless (Scan.one is_char_eof) (!!! "bad input" ( comment - || (keyword "For" -- whitespace) |-- + || (keyword "For" -- whitespace1) |-- Scan.repeat1 (Scan.unless (keyword ":") any) --| keyword ":" >> make_token Traceability || Scan.max leq_token diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Lifting/lifting_def.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,291 @@ +(* Title: HOL/Tools/Lifting/lifting_def.ML + Author: Ondrej Kuncar + +Definitions for constants on quotient types. +*) + +signature LIFTING_DEF = +sig + val add_lift_def: + (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory + + val lift_def_cmd: + (binding * string option * mixfix) * string -> local_theory -> Proof.state + + val can_generate_code_cert: thm -> bool +end; + +structure Lifting_Def: LIFTING_DEF = +struct + +(** Interface and Syntax Setup **) + +(* Generation of the code certificate from the rsp theorem *) + +infix 0 MRSL + +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm + +fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) + | get_body_types (U, V) = (U, V) + +fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) + | get_binder_types _ = [] + +fun force_rty_type ctxt rty rhs = + let + val thy = Proof_Context.theory_of ctxt + val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs + val rty_schematic = fastype_of rhs_schematic + val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty + in + Envir.subst_term_types match rhs_schematic + end + +fun unabs_def ctxt def = + let + val (_, rhs) = Thm.dest_equals (cprop_of def) + fun dest_abs (Abs (var_name, T, _)) = (var_name, T) + | dest_abs tm = raise TERM("get_abs_var",[tm]) + val (var_name, T) = dest_abs (term_of rhs) + val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt + val thy = Proof_Context.theory_of ctxt' + val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T))) + in + Thm.combination def refl_thm |> + singleton (Proof_Context.export ctxt' ctxt) + end + +fun unabs_all_def ctxt def = + let + val (_, rhs) = Thm.dest_equals (cprop_of def) + val xs = strip_abs_vars (term_of rhs) + in + fold (K (unabs_def ctxt)) xs def + end + +val map_fun_unfolded = + @{thm map_fun_def[abs_def]} |> + unabs_def @{context} |> + unabs_def @{context} |> + Local_Defs.unfold @{context} [@{thm comp_def}] + +fun unfold_fun_maps ctm = + let + fun unfold_conv ctm = + case (Thm.term_of ctm) of + Const (@{const_name "map_fun"}, _) $ _ $ _ => + (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm + | _ => Conv.all_conv ctm + val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) + in + (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm + end + +fun prove_rel ctxt rsp_thm (rty, qty) = + let + val ty_args = get_binder_types (rty, qty) + fun disch_arg args_ty thm = + let + val quot_thm = Lifting_Term.prove_quot_theorem ctxt args_ty + in + [quot_thm, thm] MRSL @{thm apply_rsp''} + end + in + fold disch_arg ty_args rsp_thm + end + +exception CODE_CERT_GEN of string + +fun simplify_code_eq ctxt def_thm = + Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm + +fun can_generate_code_cert quot_thm = + case Lifting_Term.quot_thm_rel quot_thm of + Const (@{const_name HOL.eq}, _) => true + | Const (@{const_name invariant}, _) $ _ => true + | _ => false + +fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) = + let + val thy = Proof_Context.theory_of ctxt + val quot_thm = Lifting_Term.prove_quot_theorem ctxt (get_body_types (rty, qty)) + val fun_rel = prove_rel ctxt rsp_thm (rty, qty) + val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs} + val abs_rep_eq = + case (HOLogic.dest_Trueprop o prop_of) fun_rel of + Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm + | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} + | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" + val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm + val unabs_def = unabs_all_def ctxt unfolded_def + val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm + val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq} + val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong} + val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans} + in + simplify_code_eq ctxt code_cert + end + +fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = + let + val quot_thm = Lifting_Term.prove_quot_theorem lthy (get_body_types (rty, qty)) + in + if can_generate_code_cert quot_thm then + let + val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty) + val add_abs_eqn_attribute = + Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I) + val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute); + in + lthy + |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert]) + end + else + lthy + end + +fun define_code_eq code_eqn_thm_name def_thm lthy = + let + val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm + val code_eq = unabs_all_def lthy unfolded_def + val simp_code_eq = simplify_code_eq lthy code_eq + in + lthy + |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq]) + end + +fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = + if body_type rty = body_type qty then + define_code_eq code_eqn_thm_name def_thm lthy + else + define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy + + +fun add_lift_def var qty rhs rsp_thm lthy = + let + val rty = fastype_of rhs + val absrep_trm = Lifting_Term.absrep_fun lthy (rty, qty) + val rty_forced = (domain_type o fastype_of) absrep_trm + val forced_rhs = force_rty_type lthy rty_forced rhs + val lhs = Free (Binding.print (#1 var), qty) + val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) + val (_, prop') = Local_Defs.cert_def lthy prop + val (_, newrhs) = Local_Defs.abs_def prop' + + val ((_, (_ , def_thm)), lthy') = + Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy + + fun qualify defname suffix = Binding.name suffix + |> Binding.qualify true defname + + val lhs_name = Binding.name_of (#1 var) + val rsp_thm_name = qualify lhs_name "rsp" + val code_eqn_thm_name = qualify lhs_name "rep_eq" + in + lthy' + |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm]) + |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty) + end + +fun mk_readable_rsp_thm_eq tm lthy = + let + val ctm = cterm_of (Proof_Context.theory_of lthy) tm + + fun norm_fun_eq ctm = + let + fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy + fun erase_quants ctm' = + case (Thm.term_of ctm') of + Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm' + | _ => (Conv.binder_conv (K erase_quants) lthy then_conv + Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm' + in + (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm + end + + fun simp_arrows_conv ctm = + let + val unfold_conv = Conv.rewrs_conv + [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, + @{thm fun_rel_def[THEN eq_reflection]}] + val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq + fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 + in + case (Thm.term_of ctm) of + Const (@{const_name "fun_rel"}, _) $ _ $ _ => + (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm + | _ => Conv.all_conv ctm + end + + val unfold_ret_val_invs = Conv.bottom_conv + (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy + val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv) + val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} + val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy + val beta_conv = Thm.beta_conversion true + val eq_thm = + (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm + in + Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2) + end + + + +fun lift_def_cmd (raw_var, rhs_raw) lthy = + let + val ((binding, SOME qty, mx), ctxt) = yield_singleton Proof_Context.read_vars raw_var lthy + val rhs = (Syntax.check_term ctxt o Syntax.parse_term ctxt) rhs_raw + + fun try_to_prove_refl thm = + let + val lhs_eq = + thm + |> prop_of + |> Logic.dest_implies + |> fst + |> strip_all_body + |> try HOLogic.dest_Trueprop + in + case lhs_eq of + SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm) + | _ => NONE + end + + val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) + val rty_forced = (domain_type o fastype_of) rsp_rel; + val forced_rhs = force_rty_type lthy rty_forced rhs; + val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) + val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy + val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq + val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) + + fun after_qed thm_list lthy = + let + val internal_rsp_thm = + case thm_list of + [] => the maybe_proven_rsp_thm + | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm + (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1) + in + add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy + end + + in + case maybe_proven_rsp_thm of + SOME _ => Proof.theorem NONE after_qed [] lthy + | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy + end + +(* parser and command *) +val liftdef_parser = + ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2) + --| @{keyword "is"} -- Parse.term + +val _ = + Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"} + "definition for constants over the quotient type" + (liftdef_parser >> lift_def_cmd) + + +end; (* structure *) diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Lifting/lifting_info.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,125 @@ +(* Title: HOL/Tools/Lifting/lifting_info.ML + Author: Ondrej Kuncar + +Context data for the lifting package. +*) + +signature LIFTING_INFO = +sig + type quotmaps = {relmap: string, quot_thm: thm} + val lookup_quotmaps: Proof.context -> string -> quotmaps option + val lookup_quotmaps_global: theory -> string -> quotmaps option + val print_quotmaps: Proof.context -> unit + + type quotients = {quot_thm: thm} + val transform_quotients: morphism -> quotients -> quotients + val lookup_quotients: Proof.context -> string -> quotients option + val lookup_quotients_global: theory -> string -> quotients option + val update_quotients: string -> quotients -> Context.generic -> Context.generic + val dest_quotients: Proof.context -> quotients list + val print_quotients: Proof.context -> unit + + val setup: theory -> theory +end; + +structure Lifting_Info: LIFTING_INFO = +struct + +(** data containers **) + +(* FIXME just one data slot (record) per program unit *) + +(* info about map- and rel-functions for a type *) +type quotmaps = {relmap: string, quot_thm: thm} + +structure Quotmaps = Generic_Data +( + type T = quotmaps Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof +val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory + +(* FIXME export proper internal update operation!? *) + +val quotmaps_attribute_setup = + Attrib.setup @{binding map} + ((Args.type_name true --| Scan.lift @{keyword "="}) -- + (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} -- + Attrib.thm --| Scan.lift @{keyword ")"}) >> + (fn (tyname, (relname, qthm)) => + let val minfo = {relmap = relname, quot_thm = qthm} + in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) + "declaration of map information" + +fun print_quotmaps ctxt = + let + fun prt_map (ty_name, {relmap, quot_thm}) = + Pretty.block (separate (Pretty.brk 2) + [Pretty.str "type:", + Pretty.str ty_name, + Pretty.str "relation map:", + Pretty.str relmap, + Pretty.str "quot. theorem:", + Syntax.pretty_term ctxt (prop_of quot_thm)]) + in + map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) + |> Pretty.big_list "maps for type constructors:" + |> Pretty.writeln + end + +(* info about quotient types *) +type quotients = {quot_thm: thm} + +structure Quotients = Generic_Data +( + type T = quotients Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +fun transform_quotients phi {quot_thm} = + {quot_thm = Morphism.thm phi quot_thm} + +val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof +val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory + +fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) + +fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *) + map snd (Symtab.dest (Quotients.get (Context.Proof ctxt))) + +fun print_quotients ctxt = + let + fun prt_quot (qty_name, {quot_thm}) = + Pretty.block (separate (Pretty.brk 2) + [Pretty.str "type:", + Pretty.str qty_name, + Pretty.str "quot. thm:", + Syntax.pretty_term ctxt (prop_of quot_thm)]) + in + map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt))) + |> Pretty.big_list "quotients:" + |> Pretty.writeln + end + +(* theory setup *) + +val setup = + quotmaps_attribute_setup + +(* outer syntax commands *) + +val _ = + Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions" + (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of))) + +val _ = + Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" + (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) + +end; \ No newline at end of file diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Lifting/lifting_setup.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,113 @@ +(* Title: HOL/Tools/Lifting/lifting_setup.ML + Author: Ondrej Kuncar + +Setting the lifting infranstructure up. +*) + +signature LIFTING_SETUP = +sig + exception SETUP_LIFTING_INFR of string + + val setup_lifting_infr: thm -> thm -> local_theory -> local_theory + + val setup_by_typedef_thm: thm -> local_theory -> local_theory +end; + +structure Lifting_Seup: LIFTING_SETUP = +struct + +infix 0 MRSL + +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm + +exception SETUP_LIFTING_INFR of string + +fun define_cr_rel equiv_thm abs_fun lthy = + let + fun force_type_of_rel rel forced_ty = + let + val thy = Proof_Context.theory_of lthy + val rel_ty = (domain_type o fastype_of) rel + val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty + in + Envir.subst_term_types ty_inst rel + end + + val (rty, qty) = (dest_funT o fastype_of) abs_fun + val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0) + val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of + Const (@{const_name equivp}, _) $ _ => abs_fun_graph + | Const (@{const_name part_equivp}, _) $ rel => + HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph) + | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem" + ) + val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body)); + val qty_name = (fst o dest_Type) qty + val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name) + val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy + val ((_, (_ , def_thm)), lthy'') = + Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' + in + (def_thm, lthy'') + end + +fun define_abs_type quot_thm lthy = + if Lifting_Def.can_generate_code_cert quot_thm then + let + val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} + val add_abstype_attribute = + Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I) + val add_abstype_attrib = Attrib.internal (K add_abstype_attribute); + in + lthy + |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm]) + end + else + lthy + +fun setup_lifting_infr quot_thm equiv_thm lthy = + let + val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm + val qty_full_name = (fst o dest_Type) qtyp + val quotients = { quot_thm = quot_thm } + fun quot_info phi = Lifting_Info.transform_quotients phi quotients + in + lthy + |> Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) + |> define_abs_type quot_thm + end + +fun setup_by_typedef_thm typedef_thm lthy = + let + fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy = + let + val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm + val equiv_thm = typedef_thm RS to_equiv_thm + val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy + val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm + in + (quot_thm, equiv_thm, lthy') + end + + val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm + val (quot_thm, equiv_thm, lthy') = (case typedef_set of + Const ("Orderings.top_class.top", _) => + derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp} + typedef_thm lthy + | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => + derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp} + typedef_thm lthy + | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem") + in + setup_lifting_infr quot_thm equiv_thm lthy' + end + +fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy + +val _ = + Outer_Syntax.local_theory @{command_spec "setup_lifting"} + "Setup lifting infrastracture" + (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm)) + +end; diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Lifting/lifting_term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,173 @@ +(* Title: HOL/Tools/Lifting/lifting_term.ML + Author: Ondrej Kuncar + +Proves Quotient theorem. +*) + +signature LIFTING_TERM = +sig + val prove_quot_theorem: Proof.context -> typ * typ -> thm + + val absrep_fun: Proof.context -> typ * typ -> term + + (* Allows Nitpick to represent quotient types as single elements from raw type *) + (* val absrep_const_chk: Proof.context -> flag -> string -> term *) + + val equiv_relation: Proof.context -> typ * typ -> term + + val quot_thm_rel: thm -> term + val quot_thm_abs: thm -> term + val quot_thm_rep: thm -> term + val quot_thm_rty_qty: thm -> typ * typ +end + +structure Lifting_Term: LIFTING_TERM = +struct + +exception LIFT_MATCH of string + +(* matches a type pattern with a type *) +fun match ctxt err ty_pat ty = + let + val thy = Proof_Context.theory_of ctxt + in + Sign.typ_match thy (ty_pat, ty) Vartab.empty + handle Type.TYPE_MATCH => err ctxt ty_pat ty + end + +fun equiv_match_err ctxt ty_pat ty = + let + val ty_pat_str = Syntax.string_of_typ ctxt ty_pat + val ty_str = Syntax.string_of_typ ctxt ty + in + raise LIFT_MATCH (space_implode " " + ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) + end + +(* generation of the Quotient theorem *) + +exception QUOT_THM of string + +fun get_quot_thm ctxt s = + let + val thy = Proof_Context.theory_of ctxt + in + (case Lifting_Info.lookup_quotients ctxt s of + SOME qdata => Thm.transfer thy (#quot_thm qdata) + | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found.")) + end + +fun get_rel_quot_thm ctxt s = + let + val thy = Proof_Context.theory_of ctxt + in + (case Lifting_Info.lookup_quotmaps ctxt s of + SOME map_data => Thm.transfer thy (#quot_thm map_data) + | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")")) + end + +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) + +infix 0 MRSL + +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm + +exception NOT_IMPL of string + +fun quot_thm_rel quot_thm = + let + val (Const (@{const_name Quotient}, _) $ rel $ _ $ _ $ _) = + (HOLogic.dest_Trueprop o prop_of) quot_thm + in + rel + end + +fun quot_thm_abs quot_thm = + let + val (Const (@{const_name Quotient}, _) $ _ $ abs $ _ $ _) = + (HOLogic.dest_Trueprop o prop_of) quot_thm + in + abs + end + +fun quot_thm_rep quot_thm = + let + val (Const (@{const_name Quotient}, _) $ _ $ _ $ rep $ _) = + (HOLogic.dest_Trueprop o prop_of) quot_thm + in + rep + end + +fun quot_thm_rty_qty quot_thm = + let + val abs = quot_thm_abs quot_thm + val abs_type = fastype_of abs + in + (domain_type abs_type, range_type abs_type) + end + +fun prove_quot_theorem ctxt (rty, qty) = + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (prove_quot_theorem ctxt) (tys ~~ tys') + in + if forall is_id_quot args + then + @{thm identity_quotient} + else + args MRSL (get_rel_quot_thm ctxt s) + end + else + let + val quot_thm = get_quot_thm ctxt s' + val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm + val qtyenv = match ctxt equiv_match_err qty_pat qty + val rtys' = map (Envir.subst_type qtyenv) rtys + val args = map (prove_quot_theorem ctxt) (tys ~~ rtys') + in + if forall is_id_quot args + then + quot_thm + else + let + val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s) + in + [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose} + end + end + | _ => @{thm identity_quotient} + +fun force_qty_type thy qty quot_thm = + let + val abs_schematic = quot_thm_abs quot_thm + val qty_schematic = (range_type o fastype_of) abs_schematic + val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty + fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) + val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env [] + in + Thm.instantiate (ty_inst, []) quot_thm + end + +fun absrep_fun ctxt (rty, qty) = + let + val thy = Proof_Context.theory_of ctxt + val quot_thm = prove_quot_theorem ctxt (rty, qty) + val forced_quot_thm = force_qty_type thy qty quot_thm + in + quot_thm_abs forced_quot_thm + end + +fun equiv_relation ctxt (rty, qty) = + let + val thy = Proof_Context.theory_of ctxt + val quot_thm = prove_quot_theorem ctxt (rty, qty) + val forced_quot_thm = force_qty_type thy qty quot_thm + in + quot_thm_rel forced_quot_thm + end + +end; diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 17:48:16 2012 +0200 @@ -86,7 +86,7 @@ let val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty in - [quot_thm, thm] MRSL @{thm apply_rsp''} + [quot_thm, thm] MRSL @{thm apply_rspQ3''} end in fold disch_arg ty_args rsp_thm @@ -101,11 +101,11 @@ let val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty)) val fun_rel = prove_rel ctxt rsp_thm (rty, qty) - val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs} + val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs} val abs_rep_eq = case (HOLogic.dest_Trueprop o prop_of) fun_rel of Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm - | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} + | Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm val unabs_def = unabs_all_def ctxt unfolded_def diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Tue Apr 03 17:48:16 2012 +0200 @@ -70,7 +70,7 @@ (* FIXME export proper internal update operation!? *) val quotmaps_attribute_setup = - Attrib.setup @{binding map} + Attrib.setup @{binding mapQ3} ((Args.type_name true --| Scan.lift @{keyword "="}) -- (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} -- Attrib.thm --| Scan.lift @{keyword ")"}) >> @@ -298,11 +298,11 @@ (* outer syntax commands *) val _ = - Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions" + Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions" (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of))) val _ = - Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" + Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients" (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) val _ = diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 03 17:48:16 2012 +0200 @@ -62,7 +62,7 @@ fun quotient_tac ctxt = (REPEAT_ALL_NEW (FIRST' - [rtac @{thm identity_quotient}, + [rtac @{thm identity_quotient3}, resolve_tac (Quotient_Info.quotient_rules ctxt)])) fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) @@ -259,7 +259,7 @@ val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; val inst_thm = Drule.instantiate' ty_inst - ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} + ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3} in (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1 end @@ -529,7 +529,7 @@ val prs = Quotient_Info.prs_rules lthy val ids = Quotient_Info.id_simps lthy val thms = - @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs + @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver in diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Apr 03 17:48:16 2012 +0200 @@ -356,7 +356,7 @@ | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")")) end -fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3}) infix 0 MRSL @@ -375,13 +375,13 @@ let val quot_thm_rel = get_rel_from_quot_thm quot_thm in - if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient} + if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3} else raise NOT_IMPL "nested quotients: not implemented yet" end fun prove_quot_theorem ctxt (rty, qty) = if rty = qty - then @{thm identity_quotient} + then @{thm identity_quotient3} else case (rty, qty) of (Type (s, tys), Type (s', tys')) => @@ -410,7 +410,7 @@ mk_quot_thm_compose (rel_quot_thm, quot_thm) end end - | _ => @{thm identity_quotient} + | _ => @{thm identity_quotient3} diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 03 17:48:16 2012 +0200 @@ -82,13 +82,13 @@ fun can_generate_code_cert quot_thm = case Quotient_Term.get_rel_from_quot_thm quot_thm of Const (@{const_name HOL.eq}, _) => true - | Const (@{const_name invariant}, _) $ _ => true + | Const (@{const_name Lifting.invariant}, _) $ _ => true | _ => false fun define_abs_type quot_thm lthy = if can_generate_code_cert quot_thm then let - val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} + val abs_type_thm = quot_thm RS @{thm Quotient3_abs_rep} val add_abstype_attribute = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I) val add_abstype_attrib = Attrib.internal (K add_abstype_attribute); @@ -157,7 +157,7 @@ val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 (* quotient theorem *) - val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name + val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name val quotient_thm = (quot_thm RS @{thm quot_type.Quotient}) |> fold_rule [abs_def, rep_def] @@ -313,30 +313,5 @@ "quotient type definitions (require equivalence proofs)" (quotspec_parser >> quotient_type_cmd) -(* Setup lifting using type_def_thm *) - -exception SETUP_LIFT_TYPE of string - -fun setup_lift_type typedef_thm = - let - val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm - val (quot_thm, equivp_thm) = (case typedef_set of - Const ("Orderings.top_class.top", _) => - (typedef_thm RS @{thm copy_type_to_Quotient}, - typedef_thm RS @{thm copy_type_to_equivp}) - | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) => - (typedef_thm RS @{thm invariant_type_to_Quotient}, - typedef_thm RS @{thm invariant_type_to_part_equivp}) - | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem") - in - init_quotient_infr quot_thm equivp_thm - end - -fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy - -val _ = - Outer_Syntax.local_theory @{command_spec "setup_lifting"} - "Setup lifting infrastracture" - (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm)) end; diff -r c82a0b2606a1 -r 610d9c212376 src/HOL/ex/Executable_Relation.thy --- a/src/HOL/ex/Executable_Relation.thy Tue Apr 03 17:21:33 2012 +0200 +++ b/src/HOL/ex/Executable_Relation.thy Tue Apr 03 17:48:16 2012 +0200 @@ -67,11 +67,11 @@ lemma [simp]: "rel_of_set (set_of_rel S) = S" -by (rule Quotient_abs_rep[OF Quotient_rel]) +by (rule Quotient3_abs_rep[OF Quotient3_rel]) lemma [simp]: "set_of_rel (rel_of_set R) = R" -by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) +by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl) lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]